lps2lts - Online nel cloud

PROGRAMMA:

NOME

lps2lts - genera un LTS da un LPS

SINOSSI

lps2lts [OPZIONE]... [INFILE [PROFILO]]

DESCRIZIONE

Genera un LTS dall'LPS in INFILE e salva il risultato in OUTFILE. Se INFILE non lo è
fornito, viene utilizzato stdin. Se OUTFILE non viene fornito, l'LTS non viene memorizzato.

Se viene utilizzato il rewriter 'jittyc', la variabile di ambiente MCRL2_COMPILEREWRITER
(valore predefinito: 'mcrl2compilerewriter') determina lo script che compila il rewriter,
e MCRL2_COMPILEDIR (valore predefinito: '.') determina dove vengono archiviati i file temporanei.

Nota che lps2lts può fornire più transizioni con la stessa etichetta tra qualsiasi coppia di
stati. Se ciò non è desiderato, tali transizioni possono essere rimosse applicando un forte
riduzione della bisimulazione utilizzando ad esempio lo strumento ltsconvert.

Il formato di OUTFILE è determinato dalla sua estensione (a meno che non sia specificato da un
opzione). I formati supportati sono:

'aut' per il formato Aldebaran (CADP),
'punto' per il formato GraphViz (non più supportato come formato di input),
'fsm' per il formato Macchina a stati finiti, oppure
'lts' per il formato mCRL2 LTS Se viene utilizzato il riscrittore jittyc, il
Variabile di ambiente MCRL2_COMPILEREWRITER (valore predefinito: mcrl2compilerewriter)
determina lo script che compila il rewriter e MCRL2_COMPILEDIR (valore predefinito:
'.') determina dove vengono archiviati i file temporanei. Nota che lps2lts può fornire più
transizioni con la stessa etichetta tra qualsiasi coppia di stati. Se questo non è desiderato, tale
le transizioni possono essere rimosse applicando una forte riduzione di bisimulazione usando per esempio
lo strumento ltsconvert.

VERSIONI

OPZIONE può essere uno dei seguenti:

-aNOMI, --azione=NOMI
rilevare e segnalare le azioni nel sistema delle transizioni che hanno nomi di azioni da
NAMES, un elenco separato da virgole. Questo è ad esempio utile per trovare (o dimostrare il
assenza) di un errore di azione. Viene stampato un messaggio per ogni occorrenza di uno di
questi nomi di azioni. Con il flag -t vengono generate tracce verso queste azioni

-b[NUM], --bit-hash[=NUM]
usa il bit hashing per memorizzare gli stati e memorizzare al massimo NUM stati. Ciò significa che
invece di tenere un registro completo di tutti gli stati che sono stati visitati, un po' di array
viene utilizzato per indicare se un hash di uno stato è stato visto o meno in precedenza.
Sebbene ciò significhi che questa opzione può far sì che gli stati vengano scambiati per altri
(perché sono mappati allo stesso hash), può essere utile esplorare molto grandi
LTS altrimenti non esplorabili. Il valore predefinito per NUM è approssimativamente
2*10^8 (corrisponde a circa 25MB di memoria)

--in cache
utilizzare tecniche di memorizzazione nella cache dell'enumerazione per accelerare la generazione dello spazio degli stati.

-c[NOME], --confluenza[=NOME]
applicare la priorità delle transizioni con l'etichetta dell'azione NAME. (quando nessun NAME è
fornita (cioè, '-c') viene data priorità all'azione 'ctau'. Dare priorità a
per tau usa il flag -ctau. Nota che se il processo lineare non è tau-confluente,
lo spazio degli stati generato è necessariamente bisimilare allo spazio degli stati di
l'lps. L'algoritmo di generazione utilizzato non richiede il processo lineare
essere tau convergente.

-D, -- deadlock
rilevare i deadlock (cioè per ogni deadlock viene stampato un messaggio)

-F, --divergenza
rileva le divergenze (cioè per ogni stato con una divergenza (= loop tau) un messaggio è
stampato). L'algoritmo per rilevare le divergenze è lineare per ogni stato, quindi
l'esplorazione dello spazio degli stati diventa quadratica con questa opzione attiva, causando uno stato
l'esplorazione dello spazio diventi lenta quando questa opzione è abilitata.

-yBOOL, --manichino=BOOL
sostituire le variabili libere nell'LPS con valori fittizi basati sul valore di BOOL:
'sì' (predefinito) o 'no'

--error-traccia
se si verifica un errore durante l'esplorazione, salvare una traccia nello stato che non poteva essere
esplorato

--init-size=NUM
imposta la dimensione iniziale delle tabelle hash utilizzate internamente (il valore predefinito è 10000)

-lNUM, --max=NUM
esplora al massimo NUM stati

-mNOMI, --multiazione=NOMI
rilevare e segnalare le multiazioni nel sistema delle transizioni da NAMES, una virgola
elenco separato. Funziona come -a, tranne per il fatto che le multi-azioni sono abbinate esattamente,
compresi i parametri dei dati.

--nessuna informazione
non aggiungere informazioni sullo stato a OUTFILESenza questa opzione lps2lts aggiunge lo stato
vettore per LTS. Questa opzione fa sì che queste informazioni vengano scartate e afferma
sono indicati solo da un numero progressivo. Le informazioni esplicite sullo stato sono utili per
scopi di visualizzazione, ad esempio, ma può far crescere OUTFILE
notevolmente. Notare che questa opzione è implicita quando si scrive nel formato AUT.

-oFORMATO, --fuori=FORMATO
salva l'output nel formato specificato

--fesso
utilizzare la potatura del sommario per accelerare la generazione dello spazio degli stati.

-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

-sNOME, --strategia=NOME
esplora lo spazio degli stati usando la strategia NAME: 'b', 'breadth' ricerca in ampiezza
(predefinito) 'd', 'profondità' ricerca in profondità 'p', 'priorità' priorità singola
azioni sul suo primo argomento essendo di tipo Nat dove solo quelle azioni con il
vengono selezionati i valori più bassi per questo parametro. Ad esempio, se ci sono azioni a(3) e
b(4) a(3) rimane e b(4) viene saltato. Azioni senza un primo parametro di ordinamento
Nat e le multazioni con più di un'azione vengono sempre scelte (l'opzione è
sperimentale) 'q', 'priorità' danno la priorità alle azioni sul suo primo argomento che è of
ordina Nat (vedi opzione --prioritized), e seleziona casualmente uno di questi per ottenere a
simulazione casuale con priorità (l'opzione è sperimentale) 'r', 'casuale' casuale
simulazione. Di tutti i successivi stati uno viene scelto a caso indipendentemente dal fatto che
questo stato è già stato osservato. Di conseguenza, solo simulazione casuale
termina quando viene rilevato uno stato di deadlock.

--sopprimi
in modalità verbose, non stampare messaggi di avanzamento che indicano il numero di visitati
stati e transizioni. Per grandi spazi di stato il numero di messaggi di avanzamento può
essere piuttosto orrendo. Questa funzione aiuta a sopprimerli. Altri messaggi verbosi,
come il numero totale di stati esplorati, rimangono visibili.

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

--todo-max=NUM
mantieni al massimo NUM stati negli elenchi di cose da fare; questa opzione è rilevante solo per l'ampiezza
prima ricerca, dove NUM è il numero massimo di stati per livello, e per profondità
prima ricerca, dove NUM è la profondità massima

-t[NUM], --traccia[=NUM]
Scrivi una traccia più breve per ogni stato raggiunto con un'azione da NAMES from
opzione --action, viene rilevato un deadlock con --deadlock o è una divergenza
rilevato con --divergence in un file. Non verranno scritte più di NUM tracce. Se
NUM non è fornito il numero di tracce è illimitato. Per ogni traccia che deve essere
scritto verrà creato un file univoco con estensione .trc (trace) contenente a
traccia più breve dallo stato iniziale allo stato di deadlock. Le tracce possono essere
abbastanza stampato e convertito in altri formati usando tracepp.

-u, --dati-inutilizzati
non rimuovere le parti inutilizzate della specifica dei dati

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