/** 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

// telephone system with two stations (one on the LEFT, one on the RIGHT), each including an initiator and a responder

STATION_L = (cReq_L -> cMS_L -> I3_L | cMR_L -> cInd_L -> R5_L), 
       I3_L = (okMR_L -> cConf_L -> I9_L | nokMR_L -> cConfNeg_L -> STATION_L),   
       I9_L = (dMS_L -> dMR_L -> STATION_L | dMR_L -> dMS_L -> STATION_L), 

       R5_L = (cResp_L -> okMS_L -> R9_L | cRespNeg_L -> nokMS_L -> STATION_L),  
       R9_L = (dMS_L -> dMR_L -> STATION_L | dMR_L -> dMS_L -> STATION_L). 


STATION_R  = (cReq_R -> cMS_R -> I3_R | cMR_R -> cInd_R -> R5_R), 
       I3_R = (okMR_R -> cConf_R -> I9_R | nokMR_R -> cConfNeg_R -> STATION_R),   
       I9_R = (dMS_R -> dMR_R -> STATION_R | dMR_R -> dMS_R -> STATION_R), 

       R5_R = (cResp_R -> okMS_R -> R9_R | cRespNeg_R -> nokMS_R -> STATION_R),  
       R9_R = (dMS_R -> dMR_R -> STATION_R | dMR_R -> dMS_R -> STATION_R). 


// medium de communication for initiator on the left
MIL = (cMS_L -> cMR_R -> MIL  | dMS_L -> dMR_R -> MIL   | 
       okMS_R -> okMR_L -> MIL | nokMS_R -> nokMR_L -> MIL  | dMS_R -> dMR_L -> MIL). 

// medium de communication  for initiator on the rightft
MIR = (cMS_R -> cMR_L -> MIR  | dMS_R -> dMR_L -> MIR   | 
       okMS_L -> okMR_R -> MIR | nokMS_L -> nokMR_R -> MIR  | dMS_L -> dMR_R -> MIR). 

||TEL_SYS = (STATION_L || STATION_R || MIL ||  MIR).