pbes2yices

orphan:


Usage

pbes2yices   [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

Author

Ruud Koolen