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

// Same as vERSION 4, except that the service primitives are changed. 

// same service property as in Figure (b) of course notes, but making it symmetric by allowing both sides to have both roles, Initiator and Responder.
//     in the case that both sides are initiator, there will be no indication nor response primitives.
property TCP_SERVICE = (reqA -> STARTA  | reqB -> STARTB),
         STARTA = (indB -> respB -> confA -> dataExchange -> END | reqB -> START),
         STARTB = (indA -> respA -> confB -> dataExchange -> END | reqA -> START),
         START = (confA -> confB -> GO | confB -> confA -> GO),
         GO = (dataExchange -> END).

A1 = (reqA -> sAsyn -> A_SYNSENT
     | rAsyn -> A_CHECK_USER),
   A_CHECK_USER = (indA -> respA -> sAacksyn -> A_SYNRECEIVED),
   A_SYNSENT = (rAacksyn -> confA -> sAack -> dataExchange -> END
          | rAsyn-> confA -> sAack -> A_SYNRECEIVED),
   A_SYNRECEIVED = (rAack -> dataExchange -> END).
     

   B1 = (reqB -> sBsyn -> B_SYNSENT
     | rBsyn -> B_CHECK_USER),
   B_CHECK_USER = (indB -> respB -> sBacksyn -> B_SYNRECEIVED),
   B_SYNSENT = (rBacksyn -> confB -> sBack -> dataExchange -> END
          | rBsyn -> confB -> 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.