pbes2bes – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

pbes2bes – Generieren Sie ein BES aus einem PBES.

ZUSAMMENFASSUNG

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

BESCHREIBUNG

Liest das PBES aus INFILE und schreibt ein entsprechendes BES in OUTFILE. Wenn INFILE nicht vorhanden ist
vorhanden, stdin wird verwendet. Wenn OUTFILE nicht vorhanden ist, wird stdout verwendet.

OPTIONAL

zur Auswahl kann einer der folgenden sein:

-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, --aus=FORMAT
Verwenden Sie das Ausgabeformat 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

-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

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