### Solutions

```Assignment 4 - FSP
1.
A variable store values in the range 0..N and supports the
actions read and write. Model the variable as a process,
VARIABLE, using FSP. The process’s LTS graph for N=2 is
shown below. Your FSP model must produce an identical
graph.
Assignment 4 - FSP
1.
Solution.
const N = ...
range R = 0..N
VARIABLE = VAR,
VAR[i:R] = (read[i] -> VAR[i]
|write[v:R] -> VAR[v] ).
Assignment 4 - FSP
2. A drinks dispensing machine charges 15p for a can of
Sugarola. The machine accepts coins with denominations
5p, 10p and 20p and gives change. Using the alphabet
{can, in.coin, in.coin, in.coin,
out.coin, out.coin } model the machine as
an FSP process, DRINKS. A sample trace is shown below.
Assignment 4 - FSP
2. Solution.
DRINKS = CREDIT,
CREDIT
= (in.coin -> CREDIT
|in.coin -> CREDIT
|in.coin -> CHANGE),
CREDIT
= (in.coin -> CREDIT
|in.coin -> CHANGE
|in.coin -> CHANGE),
CREDIT = (in.coin -> CHANGE
|in.coin -> CHANGE
|in.coin -> CHANGE),
CHANGE
= (can -> DRINKS),
CHANGE
= (can -> out.coin
-> DRINKS),
CHANGE = (can -> out.coin -> DRINKS),
CHANGE = (can -> out.coin
-> out.coin -> DRINKS).
Assignment 4 - FSP
3. Consider the following scenario.
There are n bees and a hungry bear. They share a pot of
honey. The pot is initially empty; its capacity is H
portions of honey. The bear waits until the pot is full,
eats all the honey and waits until the pot is full again:
this pattern repeats forever. Each bee repeatedly
gathers one portion of honey and puts it into the pot; if
the pot is full when a bee arrives it must wait until the
bear has eaten the honey before adding its portion: this
pattern repeats forever.
Model this scenario using FSP. The LTS graph for 4 bees is
shown below. Your FSP model must produce an identical
graph.
3. continued.
Assignment 4 - FSP
3. Solution.
Assignment 4 - FSP
const H=4
const N=3
BEE = (addhoney -> BEE).
BEAR = (eat -> BEAR).
POT = POT,
POT[i:0..H] = (when (i<H) [j:0..N].addhoney -> POT[i+1]
|when (i==H) eat -> POT).
||HONEYBEAR = ([i:0..N]:BEE || BEAR || POT).
Assignment 4 - FSP
3. A, S and J work in a bar. A washes the dirty glasses one
at a time and places each on a workspace. The workspace
can hold a maximum of 10 glasses. S and J remove the
glasses from the workspace one at a time and dry them.
[You can ignore what happens to a glass after it is dried.]
Unfortunately, there is only one drying cloth so S and J
have to take turns at using it. However, as J is able to
dry faster he dries two glasses at each turn while S only
dries one. S takes the first turn at drying.
Model the concurrent activity in the bar by completing the
following FSP template.
Assignment 4 - FSP
3. continued.
S = (sdry -> S).
J = (jdry -> jdry -> J).
A = (wash -> A).
// gw is the number of glasses washed.
// j is the number of glasses washed by J in this turn.
// turn indicates whose turn it is to wash.
WORKSPACE(N=5) = WS,
WS[gw:0..N][j:0..1][turn:0..1] = (..).
||BAR = (S || J || A || WORKSPACE(10)).
Assignment 4 - FSP
3. continued. A sample trace is shown below.
Assignment 4 - FSP
3. Solution.
S = (sdry -> S).
J = (jdry -> jdry -> J).
A = (wash -> A).
WORKSPACE(N=5) = WS,
WS[gw:0..N][j:0..1][turn:0..1] =
(gw[gw]-> WS[gw][j][turn]
|when (gw<N) wash -> WS[gw+1][j][turn]
|when (gw>0 && turn==0) sdry ->
WS[gw-1]
|when (gw>0 && j==0 && turn==1) jdry ->
WS[gw-1][turn]
|when (gw>0 && j==1 && turn==1) jdry ->
WS[gw-1]).
||BAR = (S || J || A || WORKSPACE(20)).
```