xenial (1) ltscompare.1.gz

Provided by: mcrl2_201409.0-1ubuntu1_amd64 bug

NAME
       ltscompare - compare two LTSs


SYNOPSIS
       ltscompare [OPTION]... [INFILE1] INFILE2


DESCRIPTION
       Determine  whether  or  not  the labelled transition systems (LTSs) in INFILE1 and INFILE2 are related by
       some equivalence or preorder. If INFILE1 is not supplied, stdin is used.

       The input formats are determined by the contents of INFILE1 and INFILE2.  Options --in1 and --in2 can  be
       used to force the input format of INFILE1 and INFILE2, respectively. 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


OPTIONS
       OPTION can be any of the following:

       -c, --counter-example
              generate counter example traces if the input lts's are not equivalent

       -eNAME), --equivalence=NAME)
              use  equivalence NAME (not allowed in combination with -p/--preorder): 'none' identity equivalence
              (default) 'bisim' strong bisimilarity 'branching-bisim' branching bisimilarity 'dpbranching-bisim'
              divergence   preserving  branching  bisimilarity  'weak-bisim'  weak  bisimilarity  'dpweak-bisim'
              divergence preserving weak bisimilarity 'sim' strong simulation equivalence 'trace'  strong  trace
              equivalence 'weak-trace' weak trace equivalence

       -iFORMAT, --in1=FORMAT
              use FORMAT as the format for INFILE1 (or stdin)

       -jFORMAT, --in2=FORMAT
              use FORMAT as the format for INFILE2

       -pNAME, --preorder=NAME
              use  preorder  NAME (not allowed in combination with -e/--equivalence): 'unknown' unknown preorder
              (default) 'sim' strong simulation preorder 'trace' strong trace preorder 'weak-trace'  weak  trace
              preorder

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


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


       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/ltscompare.html>.