Conflicting Priorities in occam

[Adrian Lawrence <adrian.lawrence@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>]

Dressed CSPP and SKIP guards
~~~~~~~~~~~~~~~~~~~~~~~~~~~~

I have now rebuilt CSPP with dressed semantics. One motive was to be able
to specify SKIP guards in a PRI ALT neatly. Here it is

PRI ALT
  ?x
    P         = (x --> P) <| x \in X |> Q ,
  SKIP
    Q

approximately. Yes pseudo-occam. And my official version is
     (x --> P) <| \sigma X \spot x \in X |> Q
where the \sigma is quantifier-like and flags that X is not free.
X is the environmental offer: if x is available, it is performed followed
by P. Otherwise Q. 

It was impossible to define P <| x \in X |> Q in undressed semantics.

There are other benefits some of which I have mentioned before, possibly
the most important is that now
    (a --> P) [<] (a --> Q) = (a --> P)
which should make Peter happy. 

There is still a fair bit of work left in checking the whole structure, but
the semantics of the constructors is now done, including the new one above.

Note for those who saw a previous example of a Skip-guard in CSPP:
that example was correct CSPP, but did not reflect occam semantics. It
promoted the initial actions of the subsequent process into guards! Sorry,
I missed that until the penny dropped when contemplating Denis' example.

I won't have time for much more work on this until I get back from FemSys99...

Adrian
-- 
A E Lawrence, MA., DPhil.  	adrian.lawrence@xxxxxxxxxxxxxx
MicroProcessor Unit, 13, Banbury Road, Oxford. OX2 6NN. UK.                
Voice: (+44)-1865-273274,  Fax: (+44)-1865-273275