ltsinfo

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

Usage

ltsinfo   [OPTION]... [INFILE]

Description

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

-iFORMAT , --in=FORMAT

use FORMAT as the input format

-l , --state-label

print the labels of states

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

--help-all

display help information, including hidden and experimental options

Author

Muck van Weerdenburg