User manual/pbessolve

From MCRL2

Solve a PBES. (EXPERIMENTAL)

Contents 1 Synopsis 2 Short description 3 Options 4 Author 5 Bug reporting

Synopsis

pbessolve [OPTION]... [INFILE]

Short description

The pbessolve tool solves the parameterised boolean equation system (PBES) in INFILE and writes the result to stdout. If INFILE is not present, stdin is used.

Options

OPTION can be any of the following:

-bNUM, --bound=NUM

limit the number of approximation steps to NUM

-i, --interactive

turn on the manual guidance of the approximation process

-p, --pnf

use the prenex normal form for the approximation

-rNAME, --rewriter=NAME

use rewrite strategy NAME

-sSOLVER, --solver=SOLVER

use the SOLVER to remove inconsistent paths from BDDs:

• 'cvc' for the SMT solver CVC3 (default),
• 'fast' for the SMT solver CVC3 (fast variant),
• 'ario' for the SMT solver Ario

Standard options:

-q, --quiet

do not display warning messages

-v, --verbose

display short intermediate messages

-d, --debug

display detailed intermediate messages

-h, --help

display help information

--version

display version information

Author

Written by Simona Orzan.

Bug reporting

Report bugs at our issue tracking system.