pbes2cvc4
- orphan:
Usage
pbes2cvc4 [OPTION]... [INFILE [OUTFILE]]
Description
Solves (P)BES from INFILE. If INFILE is not present, stdin is used.
Command line options
-gGOAL
, --goal=GOAL
produce an SMT file for proving GOAL:
disjunctiveWitness
a witness for a disjunctive PBES; if satisfiable, shows that the value of the PBES is true
disjunctiveAcyclicUnrolling
an acyclic unrolling for a disjunctive PBES; if unsatisfiable, shows that the value of the PBES is false
conjunctiveWitness
a witness for a conjunctive PBES; if satisfiable, shows that the value of the PBES is false
conjunctiveAcyclicUnrolling
an acyclic unrolling for a disjunctive PBES; if unsatisfiable, shows that the value of the PBES is true
-iFORMAT
, --in=FORMAT
use input format FORMAT:
pbes
PBES in internal format
pgsolver
BES in PGSolver format
text
PBES in textual (mCRL2) format
-lNUM
, --levels=NUM
unroll NUM levels
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
Standard options
-q
, --quiet
do not display warning messages
-v
, --verbose
display short log messages
-d
, --debug
display detailed log messages
--log-level=LEVEL
display log messages up to and including level; either warn, verbose, debug or trace
-h
, --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options