maria - Online di Awan

PROGRAM:

NAMA

maria - Penganalisis Jangkauan Modular untuk jaring Petri tingkat tinggi

RINGKASAN

Maria [Pilihan] arsip...

DESKRIPSI

Halaman manual ini mendokumentasikan secara singkat Maria memerintah. Dokumentasi yang lebih lengkap adalah
tersedia dalam format Info GNU; Lihat di bawah.

Maria adalah program yang menganalisis model sistem konkuren, dijelaskan dalam inputnya
bahasa yang didasarkan pada Jaring Sistem Aljabar. Formalisme dipresentasikan oleh Ekkart
Kindler dan Hagen Völzer di ICATPN'98, keluwesan in Aljabar Nets.
Jaring Sistem Aljabar adalah kerangka kerja yang tidak mendefinisikan tipe data atau aljabar apa pun
operasi. Sistem tipe data dan operasi di Maria dirancang dengan tingkat tinggi
bahasa pemrograman dan spesifikasi dalam pikiran. Meskipun demikian, setiap model Maria memiliki
pembukaan terbatas.
Untuk memastikan interoperabilitas dengan alat jaringan Petri tingkat rendah, Maria menerjemahkan pengidentifikasi dalam
membuka jaring ke string karakter alfanumerik dan garis bawah. Filternya
nama lipat.pl dapat digunakan atau diadaptasi untuk meningkatkan keterbacaan pengidentifikasi.

PILIHAN

Maria mengikuti sintaks baris perintah GNU yang biasa, dengan opsi panjang dimulai dengan dua
tanda hubung (`-'). Ringkasan opsi disertakan di bawah ini. Untuk deskripsi lengkap, lihat
file Info.

-a membatasi, --array-batas=membatasi
Batasi ukuran tipe indeks array menjadi membatasi nilai-nilai yang mungkin. Batas 0
menonaktifkan pemeriksaan.

-b model, --luasnya-pencarian pertama=model
Hasilkan grafik jangkauan dari model menggunakan pencarian luas-pertama.

-C direktori, --kompilasi=direktori
Hasilkan kode C di direktori untuk mengevaluasi ekspresi dan untuk level rendah
rutinitas algoritma analisis instance transisi. Ketika opsi ini digunakan,
kesalahan evaluasi dilaporkan dengan cara yang sedikit berbeda. Penerjemah
menampilkan penilaian dan ekspresi yang menyebabkan kesalahan pertama dalam suatu keadaan; NS
kode yang dikompilasi menampilkan jumlah kesalahan. Untuk alasan kinerja,
kode yang dihasilkan tidak memeriksa kesalahan luapan saat menambahkan item ke multi-set.

-C, --tidak dikompilasi
Lawan dari -C. Evaluasi semua ekspresi dalam penerjemah bawaan. Ini adalah
perilaku default.

-D simbol, --tentukan=simbol
Tentukan simbol praprosesor simbol.

-d model, --kedalaman-pencarian-pertama=model
Hasilkan grafik jangkauan dari model menggunakan pencarian mendalam-pertama.

-E selang, --tepi =selang
Saat membuat grafik jangkauan, laporkan ukuran grafik setelah setiap
selang tepi yang dihasilkan.

-e tali, --eksekusi=tali
Eksekusi tali.

-g file grafik, --grafik=file grafik
Muat grafik jangkauan yang dihasilkan sebelumnya dari file grafik.rgh.

-H h[,f[,t]], --hash=h[,f[,t]]
Konfigurasikan parameter untuk verifikasi probabilistik (-P). Alokasikan t universal
fungsi hash dari f elemen dan tabel hash yang sesuai dari h bit masing-masing. Keduanya h
dan f akan dibulatkan ke nilai berikutnya yang sesuai.

-?, -H, --membantu
Cetak ringkasan opsi baris perintah ke Maria dan keluar.

-I direktori, --termasuk=direktori
Menambahkan direktori ke daftar direktori yang dicari termasuk file.

-i kolom, --lebar=kolom
Atur margin kanan output ke kolom. Standarnya adalah 80.

-j proses, --pekerjaan=proses
Saat memeriksa properti keselamatan (opsi -L, -M dan -P), gunakan pekerja sebanyak ini
proses untuk mempercepat analisis pada komputer multiprosesor. Lihat juga -k dan
-Z.

-k pelabuhan[/tuan rumah], --menghubungkan=pelabuhan[/tuan rumah]
Distribusikan pemeriksaan model keamanan (opsi -L, -M dan -P) dalam jaringan TCP/IP. Untuk
server, hanya pelabuhan ditentukan sebagai integer 16-bit unsigned, biasanya antara
1024 dan 65535. Untuk proses pekerja, pelabuhan/tuan rumah menentukan port dan
alamat servernya. Lihat juga -j.

-L model, --tanpa rugi=model
Beban model dan bersiap untuk menganalisisnya dengan membangun satu set status yang dapat dijangkau
dalam file disk. Lihat juga -M, -P, -j dan -k.

-m model, --model=model
Beban model dan hapus grafik jangkauannya.

-M model, --md5-dipadatkan=model
Beban model dan bersiaplah untuk menganalisisnya dengan membuat perkiraan yang berlebihan dari
kumpulan status yang dapat dijangkau dalam memori utama. Lihat juga -P, -L, -j dan -k.

-N cregexp, --nama=cregexp
Tentukan nama yang diizinkan dalam konteks c sebagai ekspresi reguler yang diperluas regexp.
Konteks diidentifikasi oleh karakter pertama dari string parameter; NS
karakter berikutnya merupakan ekspresi reguler yang memungkinkan nama harus
cocok.

-n cregexp, --no-nama=cregexp
Tentukan nama yang tidak diizinkan dalam konteks c sebagai ekspresi reguler yang diperluas
regexp.
Jika keduanya -N dan dan -n ditentukan untuk konteks c, maka pertandingan yang memungkinkan membutuhkan
hak lebih tinggi. Misalnya, untuk mengharuskan semua nama tipe yang ditentukan pengguna menjadi
diakhiri dengan _t, sebutkan -tidak -Nt'_t$'. Kutipan dalam parameter terakhir adalah
diperlukan untuk menghilangkan arti khusus dari $ di shell baris perintah Anda adalah
mungkin menggunakan untuk memanggil Maria.

-P model, --probabilistik=model
Beban model dan bersiap untuk menganalisisnya dengan membangun satu set status yang dapat dijangkau
di memori utama dengan menggunakan teknik yang disebut keadaan bit hashing.

-p Command, --properti-penerjemah=Command
Tentukan perintah yang akan digunakan untuk menerjemahkan properti automata. Perintah harus
baca rumus dari input standar dan tulis otomat yang sesuai
deskripsi ke output standar. Penerjemah lbt kompatibel dengan ini
.

-q membatasi, --batas-kuantifikasi=membatasi
Cegah kuantifikasi (jumlah multi-set) dari jenis yang memiliki lebih dari membatasi mungkin
nilai-nilai. Batas 0 menonaktifkan pemeriksaan.

-U simbol, --tidak ditentukan=simbol
Undefine simbol praprosesor simbol.

-u [a][f[file keluar]], --terbuka=[a][f[file keluar]]
Buka jaring menggunakan algoritma a dan tulis dalam format f untuk file keluar. Jika file keluar
tidak ditentukan, buang jaring yang tidak dilipat ke output standar. Kemungkinan format
adalah m (Maria (dapat dibaca manusia), default), l (LoLA), p (PEP), dan r (MELECUT). Di sana
adalah dua algoritma: tradisional (default) dan dikurangi dengan membangun a bisa ditutupi
menandai (M).

-V, --Versi: kapan
Cetak nomor versi Maria dan keluar.

-di, --bertele-tele
Tampilkan informasi verbose pada berbagai tahap analisis.

-W, --peringatan
Aktifkan peringatan tentang konstruksi jaringan yang mencurigakan. Ini adalah perilaku default.

-w, --tidak ada peringatan
Lawan dari -W. Nonaktifkan semua peringatan.

-x basis angka, --radix=basis angka
Tentukan basis nomor untuk keluaran diagnostik. Nilai yang diizinkan untuk basis angka adalah
Oktober, oktal, 8, hex, heksadesimal, 16, Desember, desimal dan 10. Standarnya adalah menggunakan
angka desimal.

-Y, --kompres-tersembunyi
Kurangi kumpulan status yang dapat dijangkau dengan tidak menyimpan status penerus dari
contoh transisi yang a menyembunyikan kondisi berlaku. Penerus yang tersembunyi adalah
disimpan ke set status terpisah. Opsi ini dapat menghemat memori (-L or -m) atau mengurangi
probabilitas bahwa keadaan dihilangkan (-M or -P), dan dapat meningkatkan
efisiensi analisis paralel (-j or -k), tetapi juga dapat meningkat secara signifikan
kebutuhan waktu prosesor. Opsi ini juga berfungsi dengan model keaktifan
memeriksa, tetapi tidak ada jaminan bahwa nilai kebenaran dari properti liveness
tetap tidak berubah. Opsi ini dapat dikombinasikan dengan -Z.

-y, --tanpa-kompres-tersembunyi
Lawan dari -Y. Ini adalah perilaku default.

-Z, --kompres-jalur
Kurangi kumpulan status yang dapat dijangkau dengan tidak menyimpan status perantara yang memiliki
paling satu penerus. Opsi ini dapat menghemat memori (-L or -m) atau mengurangi
probabilitas bahwa keadaan dihilangkan (-M or -P), dan dapat meningkatkan efisiensi
analisis paralel (-j or -k), tetapi juga dapat sangat meningkatkan
kebutuhan waktu prosesor. Opsi ini juga berfungsi dengan pemeriksaan model keaktifan,
tetapi tidak ada jaminan bahwa nilai kebenaran dari properti liveness tetap ada
tidak berubah. Opsi ini dapat dikombinasikan dengan -Y.

-z, --tanpa-kompres-jalur
Lawan dari -Z. Ini adalah perilaku default.

Gunakan maria online menggunakan layanan onworks.net