a3/code/tcpmodel.icl

   1 module tcpmodel
   2
   3 import gast, TCPIP
   4
   5 derive bimap []
   6 derive gEq State
   7 derive gLess State
   8 derive genShow State
   9 derive ggen Input
  10 derive genShow Input
  11 derive gEq Output
  12 derive genShow Output
  13
  14 /* connection settings */
  15 hostIP = "192.168.0.14"
  16 hostPort = 1203
  17
  18 /* states */
  19 :: State = Listen | ReceivedSYN | Established | Waiting | Closed | WaitClose | ConnectionError
  20
  21 instance == State where
  22         (==) Listen Listen = True
  23         (==) ReceivedSYN ReceivedSYN = True
  24         (==) Established Established = True
  25         (==) Waiting Waiting = True
  26         (==) Closed Closed = True
  27         (==) WaitClose WaitClose = True
  28         (==) ConnectionError ConnectionError = True
  29         (==) _ _ = False
  30
  31 /* input (received from client) */
  32 :: Input = InSYN | InACK | InDATA | InRST | InFIN
  33
  34 instance toString Input where
  35         toString InSYN = "SYN"
  36         toString InACK = "ACK"
  37         toString InRST = "RST"
  38         toString InFIN = "FIN"
  39         toString InDATA = "DATA"
  40
  41 /* output (sent to client) */
  42 :: Output = OutSYN | OutACK | OutDATA | OutFIN
  43
  44 toOutput :: String -> [Output]
  45 toOutput "SYN-ACK" = [OutSYN, OutACK]
  46 toOutput "ACK" = [OutACK]
  47 toOutput "DATA" = [OutDATA]
  48 toOutput "TO" = []
  49
  50 /* state transitions */
  51 stateTrans :: State Input -> [Trans Output State]
  52 stateTrans Listen InSYN = [Pt [OutSYN, OutACK] ReceivedSYN]
  53 stateTrans Listen InFIN = [Pt [] ConnectionError]
  54 stateTrans Listen InACK = [Pt [] ConnectionError]
  55 stateTrans Listen InDATA = [Pt [] ConnectionError]
  56 stateTrans Listen InRST = [Pt [] ConnectionError]
  57
  58 stateTrans ReceivedSYN InSYN = [Pt [OutSYN,OutACK] ConnectionError]
  59 stateTrans ReceivedSYN InRST = [Pt [] Listen]
  60 stateTrans ReceivedSYN InACK = [Pt [] Established]
  61 stateTrans ReceivedSYN InFIN = [Pt [OutACK] Closed]
  62 stateTrans ReceivedSYN InDATA = [Pt [OutACK] Established]
  63
  64 stateTrans Established InSYN = [Pt [] ConnectionError, Pt [OutACK] ConnectionError, Pt [OutDATA] ConnectionError] // connection error returns whatever it wants?
  65 stateTrans Established InDATA = [Pt [OutACK] Waiting, Pt [OutDATA] Established, Pt [] Established] // last one resend?
  66 stateTrans Established InRST = [Pt [] ConnectionError, Pt [OutACK] ConnectionError, Pt [OutDATA] ConnectionError] // connection error returns whatever it wants?
  67 stateTrans Established InFIN = [Pt [OutACK] Closed, Pt [] WaitClose]
  68 stateTrans Established InACK = [Pt [] ConnectionError]
  69
  70 stateTrans Waiting InACK = [Pt [] Established]
  71 stateTrans Waiting _ = [Pt [] ConnectionError, Pt [OutACK] ConnectionError, Pt [OutDATA] ConnectionError]
  72
  73 stateTrans WaitClose InACK = [Pt [OutACK] Closed]
  74 stateTrans WaitClose _ = [Pt [] ConnectionError]
  75
  76 /* sut state */
  77 :: *SutState :== (StringSChannel, StringRChannel, *World)
  78
  79 /* adapter for SUT communication */
  80 adapter :: *SutState Input -> ([Output], *SutState)
  81 adapter (s, r, world) i
  82         # (s, world) = send (toString i) s world
  83         # (cmd, r, world) = receive r world
  84         = (toOutput cmd, (s, r, world))
  85
  86 /* reset SUT */
  87 reset :: *SutState -> *SutState
  88 reset (s, r, world)
  89         # (s, world) = send "SUT-RESET" s world
  90         = (s, r, world)
  91
  92 /* all endstates */
  93 endstate :: [State] -> Bool
  94 endstate sts = isMember Closed sts || isMember ConnectionError sts
  95
  96 /* testing options */
  97 options = [Nsequences 10000, Stop endstate]
  98
  99 /* testing program */
 100 Start world
 101         /* open console */
 102         # (console, world) = stdio world
 103         /* setup connection with adapter */
 104         # (Just adr, world) = lookupIPAddress hostIP world
 105         # (to, mcon, world) = connectTCP_MT Nothing (adr, hostPort) world
 106         | to <> TR_Success
 107                 # console = console <<< "ERROR: can't connect to SUT!\n"
 108                 # (_, world) = fclose console world
 109                 = world
 110         # (Just con) = mcon
 111         /* open files */
 112         # (_, file, world) = fopen "testOut.txt" FWriteText world
 113         /* perform testing */
 114         # st = (toStringSChannel con.sChannel, toStringRChannel con.rChannel, world)
 115         # ((_, _, world), console, file) = testConfSM options stateTrans Listen adapter st reset console file
 116         /* close connection */
 117         /* close files */
 118         # (_, world) = fclose file world
 119         # (_, world) = fclose console world
 120         /* done */
 121         = world
 122