# Conflicting Priorities in occam

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...