Labelled Transition System Analyser
Version 2.2
(1st September 2001)
This new version of the LTSA has the following new features:
-
Extensively revised user interface.
- On the fly safety and progress analysis allowing complete analysis of much larger state spaces.
- Approximate safety analysis using Holtzmann's SuperTrace algorithm for larger state spaces.
-
Support for sequential composition - the FSP additions are described in
a pdf document- included in download.
-
Support for graphic animation using SceneBeans (by Nat Pryce) - see
the draft paper
- No limit on potential statespace (previoursly 2**63)
- Partial Order Reduction during composition and analysis (see ReadMe in Zip)
SceneBeans documentation now at http://www-dse.doc.ic.ac.uk/Software/SceneBeans/
Installation
This version of the LTSA requires the Java 1.3 runtime environment.
To run LTSA V2.2, unzip this file and look at the README file.
Use the help menu to find out about the new features and facilities
The download contains a set of example graphic animations in addition
to the examples from the book. An animation is executed after loading an
FSP script by selecting it from the Check/Run
menu. Unfortunately, documentation for writing animations is as yet sketchy.