pbessymbolicbisim
This tool is aimed at solving parameterised Boolean equation systems with an infinite underlying Boolean equation system. Most other tools, such as pbessolve and pbesinst, rely on enumeration of the data domain to generate the corresponding BES. To avoid this, pbessymbolicbisim applies symbolic techniques to represent infinite sets.
For intermediate simplification of the symbolic representation, the tool relies
on one of several simplifying strategies, which can be selected with the option
-s/–simplifier. The fm simplifier is based on the Fourier-Motzkin
algorithm and only works on linear inequalities.
To track the progress of the tool, one can use the option –log-level=status. The option –fine-initial causes the algorithm to start off with a finer partition. In general, this will lead to a longer runtimes. However, in certain cases, it drastically speeds up the algorithm.
The option –no-early-termination/-t in some cases also speeds up the algorithm. When this option is supplied, no early termination checks are done at the start of every iteration. This can lead to a speed up of at most a factor two. However, the resulting proof graph may be much larger, negating the speed-up.
If the tool spends a lot of time on parity game generation, it might help to set the option –refine-steps/-n to 2 or 3. It saves some overhead by generating a parity game less often, but it may easily lead to a larger proof graph.
To run this tool, the Z3 SMT-solver should be installed and its bin-directory has to be added to the PATH variable.
- orphan:
Usage
pbessymbolicbisim [OPTION]... [INFILE]
Description
Computes the solution to the given PBES using symbolic bismulation techniques. Mostly useful for PBESs of low complexity with an infinite underlying BES. This tool is experimental.
Command line options
--fine-initial
use a fine initial partition, such that each block contains only one PBES variable
-t , --no-early-termination
do not use knowledge of simulation relations to perform early termination detection. Using this option might lead to a larger proof graph, although the runtime might become lower since the overhead of early termination checking is avoided.
-QNUM , --qlimit=NUM
limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited).
--randomize
randomly shuffle blocks between splits
-nNUM , --refine-steps=NUM
perform the given number of refinement steps between each search for a proof graph
-rNAME , --rewriter=NAME
use rewrite strategy NAME:
jittyjitty rewriting
jittyccompiled jitty rewriting
jittypjitty rewriting with prover
-sMODE , --simplifier=MODE
set the simplifying strategy for expressions
fmUse functions from the mCRL2 data library to eliminate redundant inequalities
finiteOnly simplify expressions over finite discrete data
identityDo not simplify expressions
autoAutomatically select the best simplifier
--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