pbes2bool – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

pbes2bool – Generieren Sie ein BES aus einem PBES und lösen Sie es.

ZUSAMMENFASSUNG

pbes2bool [zur Auswahl]...[IM ORDNER]

BESCHREIBUNG

Löst (P)BES aus INFILE. Wenn INFILE nicht vorhanden ist, wird stdin verwendet.

OPTIONAL

zur Auswahl kann einer der folgenden sein:

-c, --Schalter
Drucken Sie am Ende einen Baum aus, der mit Instanziierungen der linken Seite von beschriftet ist
Gleichungen; Dieser Baum ist ein Hinweis darauf, wie pbes2bool zur Gültigkeit kam bzw
Ungültigkeit des PBES

-eLEVEL, --löschen=LEVEL
Verwenden Sie die Entfernungsebene LEVEL, um BES-Variablen zu entfernen. „None“ entfernt generierte BES nicht
Variablen. Dies kann zu einer übermäßigen Speichernutzung führen. (Standard) 'einige' entfernen
generierte BES-Variablen, die nicht verwendet werden, es sei denn, die rechte Seite davon
Gleichung ist wahr oder falsch. Der rhss von Variablen muss ggf. neu berechnet werden
erneut angetroffen, was ganz normal ist. 'all' entfernt jede bes-Variable, die vorhanden ist
wird in keiner Gleichung mehr verwendet. Das ist ziemlich speichereffizient, kann aber sein
sehr zeitaufwändig, da der Rhss der entfernten BES-Variablen möglicherweise sein muss
ziemlich oft neu berechnet.

-H, --hashtables
Verwenden Sie Hashtabellen beim Ersetzen in BES-Gleichungen und übersetzen Sie intern
Ausdrücke zu binären Entscheidungsdiagrammen (aus Leistungsgründen nicht empfohlen)

-iFORMAT, --In=FORMAT
Verwenden Sie das Eingabeformat FORMAT: 'pbes' PBES im internen Format 'pbes_text' PBES in
internes Textformat 'text' PBES im Textformat (mCRL2) Format 'bes' BES in intern
Format „bes_text“ BES im internen Textformat „cwi“ BES im CWI-Format „pgsolver“
BES im PGSolver-Format

-oFORMAT, --Ausgabe=FORMAT
Verwenden Sie das Ausgabeformat FORMAT (diese Option ist veraltet. Verwenden Sie das Tool pbes2bes
stattdessen).

-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

-zSUCHE, --Suche=SUCHE
Verwenden Sie die Suchstrategie SUCHE: 'Breite zuerst'. Berechnen Sie die rechte Seite von
boolesche Variablen nach dem Prinzip „Wer zuerst kommt, mahlt zuerst“. Dies ist vergleichbar mit a
Breitensuche. Dies eignet sich gut zum Generieren von Gegenbeispielen. (Standard)
'Tiefe zuerst' Berechnet die rechte Seite einer booleschen Variablen, wo die letzte ist
Die generierte Variable wird zunächst untersucht. Dies entspricht einem Depth-First
suchen. Dies kann die Breitensuche erheblich übertreffen, wenn die Gültigkeit von
Eine Formel wird nach einer größeren Tiefe ermittelt. 'b' Kurzschrift für Breite zuerst.
'd' Kurzschrift für „Depth-First“.

-sSTRAT, --Strategie=STRAT
Substitutionsstrategie verwenden STRAT: '0' Berechne alle möglichen booleschen Gleichungen
vom Ausgangszustand ohne Optimierung erreicht. Das sind die meisten Daten
effiziente Option pro generierter Gleichung. (Standard) '1' Optimieren bis sofort
Ersetzen der rechten Seite durch bereits untersuchte Variablen, die wahr sind
oder false beim Generieren eines Ausdrucks. Dies ist genauso speichereffizient wie 0. '2' In
Ersetzen Sie zusätzlich zu 1 auch Variablen, die wahr oder falsch sind, in ein bereits
erzeugt auf der rechten Seite. Dies kann dazu führen, dass bestimmte Variablen nicht mehr erreichbar sind
(z. B. X0 in X0 und X1, wenn X1 falsch wird, vorausgesetzt, X0 kommt nirgendwo anders vor.
Es wird gepflegt, welche Variablen nicht mehr erreichbar sind, da diese nicht mehr erreichbar sind
Untersucht werden. Abhängig vom PBES kann dies die Größe des verringern
generiert BES erheblich, erfordert jedoch einen größeren Speicherbedarf. '3' Zoll
Zusätzlich zu 2 untersuchen Sie für generierte Variablen, ob sie in einer Schleife auftreten.
sodass sie je nach Festkommasymbol auf wahr oder falsch gesetzt werden können.
Dies kann die zum Erstellen einer Gleichung benötigte Zeit erheblich verlängern.

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

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