User manual/ltsgraph

From MCRL2

< User manual(Redirected from User manual/Ltsgraph)

Jump to: navigation, search

User manual

Tool manual pages

Contents

Visualise an LTS as a graph and manipulate its layout.

1 Synopsis
2 Short description
3 Options
4 Detailed description
- 4.1 Theory
- 4.2 Functionality
5 References
6 Author
7 Bug reporting

Synopsis

ltsgraph [OPTION]... [INFILE]

Short description

The ltsgraph tool draws the graph described by INFILE using a graphical user interface. If INFILE is not supplied the tool starts without a drawing. INFILE can have any one of the following extensions:

.aut: Aldebaran format (CADP)
.bcg: Binary Coded Graph format (CADP)
.dot: GraphViz format
.fsm: Finite State Machine format
.lts: mCRL2 format
.xml: ltsgraph layout format
.svc: mCRL or (generic) format

The main window of the tool shows the labelled transition system described by the input file as a directed, labelled graph. Using the dialogs found in the "Tools" menu, the graph's layout and several other visualization settings can be manipulated. The layout of the graph can also be manipulated by dragging vertices (states).

Options

OPTION can be any of the following standard options:

-q, --quiet: do not display warning messages

-v, --verbose: display short intermediate messages

-d, --debug: display detailed intermediate messages

-h, --help: display help information

--version: display version information

Detailed description

Theory

The ltsgraph tool uses a basic force directed layout method to position the vertices in a 2 dimensional space. In general such layout methods use a force system based on vertices and edges. The goal is to find an equilibrium state, where the sum of forces is 0. The method used by ltsgraph uses springs and electrical forces. vertices are modelled as electrically charged particles that repel each other more when they come closer together. Edges are modelled as springs that generate a force on both connected vertices depending on the zero-energy length of the spring. The spring exerts an repelling force when smaller than zero-energy length and a attractive force otherwise.

Write $x u, y u$ for the x-coordinate respectively the y-coordinate of a vertex u. Let u and v be atbitrary vertices and d(u,v) be a distance measure (usually Euclidean distance). The x-component of the electrical (repelling) force that a vertex u exerts on vertex v is defined as follows:

$F^{electric}_{x}(u,v) = \frac{e_{u,v}}{d(u,v)^{2}} * \frac{x_{v} - x_{u}}{d(u,v)}$

Where $e u, v$ represents the strength of the electrical repulsion between u and v. Let u and v be vertices such that $(u,v) \in E$ . The x-component of the force exerted by the spring on v is:

$F^{spring}_{x}(u,v) = s_{u,v} * log(\frac{d(v,u)}{l_{u,v}}) * \frac{x_{v} - x_{u}}{d(v,u)}$

Where $s u, v$ is the stiffness of the spring and $l u, v$ is the zero-energy length of the spring between points u and v. The observant reader may point out that the last definition does not follow Hook's law that describes how a spring works in the physical world. Instead we used the alternate spring model more suitable for the purpose of computing graph layouts <ref name=[Eades84]>P.A. Eades, “A heuristic for graph drawing”, Congressus Nutnerantiunt, vol. 42, pages 149–160, 1984</ref>.

An algorithm is needed to simulate these forces and apply them to generate new graph layouts. The input to the algorithm is a graph $(V, E)$ and an arbitrary existing layout for a graph. The algorithm computes the sum of electric forces:

$F^{total}_{x}(v) = \sum_{u \in V}F^{electric}_{x}(u,v) + \sum_{(u,v) \in E}F^{spring}_{x}(u,v)$

The new position of a vertex v is then computed from the old coordinates by applying the total force:

$(v_{x} + F^{total}_{x}(v), v_{y} + F^{total}_{y}(v))$

A single run of the algorithm computes a new set of coordinates for all vertices: the new layout. Repeating this process until the sum of all forces is zero gives an optimal layout.

The ltsgraph tool offers three parameters e, s and l that can be used to interactively guide the positioning algorithm. There is a simple link between these three parameters and the force models described above. For all $e = e u, v, s = s u, v, l = l u, v$ for all u and v.

Functionality

The ltsgraph tool generates two dimensional graph layouts for transition systems and has some edit functionality. Apart from basic drawing, provides the following additional functionalities:

States can be dragged and dropped by the left click.
States colour can be changed by using the settings menu.
Graph layout can be optimized using the force-based algorithm described above, available from the tools menu.
States can be locked by the right click. Locked states can still be dragged and dropped but the layout algorithm will not move such nodes.
Transitions can be curved by clicking the corresponding checkbox in the settings dialog and dragging the diamond-shaped control points.
A layout can be exported to LaTeX and SVG formats, as well as an XML format describing the layout and settings of the graph. This XML format can later be imported into the tool.