This tool is aimed at generating the reachable part of the bisimulation quotient of systems with an infinite state space. Classical state-space enumeration, such as implemented in lps2lts, relies on enumeration and stores each state explicitly. To avoid this, lpssymbolicbisim applies symbolic techniques to represent infinite sets.
To run this tool, the Z3 SMT-solver should be installed and its bin-directory has to be added to the PATH variable.
The tool can only deal with specifications of limited complexity. Furthermore, there are several other restrictions:
In any case, pbessymbolicbisim is probably more powerful, since its abstractions can also rely on the information of the property being checked and it does not have to deal with actions and their parameters.
lpssymbolicbisim [OPTION]... [INFILE [OUTFILE]]
Performs partition refinement on INFILE and outputs the resulting LTS. This tool is highly experimental.
-QNUM
, --qlimit=NUM
limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).
-rNAME
, --rewriter=NAME
use rewrite strategy NAME:
jitty
jitty rewriting
jittyc
compiled jitty rewriting
jittyp
jitty rewriting with prover
-sMODE
, --simplifier=MODE
set the simplifying strategy for expressions
fm
Use functions from the mCRL2 data library to eliminate redundant inequalities
finite
Only simplify expressions over finite discrete data
identity
Do not simplify expressions
auto
Automatically select the best simplifier
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
-q
, --quiet
do not display warning messages
-v
, --verbose
display short intermediate messages
-d
, --debug
display detailed intermediate messages
--log-level=LEVEL
display intermediate messages up to and including level
-h
, --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options
Thomas Neele