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