Re: Loosing abstraction due to non-alting channels

["P.H.Welch" <P.H.Welch@xxxxxxxxx>]

I'll try to wriggle out of this as best I can:

> Consider two CSP processes:
>
> Process A(in a) {
>   while (TRUE) {
>     a?x;
>   }
> }
>
> Process B(in a) {
>   while (TRUE) {
>     ALT
>       a -> a?x;
>   }
> }
>
> Both these processes have "a*" as _pattern_. I think in CSP
> terms: A == B.
>
> However, JCSP contains channels on which ALTing is not allowed.
> Process A can be connected to such channel.  Whereas process
> B cannot be connected to such channel.  So, in JCSP: A != B.

Writing the first one above in a CSP-closer pseudo-code:

  A (chan a) = a?x --> A (a)

The second one can't be written in CSP because "a?x" is an *event* (not
a process) and can't stand alone - it has to prefix something as in the
"a?x --> something" above.  Strictly, the above is actually shorthand for
the (possibly infinite) external choice:

  A (chan a) = [](a.x --> A (a) | for all possible input values x)

But this is just syntactic wriggling on my part.  Marcel does have a point
that in CSP, the processes:

  [](a --> P)

and:

  a --> P

are the same - i.e. a one-branched choice is no choice at all!  In JCSP,
there are syntactic differences in the process constructors for the different
classes that contain the no-choice or one-choice inputs - but semantically
they remain identical (as in CSP).  Or almost - see below.

Suppose we have a JCSP process, A, whose single channel is declared to be an
AltingChannelInput and whose body contains one-branched ALTs on that channel.

Suppose we have a JCSP process, B, whose single channel is declared to be an
ChannelInput and whose body contains ordinary inputs on that channel, but is
otherwise identical to A.

Then, anywhere we could plug in A we could also plug in B.  A plugs into
*-OneChannels, which all implement ChannelInput - so B can plug in also.

The reverse is *almost* the case.  If we plug B into any *-OneChannel, A will
plug in also (since all *-OneChannels in JCSP extend AltingChannelInput).
But B can plug into *-ManyChannels as well and A can't.  Oh well ... I gave
my motivations for disallowing this elsewhere (see Marcel's original question).

So, we have the following rule: for all legal progams (i.e. those that get
past the Java compiler), the above A and B processes are the same and may
be freely intercahnged.  So I don't think things are broken too much.

More later ...

Peter.