lpsinvelm - Online in de cloud

PROGRAMMA:

NAAM

lpsinvelm - controleer invarianten en gebruik deze om summands van een LPS te vereenvoudigen of te elimineren

KORTE INHOUD

lpsinvelm [OPTIE]... --invfile=INVFILE [IN BESTAND [UITBESTAND]]

PRODUCTBESCHRIJVING

Controleert of de Booleaanse formule (een mCRL2-gegevensexpressie van de soort Bool) wordt geleverd als
invariant is een invariant van de lineaire processpecificatie (LPS) in INFILE. Als dit is
In dat geval elimineert de tool alle sommaties van de LPS waarvan de voorwaarde in strijd is met de
invariant en schrijft het resultaat naar OUTFILE. Als INFILE aanwezig is, wordt stdin gebruikt. Als
OUTFILE is niet aanwezig, stdout wordt gebruikt.

De tool kan ook worden gebruikt om de voorwaarden van de sommaties van de gegeven LPS te vereenvoudigen.

OPTIES

OPTIE kan een van de volgende zijn:

-y, --alle overtredingen
beëindig niet zodra een enkele overtreding van de invariant wordt gevonden, maar
rapporteer in plaats daarvan alle overtredingen

-c, --tegenvoorbeeld
een waardering weergeven die aangeeft waarom de invariant mogelijk wordt geschonden als deze wordt geschonden
Het is onzeker of een sommatie de invariant schendt

-o, --inductie
pas inductie toe op lijsten

-iINNVFILE, --onveranderbaar=INNVFILE
gebruik de Booleaanse formule (een mCRL2-gegevensexpressie van de soort Bool) in INVFILE as
onveranderbaar

-n, --geen controle
controleer niet of de invariant geldt voordat u onbereikbare sommaties elimineert

-e, --geen eliminatie
elimineer of vereenvoudig de sommaties niet, maar voeg de invariant aan elke voorwaarde toe

-pVOORVOEGSEL, --print-punt=VOORVOEGSEL
sla een .dot-bestand op van de resulterende BDD als het onmogelijk is om te bepalen of een
sommatie schendt de invariant; PREFIX wordt gebruikt als voorvoegsel van de uitvoerbestanden

-QNUM, --qlimiet=NUM
beperk de opsomming van kwantoren tot NUM variabelen. (Standaard NUM=1000, NUM=0 voor
onbeperkt).

-rNAAM, --herschrijver=NAAM
gebruik herschrijfstrategie NAAM: 'jitty' jitty herschrijven (standaard) 'jittyc' gecompileerd
jitty herschrijven 'jittyp' jitty herschrijven met spreekwoord

-l, --vereenvoudig-alles
vereenvoudig de voorwaarden van alle sommaties, in plaats van alleen de sommaties te elimineren
waarvan de voorwaarden in combinatie met de invariant tegenstrijdigheden zijn

-zOPLOSSING, --smt-oplosser=OPLOSSING
gebruik SOLVER om inconsistente paden te verwijderen uit de intern gebruikte BDD's (standaard
er wordt geen padeliminatie toegepast): 'cvc' de SMT-oplosser CVC3

-tLIMIT, --tijdslimiet=LIMIT
besteed maximaal LIMIT seconden aan het bewijzen van een enkele formule

--tijden[=FILE]
timingmetingen toevoegen aan FILE. Metingen worden naar de standaardfout geschreven als
er is geen BESTAND aanwezig

Standaard opties:

-q, --stil
geen waarschuwingsberichten weergeven

-v, --uitgebreid
korte tussenberichten weergeven

-d, --debuggen
gedetailleerde tussenberichten weergeven

--Log niveau=NIVEAU
tussenberichten weergeven tot en met niveau

-h, --help
help informatie weergeven

--versie
versie-informatie weergeven

Gebruik lpsinvelm online met behulp van onworks.net-services