maria - Online sa Cloud

PROGRAMA:

NAME

maria - Modular Reachability Analyzer para sa mataas na antas ng Petri nets

SINOPSIS

Mary [pagpipilian] file...

DESCRIPTION

Ang manu-manong pahinang ito ay nagdodokumento ng maikling Mary utos. Ang mas kumpletong dokumentasyon ay
magagamit sa GNU Info format; tingnan sa ibaba.

Mary ay isang programa na nagsusuri ng mga modelo ng mga kasabay na sistema, na inilarawan sa input nito
wika na batay sa Algebraic System Nets. Ang pormalismo ay ipinakita ni Ekkart
Kindler at Hagen Völzer sa ICATPN'98, flexibility in Algebraic nets.
Ang Algebraic System Nets ay isang balangkas na hindi tumutukoy sa anumang uri ng data o algebraic
mga operasyon. Ang sistema ng uri ng data at ang mga operasyon sa Maria ay dinisenyo na may mataas na antas
programming at specification na mga wika sa isip. Sa kabila nito, ang bawat modelo ng Maria ay may isang
may hangganang paglalahad.
Para matiyak ang interoperability sa mababang antas ng Petri net tools, isinasalin ni Maria ang mga identifier
nagbukas ng mga lambat sa mga string ng alpha-numerical na mga character at underscore. Ang filter
foldname.pl maaaring gamitin o iakma upang mapabuti ang pagiging madaling mabasa ng mga identifier.

Opsyon

Sinusunod ni Maria ang karaniwang GNU command line syntax, na may mahabang opsyon na nagsisimula sa dalawa
mga gitling (`-'). Ang isang buod ng mga opsyon ay kasama sa ibaba. Para sa kumpletong paglalarawan, tingnan
ang mga file ng Impormasyon.

-a limitasyon, --array-limit=limitasyon
Limitahan ang laki ng mga uri ng array index sa limitasyon posibleng mga halaga. Isang limitasyon ng 0
hindi pinapagana ang mga tseke.

-b modelo, --breadth-first-search=modelo
Bumuo ng reachability graph ng modelo gamit ang breadth-first search.

-C direktoryo, --compile=direktoryo
Bumuo ng C code sa direktoryo para sa pagsusuri ng mga expression at para sa mababang antas
nakagawian ng algorithm ng pagsusuri sa paglilipat. Kapag ginamit ang opsyong ito,
Ang mga error sa pagsusuri ay iniuulat sa isang bahagyang naiibang paraan. Ang interpreter
ipinapakita ang valuation at expression na naging sanhi ng unang error sa isang estado; ang
ipinapakita ng pinagsama-samang code ang bilang ng mga error. Para sa mga kadahilanang pagganap, ang
hindi sinusuri ng nabuong code ang mga error sa overflow kapag nagdaragdag ng mga item sa mga multi-set.

-c, --walang-compile
Ang kabaligtaran ng -C. Suriin ang lahat ng mga expression sa built-in na interpreter. Ito ay
ang default na pag-uugali.

-D simbolo, --define=simbolo
Tukuyin ang simbolo ng preprocessor simbolo.

-d modelo, --depth-first-search=modelo
Bumuo ng reachability graph ng modelo gamit ang depth-first search.

-E agwat, --mga gilid=agwat
Kapag bumubuo ng graph ng reachability, iulat ang laki ng graph pagkatapos ng bawat isa
agwat nabuong mga gilid.

-e pisi, --execute=pisi
Isakatuparan pisi.

-g graphfile, --graph=graphfile
Mag-load ng dating nabuong graph ng reachability mula sa graphfile.rgh.

-H h[,f[,t]], --hashes=h[,f[,t]]
I-configure ang mga parameter para sa probabilistic verification (-P). Maglaan t pangkalahatan
hash function ng f mga elemento at kaukulang hash table ng h bit bawat isa. pareho h
at f ay i-round up sa susunod na naaangkop na mga halaga.

-?, -h, - Tumulong
Mag-print ng buod ng mga opsyon sa command-line kay Maria at lumabas.

-I direktoryo, --include=direktoryo
Mag-aplay direktoryo sa listahan ng mga direktoryo na hinanap para sa isama ang mga file.

-i haligi, --lapad=haligi
Itakda ang kanang margin ng output sa haligi. Ang default ay 80.

-j mga proseso, --mga trabaho=mga proseso
Kapag sinusuri ang mga katangian ng kaligtasan (mga opsyon -L, -M at -P), gamitin itong maraming manggagawa
mga proseso upang mapabilis ang pagsusuri sa isang multiprocessor na computer. Tingnan din -k at
-Z.

-k port[/marami], --kunekta =port[/marami]
Ipamahagi ang pagsusuri sa modelo ng kaligtasan (mga opsyon -L, -M at -P) sa isang TCP/IP network. Para sa
ang server, lamang port ay tinukoy bilang isang 16-bit na unsigned integer, kadalasan sa pagitan
1024 at 65535. Para sa mga proseso ng manggagawa, port/marami tumutukoy sa port at ang
address ng server. Tingnan din -j.

-L modelo, --walang pagkawala=modelo
Load modelo at maghanda para sa pagsusuri nito sa pamamagitan ng pagbuo ng isang hanay ng mga maaabot na estado
sa mga file ng disk. Tingnan din -M, -P, -j at -k.

-m modelo, --modelo=modelo
Load modelo at i-clear ang reachability graph nito.

-M modelo, --md5-compacted=modelo
Load modelo at maghanda para sa pagsusuri nito sa pamamagitan ng pagbuo ng isang over-approximation ng
set ng mga naaabot na estado sa pangunahing memorya. Tingnan din -P, -L, -j at -k.

-N cregexp, --pangalan=cregexp
Tukuyin ang mga pangalang pinapayagan sa konteksto c bilang pinalawig na regular na expression regexp.
Natutukoy ang konteksto sa pamamagitan ng unang karakter ng string ng parameter; ang
Ang mga sumusunod na character ay bumubuo ng regular na expression na pinapayagan ang mga pangalan ay dapat
tumutugma.

-n cregexp, --no-name=cregexp
Tukuyin ang mga pangalan na hindi pinapayagan sa konteksto c bilang pinalawig na regular na expression
regexp.
Kung pareho -N at at -n ay tinukoy para sa isang konteksto c, pagkatapos ay ang pagpapahintulot na tugma ay tumatagal
karapatan sa pangunguna. Halimbawa, upang hilingin na ang lahat ng mga pangalan ng uri na tinukoy ng gumagamit ay
winakasan ng _t, tukuyin -nt -Nt'_t$'. Ang mga quote sa huling parameter ay
kinakailangang alisin ang espesyal na kahulugan mula sa $ sa shell ng command line ikaw ay
malamang na ginagamit upang tawagan si Maria.

-P modelo, --probabilistic=modelo
Load modelo at maghanda para sa pagsusuri nito sa pamamagitan ng pagbuo ng isang hanay ng mga maaabot na estado
sa pangunahing memorya sa pamamagitan ng paggamit ng isang pamamaraan na tinatawag na bitstate hashing.

-p utos, --property-translator=utos
Tukuyin ang command na gagamitin para sa pagsasalin ng property automata. Ang utos ay dapat
magbasa ng formula mula sa karaniwang input at magsulat ng kaukulang automat
paglalarawan sa karaniwang output. Ang Tagapagsalin lbt ay tugma dito
pagpipilian.

-q limitasyon, --quantification-limit=limitasyon
Pigilan ang quantification (multi-set sum) ng mga uri na may higit sa limitasyon maaari
mga halaga. Hindi pinapagana ng limitasyong 0 ang mga tseke.

-U simbolo, --undefine=simbolo
I-undefine ang simbolo ng preprocessor simbolo.

-u [a][f[outfile]], --unfold=[a][f[outfile]]
Buksan ang net gamit ang algorithm a at isulat ito sa format f sa outfile. Kung outfile
ay hindi tinukoy, itapon ang nakabukang lambat sa karaniwang output. Mga posibleng format
ay m (Maria (nababasa ng tao), default), l (LoLA), p (PEP), at r (PROD). doon
ay dalawang algorithm: tradisyonal (default) at binawasan sa pamamagitan ng pagbuo ng a masakop
pagmamarka (M).

-V, --bersyon
I-print ang numero ng bersyon ng Maria at lumabas.

-sa, --verbose
Magpakita ng verbose na impormasyon sa iba't ibang yugto ng pagsusuri.

-W, --mga babala
Paganahin ang mga babala tungkol sa mga kahina-hinalang net construct. Ito ang default na pag-uugali.

-w, --walang-babala
Ang kabaligtaran ng -W. Huwag paganahin ang lahat ng mga babala.

-x base ng numero, --radix=base ng numero
Tukuyin ang base ng numero para sa diagnostic na output. Mga pinapayagang halaga para sa base ng numero ay
Oktubre, octal, 8, hex, hexadecimal, 16, Disyembre, decimal at 10. Ang default ay ang gamitin
mga numero ng decimal.

-Y, --compress-nakatago
Bawasan ang hanay ng mga maaabot na estado sa pamamagitan ng hindi pag-iimbak ng mga kahalili na estado ng
transitions instances for which a itago hawak ng kondisyon. Ang mga nakatagong kahalili ay
nakaimbak sa isang hiwalay na set ng estado. Ang pagpipiliang ito ay maaaring mag-save ng memorya (-L or -m) o bawasan
ang posibilidad na ang mga estado ay tinanggal (-M or -P), at maaari nitong mapabuti ang
kahusayan ng parallel analysis (-j or -k), ngunit maaari rin itong tumaas nang malaki
ang kinakailangan sa oras ng processor. Gumagana rin ang opsyon sa liveness model
sinusuri, ngunit walang garantiya na ang katotohanan ay pinahahalagahan ng mga ari-arian ng liveness
mananatiling hindi nagbabago. Ang pagpipiliang ito ay maaaring isama sa -Z.

-y, --walang-compress-nakatago
Ang kabaligtaran ng -Y. Ito ang default na pag-uugali.

-Z, --compress-paths
Bawasan ang hanay ng mga naaabot na estado sa pamamagitan ng hindi pag-iimbak ng mga intermediate na estado na mayroon sa
karamihan sa isang kahalili. Ang pagpipiliang ito ay maaaring mag-save ng memorya (-L or -m) o bawasan ang
posibilidad na ang mga estado ay tinanggal (-M or -P), at maaari itong mapabuti ang kahusayan
ng parallel analysis (-j or -k), ngunit maaari rin nitong mapataas nang malaki ang
kinakailangan sa oras ng processor. Gumagana rin ang opsyon sa liveness model checking,
ngunit walang garantiya na mananatili ang mga katotohanang halaga ng mga ari-arian ng liveness
hindi nagbabago. Ang pagpipiliang ito ay maaaring isama sa -Y.

-z, --no-compress-paths
Ang kabaligtaran ng -Z. Ito ang default na pag-uugali.

Gamitin ang maria online gamit ang mga serbisyo ng onworks.net