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
As these sets of state labels can be large, the flag
of ltsconvert can be used to remove these state labels in the resulting
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).
ltsconvert [OPTION]... [INFILE [OUTFILE]]
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
generate an equivalent LTS, preserving equivalence NAME:
strong bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
strong bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]
strong bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
strong bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]
branching bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]
branching bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]
divergence-preserving branching bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
divergence-preserving branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]
divergence-preserving branching bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
divergence-preserving branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]
divergence-preserving weak bisimilarity
strong simulation equivalence
strong ready simulation equivalence
strong trace equivalence
weak trace equivalence
tau star reduction
use FORMAT as the input format.
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.
do not perform a reachability check on the input LTS.
remove the state information. This can be useful when state labels are huge.
use FORMAT as the output format.
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.
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
do not display warning messages
display short intermediate messages
display detailed intermediate messages
display intermediate messages up to and including level
display help information
display version information
display help information, including hidden and experimental options