lpsconfcheck - Online in de cloud

PROGRAMMA:

NAAM

lpsconfcheck - markeer samenvloeiende tau-summands van een LPS

KORTE INHOUD

lpsconfcheck [OPTIE]... [IN BESTAND [UITBESTAND]]

PRODUCTBESCHRIJVING

Controleert welke tau-summands van de mCRL2 LPS in INFILE confluent zijn, markeert ze door ze te hernoemen
naar ctau en schrijf het resultaat naar OUTFILE. Als INFILE niet aanwezig is, wordt stdin gebruikt. Als
OUTFILE is niet aanwezig, stdout wordt gebruikt.

OPTIES

OPTIE kan een van de volgende zijn:

-a, --check-alles
controleer de samenvloeiing van tau-summands met betrekking tot alle andere summands, in plaats van
doorgaan met de volgende tau-summand zodra een summand wordt aangetroffen
niet samenvloeiend met de huidige tau-summand

-c, --tegenvoorbeeld
een taxatie weergeven waarvoor de confluentievoorwaarde niet geldt, in het geval dat de
aangetroffen toestand is noch een tegenstrijdigheid, noch een tautologie

-g, --genereren-invarianten
probeer te bewijzen dat de gereduceerde confluentievoorwaarde een invariant is van de LPS, in
geval de confluentievoorwaarde geen tautologie is

-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 controleert op confluentie

-m, --geen-markering
markeer de samenvloeiende tau-summands niet; aangezien er geen wijzigingen zijn aangebracht in de LPS,
er wordt niets naar OUTFILE geschreven

-pVOORVOEGSEL, --print-punt=VOORVOEGSEL
bewaar een .dot-bestand van de resulterende BDD voor het geval twee sommaties niet kunnen worden bewezen
samenvloeiend; 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

-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

-sNUM, --som=NUM
elimineer of vereenvoudig de som met alleen het nummer NUM

-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 lpsconfcheck online met behulp van onworks.net-services