Ini ialah arahan maria 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
maria - Penganalisis Kebolehcapaian Modular untuk jaring Petri peringkat tinggi
SINOPSIS
Mary [pilihan] fail...
DESCRIPTION
Halaman manual ini mendokumentasikan secara ringkas Mary perintah. Dokumentasi yang lebih lengkap ialah
tersedia dalam format Maklumat GNU; lihat di bawah.
Mary ialah program yang menganalisis model sistem serentak, diterangkan dalam inputnya
bahasa yang berasaskan Jaring Sistem Algebra. Formalisme itu disampaikan oleh Ekkart
Kindler dan Hagen Völzer di ICATPN'98, Fleksibiliti in Algebra Nets.
Jaring Sistem Algebra ialah rangka kerja yang tidak mentakrifkan sebarang jenis data atau algebra
operasi. Sistem jenis data dan operasi dalam Maria direka bentuk dengan tahap tinggi
bahasa pengaturcaraan dan spesifikasi dalam fikiran. Walaupun begitu, setiap model Maria mempunyai a
terbentang terhingga.
Untuk memastikan kesalingoperasian dengan alatan bersih Petri peringkat rendah, Maria menterjemahkan pengecam dalam
jaring terbentang kepada rentetan aksara alfa-nombor dan garis bawah. Penapis
foldname.pl boleh digunakan atau disesuaikan untuk meningkatkan kebolehbacaan pengecam.
PILIHAN
Maria mengikut sintaks baris arahan GNU yang biasa, dengan pilihan panjang bermula dengan dua
sempang (`-'). Ringkasan pilihan disertakan di bawah. Untuk penerangan lengkap, lihat
fail Maklumat.
-a menghadkan, --had-tatasusunan=menghadkan
Hadkan saiz jenis indeks tatasusunan kepada menghadkan nilai yang mungkin. Had 0
melumpuhkan cek.
-b model, --breadth-first-search=model
Hasilkan graf kebolehcapaian bagi model menggunakan carian luas-dahulu.
-C direktori, --compile=direktori
Hasilkan kod C dalam direktori untuk menilai ungkapan dan untuk peringkat rendah
rutin algoritma analisis contoh peralihan. Apabila pilihan ini digunakan,
ralat penilaian dilaporkan dengan cara yang sedikit berbeza. Jurubahasa
memaparkan penilaian dan ungkapan yang menyebabkan ralat pertama dalam keadaan; yang
kod yang disusun memaparkan bilangan ralat. Atas sebab prestasi,
kod yang dijana tidak menyemak ralat limpahan apabila menambah item pada berbilang set.
-c, --tiada-kompilasi
Bertentangan dengan -C. Nilai semua ungkapan dalam penterjemah terbina dalam. Ini adalah
tingkah laku lalai.
-D lambang, --define=lambang
Tentukan simbol prapemproses lambang.
-d model, --depth-first-search=model
Hasilkan graf kebolehcapaian bagi model menggunakan carian mendalam-dahulu.
-E selang, --tepi=selang
Apabila menjana graf kebolehcapaian, laporkan saiz graf selepas setiap
selang tepi yang dihasilkan.
-e rentetan, --laksanakan=rentetan
Melaksanakan rentetan.
-g fail graf, --graf=fail graf
Muatkan graf kebolehcapaian yang dijana sebelum ini daripada fail graf.rgh.
-H h[,f[,t]], --cincang =h[,f[,t]]
Konfigurasikan parameter untuk pengesahan kebarangkalian (-P). memperuntukkan t sejagat
fungsi hash daripada f elemen dan jadual cincang yang sepadan bagi h bit setiap satu. Kedua-duanya h
and f akan dibundarkan kepada nilai yang sesuai seterusnya.
-?, -h, - membantu
Cetak ringkasan pilihan baris arahan kepada Maria dan keluar.
-I direktori, --termasuk=direktori
Tambah direktori ke senarai direktori yang dicari termasuk fail.
-i lajur, --lebar=lajur
Tetapkan margin kanan output kepada lajur. Lalai ialah 80.
-j proses, --pekerjaan=proses
Apabila menyemak sifat keselamatan (pilihan -L, -M and -P), gunakan pekerja yang ramai ini
proses untuk mempercepatkan analisis pada komputer berbilang pemproses. Lihat juga -k and
-Z.
-k pelabuhan[/tuan rumah], --sambung=pelabuhan[/tuan rumah]
Edarkan pemeriksaan model keselamatan (pilihan -L, -M and -P) dalam rangkaian TCP/IP. Untuk
pelayan, sahaja pelabuhan ditentukan sebagai integer tidak bertanda 16-bit, biasanya antara
1024 dan 65535. Untuk proses pekerja, pelabuhan/tuan rumah menentukan pelabuhan dan
alamat pelayan. Lihat juga -j.
-L model, --tak rugi=model
Muatkan model dan bersedia untuk menganalisisnya dengan membina satu set keadaan boleh dicapai
dalam fail cakera. Lihat juga -M, -P, -j and -k.
-m model, --model=model
Muatkan model dan kosongkan graf kebolehcapaiannya.
-M model, --md5-compacted=model
Muatkan model dan bersedia untuk menganalisisnya dengan membina lebihan anggaran
set keadaan boleh dicapai dalam ingatan utama. Lihat juga -P, -L, -j and -k.
-N cregexp, --nama=cregexp
Nyatakan nama yang dibenarkan dalam konteks c sebagai ungkapan biasa lanjutan regexp.
Konteks dikenal pasti oleh aksara pertama rentetan parameter; yang
aksara yang berjaya membentuk ungkapan biasa yang membenarkan nama mesti
sepadan.
-n cregexp, --no-name=cregexp
Nyatakan nama yang tidak dibenarkan dalam konteks c sebagai ungkapan biasa lanjutan
regexp.
Sekiranya kedua-duanya -N dan dan -n ditentukan untuk konteks c, maka perlawanan yang dibenarkan itu mengambil masa
keutamaan. Sebagai contoh, untuk menghendaki semua nama jenis yang ditentukan pengguna
ditamatkan dengan _t, nyatakan -nt -Nt'_t$'. Petikan dalam parameter terakhir ialah
diperlukan untuk membuang makna khas daripada $ dalam shell baris arahan anda berada
mungkin menggunakan untuk memanggil Maria.
-P model, --kebarangkalian=model
Muatkan model dan bersedia untuk menganalisisnya dengan membina satu set keadaan boleh dicapai
dalam ingatan utama dengan menggunakan teknik yang dipanggil keadaan bit hash.
-p arahan, --property-penterjemah=arahan
Tentukan arahan untuk digunakan untuk menterjemah automata harta. Perintah itu sepatutnya
baca formula daripada input standard dan tulis automaton yang sepadan
penerangan kepada keluaran piawai. Penterjemah lbt serasi dengan ini
pilihan.
-q menghadkan, --had-kuantisasi=menghadkan
Elakkan kuantifikasi (jumlah berbilang set) jenis yang mempunyai lebih daripada menghadkan mungkin
nilai. Had 0 melumpuhkan semakan.
-U lambang, --udefine=lambang
Nyahtakrifkan simbol prapemproses lambang.
-u [a][f[fail luar]], --terbuka=[a][f[fail luar]]
Buka jaring menggunakan algoritma a dan tulis dalam format f kepada fail luar. Jika fail luar
tidak dinyatakan, buang jaring yang tidak dilipat ke output standard. Format yang mungkin
adalah m (Maria (boleh dibaca manusia), lalai), l (LoLA), p (PEP), dan r (PROD). di sana
ialah dua algoritma: tradisional (lalai) dan dikurangkan dengan membina a boleh dilindungi
menandakan (M).
-V, --versi
Cetak nombor versi Maria dan keluar.
-v, --verbose
Paparkan maklumat verbose pada peringkat analisis yang berbeza.
-W, --amaran
Dayakan amaran tentang binaan bersih yang mencurigakan. Ini ialah tingkah laku lalai.
-w, --tiada-amaran
Bertentangan dengan -W. Lumpuhkan semua amaran.
-x asas nombor, --radix=asas nombor
Nyatakan pangkalan nombor untuk output diagnostik. Nilai yang dibenarkan untuk asas nombor adalah
Oktober, oktal, 8, heks, perenambelasan, 16, disember, Perpuluhan and 10. Lalai adalah untuk menggunakan
nombor perpuluhan.
-Y, --mampat-tersembunyi
Kurangkan set keadaan boleh dicapai dengan tidak menyimpan keadaan pengganti
contoh peralihan yang a menyembunyikan syarat memegang. Pengganti yang tersembunyi ialah
disimpan ke set keadaan yang berasingan. Pilihan ini mungkin menjimatkan memori (-L or -m) atau mengurangkan
kebarangkalian bahawa keadaan ditinggalkan (-M or -P), dan ia boleh menambah baik
kecekapan analisis selari (-j or -k), tetapi ia juga mungkin meningkat dengan ketara
keperluan masa pemproses. Pilihan ini juga berfungsi dengan model liveness
memeriksa, tetapi tidak ada jaminan bahawa nilai kebenaran harta hidup
kekal tidak berubah. Pilihan ini boleh digabungkan dengan -Z.
-y, --tiada-mampat-tersembunyi
Bertentangan dengan -Y. Ini ialah tingkah laku lalai.
-Z, --laluan-mampat
Kurangkan set keadaan boleh dicapai dengan tidak menyimpan keadaan perantaraan yang mempunyai at
kebanyakan satu pengganti. Pilihan ini mungkin menjimatkan memori (-L or -m) atau kurangkan
kebarangkalian bahawa keadaan ditinggalkan (-M or -P), dan ia boleh meningkatkan kecekapan
analisis selari (-j or -k), tetapi ia juga boleh meningkatkan dengan ketara
keperluan masa pemproses. Pilihan ini juga berfungsi dengan semakan model keaktifan,
tetapi tidak ada jaminan bahawa nilai kebenaran harta hidup kekal
tidak berubah. Pilihan ini boleh digabungkan dengan -Y.
-z, --tiada-mampat-laluan
Bertentangan dengan -Z. Ini ialah tingkah laku lalai.
Gunakan maria dalam talian menggunakan perkhidmatan onworks.net
