lpsbisim2pbes
Construct a PBES that expresses whether the two LPSs given as input are equal modulo some behavioural equivalence relation specified with option -b/–bisimulation. The two LPSs used to construct the PBES are equivalent if and only if the solution to the PBES is true.
A precise definition of the construction of the PBES can be found in [CBPW07].
T. Chen, B. Ploeger, J. van de Pol, and T. A. C. Willemse: Equivalence Checking for Infinite Systems using Parameterized Boolean Equation Systems, in CONCUR 2007, vol. 4703 of LNCS, pp. 120–135.
- orphan:
Usage
lpsbisim2pbes [OPTION]... INFILE1 [INFILE2 [OUTFILE]]
Description
Reads two files containing an LPS, and computes a PBES that expresses bisimulation between the two. If OUTFILE is not present, standard output is used.
Command line options
-bNAME , --bisimulation=NAME
generate a PBES for the bisimulation type NAME:
strong-bisimstrong bisimulation
weak-bisimweak bisimulation
branching-bisimbranching bisimulation
branching-simbranching simulation equivalence
-n , --normalize
normalize the result
-oFORMAT , --out=FORMAT
use output format FORMAT:
besBES in internal format
pbesPBES in internal format
pgsolverBES in PGSolver format
textPBES in textual (mCRL2) format
--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 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