pressolve
- orphan:
Usage
pressolve [OPTION]... [INFILE]
Description
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,gausssolve the res using gauss elimination; this is guaranteed to terminate but may require an excessive amount of time.
n,numericalsolve the res by a numerical recursive algorithm; this is not guaranteed to terminate.
m,numerical_directedsolve the res by a numerical recursive algorithm with directed propagation; this is not guaranteed to terminate.
-iFORMAT , --in=FORMAT
use input format FORMAT:
presPRES 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:
jittyjitty rewriting
jittyccompiled jitty rewriting
jittypjitty rewriting with prover
--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 log messages
-d , --debug
display detailed log messages
--log-level=LEVEL
display log messages up to and including level; either warn, verbose, debug or trace
-h , --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options