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


pbes2bool   [OPTION]... [INFILE]


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


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.


use input format FORMAT:


PBES in internal format


Prune the todo list periodically.

-QNUM , --qlimit=NUM

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

-rNAME , --rewriter=NAME

use rewrite strategy NAME:


jitty rewriting


compiled jitty rewriting


jitty rewriting with prover

-zNAME , --search-strategy=NAME

Use search strategy NAME:


Leads to smaller counter examples


-sNAME , --solve-strategy=NAME

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


No on-the-fly solving is applied


Propagate solved equations using an attractor.


Detect winning loops.


Solve subgames using a fatal attractor.


Solve subgames using the solver.


run with NUM threads (default=1).


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


display intermediate messages up to and including level

-h , --help

display help information


display version information


display help information, including hidden and experimental options


Wieger Wesselink