Plan
School of Computing and Information Systems
SWEN90004 Modelling Complex Software Systems
Concurrency Workshop 3, Week 4, Semester 1, 2021
Introduction to LTSA
This workshop aims to give you an introduction to FSP and to using LTSA.
LTSA is installed on the lab machines; if you prefer to use your own laptop, it can be downloaded from http://www.doc.ic.ac.uk/~jnm/book/ltsa/download.html (you should also download the
additional animation modules from that page).
The exercises
1. Start up LTSA. In the Edit tab, design an FSP model that describes the process in the figure below, which describes flipping a coin and calling.
To generate the labelled transition system (LTS) that corresponds to your FSP model, select Build ! Compile, then go to the Draw tab, and select your model from the left pane.
2. Give an FSP description of a program that accepts as input an integer in the range 1..4, and outputs the square of that integer.
You can animate your model using Check ! Run ! DEFAULT.
3. A sensor measures the water level of a tank. The level is measured in units 0..6. The sensor reads the level and outputs a ‘low’ signal if the level is less than 2 and a ‘high’ signal if the level is greater than 4; otherwise it outputs ‘ok’. Model the sensor as an FSP process SENSOR.
4. A drinks dispensing machine charges 15c for a can of soft drink. The machine accepts coins with denominations 5c, 10c and 20c and gives change. Model the machine as an FSP process DRINKS. List any assumptions that you make in your model.
Challenge Task
If you get this far and want to be challenged further, try the following task.
5. Define an FSP process P with alphabet {up,down,left,right}, which represents the move-
ment of a pebble on an N⇥N board, such as the one shown below.
•
Is it possible to define a similar FSP process for an infinitely-sized board?