lpsinvelm - Online în cloud

PROGRAM:

NUME

lpsinvelm - verificați invarianții și utilizați-i pentru a simplifica sau elimina sumandu-le unui LPS

REZUMAT

lpsinvelm [OPȚIUNE]... --invfile=INVFILE [INFIL [OUTFILE]]

DESCRIERE

Verifică dacă formula booleană (o expresie de date mCRL2 de sortare Bool) este furnizată ca
invariant este un invariant al specificației procesului liniar (LPS) în INFILE. Dacă aceasta este
În acest caz, instrumentul elimină toate sumele LPS a căror condiție încalcă
invariant și scrie rezultatul în OUTFILE. Dacă INFILE este prezent, se utilizează stdin. Dacă
OUTFILE nu este prezent, este folosit stdout.

Instrumentul poate fi folosit și pentru a simplifica condițiile sumelor LPS-ului dat.

OPŢIUNI

OPȚIUNE poate fi oricare dintre următoarele:

-y, --toate-încălcări
nu termina imediat ce se constată o singură încălcare a invariantului, dar
raportați în schimb toate încălcările

-c, --contra exemplu
afișează o evaluare care indică de ce invariantul ar putea fi încălcat dacă acesta
este incert dacă un sumand încalcă invariantul

-o, --inducţie
aplicați inducția pe liste

-iINVFILE, --invariant=INVFILE
utilizați formula booleană (o expresie de date mCRL2 de sortare Bool) în INVFILE ca
invariant

-n, --nu-verifica
nu verificați dacă invariantul se menține înainte de a elimina sumandele inaccesibile

-e, --nu-eliminare
nu eliminați sau simplificați sumandule, ci adăugați invariantul la fiecare condiție

-pPREFIX, --print-dot=PREFIX
salvați un fișier .dot al BDD-ului rezultat dacă este imposibil să determinați dacă a
sumand încalcă invariantul; PREFIX va fi folosit ca prefix al fișierelor de ieșire

-QNUM, --qlimit=NUM
limitați enumerarea cuantificatorilor la NUM variabile. (Implicit NUM=1000, NUM=0 pentru
nelimitat).

-rNUME, --rescriere=NUME
utilizați strategia de rescrire NUME: „jitty” rescriere nervoasă (implicit) „jittyc” compilat
rescriere nervoasă 'jittyp' rescriere nervoasă cu prover

-l, --simplifica-toate
simplificați condițiile tuturor sumelor, în loc să eliminați doar sumele
ale căror condiţii în legătură cu invariantul sunt contradicţii

-zSOLVER, --smt-solver=SOLVER
utilizați SOLVER pentru a elimina căile inconsistente din BDD-urile utilizate intern (în mod implicit,
nu se aplică nicio eliminare a căii): „cvc” solutorul SMT CVC3

-tLIMITĂ, --limita=LIMITĂ
petrece cel mult LIMIT secunde pentru a demonstra o singură formulă

--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 lpsinvelm online folosind serviciile onworks.net