Dies ist der Befehl mona, 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
mona – ein Entscheidungsverfahren für die Logiken WS1S und WS2S
ZUSAMMENFASSUNG
mona [ Optionen ] Mona-Datei
BESCHREIBUNG
MONA ist ein Werkzeug, das Formeln in den Logiken WS1S oder WS2S in endliche Zustände übersetzt
Automaten, dargestellt durch BDDs. Die Formeln können zeitliche Suchmuster ausdrücken
Eigenschaften reaktiver Systeme, Parse-Tree-Einschränkungen usw. MONA analysiert auch die
Automat, der sich aus der Kompilierung ergibt, und bestimmt, ob die Formel gültig ist und,
Wenn die Formel ungültig ist, wird ein Gegenbeispiel generiert.
Das MONA-Projekt ist ein Forschungsprojekt am Institut für Informatik in Aarhus
University.
Die vollständige Dokumentation, der GPL-Quellcode und zugehörige Forschungsarbeiten sind unter verfügbar
Homepage des MONA-Projekts unter http://www.brics.dk/mona
OPTIONAL
-w Gibt den gesamten Automaten aus. Standardmäßig wird nur die Größe ausgegeben.
-n Automaten nicht analysieren. Standardmäßig wird auf Gültigkeit und Unerfüllbarkeit analysiert
und ein zufriedenstellendes Beispiel und Gegenbeispiel zu generieren.
-t Gibt die verstrichene Zeit für jede Phase aus. Wenn auch -s verwendet wird, die Zeit für jeden Automaten
Der Vorgang wird ebenfalls ausgedruckt.
-s Statistiken drucken. Druckt Informationen zu jedem Automatenvorgang und eine Zusammenfassung.
-i Gibt Zwischenautomaten aus (impliziert -s).
-d AST, Symboltabelle und Code-DAG ausgeben. Nützlich zum Debuggen.
-q Ruhig, Fortschritt nicht drucken.
-e Separate Kompilierung aktivieren. (Siehe die Umgebungsvariable MONALIB unten.)
-oN Codeoptimierungsstufe N (0=keine, 1=sicher, 2=heuristisch) (Standard 1).
-r Deaktiviert die Neuordnung des BDD-Index und verwendet die Reihenfolge der Deklaration als Indexordnung. Standard
besteht darin, BDD-Indizes heuristisch neu zu ordnen.
-f Erzwingt den normalen Ausgabestil im Baummodus. Gilt nur für den WSRT-Modus.
-m Alternative M2L-Str-Emulation (v1.3-Stil).
-h Aktiviert die geerbte Akzeptanzanalyse.
-u Ausgabeautomaten einschränken. Erstellen Sie konventionelle Automaten, indem Sie „don't-care“ umwandeln
Staaten können Staaten „ablehnen“ und minimieren.
-gw Gibt den gesamten Automaten im Graphviz-Format aus (impliziert -n -q). (Graphviz ist verfügbar
at http://www.graphviz.org/)
-gs Ausgabe eines zufriedenstellenden Beispielbaums im Graphviz-Format (impliziert -q).
-gc Gegenbeispielbaum im Graphviz-Format ausgeben (impliziert -q).
-gd Code-DAG im Graphviz-Format ausgeben (impliziert -n -q).
-xw Gibt den gesamten Automaten im externen Format aus (impliziert -n -q). „Externes Format“ ist das
Das von dfalib und gtalib verwendete Format finden Sie im Quellpaket.
MONALIB
Definiert das Verzeichnis, das für separate Kompilierungsautomaten verwendet wird (Standard ist aktuell).
Verzeichnis).
Nutzen Sie Mona online über die Dienste von onworks.net
