Tools

LTSA-Delforge

LTSA-Delforge is an extension of LTSA adding extensive LTS layout capabilities. It offers different layout algorithms, the possibility to manually edit the graph, navigate from state to state and more. LTSA-Delforge was developed by Cédric Delforge for his Master's thesis.

LTSA is a verification tool for concurrent systems developed at Imperial College London. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. System components are described in a process algebra notation (FSP) and compiled into finite Labelled Transition Systems (LTS), on which compositional reachability analysis can be performed. LTSA is available from the LTSA home page.

LTSA-Delforge features a new "Layout" window for displaying LTS, with the following capabilities:

Apply different graph layout algorithms (force-based, circular, tree-based) to all or part of the graph.
View multiple graphs at once.
Visualize and select strongly connected components.
Manually select and arrange states.
Navigate transitions forward and backward, find reachable/reaching states.
Visually simulate an LTS by clicking next states.
View current states during LTSA animations.
Export graph in PDF, SVG, PNG formats.

LTSA-Delforge is based on LTSA 3.0 and uses JUNG, an open-source Java library for modelling, analyzing and visualizing graphs.

LTSA-Delforge is provided as a ZIP archive containing the program (a clickable JAR file) and a user manual.

Download LTSA-Delforge