RE: CDL collision resolution

 Following is exactly the same text as I sent on 21 sept, but in plain
text so the arrows archive correctly.
 
Peter
------------------
 
 
 CDL collisions and distributed choice
 

Collision resolution isn't arbitrary, but is a reflection of the
reversibility of state changes in the parties. For example, with a
request/acceptance, with the requestor (buyer) allowed to cancel an
unaccepted request, the collision resolution is a business question -
which will be determined by the economic power of the parties, how
difficult it is for each to deal with the contradiction of their wishes
etc. ( In turn, the protocol design decision will then affect the
implementation and use of the protocol - if the cancel wins, then the
supplier may wait a bit before actually starting work on delivery.) Let
us assume that the argument is won by the suppliers - when they send
accept, they mean it and will go ahead with cutting the metal. If cancel
crosses with accept, the cancel is ignored. But the supplier won't
accept an order that he has been told has been cancelled.
 
So the following sequences are valid (these are clearer with sloping
lines)
 
--- request  ---->
<--- accept ---
 
--- request --->
--- cancel --->
<--- cancelled    (without this the buyer will never know the collision
did not occur)
 
--- request --->
-- cancel       (crosses with the accept)
<--- accept --
              --->                  (cancel arrives and is ignored)
 
But supposing the suppliers decision to accept occurs just as the cancel
is passing into the suppliers system. Then the observed exchange is
 
--- request -- >
--- cancel ---->
<---- accept -
 
which wasn't supposed to be allowed.  But all we've done is move the
observation point a bit to the left. In a real implementation that could
well be the observed behaviour - messages can pass in buffers and be
dealt with by different threads.
 
To capture what is really going on we need to have a representation of
the state change in the supplier. This state is NOT private, precisely
because it determines what the directly observable behaviour is. We then
have
 
--- request --->
  ACCEPT
<--- accept -
 
--- request ---->
--- cancel --->
<--- cancelled -
 
--- request --->
  ACCEPT
--- cancel ---->
<--- accept -
 
and I don't need sloping lines anymore.
 
If you hate variables, you can achieve the same effect with another
message exchange to an additional role 
 
--- request --->
            -- check acceptance --->
  <--- decide to accept -
<---  accept --
 
which I suspect may go into pi better. But it's really just the same
thing. In either case the acceptance decision is part of the public
choreography, although only visible to the buyer via the choreography.
 
Taking this approach, that collision resolution is determined by state
changes at one party is also applicable to the multi-party cases. As an
example:
 Chair sends "Any objections ?" to all members
 Members can send "Objection" to chair
 If any Objection received, Chair sends "Failed" to all members
 If no Objection received, after some time determined by Chair, Chair
determines that motion is approved and sends "Approved" to all members
 If Objection arrives at Chair after decision is made, it is ignored
 
With a priority on each relationship, the chair might have sent Approved
out to some members but then get an Objection arriving from another. On
that relationship, the Objection got there in time - but in fact it
didn't, the decision has been made.
(again the actual decision can be modeled as variable assignment or as
the receipt of a single message on another ("internal") relationship)