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
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.
pbessymbolicbisim [OPTION]... [INFILE]
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
use a fine initial partition, such that each block contains only one PBES variable
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.
limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).
randomly shuffle blocks between splits
perform the given number of refinement steps between each search for a proof graph
use rewrite strategy NAME:
compiled jitty rewriting
jitty rewriting with prover
set the simplifying strategy for expressions
Use functions from the mCRL2 data library to eliminate redundant inequalities
Only simplify expressions over finite discrete data
Do not simplify expressions
Automatically select the best simplifier
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