pressolve   [OPTION]... [INFILE]


Solves (P)BES from INFILE. If INFILE is not present, stdin is used. The PRES 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 PRES.

Command line options

-aNAME , --algorithm=NAME

select the algorithm NAME to solve the res after it is generated.

g, gauss

solve the res using gauss elimination; this is guaranteed to terminate but may require an excessive amount of time.

n, numerical

solve the res by a numerical recursive algorithm; this is not guaranteed to terminate.

m, numerical_directed

solve the res by a numerical recursive algorithm with directed propagation; this is not guaranteed to terminate.


use input format FORMAT:


PRES in internal format

-pNUM , --precision=NUM

provide an answer within precision 10^-precision. [AS IT STANDS THIS IS THE NOW THE DIFFERENCE BETWEEN TWO ITERATIONS]

-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


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


Jan Friso Groote