maria - Online in de cloud

PROGRAMMA:

NAAM

maria - Modular Reachability Analyzer voor petrinetten op hoog niveau

KORTE INHOUD

maria [opties] bestanden...

PRODUCTBESCHRIJVING

Deze handleiding documenteert in het kort de: maria opdracht. Meer volledige documentatie is:
beschikbaar in het GNU Info-formaat; zie onder.

maria is een programma dat modellen van gelijktijdige systemen analyseert, beschreven in de invoer
taal die is gebaseerd op algebraïsche systeemnetten. Het formalisme werd gepresenteerd door Ekkart
Kindler en Hagen Völzer op ICATPN'98, Flexibiliteit in algebraïsch Netten.
Algebraic System Nets is een raamwerk dat geen gegevenstypes of algebraïsche definieert
activiteiten. Het gegevenstypesysteem en de bewerkingen in Maria zijn ontworpen met high-level
programmeer- en specificatietalen in gedachten. Desondanks heeft elk Maria-model een
eindig ontvouwen.
Om interoperabiliteit met low-level Petri net-tools te garanderen, vertaalt Maria identifiers in
uitgevouwen netten tot reeksen van alfanumerieke tekens en onderstrepingstekens. het filter
vouwnaam.pl kunnen worden gebruikt of aangepast om de leesbaarheid van de identifiers te verbeteren.

OPTIES

Maria volgt de gebruikelijke syntaxis van de GNU-opdrachtregel, met lange opties die beginnen met twee
streepjes (`-'). Hieronder vindt u een overzicht van de mogelijkheden. Voor een volledige beschrijving, zie
de Info-bestanden.

-a begrenzing, --array-limiet=begrenzing
Beperk de grootte van array-indextypen tot: begrenzing Mogelijke waarden. Een limiet van 0
schakelt de controles uit.

-b model, --wide-first-search=model
Genereer de bereikbaarheidsgrafiek van model met behulp van breedte-eerst zoeken.

-C directory, --compileren=directory
Genereer C-code in directory voor het evalueren van uitdrukkingen en voor het lage niveau
routines van het algoritme voor de analyse van de overgangsinstantie. Wanneer deze optie wordt gebruikt,
evaluatiefouten worden op een iets andere manier gerapporteerd. De tolk
geeft de waardering en uitdrukking weer die de eerste fout in een staat hebben veroorzaakt; de
gecompileerde code geeft het aantal fouten weer. Om prestatieredenen is de
gegenereerde code controleert niet op overloopfouten bij het toevoegen van items aan multisets.

-C, --niet-compileren
Het tegenovergestelde van -C. Evalueer alle uitdrukkingen in de ingebouwde tolk. Dit is
het standaardgedrag.

-D symbool, --definiëren=symbool
Definieer het preprocessor-symbool symbool.

-d model, -- depth-first-search=model
Genereer de bereikbaarheidsgrafiek van model met behulp van diepte-eerst zoeken.

-E interval, --randen=interval
Bij het genereren van de bereikbaarheidsgrafiek, rapporteer de grootte van de grafiek na elke
interval gegenereerde randen.

-e snaar, --uitvoeren=snaar
Uitvoeren snaar.

-g grafiekbestand, --grafiek=grafiekbestand
Laad een eerder gegenereerde bereikbaarheidsgrafiek van grafiekbestand.rgh.

-H h[,f[,t]], --hashes=h[,f[,t]]
Configureer de parameters voor probabilistische verificatie (-P). toewijzen t universeel
hash-functies van f elementen en bijbehorende hashtabellen van h stukjes elk. Beide h
en f worden afgerond naar de volgende geschikte waarden.

-?, -H, --help
Druk een samenvatting van de opdrachtregelopties af naar Maria en sluit af.

-I directory, --include=directory
toevoegen directory naar de lijst met gezochte mappen inclusief bestanden.

-i kolommen, --breedte=kolommen
Stel de rechtermarge van de uitvoer in op kolommen. De standaardwaarde is 80.

-j processen, --banen=processen
Bij het controleren van veiligheidseigenschappen (opties -L, -M en -P), gebruik zoveel worker
processen om de analyse op een computer met meerdere processors te versnellen. Zie ook -k en
-Z.

-k port[/gastheer], --verbinden=port[/gastheer]
Verspreid veiligheidsmodelcontrole (opties -L, -M en -P) in een TCP/IP-netwerk. Voor
de server, alleen port wordt gespecificeerd als een 16-bits geheel getal zonder teken, meestal tussen
1024 en 65535. Voor de arbeidsprocessen, port/gastheer specificeert de poort en de
adres van de server. Zie ook -j.

-L model, --verliesloos=model
Laden model en bereid je voor op het analyseren ervan door een reeks bereikbare toestanden te construeren
in schijfbestanden. Zie ook -M, -P, -j en -k.

-m model, --model=model
Laden model en de bereikbaarheidsgrafiek wissen.

-M model, --md5-gecomprimeerd=model
Laden model en bereid je voor op het analyseren ervan door een overschatting te construeren van
reeks bereikbare toestanden in het hoofdgeheugen. Zie ook -P, -L, -j en -k.

-N cregeexp, --naam=cregeexp
Geef de namen op die in context zijn toegestaan c als de uitgebreide reguliere expressie regexp.
De context wordt geïdentificeerd door het eerste teken van de parameterreeks; de
volgende karakters vormen de reguliere expressie die toegestane namen moeten
overeenkomen.

-n cregeexp, --geen-naam=cregeexp
Geef de namen op die niet zijn toegestaan ​​in context c als de uitgebreide reguliere expressie
regexp.
Als beide -N en en -n zijn opgegeven voor een context c, dan duurt de toegestane wedstrijd
voorrang. Om bijvoorbeeld te vereisen dat alle door de gebruiker gedefinieerde typenamen
beëindigd met _t, specificeer -nt -Nt'_t$'. De aanhalingstekens in de laatste parameter zijn
nodig om de speciale betekenis te verwijderen van $ in de opdrachtregelshell ben je
waarschijnlijk gebruikt om Maria aan te roepen.

-P model, --probabilistisch=model
Laden model en bereid je voor op het analyseren ervan door een reeks bereikbare toestanden te construeren
in het hoofdgeheugen met behulp van een techniek genaamd bitstaat hashing.

-p commando, --eigenschap-vertaler=commando
Geef de opdracht op die moet worden gebruikt voor het vertalen van eigenschapsautomaten. De opdracht moet
lees een formule uit de standaardinvoer en schrijf een bijbehorende automaat
beschrijving naar de standaarduitvoer. De vertaler pond is hiermee compatibel
optie.

-q begrenzing, --kwantificatie-limiet=begrenzing
Voorkom kwantificering (multi-set sum) van typen met meer dan begrenzing mogelijk
waarden. Een limiet van 0 schakelt de controles uit.

-U symbool, --ongedaan maken=symbool
Definieer het preprocessor-symbool symbool.

-u [a][f[uitbestand]], --ontvouwen=[a][f[uitbestand]]
Ontvouw het net met behulp van algoritme a en schrijf het in formaat f naar uitbestand. Indien uitbestand
niet is opgegeven, dumpt u het uitgevouwen net naar de standaarduitvoer. Mogelijke formaten
zijn m (Maria (door mensen leesbaar), standaard), l (LoLA), p (PEP), en r (PROD). Daar
zijn twee algoritmen: traditioneel (standaard) en gereduceerd door a . te construeren dekbaar
het merken (M).

-V, --versie
Print het versienummer van Maria en sluit af.

-in, --uitgebreid
Uitgebreide informatie weergeven over verschillende stadia van de analyse.

-W, --waarschuwingen
Schakel waarschuwingen over verdachte netconstructies in. Dit is het standaardgedrag.

-w, --geen waarschuwingen
Het tegenovergestelde van -W. Schakel alle waarschuwingen uit.

-x nummerbasis, --radix=nummerbasis
Geef de nummerbasis op voor diagnostische uitvoer. Toegestane waarden voor nummerbasis zijn
oktober, octaal, 8, hex, hexadecimaal, 16, december, decimale en 10. De standaard is om te gebruiken
decimale getallen.

-Ja, --comprimeren-verborgen
Verminder de reeks bereikbare toestanden door de opvolgende toestanden van niet op te slaan
overgangen waarvoor a verstoppen conditie houdt. De verborgen opvolgers zijn
opgeslagen in een aparte statusset. Deze optie kan geheugen besparen (-L or -m) of verminderen
de kans dat staten worden weggelaten (-M or -P), en het kan de verbeteren
efficiëntie van parallelle analyse (-j or -k), maar het kan ook aanzienlijk toenemen
de vereiste processortijd. De optie werkt ook met het liveness-model
controleren, maar er is geen garantie dat de waarheidswaarden van eigenschappen van levendigheid
blijft onveranderd. Deze optie kan worden gecombineerd met: -Z.

-ja, --geen-comprimeren-verborgen
Het tegenovergestelde van -Y. Dit is het standaardgedrag.

-Z, --comprimeer-paden
Verminder de reeks bereikbare toestanden door geen tussenliggende toestanden op te slaan die at . hebben
meest één opvolger. Deze optie kan geheugen besparen (-L or -m) of verminder de
kans dat staten worden weggelaten (-M or -P), en het kan de efficiëntie verbeteren
van parallelle analyse (-j or -k), maar het kan ook de
processortijd nodig. De optie werkt ook met controle van het liveness-model,
maar er is geen garantie dat de waarheidswaarden van levendigheidseigenschappen blijven bestaan
onveranderd. Deze optie kan worden gecombineerd met: -Y.

-z, --geen-comprimeer-paden
Het tegenovergestelde van -Z. Dit is het standaardgedrag.

Maria online gebruiken met onworks.net-services