Department of Computing and Information Systems SWEN90004 Modelling Complex Software Systems Some Concurrency Workshop 3 solutions
The exercises
1. Here is an FSP definition of the coin process:
COIN = (heads-> win -> COIN | tails -> lose -> COIN).
2. Here is an FSP description of the squaring process:
MIN 0 MAX 4
SQUARE = (in[i:T] -> out[i*i] -> SQUARE).
3. Here is an FSP description of the water level sensor:
/*
* FSP code for a sensor that monitors a tank volume and checks
* whether the level is low, high, or ok.
*/
// The readings of the level are assumed to be provided by an
// external process; the action reading[v] means a reading of
// ‘v’ is received. There are 7 different levels:
range T = 0..6
SENSOR
= (read[v:T] -> MEASURE[v]),
MEASURE[v:T]
=(when(v<2) low ->SENSOR
| when (v > 4) high -> SENSOR |when(v>1&&v<5)ok ->SENSOR
). 32 E4
const N = 4
range T = 0..N
4. The drinks dispensing machine:
/*
* FSP code for a drinks dispensing machine.
* Assumption: Once there is 15 cents to buy the drink,
* the user cannot add more coins.
*/
DRINKS
= CREDIT[0],
// Inserting money is modelled using an indexed process,
// where the index represents the amount entered so far
CREDIT[i:0..30]
= ( when (i <= 10) insert[5] -> CREDIT[i+5]
| when (i <= 10) insert[10] -> CREDIT[i+10]
| when (i <= 10) insert[20] -> CREDIT[i+20]
// When credit is sufficient, give i-15 in change
// (since the cost is 15 cents):
| when (i >= 15) press_button -> CHANGE[i-15]
),
// 20c change is not possible: the maximal input is 10+20,
// so the maximal change is 15. The index represents the
// amount of change owing:
1310
CHANGE[i:0..15]
= ( when (i > 10)
return[10] -> CHANGE[i-10]
| when (i >= 5 && i < 20) return[5] -> CHANGE[i-5]
|when(i<5) 135 dummy ->END )\{dummy}. KD
5. Moving around on the 4 ⇥ 4 board:
/*
* FSP code for a pebble moving around on an NxN board.
*/
const N = 4
range T = 1..N
P = STATE[1][1], // The pebble starts in row 1, column 1
STATE[row:T][col:T]
= ( when (row > 1) down -> STATE[row-1][col]
| when (row < N) up -> STATE[row+1][col]
| when (col > 1) left -> STATE[row][col-1]
| when (col < N) right -> STATE[row][col+1]
).