[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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
P = (x --> P) <| x \in X |> 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...
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