xenial (1) ltsconvert.1.gz

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 (no longer supported as input 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 'weak-bisim' weak
              bisimilarity  'weak-bisim-sig'  weak  bisimilarity  using  signature   refinement   'dpweak-bisim'
              divergence preserving weak bisimilarity 'dpweak-bisim-sig' divergence preserving weak 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 © 2014 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>.