LTS-Analyser - a simple useful tool for analysing labelled transition systems

This tool was developed in the UK for providing practical support for modeling concurrent system and is used for the examples in the book "Concurrency: State Models and Java Programs".

There exist the original version, very simple (which I use in class), which comes as a Java application (or can be downloaded here). A new version has been integrated into the Eclipse platform and has basically the same functionality (download here). Both version contain all the examples from the book. The Eclipse version has also some documentation: a help-guide which contains as Appendix A a useful Quick Reference Guide. In this course SEG-2106, we only use a few features of the LTS tool, and you will be able to understand most by just looking at the examples given in the course notes.

All LTSA examples used in the SEG-2106 course can be found here.

Mini-Introduction to the syntax of LTSA model descriptions

We use the example of the hotel system (version 1) to explain the basic features of LTSA. Here is the text of this example:

// state machine of the client: it has only one state, all client actions are possible any time.
CLIENT = (checkIn -> CLIENT | checkOut -> CLIENT |
eat -> CLIENT | payCash -> CLIENT | chargeRoom -> CLIENT).

// state machine of a restaurant. The alphabet of this LTS is {eat, payCash, chargeRoom}
RESTAURANT = (eat -> DONE),
DONE = (payCash -> RESTAURANT | chargeRoom -> RESTAURANT).

// state machine of a room. The alphabet of this LTS is {checkIn, checkOut, chargeRoom}
ROOM = (checkIn -> OCCUPIED),
OCCUPIED = (checkOut -> ROOM | chargeRoom -> OCCUPIED).

ROOM2 = (checkIn -> checkOut -> ROOM2).

// The system consists of one client, one restaurant and one room
||SYSTEM = (CLIENT || RESTAURANT || ROOM).
// List of interactions in this system:
// (a) Rendezvous involving the CLIENT and the RESTAURANT: eat, payCash
// (b) Rendezvous involving the CLIENT and the ROOM: checkIn, checkOut
// (c) Rendezvous involving all three objects: chargeRoom

As the last line indicates, the system consists of three state machines that work concurrently. Working concurrently, means that transitions of different state machines that have the same name can only be execute jointly, that is, in rendezvous. There is a fourth state machine definition, called ROOM2, but it is not really used.

The first two lines define the state machine CLIENT. CLIENT is the name of the state machine and also the name of its initial state. All state names are written in upper case characters. The CLIENT machine has only one state. The words in lower case characters are transition names. The first line indicates that from the CLIENT state, the machine can make a checkIn transition which leads to the next state CLIENT, or a check-out transition that leads to the same state. Etc. The definition of state machine is terminated by a dot "."

The RESTAURANT state machine has two states, the initial state RESTAURANT and another state called DONE.The first line of its definition indicates that from the initial state, there is only one transition named eat. The second line defines the transitions available from the state DONE. Note that all transitions from a given state are put in paranthesis, followed by a comma "," if this is not the last state of the machine definition.

Note that some of the states of a state machine may not be explicitely mentioned (they have no name). For instance, the definition of the ROOM2 state machine has two states: ROOM2 and the state reached after the transition checkIn. This second state is in-between the transitions checkIn and the following checkOut. After checkOut, the machine is again in its initial state ROOM2.

Note: It is important to note for each state machine the set of transition names, which is called the "alphabet" of the machine. It is the set of interactions in which it participates. If there is an intersection between the alphabets of two (or more) machines, then the transitions with these names can only be executed in rendezvous. A transition with a name that is unique to the given machine, is executed independently of the other machines within the system. For instance, the transition eat is performed by RESTAURANT independently of other machines, check-in is performed by CLIENT and ROOM in rendezvous, and chargeRoom is executed in rendezvous by all three machines (and it can only occur if all three machines are in a respective state where this transition is allowed).

Mini-Introduction to the commands of the LTSA tool

The LTSA tool has the drop-down menues File, Edit, Check, Build, Window, Help and Options. Below are three buttons: Edit, Output, and Draw. A typical steps of using the tool are the following:

1. Use the editing functions to create a model definition.
2. Use the commands Build -> Parse and Build -> Compile to create in internal representation of the model for further processing.
3. View the graphic representation of the state machines included in your model by clicking on Draw and then clicking on the name of the state machine you what to visualize. Note that the graphical representation does not include the state names of your model (since these names have no semantic meaning, that is, they can be changed without changing the meaning of the model)
4. In the textual field "Target Composition" of the tool, select the composition that you would like to simulate. Note, the hotel model contains only one composition, the one that is called SYSTEM. The syntax for the definition of a composition is a composition name preceeded by "||" and at the right side the names of the state machines (separated by "||" ) that should be executed concurrently. In the case of the hotel example, the SYSTEM is already selected by the tool.
5. Execute the command Build -> Compose, which builds a global model of these state machines running concurrently with rendezvous interactions.
6. View the graphic representation of the composition.
7. Use the command Check-> Run to perform a interactive simulation of the composed system. During the execution, you may look at the graphical representation of each machine, or the global system. A stats in red is the current states of the machine.
8. Use the command Check -> Safety to check whether there is the possibility that the composed system may enter a blocking state (a state without any transition), called a deadlock.

Verification options in LTSA

• Deadlock: LTSA checks whether a composed system as a deadlock. A state in a single component that has no transition is considered an Error state. A state with name END is considered the normal end state of a behavior.
• Test sequences: One can define a sequence of interactions and compose this sequence with the system specification. If there is a deadlock, the test sequence cannot be performed by the specified system.
  • Attention: The sequence may have a smaller alphabet than the system. In this case, interactions not in the sequence alphabet may be interspersed in the sequence at any point.
  • Examples are given in the Hotel V3 example.
• Safeness properties: Using the keyword property, one may define a behavior and compose it with the system. This composition checks that all possible execution sequences of the system (when projected onto the alphabet of the property behavior) are allowed sequences according to the property. Note: The property is usually a more abstract view of the system behavior, for instance the service specification of a protocol system.
  • Examples are given in the Hotel V3 example.