Introducing Spin.

[A E Lawrence <A.E.Lawrence@xxxxxxxxxxx>]

In standard (FD) CSP div has two responsibilities:-

1) to model livelock;

and

2) to represent the worst possible process (it is the bottom of the 
refinement partial order).


In CSPP, "div" only describes livelock, matching 1) but not 2) above.
CSPP "div" is very far from the bottom of the refinement order: it is 
immediately below the top miraculous element.

This is a source of confusion for people familiar with the standard 
interpretation, not helped by the connotations of "divergence".

I have therefore decided to do what I ought to have done much earlier: 
change the name. So I will now call it "Spin". Hence in CSPP we have the 3 
elementary  processes (Stop, Skip, Spin) whereas it is (Stop,Skip,div) in 
standard CSP.

So standard CSP is more abstract than CSPP in handling livelock: in fact it 
cannot represent pure livelock.

This is only a change in the name: nothing else. One reason that I stayed 
with div for so long is that in practical CSP most uses of "div" can just 
be replaced by "Spin" to get the equivalent CSPP. The reverse was not 
always true, hence the confusion...

I have updated the tutorial to reflect this change, although that is 
primarily about standard CSP:

  http://www-staff.lboro.ac.uk/~coael/download/csptut.pdf
and
  http://www-staff.lboro.ac.uk/~coael/download/csptut.pdf.bz2 .

And all the gory details in
  http://www-staff.lboro.ac.uk/~coael/download/thcspp.ps.gz
have also been updated to use Spin.

Comments welcome. Thanks to Michael Goldsmith for making me think about this.

Adrian

--
Dr A E Lawrence
http://www-staff.lboro.ac.uk/~coael/