Ini adalah perintah mona yang dapat dijalankan di penyedia hosting gratis OnWorks menggunakan salah satu dari beberapa workstation online gratis kami seperti Ubuntu Online, Fedora Online, emulator online Windows atau emulator online MAC OS
PROGRAM:
NAMA
mona - prosedur keputusan untuk logika WS1S dan WS2S
RINGKASAN
mona [ Pilihan ] file mona
DESKRIPSI
MONA adalah alat yang menerjemahkan rumus dalam logika WS1S atau WS2S menjadi keadaan terbatas
automata diwakili oleh BDD. Rumus dapat mengekspresikan pola pencarian, temporal
properti sistem reaktif, batasan pohon parse, dll. MONA juga menganalisis
otomat yang dihasilkan dari kompilasi, dan menentukan apakah rumus tersebut valid dan,
jika rumus tidak valid, menghasilkan contoh tandingan.
Proyek MONA adalah proyek penelitian di Departemen Ilmu Komputer, Aarhus
Universitas.
Dokumentasi lengkap, kode sumber GPL, dan makalah penelitian terkait tersedia dari
Beranda proyek MONA di http://www.brics.dk/mona
PILIHAN
-w Keluarkan seluruh otomat. Defaultnya adalah hanya menampilkan ukurannya.
-n Jangan menganalisis otomat. Defaultnya adalah menganalisis validitas dan ketidakpuasan
dan untuk menghasilkan contoh dan kontra-contoh yang memuaskan.
-t Cetak waktu yang telah berlalu untuk setiap fase. Jika -s juga digunakan, waktu untuk setiap otomat
operasi juga dicetak.
-s Cetak statistik. Mencetak informasi untuk setiap operasi otomat dan ringkasan.
-i Mencetak automata perantara (menyiratkan -s).
-d Buang AST, simbol, dan kode DAG. Berguna untuk debugging.
-q Tenang, jangan mencetak kemajuan.
-e Aktifkan kompilasi terpisah. (Lihat variabel lingkungan MONALIB di bawah.)
-on Tingkat optimasi kode N (0=tidak ada, 1=aman, 2=heuristik) (default 1).
-r Nonaktifkan pengurutan ulang indeks BDD, gunakan urutan deklarasi sebagai pengurutan indeks. Bawaan
adalah menyusun ulang indeks BDD secara heuristik.
-f Memaksa gaya keluaran mode pohon normal. Hanya berlaku untuk mode WSRT.
-m Alternatif M2L-Str emulasi (gaya v1.3).
-h Mengaktifkan analisis penerimaan yang diwariskan.
-u Membatasi automata keluaran. Buat automata konvensional dengan mengonversi "tidak peduli"
menyatakan untuk "menolak" menyatakan dan meminimalkan.
-gw Output seluruh otomat dalam format Graphviz (menyiratkan -n -q). (Graphviz tersedia
at http://www.graphviz.org/)
-gs Output pohon contoh yang memuaskan dalam format Graphviz (menyiratkan -q).
-gc Output pohon contoh kontra dalam format Graphviz (menyiratkan -q).
-gd Dump code DAG dalam format Graphviz (menyiratkan -n -q).
-xw Keluarkan seluruh otomat dalam format eksternal (menyiratkan -n -q). "Format eksternal" adalah
format yang digunakan oleh dfalib dan gtalib, lihat paket sumber.
LINGKUNGAN
MONALIB
Mendefinisikan direktori yang digunakan untuk automata kompilasi terpisah (default adalah saat ini
direktori).
Gunakan mona online menggunakan layanan onworks.net
