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:
The tool cannot deal very well with actions that have data parameters. Actions with Boolean parameters will not lead to a large slowdown, but for larger domains, scalability will be an issue.
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.
Command line options
limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).
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