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.

The graph can be rotated by dragging with the right mouse button or dragging with the left mouse button while holding the shift key. Zooming in and out is possible by using the mouse wheel or by dragging the mouse up/down while holding the middle mouse button. The graph can be moved around by holding the “Control” button and dragging with the mouse.

ltsview supports simulation of the system in a way similar to lpsxsim. Simulation can be started from the initial state by clicking “Start” in the simulation window (which can be turned on/off in the “View” menu). By double clicking one of the next states in the simulation window, the simulation progresses to that state.

A useful feature of ltsview is the possibility to find a trace to a state. First, make sure that no simulation is currently running. Turn on the “Display states” option from the “View” menu and select a state by clicking on it. Now start a simulation and click the button “Backtrace”. A trace from the initial state to the selected state will now be shown in the graph. The “Undo” button allows you to step through that trace backwards.

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)

orphan:


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

Author

Bas Ploeger, Carst Tankink, Ruud Koolen