ltsview

Visualise a labelled transition system (LTS) using a 3D view.

The tool clusters states based on structural properties. These clusters are then visualised to form a backbone of the LTS on which the states and transitions can be drawn. The tool provides functionalities to explore the visualisation (zooming, panning, rotating), mark deadlocks, mark states based on the values of their state vector parameters and mark transitions based on their labels. An image of the visualisation can also be saved in various bitmap formats. The approach is described in detail in [HWW01].

Note

In contrast to ltsgraph this tool is able to handle large state spaces.

References

[HWW01]

F. van Ham, H. van de Wetering and J.J. van Wijk. “Visualization of State Transition Graphs.” In: Proc. IEEE Symp. Information Visualization 2001, IEEE CS Press, pp. 59-66, 2001. (DOI) (PDF)

Manual page for LTSView

Usage

LTSView   [OPTION]... [INFILE]

Description

Start the LTSView application. If INFILE is supplied then the LTS in INFILE is loaded into the application.

The input format is determined by the contents of INFILE. If that fails, an attempt is made to force the input format based on the file extension. The supported formats with file extensions are:

Aldebaran format (CADP; .aut); GraphViz format (.dot); Finite State Machine format (.fsm); mCRL SVC format (.svc); mCRL2 format (*.lts).

Command line options

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

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Bas Ploeger, Carst Tankink, Ruud Koolen