/** TCP simplified
 *  
 *  Gregor v. Bochmann, January 2015 */

// we state here the following service property:
//  dataExchange can only occur after Listen and Connect have occurred (in any order). 
property TCP_SERVICE = (listen -> TS2  |  connect -> TS3),
TS2 = (connect -> TS4),
TS3 = (listen -> TS4),
TS4 = (dataExchange -> END).

// behavior of INITIATOR protocol entity:
I1 = (connect -> sIsyn -> rIacksyn -> sIack -> dataExchange -> END).

// behavior of RESPONDER protocol entity:
R1 = (listen -> rRsyn -> sRacksyn -> rRack -> dataExchange -> END).

// communifation medium: MIR from Initiator to Responder - MRI from Responder to Initiator
// assumption: at most one message in transit at any given time.
MIR = (sIsyn -> rRsyn -> MIR | sIack -> rRack -> MIR). 
MRI = (sRacksyn -> rIacksyn -> MRI). 
// MIR = (sIsyn -> rRsyn -> MIR | sIacksyn -> rRacksyn -> MIR | sIack -> rRack -> MIR). 
// MRI = (sRsyn -> rIsyn -> MRI | sRacksyn -> rIacksyn -> MRI | sRack -> rIack -> MRI). 

// global system
||SYSTEM = (I1 || R1 || MIR || MRI).

||Check_Service = (SYSTEM || TCP_SERVICE).