Questo è il comando mona che può essere eseguito nel provider di hosting gratuito OnWorks utilizzando una delle nostre molteplici workstation online gratuite come Ubuntu Online, Fedora Online, emulatore online Windows o emulatore online MAC OS
PROGRAMMA:
NOME
mona - una procedura di decisione per le logiche WS1S e WS2S
SINOSSI
mona [ Opzioni ] file-mona
DESCRIZIONE
MONA è uno strumento che traduce formule nelle logiche WS1S o WS2S in stati finiti
automi rappresentati da BDD. Le formule possono esprimere modelli di ricerca, temporali
proprietà dei sistemi reattivi, analisi dei vincoli dell'albero, ecc. MONA analizza anche il
automa risultante dalla compilazione, e determina se la formula è valida e,
se la formula non è valida, genera un controesempio.
Il progetto MONA è un progetto di ricerca presso il Dipartimento di Informatica, Aarhus
University.
La documentazione completa, il codice sorgente GPL e i relativi documenti di ricerca sono disponibili presso il
Home page del progetto MONA su http://www.brics.dk/mona
VERSIONI
-w Emette l'intero automa. L'impostazione predefinita è solo l'output della sua dimensione.
-n Non analizzare l'automa. L'impostazione predefinita è analizzare la validità e l'insoddisfazione
e per generare un esempio soddisfacente e controesempio.
-t Stampa il tempo trascorso per ogni fase. Se si usa anche -s, il tempo per ogni automa
viene stampata anche l'operazione.
-s Stampa le statistiche. Stampa le informazioni per ogni operazione dell'automa e un riepilogo.
-i Stampa gli automi intermedi (implica -s).
-d Scarica AST, tabella dei simboli e codice DAG. Utile per il debug.
-q Silenzioso, non stampa i progressi.
-e Abilita la compilazione separata. (Vedi la variabile d'ambiente MONALIB di seguito.)
-oN Livello di ottimizzazione del codice N (0=nessuno, 1=sicuro, 2=euristico) (default 1).
-r Disabilita il riordino dell'indice BDD, usa l'ordine di dichiarazione come ordinamento dell'indice. Predefinito
consiste nel riordinare euristicamente gli indici BDD.
-f Forza il normale stile di output in modalità albero. Applicabile solo per la modalità WSRT.
-m Emulazione alternativa M2L-Str (stile v1.3).
-h Abilita l'analisi di accettazione ereditata.
-u Automi di output senza restrizioni. Crea automi convenzionali convertendo "non importa"
afferma di "rifiutare" gli stati e minimizza.
-gw Emette l'intero automa in formato Graphviz (implica -n -q). (Graphviz è disponibile
at http://www.graphviz.org/)
-gs Albero di esempio di output soddisfacente in formato Graphviz (implica -q).
-gc Albero di controesempio di output in formato Graphviz (implica -q).
-gd Scarica il codice DAG in formato Graphviz (implica -n -q).
-xw Emette l'intero automa in formato esterno (implica -n -q). "Formato esterno" è il
formato utilizzato da dfalib e gtalib, vedere il pacchetto sorgente.
AMBIENTE
MONALIB
Definisce la directory usata per gli automi a compilazione separata (l'impostazione predefinitaècorrente
rubrica).
Usa mona online utilizzando i servizi onworks.net
