ltscompare

The tool ltscompare compares two transition systems that both must have the either the extension .aut, .lts or .fsm. The transition systems should not be probabilistic.

The transition systems can either be compared using an equivalence relation (option --equivalence) or a preorder (option --preorder). The list of available equivalences is provided below.

There are two useful options. One allows to generate counter examples in the form of a trace (option --counter-example). These counter examples are useful for trace based equivalences. They can also be generated for some variants of bisimulation, but in this case they can also point to states where the two transition systems are nondeterministic.

The second useful option is to hide some actions while doing the comparisons (option --tau= followed by a comma separated list of actions). Counter examples are provided without applying hiding.

Manual page for ltscompare

Usage

ltscompare   [OPTION]... [INFILE1] INFILE2

Description

Determine whether or not the labelled transition systems (LTSs) in INFILE1 and INFILE2 are related by some equivalence or preorder. If INFILE1 is not supplied, stdin is used.

The input formats are determined by the contents of INFILE1 and INFILE2. Options –in1 and –in2 can be used to force the input format of INFILE1 and INFILE2, respectively. The supported formats are:
‘aut’ for the Aldebaran format (CADP), ‘dot’ for the GraphViz format (no longer supported as input format), ‘fsm’ for the Finite State Machine format, or ‘lts’ for the mCRL2 LTS format

Command line options

-c , --counter-example

generate counter example traces if the input lts’s are not equivalent

-eNAME) , --equivalenceNAME)

use equivalence NAME (not allowed in combination with -p/–preorder):

none

identity equivalence

bisim

strong bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017]

bisim-gv

strong bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]

bisim-dnj

strong bisimilarity using the O(m log n) algorithm directly on an LTS. This option is experimental.

branching-bisim

branching bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017]

branching-bisim-gv

branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]

branching-bisim-dnj

branching bisimilarity using the O(m log n) algorithm directly on an LTS. This option is experimental.

dpbranching-bisim

divergence-preserving branching bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017]

dpbranching-bisim-gv

divergence-preserving branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]

dpbranching-bisim-dnj

divergence-preserving branching bisimilarity using the O(m log n) algorithm directly on an LTS. This option is experimental.

weak-bisim

weak bisimilarity

dpweak-bisim

divergence-preserving weak bisimilarity

sim

strong simulation equivalence

ready-sim

strong ready simulation equivalence

trace

strong trace equivalence

weak-trace

weak trace equivalence

-iFORMAT , --in1FORMAT

use FORMAT as the format for INFILE1 (or stdin)

-jFORMAT , --in2FORMAT

use FORMAT as the format for INFILE2

-pNAME , --preorderNAME

use preorder NAME (not allowed in combination with -e/–equivalence):

unknown

default void preorder

sim

strong simulation preorder

ready-sim

strong ready simulation preorder

trace

strong trace preorder

weak-trace

weak trace preorder

trace-ac

trace preorder based on an anti chain algorithm

weak-trace-ac

weak trace preorder based on an anti chain algorithm

failures

failures refinement

weak-failures

weak failures refinement

failures-divergence

failures divergence refinement (automatically weak)

-sNAME , --strategyNAME

explore the state space using strategy NAME (only for antichain based algorithms; includes all failures refinements) :

b, breadth

breadth-first search

d, depth

depth-first search

--tauACTNAMES

consider actions with a name in the comma separated list ACTNAMES to be internal (tau) actions in addition to those defined as such by the input

--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-levelLEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Muck van Weerdenburg