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’’’
- orphan:
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 log messages
-d , --debug
display detailed log messages
--log-level=LEVEL
display log messages up to and including level; either warn, verbose, debug or trace
-h , --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options