ltsconvert - Online în cloud

PROGRAM:

NUME

ltsconvert - convertiți și, opțional, minimizați un LTS

REZUMAT

Se convertesc [OPȚIUNE]... [INFIL [OUTFILE]]

DESCRIERE

Convertiți sistemul de tranziție etichetat (LTS) de la INFILE la OUTFILE în modul solicitat
format după aplicarea metodei de minimizare selectată (implicit nu este niciunul). Dacă OUTFILE este
nu este furnizat, se folosește stdout. Dacă nu este furnizat INFILE, se utilizează stdin.

Formatul de ieșire este determinat de extensia OUTFILE, în timp ce formatul de intrare este
determinată de conținutul INFILE. Opțiunile --in și --out pot fi folosite pentru a forța intrarea
și formate de ieșire. Formatele acceptate sunt:
„aut” pentru formatul Aldebaran (CADP),
„punct” pentru formatul GraphViz (nu mai este acceptat ca format de intrare),
„fsm” pentru formatul de mașină cu stări finite sau
„lts” pentru formatul mCRL2 LTS (implicit)

OPŢIUNI

OPȚIUNE poate fi oricare dintre următoarele:

-D, --determină
determina LTS

-eNUME, --echivalenţă=NUME
generați un LTS echivalent, păstrând echivalența NUME: „niciun” identitate
echivalență (implicit) „bisim” bisimilaritate puternică „bisim-sig” bisimilaritate puternică
folosirea rafinamentului semnăturii „ramificare-bisim” ramificare bisimilaritate „ramificare-
bisimilaritate de ramificare bisim-sig folosind rafinarea semnăturii „dpbranching-bisim”
divergența care păstrează bisimilaritatea ramificației „dpbranching-bisim-sig” divergența
păstrarea bisimilarității de ramificare folosind rafinamentul semnăturii „weak-bisim” slab
bisimilaritate „weak-bisim-sig” bisimilaritate slabă folosind rafinarea semnăturii „dpweak-
divergența bisim care păstrează bisimilaritatea slabă divergența „dpweak-bisim-sig”
păstrarea bisimilarității slabe folosind simularea puternică „sim” de rafinare a semnăturii
echivalență „urme” echivalente puternice „urme slabe” echivalență cu urme slabe
'tau-star' reducerea stelei tau

-iFORMAT, --în=FORMAT
utilizați FORMAT ca format de intrare

-lFILE, --lps=FILE
utilizați FILE ca LPS din care a fost generat LTS de intrare; acest lucru ar putea fi necesar
stocați numele corecte ale parametrilor stărilor atunci când salvați în format fsm și în
convertiți LTS non-mCRL2 într-un LTS mCRL2

--nu-ajunge
nu efectuați o verificare a accesibilității pe LTS de intrare

-n, --nu-stat
omiteți informațiile de stare atunci când salvați în format punct

-oFORMAT, --afara=FORMAT
utilizați FORMAT ca format de ieșire

--tau=ACTNAMES
consideră că acțiunile cu un nume în lista ACTNAMES separate prin virgulă sunt interne
(tau) acțiuni în plus față de cele definite ca atare de intrare

--timinguri[=FILE]
adăugați măsurătorile de sincronizare la FILE. Măsurătorile sunt scrise în eroare standard dacă
nu este furnizat niciun FIȘIER

Opțiuni standard:

-q, --Liniște
nu afișați mesaje de avertizare

-v, --verbos
afișează mesaje intermediare scurte

-d, --depanare
afișează mesaje intermediare detaliate

--nivel-log=NIVEL
afișează mesaje intermediare până la nivelul inclusiv

-h, --Ajutor
afișați informații de ajutor

--versiune
afișează informații despre versiune

Utilizați ltsconvert online folosind serviciile onworks.net