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.

Manual page for pbes2bool

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

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

-fNAME , --fileNAME

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

use input format FORMAT:

pbes

PBES in internal format

--prune-todo-list

Prune the todo list periodically.

-QNUM , --qlimitNUM

limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).

-rNAME , --rewriterNAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

-zNAME , --search-strategyNAME

Use search strategy NAME:

breadth-first

Leads to smaller counter examples

depth-first

-sNAME , --solve-strategyNAME

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.

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

-d , --debug

display detailed intermediate messages

--log-levelLEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Wieger Wesselink