/** 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 is the final state for this property

A1 = (reqA -> sAsyn -> A_SYNSENT
     | rAsyn -> A_CHECK_USER),
   A_CHECK_USER = (indA -> respA -> sAacksyn -> A_SYNRECEIVED),
   A_SYNSENT = (rAacksyn -> confA -> sAack -> A_SYNRECEIVED
          | rAsyn-> confA -> sAack -> A_SYNRECEIVED),
   A_SYNRECEIVED = (rAack -> A_ESTABLISHED
          | closeA -> sAfin -> A_FIN_WAIT_1),
   A_ESTABLISHED = (rAfin -> sAack -> closeA -> sAfin -> rAack -> A1
          | closeA -> sAfin -> A_FIN_WAIT_1),
   A_FIN_WAIT_1 = (rAfin -> sAack -> rAack -> A_TIME_WAIT
         //  | rAfinack -> sAack -> A_TIME_WAIT
          | rAack -> rAfin -> sAack -> A_TIME_WAIT),
   A_TIME_WAIT = (timeoutA -> A1).
// there appears to be another error in the Wikipedia diagram. The message FIN+AK received in the state FIN WAIT 1 
//    is never sent by the other side.

// there appears to be another error also in the 1981 TCP state diagram: 
//    If the is simulaneous connection establishment from both sides, and 
//        both sides do a CLOSE from state SYN_RCVD, then there is no indication of the reception of the ack 
//                   which was send in the transition leading into the SYN_RCVD state.
// this problem is discovetred by the Safty Check of LTSA for the protocol specification given below.
     

   B1 = (reqB -> sBsyn -> B_SYNSENT
     | rBsyn -> B_CHECK_USER),
   B_CHECK_USER = (indB -> respB -> sBacksyn -> B_SYNRECEIVED),
   B_SYNSENT = (rBacksyn -> confB -> sBack -> B_SYNRECEIVED
          | rBsyn -> confB -> sBack -> B_SYNRECEIVED),
   B_SYNRECEIVED = (rBack -> B_ESTABLISHED
          | closeB -> sBfin -> B_FIN_WAIT_1),
   B_ESTABLISHED = (rBfin -> sBack -> closeB -> sBfin -> rBack -> B1
          | closeB -> sBfin -> B_FIN_WAIT_1),
   B_FIN_WAIT_1 = (rBfin -> sBack -> rBack -> B_TIME_WAIT
        //  | rBfinack -> sBack -> B_TIME_WAIT
          | rBack -> rBfin -> sBack -> B_TIME_WAIT),
   B_TIME_WAIT = (timeoutB -> B1).
     
// communifation medium
MAB = (sAsyn -> rBsyn -> MAB | sAacksyn -> rBacksyn -> MAB | sAack -> rBack -> MAB | sAfin -> rBfin -> MAB 
//   | sAfinack -> rBfinack -> MAB
   ). 
MBA = (sBsyn -> rAsyn -> MBA | sBacksyn -> rAacksyn -> MBA | sBack -> rAack -> MBA | sBfin -> rAfin -> MBA  
//    | sBfinack -> rAfinack -> 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.