maria - Online nel cloud

PROGRAMMA:

NOME

maria - Analizzatore di Raggiungibilità Modulare per reti di Petri di alto livello

SINOSSI

maria [Opzioni] file...

DESCRIZIONE

Questa pagina di manuale documenta brevemente il maria comando. La documentazione più completa è
disponibile nel formato GNU Info; vedi sotto.

maria è un programma che analizza modelli di sistemi concorrenti, descritti nel suo input
linguaggio basato su Algebraic System Nets. Il formalismo è stato presentato da Ekkart
Kindler e Hagen Völzer a ICATPN'98, Flessibilità in Algebrico Nets.
Algebric System Nets è un framework che non definisce alcun tipo di dati o algebrico
operazioni. Il sistema dei tipi di dati e le operazioni in Maria sono progettati con un alto livello
in mente i linguaggi di programmazione e di specifica. Nonostante ciò, ogni modello Maria ha un
svolgimento finito.
Per garantire l'interoperabilità con gli strumenti di rete di Petri di basso livello, Maria traduce gli identificatori in
reti spiegate a stringhe di caratteri alfanumerici e trattini bassi. Il filtro
nomepiega.pl possono essere utilizzati o adattati per migliorare la leggibilità degli identificatori.

VERSIONI

Maria segue la solita sintassi della riga di comando GNU, con opzioni lunghe che iniziano con due
trattini (`-'). Di seguito è riportato un riepilogo delle opzioni. Per una descrizione completa, vedere
i file di informazioni.

-a limitare, --limite-array=limitare
Limita la dimensione dei tipi di indice di array a limitare valori possibili. Un limite di 0
disabilita i controlli.

-b modello, --breadth-first-search=modello
Genera il grafico di raggiungibilità di modello utilizzando la ricerca in ampiezza.

-C elenco, --compilare=elenco
Genera codice C in elenco per la valutazione di espressioni e per il basso livello
routine dell'algoritmo di analisi dell'istanza di transizione. Quando si utilizza questa opzione,
gli errori di valutazione sono riportati in modo leggermente diverso. L'interprete
visualizza la valutazione e l'espressione che hanno causato il primo errore in uno stato; il
codice compilato visualizza il numero di errori. Per motivi di prestazioni, il
il codice generato non verifica gli errori di overflow quando si aggiungono elementi a più set.

-C, --no-compila
Il contrario di -C. Valuta tutte le espressioni nell'interprete integrato. Questo è
il comportamento predefinito.

-D simbolo, --definire=simbolo
Definire il simbolo del preprocessore simbolo.

-d modello, --profondità-prima-ricerca=modello
Genera il grafico di raggiungibilità di modello utilizzando la ricerca in profondità.

-E intervallo, --bordi=intervallo
Quando si genera il grafico di raggiungibilità, riportare la dimensione del grafico dopo ogni
intervallo bordi generati.

-e stringa, --esegui=stringa
Eseguire stringa.

-g file grafico, --grafico=file grafico
Carica un grafico di raggiungibilità generato in precedenza da file grafico.rgh.

-H h[,f[,t]], --hash=h[,f[,t]]
Configurare i parametri per la verifica probabilistica (-P). allocare t universale
funzioni hash di f elementi e tabelle hash corrispondenti di h bit ciascuno. Entrambi h
ed f verrà arrotondato al successivo valore appropriato.

-?, -H, --Aiuto
Stampa un riepilogo delle opzioni della riga di comando su Maria ed esci.

-I elenco, --include=elenco
Aggiungere elenco all'elenco delle directory cercate per i file di inclusione.

-i colonne, --larghezza=colonne
Imposta il margine destro dell'output su colonne. Il valore predefinito è 80.

-j i processi, --lavori=i processi
Quando si controllano le proprietà di sicurezza (opzioni -L, -M ed -P), usa questo numero di lavoratori
processi per velocizzare l'analisi su un computer multiprocessore. Guarda anche -k ed
-Z.

-k porto[/host], --connetti=porto[/host]
Distribuire il controllo del modello di sicurezza (opzioni -L, -M ed -P) in una rete TCP/IP. Per
il server, solo porto è specificato come un intero senza segno a 16 bit, di solito tra
1024 e 65535. Per i processi operai, porto/host specifica la porta e il
indirizzo del server. Guarda anche -j.

-L modello, --senza perdita=modello
Caricare modello e prepararsi per analizzarlo costruendo un insieme di stati raggiungibili
nei file del disco. Guarda anche -M, -P, -j ed -k.

-m modello, --modello=modello
Caricare modello e cancella il suo grafico di raggiungibilità.

-M modello, --md5-compattato=modello
Caricare modello e prepararsi per analizzarlo costruendo una sovra-approssimazione di
insieme di stati raggiungibili nella memoria principale. Guarda anche -P, -L, -j ed -k.

-N cregexp, --nome=cregexp
Specifica i nomi consentiti nel contesto c come l'espressione regolare estesa regexp.
Il contesto è identificato dal primo carattere della stringa di parametri; il
i caratteri successivi costituiscono l'espressione regolare che i nomi consentiti devono
incontro.

-n cregexp, --nessun nome=cregexp
Specifica i nomi non consentiti nel contesto c come l'espressione regolare estesa
regexp.
Se entrambi -N e e -n sono specificati per un contesto c, quindi la partita permettendo prende
precedenza. Ad esempio, per richiedere che tutti i nomi di tipo definiti dall'utente siano
terminato con _t, specificare -nt -Nt'_t$'. Le virgolette in quest'ultimo parametro sono
richiesto per rimuovere il significato speciale da $ nella shell della riga di comando sei
probabilmente usando per invocare Maria.

-P modello, --probabilistico=modello
Caricare modello e prepararsi per analizzarlo costruendo un insieme di stati raggiungibili
nella memoria principale utilizzando una tecnica chiamata stato di bit hashing.

-p command, --property-translator=command
Specificare il comando da utilizzare per tradurre gli automi di proprietà. Il comando dovrebbe
leggere una formula dallo standard input e scrivere un automa corrispondente
descrizione allo standard output. Il traduttore libbra è compatibile con questo
opzione.

-q limitare, --quantificazione-limite=limitare
Impedisci la quantificazione (somma multiset) di tipi con più di limitare possibile
valori. Un limite di 0 disabilita i controlli.

-U simbolo, --indefinito=simbolo
Annulla la definizione del simbolo del preprocessore simbolo.

-u [a][f[file di uscita]], --spiega=[a][f[file di uscita]]
Apri la rete usando l'algoritmo a e scrivilo in formato f a file di uscita. Se file di uscita
non è specificato, scarica la rete spiegata sullo standard output. Formati possibili
sono m (Maria (leggibile dall'uomo), impostazione predefinita), l (LoLA), p (PEP), e r (PROD). Là
sono due algoritmi: tradizionale (default) e ridotto costruendo a copribile
marcatura (M).

-V, --versione
Stampa il numero di versione di Maria ed esci.

-in, --verboso
Visualizza informazioni dettagliate sulle diverse fasi dell'analisi.

-W, --avvertenze
Abilita gli avvisi sui costrutti di rete sospetti. Questo è il comportamento predefinito.

-w, --no-avvertimenti
Il contrario di -W. Disattiva tutti gli avvisi.

-x base numerica, --radice=base numerica
Specificare la base numerica per l'output diagnostico. Valori ammessi per base numerica sono
ottobre, ottale, 8, hex, esadecimale, 16, dicembre, decimale ed 10. L'impostazione predefinita è utilizzare
numeri decimali.

-Sì, --compress-nascosto
Ridurre l'insieme degli stati raggiungibili non memorizzando gli stati successori di
istanze di transizione per cui a nascondere condizione tiene. I successori nascosti sono
memorizzato in un insieme di stati separato. Questa opzione può risparmiare memoria (-L or -m) o ridurre
la probabilità che gli stati siano omessi (-M or -P), e può migliorare il
efficienza dell'analisi parallela (-j or -k), ma può anche aumentare notevolmente
il requisito di tempo del processore. L'opzione funziona anche con il modello liveness
verifica, ma non vi è alcuna garanzia che i valori di verità delle proprietà di vitalità
rimane invariato. Questa opzione può essere combinata con -Z.

-sì, --no-compress-nascosto
Il contrario di -Y. Questo è il comportamento predefinito.

-Z, --compress-percorsi
Ridurre l'insieme degli stati raggiungibili non memorizzando gli stati intermedi che hanno at
più un successore. Questa opzione può risparmiare memoria (-L or -m) o ridurre il
probabilità che gli stati siano omessi (-M or -P), e può migliorare l'efficienza
di analisi parallela (-j or -k), ma può anche aumentare considerevolmente la
requisito di tempo del processore. L'opzione funziona anche con il controllo del modello di liveness,
ma non vi è alcuna garanzia che i valori di verità delle proprietà di vitalità rimangano
invariato. Questa opzione può essere combinata con -Y.

-z, --no-compress-percorsi
Il contrario di -Z. Questo è il comportamento predefinito.

Usa maria online usando i servizi onworks.net