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.



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 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 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). With multiple threads the stack size on a Mac is limited which can lead to bus errors.


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


display log messages up to and including level; either warn, verbose, debug or trace

-h , --help

display help information


display version information


display help information, including hidden and experimental options


Wieger Wesselink