mcrl22lps - Online nel cloud

PROGRAMMA:

NOME

mcrl22lps - traduce una specifica mCRL2 in un LPS

SINOSSI

mcrl22lps [OPZIONE]... [INFILE [PROFILO]]

DESCRIZIONE

Linearizza la specifica mCRL2 in INFILE e scrive l'LPS risultante su OUTFILE. Se
OUTFILE non è presente, viene utilizzato stdout. Se INFILE non è presente, viene utilizzato stdin.

VERSIONI

OPZIONE può essere uno dei seguenti:

-b, --binario
quando il clustering usa le funzioni di caso binario invece di n-ary; in presenza di
-w/--newstate, le variabili di stato sono codificate da un vettore di variabili booleane

-e, --solo controllo
controllare la sintassi e la semantica statica; non linearizzare

-c, --grappolo
tutte le azioni nell'LPS finale sono raggruppate. Clustering significa che somma con il
stesse etichette di azione sono raggruppate insieme. Ad esempio, a(f1) . P(g1) + a(f2) .
P(g2) è sostituito dalla somma b: Bool . a(se(b, f1, f2)) . P(se(b, f2, g2)). Il
vantaggio è che il numero di addizioni può essere ridotto in modo sostanziale in questo modo.
Lo svantaggio è che vengono introdotti operatori di somma e nuovi tipi di dati con
vengono generate funzioni ausiliarie. Per evitare la generazione di nuovi tipi,
è possibile utilizzare l'opzione -b/--binary.

-D, --delta
aggiungere un sommario true->delta a ogni stato in ogni processo; questi delta sussumono tutto
altri delta temporizzati condizionali, riducendo efficacemente il numero di riassunti delta
drasticamente nel processo lineare risultante; velocizza la linearizzazione. Questo è il
predefinito, ma non gestisce correttamente il tempo.

-lNOME, --lin-metodo=NOME
utilizzare il metodo di linearizzazione NOME: 'regolare' per generare un LPS in forma regolare
(la specifica dovrebbe essere regolare) (predefinito) 'regolare2' per una variante di 'regolare'
che utilizza più variabili di dati (utile quando "normale" non funziona) "stack" per
utilizzando i tipi di dati dello stack (utile quando "normale" e "regolare2" non funzionano)

-w, --nuovostato
le variabili di stato sono codificate utilizzando tipi enumerati anziché naturali positivi
numeri (Pos). Usando questa opzione vengono generati nuovi ordinamenti finiti chiamati Enumk
dove k è la dimensione del dominio. Inoltre, funzioni di caso ausiliari e uguaglianze
Sono definiti. In combinazione con l'opzione --binary vengono codificati gli ordinamenti finiti
da booleani. (richiede il metodo di linearizzazione 'regolare' o 'regolare2').

-z, --no-alfa
non vengono applicate riduzioni alfabetiche. Per impostazione predefinita, mcrl22lps tenta di distribuire
comunicazione, nascondere e consentire agli operatori oltre l'operatore di composizione parallela come
questo riduce la dimensione dei processi lineari intermedi. Usando questa opzione, questo
passo può essere evitato. Il nome deriva dagli assiomi dell'alfabeto nell'algebra dei processi.

-n, --nessun cluster
le azioni negli LPS intermedi non sono raggruppate prima di essere messe in parallelo.
Per impostazione predefinita, questi processi sono raggruppati per evitare un aumento del numero di
somme quando si trasformano due processi lineari paralleli in un singolo lineare
processi. Se un processo lineare con M somme viene messo in parallelo con un lineare
processo con N somme il processo risultante ha M×N + M + N somme. Sia M che
N può essere sostanzialmente ridotto raggruppando al costo di introdurre nuovi tipi
e funzioni. Vedere -c/--cluster, esp. per una breve spiegazione del raggruppamento
processo.

--no-costelmo
non cercare di applicare l'eliminazione costante quando si genera un processo lineare.

-g, --no-deltaelm
evitare di rimuovere i sommi delta spuri. A causa dell'esistenza del tempo, delta
le somme non possono essere omesse. A causa della presenza di multi-azioni il numero di
le somme possono essere enormi. L'algoritmo per rimuovere i summa delta funziona semplicemente da
confrontando ogni sommatoria delta con l'altra sommatoria per vedere se la condizione
dell'uno implica la condizione dell'altro. Chiaramente, questo ha quadratica
complessità e può richiedere molto tempo.

-f, --no-globvars
istanziare non importa valori con costanti arbitrarie, invece di modellarli
da variabili globali. Questo non ha effetto sulle variabili globali che sono dichiarate nel
specificazione.

-o, --nessuna riscrittura
non riscrivere i termini dei dati durante la linearizzazione; utile quando il sistema di riscrittura lo fa
non terminare. Questa opzione disattiva anche l'applicazione della costante
eliminazione.

-m, --no-sumem
evitare di applicare l'eliminazione della somma nella composizione parallela

-QNUM, --qlimit=NUM
limitare l'enumerazione dei quantificatori a variabili NUM. (Predefinito NUM=1000, NUM=0 per
illimitato).

-rNOME, --riscrittore=NOME
usa la strategia di riscrittura NAME: 'jitty' jitty rewriting (predefinito) 'jittyc' compilato
riscrittura jitty 'jittyp' riscrittura jitty con prover

-a, --nomi di stato
i nomi dei parametri dei dati generati sono estesi con il nome del processo in
che si verificano. Ciò rende più facile determinare da dove proviene il parametro.

-T, --a tempo
Traduci il processo in forma lineare preservando tutte le informazioni temporizzate. In parallelo
processi il numero di possibili vincoli di tempo può essere grande, rallentando
linearizzazione. Conferisci l'opzione --delta che produce una traduzione molto più veloce che
non conserva i tempi correttamente

--tempi[=RISORSE]
aggiungere le misurazioni dei tempi a FILE. Le misurazioni vengono scritte nell'errore standard se
non viene fornito alcun FILE

Opzioni standard:

-q, --silenzioso
non visualizzare messaggi di avviso

-v, --verboso
visualizzare brevi messaggi intermedi

-d, - debug
visualizzare messaggi intermedi dettagliati

--livello-log=LIVELLO
visualizzare messaggi intermedi fino al livello compreso

-h, --Aiuto
visualizzare le informazioni di aiuto

--versione
visualizzare le informazioni sulla versione

Usa mcrl22lps online utilizzando i servizi onworks.net