ltscompare

The tool ltscompare compares two transition systems that both must have 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 (option --counter-example). The counter example consist of a Hennessy-Milner formula which is true in the first input LTS and false in the second. Counter-examples are implemented and tested for the bisim, branching-bisim and trace equivalence options.

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 will only be distinguishing for the input transition systems with the hiding operation applied.

orphan:

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. If INFILE1 and/or INFILE2 is ‘-’, stdin is used. Reading two LTSs via stdin is only supported for the ‘aut’ format, these LTSs must be separated by an EOT character (x04).

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 if the input lts’s are not equivalent

--counter-example-file=NAME

the file to which the counterexample should be written

-eNAME) , --equivalence=NAME)

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

none

identity equivalence

bisim

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

bisim-gv

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

bisim-gjkw

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

bisim-gj

strong bisimilarity using the O(m log n) experimental algorithm [Groote/Jansen 2024]

branching-bisim

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

branching-bisim-gv

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

branching-bisim-gjkw

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

branching-bisim-gj

branching bisimilarity using the O(m log n) experimental algorithm [Groote/Jansen 2024]

dpbranching-bisim

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

dpbranching-bisim-gv

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

dpbranching-bisim-gjkw

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

dpbranching-bisim-gj

divergence-preserving branching bisimilarity using the O(m log n) experimental algorithm [Groote/Jansen 2024]

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

coupled-sim

coupled simulation equivalence

-iFORMAT , --in1=FORMAT

use FORMAT as the format for INFILE1 (or stdin)

-jFORMAT , --in2=FORMAT

use FORMAT as the format for INFILE2

-pNAME , --preorder=NAME

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 , --strategy=NAME

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

--tau=ACTNAMES

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

Author

Muck van Weerdenburg