Adapted from one of CAR Hoare's master classes.
Work through the examples of the use of the CSP meta-language from lectures, then attempt the following exercises.
1.1. Bank Accounts
Each customer of a bank first opens an account. He or she then makes any number of deposits and withdrawals, and finally terminates his/her account. Let us initially ignore the amount of each deposit or withdrawal, and not worry whether the account is in credit or debit. The alphabet of the account is therefore:
α ACC = {open, deposit, withdraw, terminate}
Construct the process ACC.
1.2. Coinstack
A stack of coins contains up to 30 pennies, which may be removed one at a time by the action out1p, until the stack is empty. At any time the number of coins may be brought up again to its maximum of 30 by the single action refill1. Construct the process ST1P, with
α ST1P = {out1p, refill1}
Hint: use mutual recursion to define Stn as the behaviour of the stack containing n coins.
1.3. The Ruritanian Army
The Ruritanian Army has only three ranks: Private, Captain and General. On enlisting, a soldier becomes a Private, and on promotion attains the next higher rank. A soldier at any rank may attend any number of courses. All soldiers enrolled on a course complete it successfully. Thus
α SOLDIER = {enlist, enrol, complete, promote}
Construct the process SOLDIER, taking advantage of the simplification that no soldier is promoted while on a course.
1.4. Change Giving Machine
A machine with alphabet {in5p, out2p, out1p} repeatedly gives change for 5p. The customer may choose any combination of sequences of 2p and 1p coins, provided the total value equals 5p. Construct the process CH to behave as described above.
Warning: the first events on either side of | must be different.
1.5. VMS 3 (vending machine)
The process VMS3 behaves like VMS2 (see lecture notes) except that it will accept up to three coins extra, after which it will dispense up to three chocolates.
1.6. Hedges
(1) Construct a process with alphabet {up, right} which represents the movement of a COUNTER on the board shown in the figure below, where the thick lines denote hedges through which the counter cannot move.
(2) Add to the board the minimum number of hedges that will ensure that the counter can always reach the top right-hand corner of the board, but with minimum restriction of the movement of the counter. Make the corresponding changes to the definition of your process.
Any
enquiries concerning the material on these course pages should be directed to:
G.Wells@ru.ac.za
Last updated: 14 August 2011