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



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

-a , --action-label

print the labels of actions

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

-d , --debug

display detailed log messages


display log messages up to and including level; either warn, verbose, debug or trace

-h , --help

display help information


display version information


display help information, including hidden and experimental options


Muck van Weerdenburg