Dies ist der Befehl ltsconvert, der beim kostenlosen Hosting-Anbieter OnWorks mit einer unserer zahlreichen kostenlosen Online-Workstations wie Ubuntu Online, Fedora Online, dem Windows-Online-Emulator oder dem MAC OS-Online-Emulator ausgeführt werden kann
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
