/** TCP s implified - Example of communication protocol (asymmetric version: one initiator and one responder protocol entity) * * Gregor v. Bochmann, January 2009 */ // Note: this example corresponds to the section "A communication protocol (de type TCP) - an example of reachability analysis" in the course notes of the chapter on "Communicating state machines" // Initiator I, Responder R : state 1 is idle, state 9 is connected // Service primitives: Connect request (cReq), indication (cInd), response positive (cResp) -negative (cRespNeg), confirmation positive (cConf) - negative (cConfNeg) // Protocol messages: Connect-request (cM), OK (okM), NOK (nokM), disconnect (dM): sending (suffix S) and reception (suffix R) I1 = (cReq -> cMS -> I3 // | {okMR, nokMR} -> ERROR ), I3 = (okMR -> cConf -> I9 | nokMR -> cConfNeg -> I1 // | {cReq} -> ERROR ), I9 = (dMS -> I1 | dMR -> I1). R1 = (cMR -> cInd -> R5 // | {cResp, cRespNeg} -> ERROR ), R5 = (cResp -> okMS -> R9 | cRespNeg -> nokMS -> R1 // | {cMR} -> ERROR ), R9 = (dMS -> R1 | dMR -> R1). // medium de communication de I vers R MIR = (cMS -> cMR -> MIR | dMS -> dMR -> MIR). // medium de communication de R vers I MRI = (okMS -> okMR -> MRI | nokMS -> nokMR -> MRI | dMS -> dMR -> MRI). // The communication system with an initiator and a responder: this means arbitrary interactions with the ENVIRONMENT ||TCPSYS = (I1 || R1 || MIR || MRI). // let us put two users as the ENVIRONMENT; USERI is the initiator, USERR the responder. // USERI = (cReq -> WAIT), WAIT = (cConf -> USERI | cConfNeg -> USERI). // USERR = (cInd -> ANSWER), ANSWER = (cResp -> USERR | cRespNeg -> USERR). // this is the system with the two users // ||ALL = (TCPSYS || USERI || USERR).