mcrl22lps – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

mcrl22lps – Übersetzen Sie eine mCRL2-Spezifikation in ein LPS

ZUSAMMENFASSUNG

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

BESCHREIBUNG

Linearisiert die mCRL2-Spezifikation in INFILE und schreibt die resultierenden LPS in OUTFILE. Wenn
OUTFILE ist nicht vorhanden, stdout wird verwendet. Wenn INFILE nicht vorhanden ist, wird stdin verwendet.

OPTIONAL

zur Auswahl kann einer der folgenden sein:

-b, --binär
Verwenden Sie beim Clustering binäre Fallfunktionen anstelle von n-ären Funktionen. in Anwesenheit von
-w/--newstate, Zustandsvariablen werden durch einen Vektor boolescher Variablen codiert

-e, --check-only
Syntax und statische Semantik prüfen; nicht linearisieren

-c, - Cluster
Alle Aktionen im endgültigen LPS werden geclustert. Clustering bedeutet, dass Summanden mit dem
Gleiche Aktionsbezeichnungen werden gruppiert. Zum Beispiel a(f1) . P(g1) + a(f2) .
P(g2) wird durch sum b: Bool ersetzt. a(if(b, f1, f2)) . P(if(b, f2, g2)). Der
Der Vorteil besteht darin, dass die Anzahl der Summanden auf diese Weise erheblich reduziert werden kann.
Der Nachteil besteht darin, dass Summenoperatoren eingeführt und neue Daten sortiert werden
Hilfsfunktionen werden generiert. Um die Entstehung neuer Sorten zu vermeiden,
die Option -b/--binary kann verwendet werden.

-D, --Delta
Fügen Sie jedem Zustand in jedem Prozess einen True->Delta-Summanden hinzu. Diese Deltas fassen alles zusammen
andere bedingte zeitgesteuerte Deltas, wodurch die Anzahl der Delta-Summanden effektiv reduziert wird
drastisch im resultierenden linearen Prozess; beschleunigt die Linearisierung. Dies ist das
Standardmäßig, aber es geht nicht richtig mit der Zeit um.

-lNAME/FUNKTION, --lin-Methode=NAME/FUNKTION
Verwenden Sie die Linearisierungsmethode NAME: „regular“, um ein LPS in regulärer Form zu generieren
(Angabe sollte regulär sein) (Standard) 'regular2' für eine Variante von 'regular'
das verwendet mehr Datenvariablen (nützlich, wenn „regulär“ nicht funktioniert) für „Stack“.
Verwendung von Stack-Datentypen (nützlich, wenn „regular“ und „regular2“ nicht funktionieren)

-w, --newstate
Zustandsvariablen werden mithilfe von Aufzählungstypen anstelle positiver natürlicher Typen codiert
Zahlen (Pos). Durch die Verwendung dieser Option werden neue endliche Sortierungen mit dem Namen Enumk generiert
wobei k die Größe der Domäne ist. Außerdem Hilfsfallfunktionen und Gleichheiten
sind festgelegt. In Kombination mit der Option --binary werden die endlichen Sortierungen kodiert
durch Boolesche Werte. (erfordert die Linearisierungsmethode „regular“ oder „regular2“).

-z, --no-alpha
Alphabetverkürzungen werden nicht angewendet. Standardmäßig versucht mcrl22lps zu verteilen
Kommunikations-, Versteck- und Zulassungsoperatoren über den Parallelkompositionsoperator as
Dies reduziert die Größe zwischenliegender linearer Prozesse. Durch die Verwendung dieser Option wird dies
Schritt kann vermieden werden. Der Name leitet sich von den Alphabetaxiomen der Prozessalgebra ab.

-n, --no-cluster
Die Aktionen in Zwischen-LPSs werden nicht geclustert, bevor sie parallel geschaltet werden.
Standardmäßig werden diese Prozesse geclustert, um einen Anstieg der Anzahl zu vermeiden
Summanden bei der Umwandlung zweier paralleler linearer Prozesse in einen einzigen linearen
Verfahren. Stellt man einen linearen Prozess mit M Summanden parallel zu einem linearen
Prozess mit N Summanden Der resultierende Prozess hat M×N + M + N Summanden. Sowohl M als auch
N kann durch Clustering auf Kosten der Einführung neuer Sorten erheblich reduziert werden
und Funktionen. Siehe -c/--cluster, insb. für eine kurze Erklärung der Clusterbildung
verarbeiten.

--no-constelm
Versuchen Sie nicht, beim Generieren eines linearen Prozesses eine konstante Eliminierung anzuwenden.

-g, --no-deltaelm
Vermeiden Sie das Entfernen unerwünschter Delta-Summanden. Aufgrund der Existenz von Zeit, Delta
Summanden können nicht weggelassen werden. Aufgrund des Vorhandenseins von Mehrfachaktionen ist die Anzahl der
Summanden können riesig sein. Der Algorithmus zum Entfernen von Delta-Summanden funktioniert einfach nach
Vergleichen Sie jeden Delta-Summanden mit jedem anderen Summanden, um festzustellen, ob die Bedingung erfüllt ist
des einen impliziert den Zustand des anderen. Offensichtlich ist dies quadratisch
ist komplex und kann lange dauern.

-f, --no-globvars
Instanziieren Sie Don't-Care-Werte mit beliebigen Konstanten, anstatt sie zu modellieren
durch globale Variablen. Dies hat keine Auswirkungen auf globale Variablen, die im deklariert sind
Spezifikation.

-o, --no-rewrite
Datenbegriffe während der Linearisierung nicht neu schreiben; nützlich, wenn das Rewrite-System dies tut
nicht beenden. Diese Option schaltet auch die Anwendung von Konstanten aus
Beseitigung.

-m, --no-sumelm
Vermeiden Sie die Anwendung der Summeneliminierung bei paralleler Komposition

-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

-a, --statenames
Die Namen der generierten Datenparameter werden um den Namen des Prozesses erweitert
in dem sie vorkommen. Dadurch lässt sich leichter feststellen, woher der Parameter stammt.

-T, --zeitgesteuert
Übersetzen Sie den Prozess in eine lineare Form und bewahren Sie dabei alle zeitgesteuerten Informationen. Parallel zu
Die Anzahl der möglichen Zeiteinschränkungen bei Prozessen kann groß sein und zu einer Verlangsamung führen
Linearisierung. Übertragen Sie die Option --delta, die eine viel schnellere Übersetzung ermöglicht
behält das Timing nicht korrekt bei

--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

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