ltsconvert - Online nel cloud

PROGRAMMA:

NOME

ltsconvert - converte e facoltativamente minimizza un LTS

SINOSSI

ltsconvert [OPZIONE]... [INFILE [PROFILO]]

DESCRIZIONE

Converti il ​​sistema di transizione etichettato (LTS) da INFILE a OUTFILE nella richiesta
dopo aver applicato il metodo di minimizzazione selezionato (l'impostazione predefinita è nessuno). Se OUTFILE è
non fornito, viene utilizzato stdout. Se INFILE non viene fornito, viene utilizzato stdin.

Il formato di output è determinato dall'estensione di OUTFILE, mentre il formato di input è
determinato dal contenuto di INFILE. Le opzioni --in e --out possono essere utilizzate per forzare l'input
e formati di output. 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 (predefinito)

VERSIONI

OPZIONE può essere uno dei seguenti:

-D, --determinare
determinare LTS

-eNOME, --equivalenza=NOME
generare un LTS equivalente, preservando l'equivalenza NAME: identità 'none'
equivalenza (predefinito) 'bisim' forte bisimilarità 'bisim-sig' forte bisimilarità
utilizzando il perfezionamento della firma 'ramificazione-bisim' bisimilarità di ramificazione 'ramificazione-
bisim-sig' bisimilarità di ramificazione utilizzando il perfezionamento della firma 'dpbranching-bisim'
divergenza preservando ramificazione bisimilarità 'dpbranching-bisim-sig' divergenza
preservare la bisimilarità di ramificazione utilizzando il raffinamento della firma 'debole-bisim' debole
bisimilarità 'weak-bisim-sig' bisimilarità debole utilizzando il raffinamento della firma 'dpweak-
bisim' divergenza preservando la bisimilarità debole divergenza 'dpweak-bisim-sig'
preservando la bisimilarità debole usando la simulazione forte "sim" di raffinatezza della firma
equivalenza 'traccia' equivalenza traccia forte 'traccia debole' equivalenza traccia debole
riduzione della stella tau 'tau-star'

-iFORMATO, --In=FORMATO
usa FORMAT come formato di input

-lRISORSE, --lps=RISORSE
utilizzare FILE come LPS da cui è stato generato l'LTS di input; questo potrebbe essere necessario per
memorizzare i nomi dei parametri corretti degli stati durante il salvataggio in formato fsm e in
convertire LTS non mCRL2 in LTS mCRL2

--nessuna portata
non eseguire un controllo di raggiungibilità sull'input LTS

-n, --nessuno stato
tralasciare le informazioni sullo stato quando si salva in formato punto

-oFORMATO, --fuori=FORMATO
usa FORMAT come formato di output

--tau=NOMI ATTI
considera le azioni con un nome nell'elenco separato da virgole ACTNAMES come interne
(tau) azioni in aggiunta a quelle definite come tali dall'input

--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 ltsconvert online usando i servizi onworks.net