pbessolvesymbolic
This is a solving tool for parameterised Boolean equation systems (.pbes extension) that is based on a parity game exploration technique that utilises symbolic representations. The symbolic exploration works very similar to the one implemented by lpsreach, where it is described in great detail. The main difference is that the underlying PBES is first transformed into a standard recursive format (SRF), which is in some sense very similar to a linear process.
Next, we describe useful options that are exclusive to pbessolvesymbolic. One option that can be useful to further refine the dependencies of transition groups is –split-conditions, which introduces new transition groups based on the structure of the SRF pbes and is generally safe.
Similarly to pbessolve the pbessolvesymbolic tool also contains various partial solving strategies that attempt to optimistically solve the intermediate parity games to present the solution (and terminate) early. These can be enabled with the –solve-strategy option.
Limitations
This tool is only available on macOS and Linux since the Sylvan dependency cannot be compiled by Visual Studio.
Usage
pbessolvesymbolic [OPTION]... [INFILE [OUTFILE]]
Description
Solves PBES from INFILE. If INFILE is not present, stdin is used. The PBES is first instantiated into a parity game, which is then solved using Zielonka’s algorithm.
Command line options
--cached
use transition group caching to speed up state space exploration
--chaining
reduce the amount of breadth-first iterations by applying the transition groups consecutively
--evidence-file=NAME
The file to which the evidence is written. If not set, a default name will be chosen.
-fNAME , --file=NAME
The file containing the LPS or LTS that was used to generate the PBES using lps2pbes -c. If this option is set, a counter example or witness for the encoded property will be generated. The extension of the file should be .lps in case of an LPS file, in all other cases it is assumed to be an LTS.
--groups[=GROUPS]
‘none’ (default) no summand groups
‘used’ summands with the same variables are joined ‘simple’ summands with the same read/write variables are joined a user defined list of summand groups separated by semicolons, e.g. ‘0; 1 3 4; 2 5’
--info
print read/write information of the summands
--lace-dqsize[=NUM]
set the length of Lace task queue (default 1024*1024*4)
--lace-stacksize[=NUM]
set the size of Sylvan program stack in gigabytes (0=default stack size). This is the main stack for all calculations. If it is too small a bus error occurs.
--max-iterations[=NUM]
limit number of breadth-first iterations to NUM
-m[NUM] , --memory-limit[=NUM]
Sylvan memory limit in gigabytes (default 3)
--print-exact
prints the sizes of LDDs exactly when within the representable range, and in scientific notation otherwise
--print-nodesize
print the number of LDD nodes in addition to the number of elements represented as ‘elements[nodes]’
-QNUM , --qlimit=NUM
limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited).
--reorder[=ORDER]
‘none’ (default) no variable reordering
‘random’ variables are put in a random order ‘weighted’ variables are put in an order defined by their connectivity weight ‘a user defined permutation e.g. ‘1 3 2 0 4’
--reset
set constant values when introducing parameters
-rNAME , --rewriter=NAME
use rewrite strategy NAME:
jittyjitty rewriting
jittyccompiled jitty rewriting
jittypjitty rewriting with prover
--saturation
reduce the amount of breadth-first iterations by applying the transition groups until fixed point
-sNUM , --solve-strategy=NUM
Use solve strategy NUM. All strategies except 0 periodically apply on-the-fly solving, which may lead to early termination.
0No on-the-fly solving is applied
1Detect solitair winning cycles.
2Detect solitair winning cycles with safe attractors.
3Detect forced winning cycles.
4Detect forced winning cycles with safe attractors.
5Detect fatal attractors.
6Detect fatal attractors with safe attractors.
7Solve subgames using a Zielonka solver.
-c , --split-conditions
split disjunctive conditions to obtain more summands with potentially less dependencies
--threads=NUM
run with NUM threads (default=1). With multiple threads the stack size on a Mac is limited which can lead to bus errors.
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
-t , --total
make the SRF PBES total
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