[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
In standard (FD) CSP div has two responsibilities:-
1) to model livelock;
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
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:
And all the gory details in
have also been updated to use Spin.
Comments welcome. Thanks to Michael Goldsmith for making me think about this.
Dr A E Lawrence