Conflicting Priorities in occam

[Adrian Lawrence <adrian.lawrence@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>]

Dressing up CSPP
~~~~~~~~~~~~~~~~
While sawing wood in Cornwall, I came to the conclusion that I should change
CSPP. The change is is to the underlying denotational semantics, and does
not modify the syntax. In in almost all respects, the interpretation is
unaltered.

Those of you who heard me introduce CSPP and HCSP two years ago in Twente
may remember that I discussed briefly whether events and traces should be
"dressed". And last year's WoTUG-21 CSPP paper started by introducing
dressed events. One example was
    (ball,{ball,food})
as a dressed event for a cat. The event "ball" is "dressed" with the offer
{ball,food} that evoked it.

But I funked it! It just seemed too radical a departure from conventional CSP
to extend the definition of traces. So I developed CSPP with "undressed"
events and traces to see how far I could get and whether the dressing
is really needed. And as you know, the answer seemed to be that I could do
everything that was required.

But there were a couple of consequences of deliberately and perversely throwing
away information. It is precisely because undressed semantics `forgot' the
initial offer that 
   (a --> P) [<] (a --> Q)
had to be nondeterministic. Peter was disturbed by this last year. But I was
able to show, and have continued to argue, that we can live with it. I was
addressing exactly this issue in an earlier message in this discussion when I
spoke of a_left and a_right and appropriate levels of abstraction.
But if we dress events, the problem disappears, and P will be performed
after "a" above. Of course, I can still define it to be non-deterministic
if that is thought desirable, but that would be contrived, and I would need
to be persuaded. 

Denis is partly to blame: it was his use of SKIP guards that got me thinking 
about how to capture the general case in a simple way in CSPP syntax. And
I realized that I really needed dressed semantics to do that in a nice way.

Now that I have gained confidence and experience with CSPP, it has become
perfectly clear to me that I should have used the dressed version from the
start. Although traces are really part of the semantics rather than part
of the language proper, there are times when we want to discuss them in
applications: Peter did just that in a recent message. A full dressed
trace might be <(a,A)(b,B)(c,C)>, but when the offers are irrelevant, we can
still speak of the corresponding undressed trace <abc>.

I have already sketched most of the main definitions, but there is a lot of
technical detail to rework and fill in. I am quite sure that this will go
through smoothly. In fact many things are bit easier with the extra 
information.

Anyway, this is just to let you know that I am proposing to shift the carpet 
that we have been standing on. But only slightly. And I think that you will
all approve.

I haven't replied to several questions and messages including some from Peter.
Just now, my priority is to build better and stronger foundations.
I don't know how much I can do before flying to Munich, but it should be done
by WoTUG-22. 

Summary
~~~~~~~

1) Strengthen acceptance semantics to use dressed traces and events.
2) Allows CSPP to decide "which side" performed the event in
            (a --> P) [<] (a --> Q)
   and allows CSPP to capture certain other idioms that were difficult
   or impossible in undressed semantics which ignored information which
   is obviously present.
3) The existing syntax of CSPP is not altered, and almost all laws are
   unchanged.   

Comments welcome!

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