a3/code/tcpmodel.icl

   1 module tcpmodel
   2
   3 import gast
   4
   5 derive bimap []
   6
   7 derive gEq State
   8 derive gLess State
   9 derive genShow State
  10
  11 derive ggen Input
  12 derive genShow Input
  13
  14 derive gEq Output
  15 derive genShow Output
  16
  17 /* states */
  18 :: State = Listen | ReceivedSYN | Established | Waiting | Closed
  19
  20 /* input (received from client) */
  21 :: Input = InSYN | InACK | InRST | InFIN | InUserData
  22
  23 /* output (sent to client) */
  24 :: Output = OutSYN | OutACK | OutFIN
  25
  26 /* state transitions */
  27 stateTrans :: State Input -> [Trans Output State]
  28 stateTrans Listen InSYN = [Pt [OutSYN, OutACK] ReceivedSYN]
  29 stateTrans Listen _ = [Pt [] Listen]
  30
  31 stateTrans ReceivedSYN InRST = [Pt [] Listen]
  32 stateTrans ReceivedSYN InACK = [Pt [] Established]
  33 stateTrans ReceivedSYN _ = [Pt [] ReceivedSYN]
  34
  35 stateTrans Established InACK = [Pt [OutACK] Established]
  36 stateTrans Established InUserData = [Pt [OutACK] Waiting]
  37 stateTrans Established InFIN = [Pt [OutACK] Closed]
  38 stateTrans Established _ = [Pt [] Established]
  39
  40 stateTrans Waiting InACK = [Pt [] Established]
  41 stateTrans Waiting _ = [Pt [] Waiting]
  42
  43 /* invalid test implementation of SUT */
  44 m0 :: Int Input -> ([Output], Int)
  45 m0 0 InSYN = ([OutSYN, OutACK], 1)
  46 m0 n _ = ([], n)
  47
  48 Start world = testConfSM [] stateTrans Listen m0 0 (\_ . 0) world