/** Telephone call - Example of communication protocol
 *  
 *  Gregor v. Bochmann, January 2009 */

// Note: instead of using "implied reception", we consider a non-specified reception to be an error.

// Initiator I, Responder R : state 1 is idle, state 9 is connected
// Connect request, indication, response (Negative), confirmation (Negative)
// Connect, OK, NOK messages: sending and reception

I1 = (cReq -> cMS -> I3 // | {okMR, nokMR} -> ERROR
       ),  I3 = (okMR -> cConf -> I9 | nokMR -> cConfNeg -> I1 // | {cReq} -> ERROR
       ),  I9 = (dMS -> dMR -> I1 | dMR -> dMS -> I1). 

R1 = (cMR -> cInd -> R5 // | {cResp, cRespNeg} -> ERROR
       ),  R5 = (cResp -> okMS -> R9 | cRespNeg -> nokMS -> R1 // | {cMR} -> ERROR
       ),  R9 = (dMS -> dMR -> R1 | dMR -> dMS -> 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). 

// telephone system with an initiator and a responder: this means arbitrary interactions with the ENVIRONMENT
// ||TELSYS = (I1 || R1 || MIR || MRI).

// telephone system with two stations, each including an initiator and a responder
const Left = 0  const Right = 1
range Both = Left .. Right
||STATION = (I1 || R1).
||MEDIUM = (MIR || MRI).
||TELSYS = ( station[Both] : STATION || medium[Both] : MEDIUM ).  


// 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 = (TELSYS || USERI || USERR).