maria - Online in der Cloud

PROGRAMM:

NAME/FUNKTION

maria - Modularer Erreichbarkeitsanalysator für hochrangige Petrinetze

ZUSAMMENFASSUNG

maria [Optionen] Dateien...

BESCHREIBUNG

Diese Handbuchseite dokumentiert kurz die maria Befehl. Eine vollständigere Dokumentation ist
verfügbar im GNU Info-Format; siehe unten.

maria ist ein Programm, das Modelle von nebenläufigen Systemen analysiert, beschrieben in seinem Input
Sprache, die auf algebraischen Systemnetzen basiert. Der Formalismus wurde von Ekkart . präsentiert
Kindler und Hagen Völzer auf der ICATPN'98, Flexibilität in Algebraisch Netze.
Algebraic System Nets ist ein Framework, das keine Datentypen oder algebraischen . definiert
Operationen. Das Datentypsystem und die Operationen in Maria wurden mit High-Level-
Programmier- und Spezifikationssprachen im Hinterkopf. Trotzdem hat jedes Maria-Modell ein
endliche Entfaltung.
Um die Interoperabilität mit Low-Level-Petri-Net-Tools zu gewährleisten, übersetzt Maria Identifikatoren in
entfaltete Netze zu Ketten aus alphanumerischen Zeichen und Unterstrichen. Der Filter
faltname.pl verwendet oder angepasst werden, um die Lesbarkeit der Identifikatoren zu verbessern.

OPTIONAL

Maria folgt der üblichen GNU-Befehlszeilensyntax mit langen Optionen, die mit zwei beginnen
Striche (`-'). Nachfolgend finden Sie eine Zusammenfassung der Optionen. Eine vollständige Beschreibung finden Sie unter
die Info-Dateien.

-a begrenzen, --array-limit=begrenzen
Beschränken Sie die Größe der Array-Indextypen auf begrenzen mögliche Werte. Eine Grenze von 0
deaktiviert die Prüfungen.

-b Modell, --Breite-zuerst-Suche=Modell
Generieren Sie den Erreichbarkeitsgraphen von Modell Breitensuche verwenden.

-C Verzeichnis, --compile=Verzeichnis
C-Code generieren in Verzeichnis zum Auswerten von Ausdrücken und für das Low-Level
Routinen des Analysealgorithmus für Übergangsinstanzen. Wenn diese Option verwendet wird,
Bewertungsfehler werden etwas anders gemeldet. Der Dolmetscher
zeigt die Bewertung und den Ausdruck an, die den ersten Fehler in einem Zustand verursacht haben; das
kompilierter Code zeigt die Anzahl der Fehler an. Aus Leistungsgründen ist die
generierter Code prüft nicht auf Überlauffehler, wenn Elemente zu Mehrfachgruppen hinzugefügt werden.

-C, --no-compile
Das Gegenteil von -C. Werten Sie alle Ausdrücke im integrierten Interpreter aus. Das ist
das Standardverhalten.

-D Symbol, --define=Symbol
Definieren Sie das Präprozessorsymbol Symbol.

-d Modell, --deep-first-search=Modell
Generieren Sie den Erreichbarkeitsgraphen von Modell mit Tiefensuche.

-E Intervall, --kanten=Intervall
Melden Sie beim Generieren des Erreichbarkeitsdiagramms die Größe des Diagramms nach jedem
Intervall erzeugte Kanten.

-e Schnur, --execute=Schnur
Ausführen Schnur.

-g Grafikdatei, --graph=Grafikdatei
Laden Sie einen zuvor erstellten Erreichbarkeitsgraphen von Grafikdatei.rgh.

-H h[,f[,t]], --Hashes=h[,f[,t]]
Konfigurieren Sie die Parameter für die probabilistische Überprüfung (-P). Zuweisen t allgemeine
Hash-Funktionen von f Elemente und entsprechende Hash-Tabellen von h Bits jeweils. Beide h
und f wird auf den nächsten passenden Wert aufgerundet.

-?, -H, --help
Drucken Sie eine Zusammenfassung der Befehlszeilenoptionen an Maria und beenden Sie sie.

-I Verzeichnis, --include=Verzeichnis
Anhängen Verzeichnis in die Liste der Verzeichnisse, die nach Include-Dateien durchsucht werden.

-i Spalten, --breite=Spalten
Setzen Sie den rechten Rand der Ausgabe auf Spalten. Der Standardwert ist 80.

-j anpassen, --jobs=anpassen
Bei der Prüfung der Sicherheitseigenschaften (Optionen -L, -M und -P), benutze diese vielen Arbeiter
Prozesse, um die Analyse auf einem Multiprozessor-Computer zu beschleunigen. Siehe auch -k und
-Z.

-k port [/Gastgeber], --connect=port [/Gastgeber]
Verteilen Sie die Sicherheitsmodellprüfung (Optionen -L, -M und -P) in einem TCP/IP-Netzwerk. Zum
nur der Server port wird als 16-Bit-Ganzzahl ohne Vorzeichen angegeben, normalerweise zwischen
1024 und 65535. Für die Worker-Prozesse port /Gastgeber spezifiziert den Port und die
Adresse des Servers. Siehe auch -j.

-L Modell, --lossless=Modell
Laden Sie Modell und bereiten Sie sich auf die Analyse vor, indem Sie eine Reihe von erreichbaren Zuständen konstruieren
in Festplattendateien. Siehe auch -M, -P, -j und -k.

-m Modell, --model=Modell
Laden Sie Modell und löschen Sie den Erreichbarkeitsgraphen.

-M Modell, --md5-compacted=Modell
Laden Sie Modell und bereiten Sie sich auf die Analyse vor, indem Sie eine Überapproximation von konstruieren
Menge erreichbarer Zustände im Hauptspeicher. Siehe auch -P, -L, -j und -k.

-N Cregexp, --name=Cregexp
Geben Sie die im Kontext zulässigen Namen an c als erweiterter regulärer Ausdruck regexp.
Der Kontext wird durch das erste Zeichen der Parameterzeichenfolge identifiziert; das
nachfolgende Zeichen bilden den regulären Ausdruck, den zulässige Namen haben müssen
Spiel.

-n Cregexp, --no-name=Cregexp
Geben Sie die Namen an, die im Kontext nicht zulässig sind c als erweiterter regulärer Ausdruck
regexp.
Wenn beides -N und und -n sind für einen Kontext angegeben c, dann dauert das zulassende Match
Vorrang. Um beispielsweise zu verlangen, dass alle benutzerdefinierten Typnamen
beendet mit _t, spezifizieren -nt -Nt'_t$'. Die Anführungszeichen im letzteren Parameter sind
erforderlich, um die besondere Bedeutung von zu entfernen $ in der Kommandozeilen-Shell bist du
wahrscheinlich verwendet, um Maria anzurufen.

-P Modell, --wahrscheinlichkeit=Modell
Laden Sie Modell und bereiten Sie sich auf die Analyse vor, indem Sie eine Reihe von erreichbaren Zuständen konstruieren
im Hauptspeicher mithilfe einer Technik namens Bitzustand Hashing.

-p Befehl, --property-translator=Befehl
Geben Sie den Befehl an, der zum Übersetzen von Eigenschaftsautomaten verwendet werden soll. Der Befehl sollte
eine Formel aus der Standardeingabe lesen und einen entsprechenden Automaten schreiben
Beschreibung zur Standardausgabe. Der Übersetzer LBT ist damit kompatibel
.

-q begrenzen, --quantification-limit=begrenzen
Quantifizierung (Multi-Set-Summe) von Typen mit mehr als verhindern begrenzen möglich
Werte. Ein Grenzwert von 0 deaktiviert die Prüfungen.

-U Symbol, --undefine=Symbol
Definiere das Präprozessorsymbol Symbol.

-u [a][f[Outfile]], --entfalten=[a][f[Outfile]]
Entfalte das Netz mit dem Algorithmus a und schreibe es im Format f zu Outfile. Wenn Outfile
nicht angegeben ist, werfen Sie das entfaltete Netz auf die Standardausgabe. Mögliche Formate
sind m (Maria (für Menschen lesbar), Standard), l (LoLA), p (PEP) und r (PROD). Dort
sind zwei Algorithmen: traditionell (Standard) und reduziert durch Konstruktion von a abdeckbar
Markierung (M).

-V, --Version
Drucken Sie die Versionsnummer von Maria und beenden Sie.

-in, - ausführlich
Zeigen Sie ausführliche Informationen zu verschiedenen Phasen der Analyse an.

-W, --Warnungen
Aktivieren Sie Warnungen über verdächtige Netzkonstrukte. Dies ist das Standardverhalten.

-w, --keine Warnungen
Das Gegenteil von -W. Deaktivieren Sie alle Warnungen.

-x Zahlenbasis, --radix=Zahlenbasis
Geben Sie die Zahlenbasis für die Diagnoseausgabe an. Zulässige Werte für Zahlenbasis sind
Oktober, oktal, 8, hex, hexadezimal, 16, Dez, dezimal und 10. Die Standardeinstellung ist zu verwenden
Dezimal Zahlen.

-Y, --komprimieren-versteckt
Reduzieren Sie die Menge der erreichbaren Zustände, indem Sie die Nachfolgezustände von nicht speichern
Übergangsinstanzen, für die a verstecken Zustand gilt. Die versteckten Nachfolger sind
in einem separaten Zustandssatz gespeichert. Diese Option kann Speicherplatz sparen (-L or -m) oder reduzieren
die Wahrscheinlichkeit, dass Zustände ausgelassen werden (-M or -P), und es kann die
Effizienz der Parallelanalyse (-j or -k), kann aber auch erheblich zunehmen
der Prozessorzeitbedarf. Die Option funktioniert auch mit dem Lebendigkeitsmodell
Überprüfung, aber es gibt keine Garantie dafür, dass die Wahrheitswerte von Lebendigkeitseigenschaften
bleiben unverändert. Diese Option ist kombinierbar mit -Z.

-Und, --no-compress-hidden
Das Gegenteil von -Y. Dies ist das Standardverhalten.

-Z, --compress-paths
Reduzieren Sie die Menge der erreichbaren Zustände, indem Sie Zwischenzustände mit at . nicht speichern
meisten ein Nachfolger. Diese Option kann Speicherplatz sparen (-L or -m) oder reduzieren Sie die
Wahrscheinlichkeit, dass Zustände ausgelassen werden (-M or -P), und es kann die Effizienz verbessern
der Parallelanalyse (-j or -k), kann aber auch die
Prozessorzeit benötigt. Die Option funktioniert auch mit der Lebendigkeitsmodellprüfung,
aber es gibt keine Garantie dafür, dass die Wahrheitswerte der Lebendigkeitseigenschaften erhalten bleiben
unverändert. Diese Option ist kombinierbar mit -Y.

-z, --no-compress-paths
Das Gegenteil von -Z. Dies ist das Standardverhalten.

Verwenden Sie maria online mit den onworks.net-Diensten