lpsinvelm - Online nel cloud

PROGRAMMA:

NOME

lpsinvelm - controlla gli invarianti e usali per semplificare o eliminare i riassunti di un LPS

SINOSSI

lpsinvelm [OPZIONE]... --invfile=INVFILE [INFILE [PROFILO]]

DESCRIZIONE

Controlla se la formula booleana (un'espressione di dati mCRL2 di ordinamento Bool) fornita come
invariant è un invariante della specifica del processo lineare (LPS) in INFILE. Se questo è
caso, lo strumento elimina tutte le somme del LPS la cui condizione viola la
invariant e scrive il risultato in OUTFILE. Se INFILE è presente, viene utilizzato stdin. Se
OUTFILE non è presente, viene utilizzato stdout.

Lo strumento può essere utilizzato anche per semplificare le condizioni dei riassunti del dato LPS.

VERSIONI

OPZIONE può essere uno dei seguenti:

-y, --tutte-violazioni
non terminano non appena viene trovata una singola violazione dell'invariante, ma
segnala invece tutte le violazioni

-c, --counter-esempio
visualizzare una valutazione che indica il motivo per cui l'invariante potrebbe essere violato se
è incerto se una somma viola l'invariante

-o, --induzione
applicare l'induzione alle liste

-iFILE INV, --invariante=FILE INV
usa la formula booleana (un'espressione di dati mCRL2 di sort Bool) in INVFILE as
invariante

-n, --nessun controllo
non controllare se l'invariante vale prima di eliminare le somme irraggiungibili

-e, --no-eliminazione
non eliminare o semplificare le somme, ma aggiungere l'invariante a ciascuna condizione

-pPREFISSO, --punto-stampa=PREFISSO
salvare un file .dot del BDD risultante se è impossibile determinare se a
la somma viola l'invariante; PREFIX verrà utilizzato come prefisso dei file di output

-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

-l, --semplifica-tutto
semplificare le condizioni di tutte le addizioni, invece di eliminare semplicemente le addizioni
le cui condizioni in congiunzione con l'invariante sono contraddizioni

-zRisolutore, --smt-solutore=Risolutore
utilizzare SOLVER per rimuovere percorsi incoerenti dai BDD utilizzati internamente (per impostazione predefinita,
non viene applicata alcuna eliminazione di percorso): 'cvc' il solutore SMT CVC3

-tLIMITE, --limite di tempo=LIMITE
spendi al massimo LIMIT secondi per provare una singola formula

--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 lpsinvelm online utilizzando i servizi onworks.net