/** TCP - symmetric version à la Wikipedia
 *  
 *  Gregor v. Bochmann, January 2015 */

// same service property as in Version 2
property TCP_SERVICE = (connectA -> STARTA  | connectB -> STARTB),
         STARTA = (dataExchange -> END | connectB -> START),
         STARTB = (dataExchange -> END | connectA -> START),
         START = (dataExchange -> END).

// The state diagram published in Wikipedia shows an additional alternative message to be received 
//      after having sent a sAsyn. 
//      The corresponding transition leads to the state in the responder behavior after the sending of the sBacksyn

A1 = (connectA -> sAsyn -> A_SYNSENT
     | rAsyn -> sAacksyn -> A_SYNRECEIVED),
   A_SYNSENT = (rAacksyn -> sAack -> dataExchange -> END
          | rAsyn -> sAacksyn -> A_SYNRECEIVED),
   A_SYNRECEIVED = (rAack -> dataExchange -> END).
     

B1 = (connectB -> sBsyn -> B_SYNSENT
     | rBsyn -> sBacksyn -> B_SYNRECEIVED),
   B_SYNSENT = (rBacksyn -> sBack -> dataExchange -> END
          | rBsyn -> sBacksyn -> B_SYNRECEIVED),
   B_SYNRECEIVED = (rBack -> dataExchange -> END).
     
// communifation medium, same as in Version 2
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
// CONCLUSION: there is probably a bug in the Wikipedia description of TCP, 
//      since TCP is well studied and any possibility of deadlock should have been eliminated by now.