lpssymbolicbisim

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.

Limitations

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.

Manual page for lpssymbolicbisim

Usage

lpssymbolicbisim   [OPTION]... [INFILE [OUTFILE]]

Description

Performs partition refinement on INFILE and outputs the resulting LTS. This tool is highly experimental.

Command line options

-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

Standard options

-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

Author

Thomas Neele