ltsconvert

Convert labelled transition systems (LTSs) from and to different formats. Optionally, a minimisation method can be selected that is applied on the input.

In order to convert a non-mCRL2 LTS to a mCRL2 LTS one needs to supply the original LPS with –lps. This is because actions need to be stored in the internal mCRL2 format in mCRL2 and in non-mCRL2 LTSs are represented by strings (lacking essential information such as data types).

When applied to an .lts file, and if the ltsconvert tool applies reductions, it groups the state labels of all states that are equivalent into one set of state labels for a number of reductions. The reduced state in the new state space is labelled with this set. The state labels can be inspected using the tool ltsinfo with the flag -l, or --state-label. As these sets of state labels can be large, the flag -n, or --no-state of ltsconvert can be used to remove these state labels in the resulting state space.

Note

Tools that use the fsm format may depend on state information and parameter names. This requires that this information is available in the input LTS file or that the –lps option is used (see the options sections below).

orphan:

Usage

ltsconvert   [OPTION]... [INFILE [OUTFILE]]

Description

Convert the labelled transition system (LTS) from INFILE to OUTFILE in the requested format after applying the selected minimisation method (default is none). If OUTFILE is not supplied, stdout is used. If INFILE is not supplied, stdin is used.

The output format is determined by the extension of OUTFILE, whereas the input format is determined by the content of INFILE. Options –in and –out can be used to force the input and output formats. 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 (default)

Command line options

-D , --determinise

determinise LTS

-eNAME , --equivalence=NAME

generate an equivalent LTS, preserving equivalence NAME:

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]

bisim-sig

strong bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]

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]

branching-bisim-sig

branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]

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]

dpbranching-bisim-sig

divergence-preserving branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]

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

tau-star

tau star reduction

-iFORMAT , --in=FORMAT

use FORMAT as the input format.

-lFILE , --lps=FILE

use FILE as the LPS from which the input LTS was generated; this might be needed to store the correct parameter names of states when saving in fsm format and to convert non-mCRL2 LTSs to a mCRL2 LTS.

--no-reach

do not perform a reachability check on the input LTS.

-n , --no-state

remove the state information. This can be useful when state labels are huge.

-oFORMAT , --out=FORMAT

use FORMAT as the output format.

--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, Jan Friso Groote