ltsconvert – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

ltsconvert – LTS konvertieren und optional minimieren

ZUSAMMENFASSUNG

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

BESCHREIBUNG

Konvertieren Sie das beschriftete Übergangssystem (LTS) von INFILE in OUTFILE im angeforderten Format
Format nach Anwendung der ausgewählten Minimierungsmethode (Standard ist keine). Wenn OUTFILE ist
nicht mitgeliefert, stdout wird verwendet. Wenn INFILE nicht angegeben wird, wird stdin verwendet.

Das Ausgabeformat wird durch die Erweiterung von OUTFILE bestimmt, das Eingabeformat dagegen
wird durch den Inhalt von INFILE bestimmt. Mit den Optionen --in und --out kann die Eingabe erzwungen werden
und Ausgabeformate. 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 (Standard)

OPTIONAL

zur Auswahl kann einer der folgenden sein:

-D, --bestimmen
LTS bestimmen

-eNAME/FUNKTION, --Gleichwertigkeit=NAME/FUNKTION
Generieren Sie ein äquivalentes LTS, wobei die Äquivalenzidentität NAME: „none“ erhalten bleibt
Äquivalenz (Standard) 'bisim' starke Bisimilarität 'bisim-sig' starke Bisimilarität
unter Verwendung der Signaturverfeinerung 'branching-bisim' branching bisimilarity 'branching-
bisim-sig‘ Verzweigungsbisimilarität unter Verwendung der Signaturverfeinerung „dpbranching-bisim“
Divergenz, die die Verzweigung erhält Bisimularität 'dpbranching-bisim-sig' Divergenz
Wahrung der Verzweigungsbisimilarität mithilfe der Signaturverfeinerung „schwach-bisim“ schwach
Bisimilarität 'weak-bisim-sig' schwache Bisimularität mit Signaturverfeinerung 'dpweak-
Bisim-Divergenz unter Wahrung der schwachen Bisimularität, „dpweak-bisim-sig“-Divergenz
Beibehaltung der schwachen Bisimilarität mithilfe der starken Simulation der Signaturverfeinerung „sim“.
Äquivalenz „Spur“ starke Spurenäquivalenz „schwache Spur“ schwache Spurenäquivalenz
'Tau-Stern' Tau-Stern-Reduktion

-iFORMAT, --In=FORMAT
Verwenden Sie FORMAT als Eingabeformat

-lFILE, --lps=FILE
Verwenden Sie FILE als LPS, aus dem das Eingabe-LTS generiert wurde. Dies könnte erforderlich sein
Speichern Sie die korrekten Parameternamen der Zustände beim Speichern im FSM-Format und in
Konvertieren Sie Nicht-mCRL2-LTSs in ein mCRL2-LTS

--no-reach
Führen Sie keine Erreichbarkeitsprüfung für den Eingabe-LTS durch

-n, --no-state
Lassen Sie Statusinformationen weg, wenn Sie im Punktformat speichern

-oFORMAT, --aus=FORMAT
Verwenden Sie FORMAT als Ausgabeformat

--tau=ACTNAMES
Betrachten Sie Aktionen mit einem Namen in der durch Kommas getrennten Liste ACTNAMES als intern
(tau)-Aktionen zusätzlich zu den durch die Eingabe als solche definierten Aktionen

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

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

Nutzen Sie ltsconvert online über die Dienste von onworks.net