🚀 go-pugleaf

In article <6679@ecs.soton.ac.uk> dbc@ecs.soton.ac.uk (Bryan Carpenter) writes:
>I don't see what you're getting at really.  The (communication)
>event in occam surely does take place.  In occam though
>particular events (the only ones supported---communications)
>can only be in the alphabets of *two* processes, so their occurence
>will only directly effect these two processes.
>
>CSP, of course, has the same ability to limit particular events to
>the alphabets of a subset of all processes---I don't see that events are
>necessarily all "broadcast" in the way you seem to suggest.
>
>The difference seems to have more to do with how many processes can
>share an event (in their alphabets), rather than the nature
>of the concurrency.

You are correct in noting that CSP has the ability to exclude certain
processes from interaction in some events (on the basis of their alphabet).
However, the events are all "broadcast" in nature (even when only two
processes share the event).

The problem seems to be the following.  Consider a process

  A = event1 -> SKIP

Hoare tells us that this is a process that engages in event1 and then
terminates (successfully).  The question at hand is does "execution" of
A cause event1 to "occur."  It seems to me that it does not.

If event1 is an input event, say

   event1 = c.v = c?v

and
  
   A = c?v -> SKIP

then what does "execution" of A mean?  Hoare says that process A is initially
prepared to engage in event c.v.  Since it seems to me that an input event can
not be considered to have "occurred" when taken in isolation (as in process
A, which is not composed with any other processes), I cannot interpret the
statement that a process is "prepared to engage in" an event to mean that the
event "occurs."

As a result, it would appear that

   A||B = event1 -> SKIP  (where event1 is just some event)

is a process that is "prepared to engage in event1," and not a process in
which event1 has "occured."

Therefore, CSP processes all strike me as descriptions of possible sequences
of events (and actions).  They do not strike me as descriptions of actual
sequences of events (and actions).


Disclaimer:

    I cannot understand why Hoare would choose to define CSP with such a 
conceptual problem.  Given Hoare's status relative to my own, it is probably 
far, far more likely that I am mistaken in my understanding of the definition, 
rather than that Hoare is mistaken in his definition.  Any insights into an 
error that I may have made will be appreciated.