Print basic information on a labelled transition system. The input format of a labelled transition system can either be .aut, .lts or .fsm. The following information about the LTS is shown:

  • number of states.
  • number of different action labels.
  • number of transitions.
  • whether and how many state labels there are.
  • whether the transition system has probabilistic states.

Furthermore, it is reported whether all states are reachable and wheter the lts is deterministic.

For a .lts the sets of state labels can be printed using the option ‘’‘-l’‘’

Manual page for ltsinfo


ltsinfo   [OPTION]... [INFILE]


Print information about the labelled transition system (LTS) in INFILE. If INFILE is not supplied, stdin is used.

The format of INFILE is determined by its contents. The option –in can be used to force the format for INFILE. 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

Command line options

-b , --branching-factor

print the average, minimal and maximal branching factor


use FORMAT as the input format

-l , --state-label

print the labels of states


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


display intermediate messages up to and including level

-h , --help

display help information


display version information


Muck van Weerdenburg