A tail of woe

I wrote this several years ago after pupils came to me almost in tears about a Concurrency practical. No doubt some things have improved since then. – Mike

This short report narrates the experiences of our unfortunate guinea-pig in attempting the first practical for the second-year course on Concurrency. And if a guinea-pig doesn't have a tail of woe, who does?

Solving the problem

Our trusty rodent began diligently by solving the modelling problem on paper. It took him about ten minutes, but he feels that it might occupy half an hour in a tutorial with some of his less able students. That means the students themselves might spend one or two hours on the paper exercise – and certainly there have been finals questions on modelling with about this complexity. Remember, one hour for a guinea pig is like four or five human hours.

His only mistake was to suppose at first that there would be a process corresponding to each train, but this turns out not to be necessary.

Writing the script

Bravely, our volunteer tried to express his solution in the tortured input syntax of FDR. He didn't really know where to start. The practical instructions contained no information. Should he read the very dry syntax summary in the FDR manual, or should he try to follow the examples that were handed out in lectures? He decided on the latter, but that meant a process of experiment, and the experiment couldn't begin until he was in front of the computer.

Quite by chance, our hero hit on several ideas that turned out to be crucial:

• declaring a channel by channel forward: id . id . id so that events take the form forward.A.B.C.
• writing forward!i?y!k -> for an event that insists on certain values for i and k, but allows an external choice of y.
• the notation if B then P else Q for conditional – he looked long and hard in the on-line manual for the notation P <| B |> Q that seems to be so important in CSP.
• the notation for parallel composition that we need is something like P [|{forward,reverse}|] Q. All those ['s and |'s and {'s (and more) are needed – see later!

Of course, he later found all of these things in the manual, but it was hard to digest it all at once, and the manual was on-line, so he could not prepare anything beforehand.

Fighting the tools – fit the first

Starting FDR was no problem for our hero, once he had worked out that the UNIX command was fdr2 (again, no hint in the documentation). A control panel with all sorts of buttons and lights appeared, but all the windows were empty. The bottom line said FDR session for trains.csp, but nothing else happened. What could be wrong? After pushing all the buttons he could see, still nothing. So the indomitable guinea-pig began to do what he does in French restaurants: scan the menu for something you don't understand, order it, and see what arrives. Eventually, Options / Show Status revealed a new window with the helpful remark parse error near line 28 of trains.csp. Our guinea-pig has seen such things before; in fact, he has written several compilers that give error messages that are no more helpful, although it's never occurred to him before to hide the messages away in a secret window.

So what's wrong? Somewhere near line 28 appears the definition

Sheds = 
  Shed(A) [|{done}|] Shed(B) [|{done}|] Shed(C)
    [|{done}|] Shed(D) [|{done}|] Shed(E)

This combines five processes, one for each shed, into a single process that models all five sheds, insisting that they synchronize on the done event that indicates the right engine is in the right shed. Our hero knew that parallel composition was associative, and had seen an example containing P ||| Q ||| R, so this seemed sensible.

But guinea-pigs who have programmed in assembler, C, APL and BASIC develop a nose for these things, and it soon became obvious that brackets were the thing to try. How would he explain that to his students? "Some things I can tell you; other things you just have to find out for yourself". So now we try

Sheds = 
  Shed(A) [|{done}|] (Shed(B) [|{done}|] (Shed(C)
    [|{done}|] (Shed(D) [|{done}|] Shed(E))))

Getting more readable? Not half. But this time FDR happily digests the file, and a list of processes appears in the window.

With a little more experimentation (no help from the instructions), our hero composes the claim "Spec trace-refined-by Puzzle". Why trace refinement? Is that good enough? Or should it be failures-divergences refinement? The instructions don't help. [In fact, it has to be trace refinement, because the puzzle refuses to do physically impossible events that a simple spec permits].

Fighting the tools – fit the second

After "Check" is pressed, things start to happen in the secret window (just as well our friend kept it open ...). After several seconds, and many lines of output, the following appears:

Started: 34 Finished: 29 Transitions: 3700
Started: 34 Finished: 30 Transitions: 3800
Started: 34 Finished: 30 Transitions: 3900
Started: 34 Finished: 31 Transitions: 4000Value is not an event
reverse

Error compiling Puzzle
Loading... done
Server: : failed to compile ISM

Ready

Sorry: some of that is in blue, and some in black. But you get the idea.

Funny, the thing seemed to 'compile' ok this time, and now we get this run-time error. Guinea-pigs can't cry, and that's lucky. What's wrong now? Well, to cut a long story short, our hero had written

Puzzle = Sheds [|{forward,reverse}|] Yards [|{forward,reverse}|] Tracks

as a way of putting the whole thing together – then he'd changed it into

Puzzle = (Sheds [|{forward,reverse}|] Yards) [|{forward,reverse}|] Tracks

because of earlier problems. But it turns out that you need to write

Puzzle = 
  (Sheds [|{|forward,reverse|}|] Yards) [|{|forward,reverse|}|] Tracks

because those extra |'s mean "take the set of events that can occur on these channels". Clear? It ought to be, because there's no hint in the instructions.

And now everything seems to work, and another secret window (can you find it?) lets you see the trace that solves the puzzle.

Giving up

With some sense of satisfaction, our battle-scarred protagonist made some paper tokens and followed out the solution on the picture. It worked! At that point he decided to give up. He had spent almost two hours on the practical, and had learnt nothing new about CSP after the first ten minutes. And remember, an hour in guinea-pig time is the same as three or four hours for ordinary humans ...

Oh, and in case your undergraduates come to you looking a bit red about the eyes, our indomitable friend has included his solution at the end. Fivers gratefully accepted, and cheques payable to the Guinea Pig's Claret Fund, because although our little friends are not freely moved to tears, they do like a drop or two from time to time.

---

[I've omitted the solution here in case the practical is still in use after all this time.]