- From: Williams, Stuart <skw@hplb.hpl.hp.com>
- Date: Wed, 16 Jan 2002 16:59:55 -0000
- To: "Noah Mendelsohn (E-mail)" <Noah_Mendelsohn@lotus.com>, "Christopher Ferris (E-mail)" <chris.ferris@east.sun.com>
- Cc: "Marc Hadley (E-mail)" <marc.hadley@uk.sun.com>, "Highland M Mountain (E-mail)" <highland.m.mountain@intel.com>, "Glen Daniels (E-mail)" <gdaniels@macromedia.com>, "'distobj@acm.org'" <distobj@acm.org>, "Oisin Hurley (E-mail)" <ohurley@iona.com>, "Mark A. Jones (E-mail)" <jones@research.att.com>, "'www-archive@w3.org'" <www-archive@w3.org>
- Message-ID: <5E13A1874524D411A876006008CD059F1928A5@0-mail-1.hpl.hp.com>
Hi Noah et al,
BTW, I have added a zipped copy of this text for good measure as I fear that
the linebreaks/layout will get mangled in the mail.
I think I've address all active members of the TBTF and I've copied this to
www-archive (the public archive).
I have been reflecting overnight on our conversation of yesterday evening
and think that you (Noah and Chris) are correct in suggesting that we may
have lost something by focussing solely on the wire. The main thing that we
are missing in the trace MEP and trace HTTP binding is some 'linkage'
between the MEP in the abstract and the practicalities of HTTP. So whilst we
say in the binding defn what goes on the wire between an soReq and an eoReq,
we don't say it in those terms, nor do we link success and failures from
HTTP back to the events in the algebraic expressions. I don't think that's a
hugh job, just an appropriate sentence or two in the right places to make
the connection.
The tabular style does this linkage much more explicitly.
I think that the Trace MEP description is pretty close to what we need. We
can *chose* to describe requester and responder processes instead - I have
done both below. Both are near clones of each other and near clones of the
earlier wire trace expressions [1]. The main difference is that thinking of
requester and responder brings a sense of in'ness and out'ness that is not
there when are thinking more in the mode of a wire-tap - in which case
everthing is 'in'. This was where I think Chris was going.
<aside topic="notation">
My local process algebra guru was pretty encouraging of this approach, and
made one or two comments to bring the notation inline with common CCS
(Milner) practice. State names tend to start with an uppercase letter while
actions/events start with a lower case letter. Also events/actions
connecting processes tend to be thought of action and co-action or
complementary events. The usual notation is to use over-bars on inputs and
no decoration on outputs. I have used ! instead of overbars for input
event/actions. So "soReq" is an output start of request event/action while
"!soReq" is the complementatry input event.
</aside>
The expressions for requester and responder now have 'guards' in them to
represent interaction within the local node. So the transmission of a
request or a response (at requester and responder respectively) is guarded
with a "!start" input action. Likewise, the start of receipt of a request
message at a responder and a response message at a requester is also guarded
with a "receiving" output action.
Also, in an attempt to address Noahs question about say timeouts, I have add
a "!localException" input action intended to force the message exchange in
progress to be abandoned. The "!start" and "receiving" guards could be
removed without harm if folks thinks that makes things too detailed. If we
were to do that, apart from the labelling (in's replaced with out's for
soReq, eoReq, soresp, eoResp...) requester and responder are then the same
expression, and, but for the terms in 'localException' they are the same as
the expressions we are already considering [1].
I have laid the expressions out as a state machine below, and annotated them
with the trace evolutions to the point of entry to each state (just on the
requester). Again, except for the inclusion of start, receiving and
localException they are identical to those previously presented [1].
I also had an intuition that an intermediary is a bit like a wire - at least
from the point-of-view of relaying a request response pattern. This turned
into some thing of a large exercise which I probably should have spend a bit
less time on - however I would appreciate comments/feedback.
For those remember the collosal cave adventure it became a bit like a maze
of twisty passages all different (you'll see what I mean when/if you get to
it). I think modelling (formally) the relaying of an MEP is quite a
challenge (but it *can* be done), given the potential for the intermediary
to re-time the request/response - so on the 'left' side request and response
may not overlap in time... just as preview... the 20 states without
transitions or traces (they do indeed follow and were I more proficient I
sure I could have got a machine to generate them - but they were done by
hand! There may be mistakes!).
r--- receiving request,-,-,-
rr-- receiving request, relaying request,-,-
R--- received request,-,-,-
Rr-- received request, relaying request,-,-
RR--
rrr-
Rrr-
RRr-
rrR-
RrR-
RRR-
rrrr
Rrrr
RRrr
rrRr
RrRr
RRRr
rrRR
RrRR
RRRR received request, relayed request, receieved response, relayed
response
20 states!
Anyway this modelling of the 'channel'/'wire' as a process, at least for me
was instructive and I think will serve to develop a formalism for how to
relay a request/response through intermediaries. (Its not quiet an
intermediary becaus they would allow r--r, R--r and r--r and R--R allowing
for intermediatry generated responses).
Anyway, to conclude... the process algebra expressions to model requester
and responder are near clones of each other and clones of the expression in
[1].
If your elide out connection with the local node (start, receiving,
localException) the three expressions (for requester, responder and wire)
are just relabled versions of one another. I like the economy of using just
the one articulation of the 'same' thing rather than two variants...
The model of the channel is interesting, but I think I would avoid including
it. I would use it as a basis for describing intermediary behaviour - which
for request/response is going to take 24 states (unless anyone else counts
differently). Tabular style that would be huge. It's huge below mostly
because of the inclusion of trace and state path annotations that I added to
avoid getting lost. I've included second version that removes the trace
annotations - which is about as compact as you can make it... a diagram may
help. I will also speak to my process algebra guru... I think that there may
be a way to split the intermediary RR MEP relay into two expressions and use
parallel composition - if so it will make for a much more compact expression
and be more tractable than a 24 state state diagram.
Apologies for such a large response... I know it will take some work on your
part just to evaluate it. The short is that I think that we can use the wire
trace philosophy and add a couple more sentences to make the connection
between the algebra/MEP decription and the HTTP binding description. It
maybe helpful to add the 'start', 'receiving' and 'localException' guards
and model the requester and receiver processes... which would detract from
the enonomy of presenting the expressions just once - not against it... its
a trade-off.
Regards
Stuart
!start,start
!receiving,!receiving
!localEception,localException
+---------------+ +---------------+
| | | |
| Srr-requester | | Srr-responder |
| | | |
+---------------+ +---------------+
^ +-------------+ ^
| | | |
+---------->| Srr-channel |<-----------+
soReq,!soReq | | soReq,!soReq
eoReq,!eoreq +-------------+ eoReq,!eoReq
!channelFail,channelFail !channelFail,channel fail
Relabelled xxx_left in Srr-channel) (Relabelled xxx_right in Srr
channel)
SRR Requester
-------------
[NB: This is basically the same 'structure' as the the previous wire trace
expression, with the addition of local start/success/fail indicators and the
distinction of channel failures and local exceptions (eg. timeouts or
whatever other option the requester might have for abandoning the exchange]
Srr-requester = !start.soReq.S1
//Sending Request
//[start]
S1 = eoReq.S2 + //Finished sending Request
!soResp.receiving.S3 + //Start of overlapping response
!channelfail.Fail + //Channel/media failure
!localException.Fail //Local Timeout or reason to abort
//Request sent waiting for start of response
//[start,soReq,eoReq] (from S1)
S2 = !soResp.receiving.S4 + //Start of non-overlapping response
!channelFail.Fail +
!localExpception.Fail
//Sending request and Receiving response
//[start,soReq,soResp,receiving] (from S1)
S3 = eoReq.S4 + //Finished sending, still receiving
!eoResp.S5 + //Finished receiving, still sending
!channelFail.Fail +
!localException.Fail
//Waiting to receive end of response.
//[start,soReq,eoReq,soResp,receiving] (from S1,S2)
//[start,soReq,soResp,receiving,eoReq] (from S1,S3)
S4 = !eoResp.Success + //Exchange completed successfully
!channelFail.Fail +
!localException.Fail
//End of overlapping response received, still sending request
[start,soReq,soResp,receiving,eoResp] (from S1,S3)
S5 = eoReq.Success +
!channelFail.Fail +
!localException.Fail
//Fail - abnormal termination
//[start.soReq.channelFail] (from S1)
//[start.soReq.localException] (from S1)
//[start,soReq,eoReq,channelFail] (from S1,S2)
//[start,soReq,eoReq,localException] (from S1,S2)
//[start,soReq,soResp,receiving,channelFail] (from S1,S3)
//[start,soReq,soResp,receiving,localException] (from S1,S3)
//[start,soReq,eoReq,soResp,receiving,channelFail] (from S1,S2,S4)
//[start,soReq,soResp,receiving,eoReq,channelFail] (from S1,S3,S4)
//[start,soReq,eoReq,soResp,receiving,localException] (from S1,S2,S4)
//[start,soReq,soResp,receiving,eoReq,localException] (from S1,S3,S4)
//[start,soReq,soResp,receiving,eoResp,channelFail] (from S1,S3,S5)
//[start,soReq,soResp,receiving,eoResp,localException] (from S1,S3,S5)
Fail = fail.0 //Signal local failure and stop (0 = Null process)
//Success - normal termination
//[start,soReq,eoReq,soResp,receiving,eoResp] (from S1,S2,S4)
//[start,soReq,soResp,receiving,eoReq,eoResp] (from S1,S3,S4)
//[start,soReq,soResp,receiving,eoResp,eoReq] (from S1,S3,S5)
Success = success.0 //Signal local success and stop
Rearranges to:
Srr-request = !start.soReq.(eoReq.( soResp.receiving.( !eoResp.success +
!channelFail.fail +
!localException.fail
) +
!channelFail.fail +
!localException.fail
) +
!soResp.receiving.( eoReq.( eoResp.success +
!channelFail.fail +
!localException.fail
) +
!eoResp.( eoReq.success +
!channelFail.fail
+
!localException.fail
) +
!channelFail.fail +
!localException.Fail
) +
!channelFail.fail +
!localException.fail
).0
[Personnally think that the single equation expression for the behaviour is
much less revealing than the stepwise, S1, S2... expression which reveals
the embedded statemachine. S1 etc could be given more friendly statenames
and the presentation could be augmented with a diagram]
SRR-Responder
-------------
Srr-responder = !soReq.receiving.S1
//Sending Request
S1 = !eoReq.S2 + //Finished receiving Request
!start.soResp.S3 + //Start sending overlapping response
!channelfail.Fail + //Channel/media failure
!localException.Fail //Local Timeout or reason to abort
//Request received waiting for start of response
S2 = !start.!soResp.S4 + //Start of non-overlapping response
!channelFail.Fail +
!localExpception.Fail
//Receiving request and Sending response
S3 = !eoReq.S4 + //Finished receiving request, still
sending response
eoResp.S5 + //Finished sending response, still receiving
request
!channelFail.Fail +
!localException.Fail
//Waiting to receive end of response.
S4 = eoResp.Success + //Exchange completed successfully
!channelFail.Fail +
!localException.Fail
//End of overlapping response sent, still receiving request
S5 = eoReq.Success +
!channelFail.Fail +
!localException.Fail
Fail = fail.0 //Signal local failure and stop (0 = Null process)
Success = success.0 //Signal local success and stop
[A structurally similar single expression to the one for the requester could
be generated... even cloned. You should see the structural similarity with
Srr-requester... infact apart from using the complementary events, the only
difference are the !start and receiving actions (controlling guarding start
of transmission or reportin start of reception) - apart from 'start' and
'receiving' Srr-responder is a relabeling of Srr-request with the soReq,
soResp, eoReq and eoResp replaced by their respective complements.]
SRR-Channel/SRR Intermediary
----------------------------
Srr-Channel = !soReq_left.S1
//Receiving request
// [soReq_left]
S1 = soReq_right.S2
+ channelFail_left.0
//Receiving and relaying request
//[soReq_left, soReq_right]
S2 = !eoReq_left.S3
+ !soResp_right.S4
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relaying request
//[soReq_left, soReq_right, eoReq_left]
S3 = eoReq_right.S5
+ !soResp_right.S6
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Receiving and relaying request, receiving response
//[soReq_left, soReq_right, soResp_right]
S4 = eoReq_left.S6
+ soResp_left.S7
+ !eoResp_right.S8
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and Relayed request
//[soReq_left, soReq_right, eoReq_left, eoReq_right]
S5 = !soResp_right.S9
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relaying request, Receiving response
//[soReq_left, soReq_right, eoReq_left, soResp_right] (from S3)
//[soReq_left, soReq_right, soResp_right, eoReq_left] (from S4)
S6 = eoReq_right.S9
+ soResp_left.S10
+ !eoResp_right.S11
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Receiving and relaying request, receiving and relaying response
//[soReq_left, soReq_right, soResp_right, soResp_left]
S7 = !eoReq_left.S10
+ !eoResp_right.S12
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Receiving and relaying request, received response
//[soReq_left, soReq_right, soResp_right, eoResp_right]
S8 = !eoReq_left.S11
+ soResp_left.S12
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relayed request, receiving response
//[soReq_left, soReq_right, eoReq_left, eoReq_right, soResp_right]
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoReq_right] (from
S3,S6)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoReq_right] (from
S4,S6)
S9 = soResp_left.S13
+ !eoResp_right.S14
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
// Received and relaying request, receiving and relaying response
//[soReq_left, soReq_right, eoReq_left, soResp_right, soResp_left] (from
S3,S6)
//[soReq_left, soReq_right, soResp_right, eoReq_left, soResp_left] (from
S4,S6)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoReq_left] (from S7)
S10 = eoReq_right.S13
+ !eoResp_right.S15
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relaying request, received response
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoResp_right] (from
S3,S6)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoResp_right] (from
S4,S6)
//[soReq_left, soReq_right, soResp_right, eoResp_right, eoReq_left] (from
S8)
S11 = eoReq_right.S14
+ soResp_left.S15
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Receiving and relaying request, received and relaying reponse
//[soReq_left, soReq_right, soResp_right, soResp_left, eoResp_right] (from
S7)
//[soReq_left, soReq_right, soResp_right, eoResp_right, soResp_left] (from
S8)
S12 = !eoReq_left.S15
+ eoResp_left.S16
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relayed request, receiving and relaying response
//[soReq_left, soReq_right, eoReq_left, eoReq_right, soResp_right,
soResp_left] (S9)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoReq_right,
soResp_left] (from S3,S6,S9)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoReq_right,
soResp_left] (from S4,S6,S9)
//[soReq_left, soReq_right, eoReq_left, soResp_right, soResp_left,
eoReq_right] (from S3,S6,S10)
//[soReq_left, soReq_right, soResp_right, eoReq_left, soResp_left,
eoReq_right] (from S4,S6,S10)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoReq_left,
eoReq_right] (from S7,S10)
S13 = !eoResp_right.S17
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relayed request, received response
//[soReq_left, soReq_right, eoReq_left, eoReq_right, soResp_right,
eoResp_right] (from S9)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoReq_right,
eoResp_right] (from S3,S6,S9)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoReq_right,
eoResp_right] (from S4,S6,S9)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoResp_right,
eoReq_right] (from S3,S6,S11)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoResp_right,
eoReq_right] (from S4,S6,S11)
//[soReq_left, soReq_right, soResp_right, eoResp_right, eoReq_left,
eoReq_right] (from S8,S11)
S14 = soResp_left.S17
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relaying request, received and relaying response
//[soReq_left, soReq_right, eoReq_left, soResp_right, soResp_left,
eoResp_right] (from S3,S6,S10)
//[soReq_left, soReq_right, soResp_right, eoReq_left, soResp_left,
eoResp_right] (from S4,S6,S10)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoReq_left,
eoResp_right] (from S7,S10)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoResp_right,
soResp_left] (from S3,S6,S11)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoResp_right,
soResp_left] (from S4,S6,S11)
//[soReq_left, soReq_right, soResp_right, eoResp_right, eoReq_left,
soResp_left] (from S8,S11)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoResp_right,
eoReq_left] (from S7,S12)
//[soReq_left, soReq_right, soResp_right, eoResp_right, soResp_left,
eoReq_left] (from S8,S12)
S15 = eoReq_right.S17
+ eoResp_left.S18
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Receiving and relaying request, received and relayed response
//[soReq_left, soReq_right, soResp_right, soResp_left, eoResp_right,
eoResp_left] (from S7,s12)
//[soReq_left, soReq_right, soResp_right, eoResp_right, soResp_left,
eoResp_left] (from S8,S12)
S16 = !eoReq_left.S18
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relayed request, received and relaying response
//[soReq_left, soReq_right, eoReq_left, eoReq_right, soResp_right,
soResp_left, eoResp_right] (S9,S13)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoReq_right,
soResp_left, eoResp_right] (from S3,S6,S9,S13)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoReq_right,
soResp_left, eoResp_right] (from S4,S6,S9,S13)
//[soReq_left, soReq_right, eoReq_left, soResp_right, soResp_left,
eoReq_right, eoResp_right] (from S3,S6,S10,S13)
//[soReq_left, soReq_right, soResp_right, eoReq_left, soResp_left,
eoReq_right, eoResp_right] (from S4,S6,S10,S13)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoReq_left,
eoReq_right, eoResp_right] (from S7,S10,S13)
//[soReq_left, soReq_right, eoReq_left, eoReq_right, soResp_right,
eoResp_right, soResp_left] (from S9,S14)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoReq_right,
eoResp_right, soResp_left] (from S3,S6,S9,S14)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoReq_right,
eoResp_right, soResp_left] (from S4,S6,S9,S14)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoResp_right,
eoReq_right, soResp_left] (from S3,S6,S11,S14)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoResp_right,
eoReq_right, soResp_left] (from S4,S6,S11,S14)
//[soReq_left, soReq_right, soResp_right, eoResp_right, eoReq_left,
eoReq_right, soResp_left] (from S8,S11,S14)
//[soReq_left, soReq_right, eoReq_left, soResp_right, soResp_left,
eoResp_right, eoReq_right] (from S3,S6,S10,S15)
//[soReq_left, soReq_right, soResp_right, eoReq_left, soResp_left,
eoResp_right, eoReq_right] (from S4,S6,S10,S15)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoReq_left,
eoResp_right, eoReq_right] (from S7,S10,S15)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoResp_right,
soResp_left, eoReq_right] (from S3,S6,S11,S15)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoResp_right,
soResp_left, eoReq_right] (from S4,S6,S11,S15)
//[soReq_left, soReq_right, soResp_right, eoResp_right, eoReq_left,
soResp_left, eoReq_right] (from S8,S11,S15)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoResp_right,
eoReq_left, eoReq_right] (from S7,S12,S15)
//[soReq_left, soReq_right, soResp_right, eoResp_right, soResp_left,
eoReq_left, eoReq_right] (from S8,S12,S15)
S17 = eoResp_left.S19
+ channelFail_left.0
//Received and relaying request, received and relayed response
//[soReq_left, soReq_right, eoReq_left, soResp_right, soResp_left,
eoResp_right, eoResp_left] (from S3,S6,S10,S15)
//[soReq_left, soReq_right, soResp_right, eoReq_left, soResp_left,
eoResp_right, eoResp_left] (from S4,S6,S10,S15)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoReq_left,
eoResp_right, eoResp_left] (from S7,S10,S15)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoResp_right,
soResp_left, eoResp_left] (from S3,S6,S11,S15)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoResp_right,
soResp_left, eoResp_left] (from S4,S6,S11,S15)
//[soReq_left, soReq_right, soResp_right, eoResp_right, eoReq_left,
soResp_left, eoResp_left] (from S8,S11,S15)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoResp_right,
eoReq_left, eoResp_left] (from S7,S12,S15)
//[soReq_left, soReq_right, soResp_right, eoResp_right, soResp_left,
eoReq_left, eoResp_left] (from S8,S12,S15)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoResp_right,
eoResp_left, eoReq_left] (from S7,s12,S16)
//[soReq_left, soReq_right, soResp_right, eoResp_right, soResp_left,
eoResp_left, eoReq_left] (from S8,S12,S16)
S18 = eoReq_right.S19
+ channelFail_right.0
//Received and relayed request, received and relayed response
//[soReq_left, soReq_right, eoReq_left, eoReq_right, soResp_right,
soResp_left, eoResp_right, eoResp_left] (S9,S13,S17)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoReq_right,
soResp_left, eoResp_right, eoResp_left] (from S3,S6,S9,S13,S17)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoReq_right,
soResp_left, eoResp_right, eoResp_left] (from S4,S6,S9,S13,S17)
//[soReq_left, soReq_right, eoReq_left, soResp_right, soResp_left,
eoReq_right, eoResp_right, eoResp_left] (from S3,S6,S10,S13,S17)
//[soReq_left, soReq_right, soResp_right, eoReq_left, soResp_left,
eoReq_right, eoResp_right, eoResp_left] (from S4,S6,S10,S13,S17)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoReq_left,
eoReq_right, eoResp_right, eoResp_left] (from S7,S10,S13,S17)
//[soReq_left, soReq_right, eoReq_left, eoReq_right, soResp_right,
eoResp_right, soResp_left, eoResp_left] (from S9,S14,S17)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoReq_right,
eoResp_right, soResp_left, eoResp_left] (from S3,S6,S9,S14,S17)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoReq_right,
eoResp_right, soResp_left, eoResp_left] (from S4,S6,S9,S14,S17)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoResp_right,
eoReq_right, soResp_left, eoResp_left] (from S3,S6,S11,S14,S17)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoResp_right,
eoReq_right, soResp_left, eoResp_left] (from S4,S6,S11,S14,S17)
//[soReq_left, soReq_right, soResp_right, eoResp_right, eoReq_left,
eoReq_right, soResp_left, eoResp_left] (from S8,S11,S14,S17)
//[soReq_left, soReq_right, eoReq_left, soResp_right, soResp_left,
eoResp_right, eoReq_right, eoResp_left] (from S3,S6,S10,S15,S17)
//[soReq_left, soReq_right, soResp_right, eoReq_left, soResp_left,
eoResp_right, eoReq_right, eoResp_left] (from S4,S6,S10,S15,S17)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoReq_left,
eoResp_right, eoReq_right, eoResp_left] (from S7,S10,S15,S17)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoResp_right,
soResp_left, eoReq_right, eoResp_left] (from S3,S6,S11,S15,S17)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoResp_right,
soResp_left, eoReq_right, eoResp_left] (from S4,S6,S11,S15,S17)
//[soReq_left, soReq_right, soResp_right, eoResp_right, eoReq_left,
soResp_left, eoReq_right, eoResp_left] (from S8,S11,S15,S17)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoResp_right,
eoReq_left, eoReq_right, eoResp_left] (from S7,S12,S15,S17)
//[soReq_left, soReq_right, soResp_right, eoResp_right, soResp_left,
eoReq_left, eoReq_right, eoResp_left] (from S8,S12,S15,S17)
//[soReq_left, soReq_right, eoReq_left, soResp_right, soResp_left,
eoResp_right, eoResp_left, eoReq_right] (from S3,S6,S10,S15,S18)
//[soReq_left, soReq_right, soResp_right, eoReq_left, soResp_left,
eoResp_right, eoResp_left, eoReq_right] (from S4,S6,S10,S15,S18)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoReq_left,
eoResp_right, eoResp_left, eoReq_right] (from S7,S10,S15,S18)
//[soReq_left, soReq_right, eoReq_left, soResp_right, eoResp_right,
soResp_left, eoResp_left, eoReq_right] (from S3,S6,S11,S15,S18)
//[soReq_left, soReq_right, soResp_right, eoReq_left, eoResp_right,
soResp_left, eoResp_left, eoReq_right] (from S4,S6,S11,S15,S18)
//[soReq_left, soReq_right, soResp_right, eoResp_right, eoReq_left,
soResp_left, eoResp_left, eoReq_right] (from S8,S11,S15,S18)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoResp_right,
eoReq_left, eoResp_left, eoReq_right] (from S7,S12,S15,S18)
//[soReq_left, soReq_right, soResp_right, eoResp_right, soResp_left,
eoReq_left, eoResp_left, eoReq_right] (from S8,S12,S15,S18)
//[soReq_left, soReq_right, soResp_right, soResp_left, eoResp_right,
eoResp_left, eoReq_left, eoReq_right] (from S7,s12,S16,S18)
//[soReq_left, soReq_right, soResp_right, eoResp_right, soResp_left,
eoResp_left, eoReq_left, eoReq_right] (from S8,S12,S16,,S18)
S19 = STOP
STOP = 0
//Repeat of the above without trace evolutions.
SRR-Channel/SRR Intermediary
----------------------------
Srr-Channel = !soReq_left.S1
//Receiving request
S1 = soReq_right.S2
+ channelFail_left.0
//Receiving and relaying request
S2 = !eoReq_left.S3
+ !soResp_right.S4
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relaying request
S3 = eoReq_right.S5
+ !soResp_right.S6
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Receiving and relaying request, receiving response
S4 = eoReq_left.S6
+ soResp_left.S7
+ !eoResp_right.S8
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and Relayed request
S5 = !soResp_right.S9
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relaying request, Receiving response
S6 = eoReq_right.S9
+ soResp_left.S10
+ !eoResp_right.S11
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Receiving and relaying request, receiving and relaying response
S7 = !eoReq_left.S10
+ !eoResp_right.S12
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Receiving and relaying request, received response
S8 = !eoReq_left.S11
+ soResp_left.S12
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relayed request, receiving response
S9 = soResp_left.S13
+ !eoResp_right.S14
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
// Received and relaying request, receiving and relaying response
S10 = eoReq_right.S13
+ !eoResp_right.S15
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relaying request, received response
S11 = eoReq_right.S14
+ soResp_left.S15
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Receiving and relaying request, received and relaying reponse
S12 = !eoReq_left.S15
+ eoResp_left.S16
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relayed request, receiving and relaying response
S13 = !eoResp_right.S17
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relayed request, received response
S14 = soResp_left.S17
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relaying request, received and relaying response
S15 = eoReq_right.S17
+ eoResp_left.S18
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Receiving and relaying request, received and relayed response
S16 = !eoReq_left.S18
+ channelFail_left.channelFail_right.0
+ channelFail_right.channelFail_left.0
//Received and relayed request, received and relaying response
S17 = eoResp_left.S19
+ channelFail_left.0
//Received and relaying request, received and relayed response
S18 = eoReq_right.S19
+ channelFail_right.0
//Received and relayed request, received and relayed response
S19 = STOP
STOP = 0
Attachments
- application/octet-stream attachment: wire_v_request_responder.zip
Received on Wednesday, 16 January 2002 12:01:46 UTC