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
select the algorithm NAME to solve the res after it is generated.
solve the res using gauss elimination; this is guaranteed to terminate but may require an excessive amount of time.
solve the res by a numerical recursive algorithm; this is not guaranteed to terminate.
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
provide an answer within precision 10^-precision. [AS IT STANDS THIS IS THE NOW THE DIFFERENCE BETWEEN TWO ITERATIONS]
limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).
use rewrite strategy NAME:
compiled jitty rewriting
jitty rewriting with prover
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
do not display warning messages
display short log messages
display detailed log messages
display log messages up to and including level; either warn, verbose, debug or trace
display help information
display version information
display help information, including hidden and experimental options