NAME

       ltsconvert - convert and optionally minimise an LTS

SYNOPSIS

       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,
         'fsm' for the Finite State Machine format, or
         'lts' for the mCRL2 LTS format (default)

OPTIONS

       OPTION can be any of the following:

       -D, --determinise
              determinise LTS

       -eNAME, --equivalence=NAME
              generate   an   equivalent   LTS,  preserving  equivalence  NAME:  'none'  identity
              equivalence (default) 'bisim' strong bisimilarity 'bisim-sig'  strong  bisimilarity
              using  signature  refinement  'branching-bisim'  branching bisimilarity 'branching-
              bisim-sig' branching bisimilarity using  signature  refinement  'dpbranching-bisim'
              divergence  preserving  branching  bisimilarity  'dpbranching-bisim-sig' divergence
              preserving  branching  bisimilarity  using  signature   refinement   'sim'   strong
              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
              leave out state information when saving in dot format

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

AUTHOR

       Written by Muck van Weerdenburg, Jan Friso Groote.

REPORTING BUGS

       Report bugs at <http://www.mcrl2.org/issuetracker>.

COPYRIGHT

       Copyright © 2012 Technische Universiteit Eindhoven.
       This is free software.  You may redistribute copies of it under the  terms  of  the  Boost
       Software  License  <http://www.boost.org/LICENSE_1_0.txt>.   There  is NO WARRANTY, to the
       extent permitted by law.

SEE ALSO

       See also the manual at <http://www.mcrl2.org/release/user_manual/tools/ltsconvert.html>.

ltsconvert mCRL2 toolset 201210.1 (ReleaseNovember 2012                             LTSCONVERT(1)