The following exercises are from Chapter 2 / Exercises.
2.2 A variable stores values in the range 0..N and supports the actions read and write. Model the variable as a process, VARIABLE, using FSP. For N=2, check that it can perform the actions given by the trace:
write.2 -> read.2 -> read.2 -> write.1 -> write.0 -> read.0
2.3 A bistable digital circuit receives a sequence of trigger inputs and alternately outputs 0 and 1. Model the process BISTABLE using FSP, and check that it produces the required output, i.e. it should perform the actions given by the trace
trigger -> 1 -> trigger -> 0 -> trigger -> 1 -> trigger -> 0 -> ...Note: the alphabet of BISTABLE will be {[0],[1],trigger}
2.5 A drinks dispensing machine charges 15p for a can of Sugarola. The machine accepts coins with denominations 5p, 10p and 20p and gives change. Model the machine as an FSP process, DRINKS. One way to approach this is to define a family of processes which correspond to how much money has been inserted so far for this transaction, and a family of processes which correspond to having received enough money to pay for the drink, and remembering how much money needs to be returned in change. You could call these: CREDIT[i:0..N] and CHANGE[i:0..N]