pbes2bool

Note

Note: pbes2bool has been superseded by the tool pbessolve. Running pbes2bool invokes the latter. The old functionality of pbes2bool can be found in the deprecated tool pbes2booldeprecated, provided you have installed the deprecated tools.

orphan:


Usage

pbes2bool   [OPTION]... [INFILE]

Description

Solves (P)BES from INFILE. If INFILE is not present, stdin is used. The PBES is first instantiated into a parity game, which is then solved using Zielonka’s algorithm. It supports the generation of a witness or counter example for the property encoded by the PBES.

Command line options

--evidence-file=NAME

The file to which the evidence is written. If not set, a default name will be chosen.

-fNAME , --file=NAME

The file containing the LPS or LTS that was used to generate the PBES using lps2pbes -c. If this option is set, a counter example or witness for the encoded property will be generated. The extension of the file should be .lps in case of an LPS file, in all other cases it is assumed to be an LTS.

-iFORMAT , --in=FORMAT

use input format FORMAT:

pbes

PBES in internal format

--prune-todo-list

Prune the todo list periodically.

-QNUM , --qlimit=NUM

limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited).

-rNAME , --rewriter=NAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

-zNAME , --search-strategy=NAME

Use search strategy NAME:

breadth-first

Leads to smaller counter examples

depth-first

-sNAME , --solve-strategy=NAME

Use solve strategy NAME. Strategies 1-4 periodically apply on-the-fly solving, which may lead to early termination.

0

No on-the-fly solving is applied

1

Propagate solved equations using an attractor.

2

Detect winning loops.

3

Solve subgames using a fatal attractor.

4

Solve subgames using the solver.

--threads=NUM

run with NUM threads (default=1). With multiple threads the stack size on a Mac is limited which can lead to bus errors.

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

Wieger Wesselink