/** TCP simplified - Example of a communication protocol (symmetric version)
 *  
 *  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) - for instance, "dMS_R" means disconnect message sent by right station.

// The communication system has two stations (one on the LEFT, one on the RIGHT), each including the functionality of an initiator and a responder (indicated by suffix _L and _R, respectively)


STATION_L = (cReq_L -> cMS_L -> I3_L | cMR_L -> cInd_L -> R5_L), 
       I3_L = (okMR_L -> cConf_L -> S9_L | nokMR_L -> cConfNeg_L -> STATION_L),   
       R5_L = (cResp_L -> okMS_L -> S9_L | cRespNeg_L -> nokMS_L -> STATION_L), 
       S9_L = (dMS_L -> STATION_L | dMR_L -> STATION_L). 

STATION_R  = (cReq_R -> cMS_R -> I3_R | cMR_R -> cInd_R -> R5_R), 
       I3_R = (okMR_R -> cConf_R -> S9_R | nokMR_R -> cConfNeg_R -> STATION_R),   
       R5_R = (cResp_R -> okMS_R -> S9_R | cRespNeg_R -> nokMS_R -> STATION_R),  
       S9_R = (dMS_R -> STATION_R | dMR_R -> STATION_R). 

// medium de communication from left to right
MLR = (cMS_L -> cMR_R -> MLR  | dMS_L -> dMR_R -> MLR   | 
       okMS_L -> okMR_R -> MLR | nokMS_L -> nokMR_R -> MLR). 

// medium de communication  from right to left 
MRL = (cMS_R -> cMR_L -> MRL  | dMS_R -> dMR_L -> MRL   | 
       okMS_R -> okMR_L -> MRL | nokMS_R -> nokMR_L -> MRL). 

||TCP_SYS = (STATION_L || STATION_R || MLR ||  MRL ).