lps2lts – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

lps2lts – Generieren Sie ein LTS aus einem LPS

ZUSAMMENFASSUNG

lps2lts [zur Auswahl]... [IM ORDNER [AUSGABE]]

BESCHREIBUNG

Generieren Sie ein LTS aus dem LPS in INFILE und speichern Sie das Ergebnis in OUTFILE. Wenn INFILE nicht vorhanden ist
Wird mitgeliefert, wird stdin verwendet. Wenn OUTFILE nicht angegeben wird, wird das LTS nicht gespeichert.

Wenn der Rewriter „jittyc“ verwendet wird, dann die Umgebungsvariable MCRL2_COMPILEREWRITER
(Standardwert: 'mcrl2compilerewriter') bestimmt das Skript, das den Rewriter kompiliert.
und MCRL2_COMPILEDIR (Standardwert: '.') bestimmt, wo temporäre Dateien gespeichert werden.

Beachten Sie, dass lps2lts zwischen jedem Paar mehrere Übergänge mit derselben Bezeichnung liefern kann
Zustände. Ist dies nicht erwünscht, können solche Übergänge durch Auftragen eines starken Klebers entfernt werden
Bisimulationsreduktion, beispielsweise mit dem Tool ltsconvert.

Das Format von OUTFILE wird durch seine Erweiterung bestimmt (es sei denn, es wird durch eine angegeben).
Möglichkeit). Die unterstützten Formate sind:

'aut' für das Aldebaran-Format (CADP),
„Punkt“ für das GraphViz-Format (wird nicht mehr als Eingabeformat unterstützt),
„fsm“ für das Finite-State-Machine-Format oder
„lts“ für das mCRL2-LTS-Format. Wenn der Jittyc-Rewriter verwendet wird, dann wird der
Umgebungsvariable MCRL2_COMPILEREWRITER (Standardwert: mcrl2compilerewriter)
bestimmt das Skript, das den Rewriter kompiliert, und MCRL2_COMPILEDIR (Standardwert:
'.') bestimmt, wo temporäre Dateien gespeichert werden. Beachten Sie, dass lps2lts mehrere liefern kann
Übergänge mit derselben Bezeichnung zwischen beliebigen Zustandspaaren. Ist dies nicht erwünscht, z
Übergänge können beispielsweise durch Anwendung einer starken Bisimulationsreduktion entfernt werden
das Tool ltsconvert.

OPTIONAL

zur Auswahl kann einer der folgenden sein:

-aNAMEN, --Handlung=NAMEN
Erkennen und melden Sie Aktionen im Übergangssystem, die Aktionsnamen haben von
NAMEN, eine durch Kommas getrennte Liste. Dies ist zum Beispiel nützlich, um das zu finden (oder zu beweisen).
Abwesenheit) eines Aktionsfehlers. Für jedes Vorkommen einer davon wird eine Nachricht gedruckt
diese Aktionsnamen. Mit dem Flag -t werden Traces zu diesen Aktionen generiert

-b[NUM], --bit-hash[=NUM]
Verwenden Sie Bit-Hashing zum Speichern von Zuständen und speichern Sie höchstens NUM Zustände. Das bedeutet, dass
Anstatt eine vollständige Aufzeichnung aller besuchten Staaten zu führen, wird ein Bit-Array verwendet
wird verwendet, um anzuzeigen, ob ein Hash eines Zustands bereits zuvor gesehen wurde oder nicht.
Dies bedeutet jedoch, dass diese Option dazu führen kann, dass Staaten mit anderen verwechselt werden
(Da sie demselben Hash zugeordnet sind), kann es nützlich sein, sehr große Datenmengen zu erkunden
LTSs, die sonst nicht erkundebar sind. Der Standardwert für NUM ist ungefähr
2*10^8 (das entspricht etwa 25 MB Speicher)

- zwischengespeichert
Verwenden Sie Aufzählungs-Caching-Techniken, um die Zustandsraumgenerierung zu beschleunigen.

-c[NAME/FUNKTION], --Zusammenfluss[=NAME/FUNKTION]
Wenden Sie die Priorisierung von Übergängen mit der Aktionsbezeichnung NAME an. (Wenn kein NAME vorhanden ist
Die angegebene Aktion (d. h. „-c“) hat Priorität für die Aktion „ctau“. Priorität geben
Um Tau zu verwenden, verwenden Sie die Flagge -ctau. Beachten Sie, dass, wenn der lineare Prozess nicht Tau-konfluent ist,
Der erzeugte Zustandsraum verzweigt sich notwendigerweise bis ähnlich zum Zustandsraum von
die LPs. Der verwendete Generierungsalgorithmus erfordert keinen linearen Prozess
Tau-konvergent sein.

-D, --Sackgasse
Deadlocks erkennen (d. h. für jeden Deadlock wird eine Meldung ausgegeben)

-F, --Abweichungen
Divergenzen erkennen (d. h. für jeden Zustand mit einer Divergenz (=Tau-Schleife) gibt es eine Nachricht
gedruckt). Der Algorithmus zur Erkennung der Divergenzen ist also für jeden Zustand linear
Wenn diese Option aktiviert ist, wird die Erkundung des Zustandsraums quadratisch und verursacht einen Zustand
Die Weltraumforschung wird langsamer, wenn diese Option aktiviert ist.

-yBOOL, --Dummy=BOOL
Ersetzen Sie freie Variablen im LPS durch Dummy-Werte basierend auf dem Wert von BOOL:
„Ja“ (Standard) oder „Nein“

--error-trace
Wenn während der Erkundung ein Fehler auftritt, speichern Sie eine Ablaufverfolgung für den Status, der nicht auftreten konnte
erforscht

--init-tsize=NUM
Legen Sie die Anfangsgröße der intern verwendeten Hash-Tabellen fest (Standard ist 10000).

-lNUM, --max=NUM
Erkunden Sie höchstens NUM Staaten

-mNAMEN, --multiaction=NAMEN
Erkennen und melden Sie Multiaktionen im Übergangssystem von NAMES, einem Komma-
getrennte Liste. Funktioniert wie -a, außer dass Mehrfachaktionen genau übereinstimmen.
einschließlich Datenparametern.

--keine Informationen
Fügen Sie OUTFILE keine Statusinformationen hinzu. Ohne diese Option fügt lps2lts den Status hinzu
Vektor zum LTS. Diese Option bewirkt, dass diese Informationen verworfen und angegeben werden
werden nur durch eine fortlaufende Nummer angezeigt. Explizite Zustandsinformationen sind nützlich für
B. zu Visualisierungszwecken, kann aber dazu führen, dass die OUTFILE wächst
wesentlich. Beachten Sie, dass diese Option beim Schreiben im AUT-Format implizit ist.

-oFORMAT, --aus=FORMAT
Speichern Sie die Ausgabe im angegebenen FORMAT

--Pflaume
Verwenden Sie Summand Pruning, um die Zustandsraumgenerierung zu beschleunigen.

-QNUM, --qlimit=NUM
Beschränken Sie die Aufzählung von Quantoren auf NUM Variablen. (Standard NUM=1000, NUM=0 für
unbegrenzt).

-rNAME/FUNKTION, --rewriter=NAME/FUNKTION
Rewrite-Strategie verwenden NAME: 'jitty' jitty rewriting (Standard) 'jittyc' kompiliert
Jitty Rewriting 'Jittyp' Jitty Rewriting mit Prover

-sNAME/FUNKTION, --Strategie=NAME/FUNKTION
Erkunden Sie den Zustandsraum mit der Strategie NAME: 'b', 'breadth' Breitensuche
(Standard) 'd', ' Depth' Tiefensuche 'p', 'priorisiert' Einzelpriorisierung
Aktionen auf sein erstes Argument sind von der Art Nat, wobei nur die Aktionen mit dem
Der niedrigste Wert für diesen Parameter wird ausgewählt. ZB wenn es Aktionen gibt a(3) und
b(4) a(3) bleibt und b(4) wird übersprungen. Aktionen ohne einen ersten Sortierparameter
Nat und Multiaktionen mit mehr als einer Aktion werden immer ausgewählt (Option ist
experimentell) 'q', 'rpriorisiert' priorisieren Aktionen anhand ihres ersten Arguments
Sortieren Sie Nat (siehe Option --prioritized) und wählen Sie zufällig eine davon aus, um eine zu erhalten
priorisierte Zufallssimulation (Option ist experimentell) 'r', 'random' random
Simulation. Aus allen nächsten Zuständen wird einer zufällig ausgewählt, unabhängig davon, ob
Dieser Zustand wurde bereits beobachtet. Daher nur Zufallssimulation
wird beendet, wenn ein Deadlock-Zustand auftritt.

--unterdrücken
Im ausführlichen Modus werden keine Fortschrittsmeldungen mit der Anzahl der Besuche gedruckt
Zustände und Übergänge. Bei großen Zustandsräumen kann die Anzahl der Fortschrittsmeldungen variieren
ganz schrecklich sein. Diese Funktion hilft, diese zu unterdrücken. Andere ausführliche Nachrichten,
B. die Gesamtzahl der erkundeten Staaten, bleiben einfach sichtbar.

--Zeiten[=FILE]
Zeitmesswerte an FILE anhängen. Messungen werden in Standardfehler geschrieben, wenn
es wird keine DATEI bereitgestellt

--todo-max=NUM
Behalten Sie höchstens NUM Zustände in Todo-Listen bei; Diese Option ist nur für die Breite relevant.
erste Suche, wobei NUM die maximale Anzahl von Zuständen pro Ebene ist, und für die Tiefe
erste Suche, wobei NUM die maximale Tiefe ist

-t[NUM], --verfolgen[=NUM]
Schreiben Sie einen kürzesten Trace zu jedem Zustand, der mit einer Aktion von NAMES from erreicht wird
Option --action, ist ein Deadlock, der mit --deadlock erkannt wurde, oder eine Divergenz
mit --divergence zu einer Datei erkannt. Es werden nicht mehr als NUM Spuren geschrieben. Wenn
NUM wird nicht angegeben, die Anzahl der Traces ist unbegrenzt. Für jeden Trace, der sein soll
Es wird eine eindeutige Datei mit der Erweiterung .trc (Trace) erstellt, die Folgendes enthält:
kürzester Trace vom Anfangszustand bis zum Deadlock-Zustand. Die Spuren können sein
Hübsch gedruckt und mit Tracepp in andere Formate konvertiert.

-u, --unused-data
Entfernen Sie keine ungenutzten Teile der Datenspezifikation

Standardoptionen:

-q, --ruhig
keine Warnmeldungen anzeigen

-v, - ausführlich
kurze Zwischennachrichten anzeigen

-d, --debuggen
detaillierte Zwischenmeldungen anzeigen

-Log-Ebene=LEVEL
Zwischenmeldungen bis einschließlich Ebene anzeigen

-h, --help
Hilfeinformationen anzeigen

--Version
Versionsinformationen anzeigen

Verwenden Sie lps2lts online über die Dienste von onworks.net