maria - Online în cloud

PROGRAM:

NUME

maria - Analizor modular de accesibilitate pentru rețele Petri de nivel înalt

REZUMAT

Mary [Opțiuni] fișiere...

DESCRIERE

Această pagină de manual documentează pe scurt Mary comanda. O documentație mai completă este
disponibil în formatul GNU Info; Vezi mai jos.

Mary este un program care analizează modele de sisteme concurente, descrise în intrarea sa
limbaj care se bazează pe rețele de sistem algebric. Formalismul a fost prezentat de Ekkart
Kindler și Hagen Völzer la ICATPN'98, Flexibilitate in Algebric Plase.
Algebraic System Nets este un cadru care nu definește niciun tip de date sau algebrice
operațiuni. Sistemul de tip de date și operațiunile din Maria sunt proiectate la nivel înalt
în minte limbajele de programare și specificații. Cu toate acestea, fiecare model Maria are un
desfăşurare finită.
Pentru a asigura interoperabilitatea cu instrumente de rețea Petri de nivel scăzut, Maria traduce identificatorii în
rețele desfășurate în șiruri de caractere alfanumerice și litere de subliniere. Filtrul
foldname.pl pot fi utilizate sau adaptate pentru a îmbunătăți lizibilitatea identificatorilor.

OPŢIUNI

Maria urmează sintaxa obișnuită a liniei de comandă GNU, cu opțiuni lungi care încep cu două
liniuțe (`-'). Un rezumat al opțiunilor este inclus mai jos. Pentru o descriere completă, vezi
fișierele Info.

-a limita, --array-limit=limita
Limitați dimensiunea tipurilor de index de matrice la limita valori posibile. O limită de 0
dezactivează verificările.

-b model, --breadth-first-search=model
Generați graficul de accesibilitate al model folosind căutarea pe lățimea întâi.

-C director, --compile=director
Generați codul C în director pentru evaluarea expresiilor și pentru nivelul scăzut
rutine ale algoritmului de analiză a instanțelor de tranziție. Când se utilizează această opțiune,
erorile de evaluare sunt raportate într-un mod ușor diferit. Interpretul
afișează evaluarea și expresia care a provocat prima eroare într-o stare; cel
codul compilat afișează numărul de erori. Din motive de performanță, the
codul generat nu verifică erorile de depășire atunci când adăugați articole la seturi multiple.

-c, --no-compilare
Opusul -C. Evaluați toate expresiile din interpretul încorporat. Aceasta este
comportamentul implicit.

-D simbol, --define=simbol
Definiți simbolul preprocesorului simbol.

-d model, --depth-first-search=model
Generați graficul de accesibilitate al model folosind căutarea în profunzime.

-E interval, --margini=interval
Când generați graficul de accesibilitate, raportați dimensiunea graficului după fiecare
interval marginile generate.

-e şir, --execute=şir
Executa şir.

-g fişier grafic, --graf=fişier grafic
Încărcați un grafic de accesibilitate generat anterior de la fişier grafic.rgh.

-H h[,f[,t]], --hashes=h[,f[,t]]
Configurați parametrii pentru verificarea probabilistică (-P). Aloca t universal
funcții hash ale f elemente și tabele hash corespunzătoare ale h biți fiecare. Ambii h
și f vor fi rotunjite la următoarele valori adecvate.

-?, -h, --Ajutor
Imprimați un rezumat al opțiunilor din linia de comandă către Maria și ieșiți.

-I director, --include=director
Adăuga director la lista de directoare căutate după fișierele includ.

-i coloane, --lățime=coloane
Setați marginea dreaptă a ieșirii la coloane. Valoarea implicită este 80.

-j procese, --locuri de muncă=procese
La verificarea proprietăților de siguranță (opțiuni -L, -M și -P), folosiți atât de mulți lucrători
procese pentru a accelera analiza pe un computer multiprocesor. Vezi si -k și
-Z.

-k port[/gazdă], --conecta=port[/gazdă]
Distribuiți verificarea modelului de siguranță (opțiuni -L, -M și -P) într-o rețea TCP/IP. Pentru
doar serverul port este specificat ca un întreg fără semn pe 16 biți, de obicei între
1024 si 65535. Pentru procesele lucratoare, port/gazdă specifică portul și
adresa serverului. Vezi si -j.

-L model, --fara pierderi=model
A incarca model și pregătiți-vă pentru analizarea acestuia prin construirea unui set de stări accesibile
în fișierele disc. Vezi si -M, -P, -j și -k.

-m model, --model=model
A incarca model și ștergeți graficul de accesibilitate.

-M model, --md5-compact=model
A incarca model și pregătiți-vă pentru analizarea acestuia prin construirea unei supraaproximări a
set de stări accesibile în memoria principală. Vezi si -P, -L, -j și -k.

-N cregexp, --nume=cregexp
Specificați numele permise în context c ca expresie regulată extinsă expresie regulată.
Contextul este identificat prin primul caracter al șirului de parametri; cel
caracterele ulterioare constituie expresia regulată pe care trebuie să le numere permise
meci.

-n cregexp, --no-name=cregexp
Specificați numele nepermise în context c ca expresie regulată extinsă
expresie regulată.
Dacă ambele -N si si -n sunt specificate pentru un context c, apoi meciul care permite
precedenta. De exemplu, pentru a solicita ca toate numele de tip definite de utilizator să fie
terminat cu _t, specifica -nt -Nt'_t$'. Citatele din ultimul parametru sunt
necesare pentru a elimina sensul special din $ în shell-ul liniei de comandă sunteți
probabil folosind pentru a o invoca pe Maria.

-P model, --probabilistic=model
A incarca model și pregătiți-vă pentru analizarea acestuia prin construirea unui set de stări accesibile
în memoria principală prin utilizarea unei tehnici numite bitstate hashing.

-p comandă, --property-translator=comandă
Specificați comanda de utilizat pentru traducerea automatelor de proprietate. Comanda ar trebui
citiți o formulă din intrarea standard și scrieți un automat corespunzător
descriere la ieșirea standard. Traducatorul lbt este compatibil cu aceasta
opțiune.

-q limita, --limita-cuantificare=limita
Preveniți cuantificarea (suma multi-set) a tipurilor care au mai mult de limita posibil
valorile. O limită de 0 dezactivează verificările.

-U simbol, --undefine=simbol
Nedefiniți simbolul preprocesorului simbol.

-u [a][f[outfile]], --desfășura=[a][f[outfile]]
Desfaceți rețeaua folosind algoritmul a și scrieți-l în format f la outfile. Dacă outfile
nu este specificat, aruncați plasa desfășurată la ieșirea standard. Formate posibile
sunt m (Maria (lizibil de om), implicit), l (LoLA), p (PEP) și r (PROD). Acolo
sunt doi algoritmi: tradițional (implicit) și redus prin construirea a acoperibil
marcare (M).

-V, --versiune
Tipăriți numărul versiunii lui Maria și ieșiți.

-v, --verbos
Afișați informații detaliate despre diferitele etape ale analizei.

-W, --Avertizări
Activați avertismentele despre construcții de rețea suspecte. Acesta este comportamentul implicit.

-w, --fără-avertismente
Opusul -W. Dezactivați toate avertismentele.

-x baza de numere, --radix=baza de numere
Specificați baza numerică pentru ieșirea de diagnosticare. Valori permise pentru baza de numere sunt
oct, octal, 8, hex, hexazecimal, 16, dec, zecimal și 10. Implicit este utilizarea
numere zecimale.

-Y, --comprima-ascuns
Reduceți setul de stări accesibile prin nestocarea stărilor succesoare ale
cazuri de tranziții pentru care a ascunde condiția se menține. Urmașii ascunși sunt
stocat într-un set de stări separat. Această opțiune poate economisi memorie (-L or -m) sau reduce
probabilitatea ca stările să fie omise (-M or -P), și poate îmbunătăți
eficiența analizei paralele (-j or -k), dar poate crește considerabil
cerința de timp a procesorului. Opțiunea funcționează și cu modelul de viață
verificare, dar nu există nicio garanție că adevărul valorează proprietățile de viață
ramane neschimbat. Această opțiune poate fi combinată cu -Z.

-y, --fără-comprimare-ascuns
Opusul -Y. Acesta este comportamentul implicit.

-Z, --comprimați-căi
Reduceți setul de stări accesibile prin ne stocarea stărilor intermediare care au at
majoritatea un succesor. Această opțiune poate economisi memorie (-L or -m) sau reduceți
probabilitatea ca stările să fie omise (-M or -P), și poate îmbunătăți eficiența
de analiză paralelă (-j or -k), dar poate crește considerabil și
cerința de timp a procesorului. Opțiunea funcționează și cu verificarea modelului de viață,
dar nu există nicio garanție că valorile de adevăr ale proprietăților de viață rămân
neschimbat. Această opțiune poate fi combinată cu -Y.

-z, --no-compress-paths
Opusul -Z. Acesta este comportamentul implicit.

Utilizați Maria online folosind serviciile onworks.net