lpsinvelm - Online sa Cloud

PROGRAMA:

NAME

lpsinvelm - suriin ang mga invariant at gamitin ang mga ito upang pasimplehin o alisin ang mga summand ng isang LPS

SINOPSIS

lpsinvelm [OPTION]... --invfile=INVFILE [INFILE [OUTFILE]]

DESCRIPTION

Sinusuri kung ang boolean formula (isang mCRL2 data expression ng sort Bool) ay ibinigay bilang
ang invariant ay isang invariant ng linear process specification (LPS) sa INFILE. Kung ito ay
kaso, inalis ng tool ang lahat ng summand ng LPS na ang kundisyon ay lumalabag sa
invariant, at isinusulat ang resulta sa OUTFILE. Kung mayroong INFILE, ginagamit ang stdin. Kung
Wala ang OUTFILE, ginagamit ang stdout.

Ang tool ay maaari ding gamitin upang pasimplehin ang mga kondisyon ng mga summand ng ibinigay na LPS.

Opsyon

OPTION maaaring alinman sa mga sumusunod:

-y, --lahat ng paglabag
huwag wakasan sa sandaling makita ang isang paglabag sa invariant, ngunit
iulat sa halip ang lahat ng paglabag

-c, --kontra-halimbawa
magpakita ng valuation na nagsasaad kung bakit posibleng lumabag ang invariant kung ito
ay hindi sigurado kung ang isang summand ay lumalabag sa invariant

-o, --induction
ilapat ang induction sa mga listahan

-iINVFILE, --invariant=INVFILE
gamitin ang boolean formula (isang mCRL2 data expression ng sort Bool) sa INVFILE bilang
invariant

-n, --walang-check
huwag suriin kung ang invariant ay humahawak bago alisin ang hindi maabot na mga summand

-e, --walang-pag-aalis
huwag alisin o pasimplehin ang mga summand, ngunit idagdag ang invariant sa bawat kundisyon

-pPREFIX, --print-tuldok=PREFIX
mag-save ng .dot file ng nagresultang BDD kung imposibleng matukoy kung a
summand ay lumalabag sa invariant; Gagamitin ang PREFIX bilang prefix ng mga output file

-QNUM, --qlimit=NUM
limitahan ang enumeration ng mga quantifier sa NUM variable. (Default na NUM=1000, NUM=0 para sa
walang limitasyon).

-rNAME, --rewriter=NAME
gumamit ng diskarte sa pagsulat muli NAME: 'jitty' jitty rewriting (default) 'jittyc' compiled
jitty rewriting 'jittyp' jitty rewriting with prover

-l, --pasimplehin-lahat
pasimplehin ang mga kondisyon ng lahat ng summands, sa halip na alisin lamang ang summands
na ang mga kondisyon kasabay ng invariant ay mga kontradiksyon

-zSOLVER, --smt-solver=SOLVER
gamitin ang SOLVER upang alisin ang mga hindi tugmang landas mula sa mga internal na ginamit na BDD (bilang default,
walang path elimination ang inilapat): 'cvc' ang SMT solver CVC3

-tLIMIT, --takdang oras=LIMIT
gumugol ng hindi hihigit sa LIMIT segundo sa pagpapatunay ng isang formula

--mga oras[=FILE]
magdagdag ng mga sukat ng timing sa FILE. Ang mga sukat ay isinusulat sa karaniwang error kung
walang FILE na ibinigay

Mga karaniwang opsyon:

-q, --tahimik
huwag magpakita ng mga mensahe ng babala

-v, --verbose
magpakita ng mga maikling intermediate na mensahe

-d, --debug
magpakita ng mga detalyadong intermediate na mensahe

--log-level=ANTAS
magpakita ng mga intermediate na mensahe hanggang sa at kabilang ang antas

-h, - Tumulong
ipakita ang impormasyon ng tulong

--bersyon
ipakita ang impormasyon ng bersyon

Gamitin ang lpsinvelm online gamit ang mga serbisyo ng onworks.net