/** 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

// Now we assume that A is initiator for estalishing and closing
A1 = (reqA -> sAsyn -> A_SYNSENT ),
   A_SYNSENT = (rAacksyn -> confA -> sAack -> A_ESTABLISHED),
   A_ESTABLISHED = (closeA -> sAfin -> A_FIN_WAIT_1),
   A_FIN_WAIT_1 = (rAack -> rAfin -> sAack -> A_TIME_WAIT),
   A_TIME_WAIT = (timeoutA -> A1).
     

   B1 = ( rBsyn -> B_CHECK_USER),
   B_CHECK_USER = (indB -> respB -> sBacksyn -> B_SYNRECEIVED),
   B_SYNRECEIVED = (rBack -> B_ESTABLISHED),
   B_ESTABLISHED = (rBfin -> sBack -> closeB -> sBfin -> rBack -> B1).
   
     
// communifation medium
MAB = (sAsyn -> rBsyn -> MAB |  sAack -> rBack -> MAB | sAfin -> rBfin -> MAB  ). 
MBA = ( sBacksyn -> rAacksyn -> MBA | sBack -> rAack -> MBA | sBfin -> rAfin -> MBA  ). 

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

||Check_Service = (TCP_SERVICE || SYSTEM).