/** TCP according to the original specification of 1981 - see  https://www.ietf.org/rfc/rfc793.txt
 *  
 *  Gregor v. Bochmann, January 2015 */

// There is a small difference with the state diagram of Wikipedia for the case that both parties play the responder role

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

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

   B1 = (connectB -> sBsyn -> B_SYNSENT
     | rBsyn -> sBacksyn -> B_SYNRECEIVED),
   B_SYNSENT = (rBacksyn -> sBack -> dataExchange -> END
          | rBsyn -> sBack -> B_SYNRECEIVED),
   B_SYNRECEIVED = (rBack -> dataExchange -> END).
     
// communifation medium
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).

// CONCLUSION: TCP has no deadlock and the description in Wikipedia is erroneous.