lpsinvelm – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

lpsinvelm – Invarianten prüfen und diese verwenden, um Summanden eines LPS zu vereinfachen oder zu eliminieren

ZUSAMMENFASSUNG

lpsinvelm [zur Auswahl]... --invfile=INVFILE [IM ORDNER [AUSGABE]]

BESCHREIBUNG

Überprüft, ob die boolesche Formel (ein mCRL2-Datenausdruck vom Typ Bool) als bereitgestellt wurde
invariant ist eine Invariante der linearen Prozessspezifikation (LPS) in INFILE. Wenn das ist
In diesem Fall eliminiert das Tool alle Summanden des LPS, deren Bedingung verletzt
invariant und schreibt das Ergebnis in OUTFILE. Wenn INFILE vorhanden ist, wird stdin verwendet. Wenn
OUTFILE ist nicht vorhanden, stdout wird verwendet.

Das Tool kann auch verwendet werden, um die Bedingungen der Summanden des gegebenen LPS zu vereinfachen.

OPTIONAL

zur Auswahl kann einer der folgenden sein:

-y, --all-Verstöße
enden nicht, sobald eine einzelne Verletzung der Invariante gefunden wird, sondern
Melden Sie stattdessen alle Verstöße

-c, --Gegenbeispiel
Zeigen Sie eine Bewertung an, die angibt, warum die Invariante möglicherweise verletzt werden könnte, wenn dies der Fall ist
ist unsicher, ob ein Summand die Invariante verletzt

-o, --Induktion
Wenden Sie die Induktion auf Listen an

-iINVDATEI, --invariant=INVDATEI
Verwenden Sie die boolesche Formel (einen mCRL2-Datenausdruck der Sortierung Bool) in INVFILE als
unveränderlich

-n, --no-check
Überprüfen Sie nicht, ob die Invariante gilt, bevor Sie nicht erreichbare Summanden eliminieren

-e, --keine Eliminierung
Eliminieren oder vereinfachen Sie Summanden nicht, sondern fügen Sie zu jeder Bedingung die Invariante hinzu

-pPRÄFIX, --print-dot=PRÄFIX
Speichern Sie eine .dot-Datei des resultierenden BDD, wenn nicht festgestellt werden kann, ob a
Summand verletzt die Invariante; PREFIX wird als Präfix der Ausgabedateien verwendet

-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

-l, --vereinfachen-alle
Vereinfachen Sie die Bedingungen aller Summanden, anstatt nur die Summanden zu eliminieren
deren Bedingungen in Verbindung mit der Invariante Widersprüche sind

-zLÖSER, --smt-solver=LÖSER
Verwenden Sie SOLVER, um inkonsistente Pfade aus den intern verwendeten BDDs zu entfernen (standardmäßig
es wird keine Pfadeliminierung angewendet): 'cvc' der SMT-Löser CVC3

-tLIMIT, --Zeitlimit=LIMIT
Verbringen Sie höchstens LIMIT Sekunden damit, eine einzelne Formel zu beweisen

--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 lpsinvelm online über die Dienste von onworks.net