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 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.
ltscompare [OPTION]... [INFILE1] INFILE2
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).
-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]
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]
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]
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
-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
Muck van Weerdenburg