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
print the labels of actions
print the average, minimal and maximal branching factor
use FORMAT as the input format
print the labels of states
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
do not display warning messages
display short intermediate messages
display detailed intermediate messages
display intermediate messages up to and including level
display help information
display version information
display help information, including hidden and experimental options