Ini ialah arahan mona yang boleh dijalankan dalam penyedia pengehosan percuma OnWorks menggunakan salah satu daripada berbilang stesen kerja dalam talian percuma kami seperti Ubuntu Online, Fedora Online, emulator dalam talian Windows atau emulator dalam talian MAC OS.
JADUAL:
NAMA
mona - prosedur keputusan untuk logik WS1S dan WS2S
SINOPSIS
mona [ pilihan ] fail mona
DESCRIPTION
MONA ialah alat yang menterjemah formula dalam logik WS1S atau WS2S ke dalam keadaan terhingga
automata yang diwakili oleh BDD. Formula mungkin menyatakan corak carian, temporal
sifat sistem reaktif, menghuraikan kekangan pokok, dll. MONA juga menganalisis
automatik yang terhasil daripada kompilasi, dan menentukan sama ada formula itu sah dan,
jika formula tidak sah, menjana contoh balas.
Projek MONA ialah projek penyelidikan di Jabatan Sains Komputer, Aarhus
University.
Dokumentasi penuh, kod sumber GPL, dan kertas penyelidikan berkaitan boleh didapati daripada
Laman utama projek MONA di http://www.brics.dk/mona
PILIHAN
-w Keluarkan keseluruhan automatik. Lalai ialah hanya mengeluarkan saiznya.
-n Jangan menganalisis automaton. Lalai adalah untuk menganalisis untuk kesahihan dan ketidakpuasan
dan untuk menjana contoh dan contoh balas yang memuaskan.
-t Cetak masa berlalu untuk setiap fasa. Jika -s juga digunakan, masa untuk setiap automaton
operasi juga dicetak.
-s Cetak statistik. Mencetak maklumat untuk setiap operasi automaton dan ringkasan.
-i Cetak automata perantaraan (menyiratkan -s).
-d Buang AST, boleh simbol dan kod DAG. Berguna untuk nyahpepijat.
-q Senyap, jangan cetak kemajuan.
-e Dayakan kompilasi berasingan. (Lihat pembolehubah persekitaran MONALIB di bawah.)
-on Tahap pengoptimuman kod N (0=tiada, 1=selamat, 2=heuristik) (lalai 1).
-r Lumpuhkan penyusunan semula indeks BDD, gunakan susunan pengisytiharan sebagai susunan indeks. lalai
adalah untuk menyusun semula indeks BDD secara heuristik.
-f Paksa gaya keluaran mod pokok biasa. Hanya terpakai untuk mod WSRT.
-m Emulasi M2L-Str alternatif (gaya v1.3).
-h Dayakan analisis penerimaan yang diwarisi.
-u Nyahsekat automata output. Cipta automata konvensional dengan menukar "tidak peduli"
menyatakan untuk "menolak" keadaan dan meminimumkan.
-gw Output seluruh automaton dalam format Graphviz (menyiratkan -n -q). (Graphviz tersedia
at http://www.graphviz.org/)
-gs Output contoh pokok yang memuaskan dalam format Graphviz (menyiratkan -q).
-gc Output pokok contoh balas dalam format Graphviz (menyiratkan -q).
-gd Buang kod DAG dalam format Graphviz (menyiratkan -n -q).
-xw Output seluruh automaton dalam format luaran (menyiratkan -n -q). "Format luaran" ialah
format yang digunakan oleh dfalib dan gtalib, lihat pakej sumber.
PERSEKITARAN
MONALIB
Mentakrifkan direktori yang digunakan untuk automata kompilasi berasingan (lalai ialah semasa
direktori).
Gunakan mona dalam talian menggunakan perkhidmatan onworks.net
