/** TCP symmetric version - Version 2
 *  
 *  Gregor v. Bochmann, January 2015 */

// Here we have two identical stations, A and B, that both support the behavior of the Initiator and Responder.

// If we copy the Initiator and Responder behaviors from the simplified TCP version to both stations A and B,
//      we get a deadlock when both parties start with listen
// This can be corrected by eliminating the listen actions - then both parties are initially ready to accept a syn message
// therefore we have eliminated the listen interaction

// We state here the following service property:
//        dataExchange can only occur after a Connect has occured at one of the two stations, or on both: 
property TCP_SERVICE = (connectA -> STARTA  | connectB -> STARTB),
         STARTA = (dataExchange -> END | connectB -> START),
         STARTB = (dataExchange -> END | connectA -> START),
         START = (dataExchange -> END).

// both entities, A and B, play both roles: Initiator and Responder
A1 = (connectA -> sAsyn -> rAacksyn -> sAack -> dataExchange -> END
     | rAsyn -> sAacksyn -> rAack -> dataExchange -> END).

B1 = (connectB -> sBsyn -> rBacksyn -> sBack -> dataExchange -> END
     | rBsyn -> sBacksyn -> rBack -> dataExchange -> END).

// communifation medium (in this symmetric version, there are more messages in each direction)
MAB = (sAsyn -> rBsyn -> MAB | sAacksyn -> rBacksyn -> MAB | sAack -> rBack -> MAB). 
MBA = (sBsyn -> rAsyn -> MBA | sBacksyn -> rAacksyn -> MBA | sBack -> rAack -> MBA). 

// global system
||SYSTEM = (A1 || B1 || MAB || MBA).

||Check_Service = (TCP_SERVICE || SYSTEM).

// VERIFICATION RESULTS: Check_Service is OK, 
//      but Safety check shows that there is a deadlock when both parties start with their Connect operation