User manual/ltsconvert

From MCRL2

< User manual(Redirected from User manual/Ltsconvert)

Jump to: navigation, search

User manual

Tool manual pages

Contents

Convert and optionally minimise an LTS.

1 Synopsis
2 Short description
3 Options
4 See also
5 Author
6 Bug reporting

Synopsis

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

Short description

The ltsconvert tool converts the labelled transition system (LTS) in INFILE to OUTFILE in the requested format after applying the selected minimisation method to INFILE (default is no minimisation). 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)
bcg: for the Binary Coded Graph format (CADP) (if BCG support is enabled)
dot: for the GraphViz format
fsm: for the Finite State Machine format
mcrl: for the mCRL SVC format
mcrl2: for the mCRL2 format (default)
svc: for the (generic) SVC format

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

Note that 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).

Options

OPTION can be any of the following:

-a, --add: do not minimise but save a copy of the original LTS extended with a state parameter indicating the bisimulation class a state belongs to; this means that every state is extended with a number in such a way that (only) equivalent states have the same number (this option only works for mCRL2 LTSs)

-D, --determinise: determinise the LTS

-eNAME, --equivalence=NAME

generate an equivalent LTS, preserving equivalence NAME:

bisim: minimise modulo strong bisimilarity
branching-bisim: minimise modulo branching bisimilarity
sim: minimise modulo strong simulation equivalence
trace: determinise and then minimise modulo trace equivalence
weak-trace: determinise and then minimise modulo weak trace equivalence

-iFORMAT, --in=FORMAT: use FORMAT format as the input format

-lFILE, --lps=FILE: use FILE as the LPS from which the input LTS was generated; this is needed to store the correct parameter names of states when saving in fsm format and to convert non-mCRL2 LTSs to a mCRL2 LTS

-n, --no-state: leave out state information when saving in dot format

--no-reach: do not perform reachability check on the input LTS

--none: do not minimise the LTS (this is the default)

-oFORMAT, --out=FORMAT: use FORMAT format as the output format

--tau=ACTNAMES: consider actions with a name in the comma separated list ACTNAMES to be a internal (tau) actions in addition to those defined as such by the input; this means that before minimisation all specified actions are first replaced by tau actions; in the case --add is used, these tau actions will only used internally to compute the equivalence classes; the output will have the original actions

Standard options: