a3/code/dotgen/tcpmodel.icl

   1 module tcpmodel
   2
   3 import gast, ESMSpec, Graphviz
   4
   5 derive bimap []
   6 derive gEq State
   7 derive gLess State
   8 derive genShow State
   9 derive ggen Input
  10 derive gEq Input
  11 derive genShow Input
  12 derive gEq Output
  13 derive genShow Output
  14
  15 /* connection settings */
  16 hostIP = "192.168.0.14"
  17 hostPort = 1203
  18
  19 /* states */
  20 :: State = Listen | ReceivedSYN | Established | Waiting | Closed | WaitClose | ConnectionError
  21
  22 instance render State where
  23         render Listen = "Listen"
  24         render ReceivedSYN = "Received SYN"
  25         render Established = "Established"
  26         render Waiting = "Waiting"
  27         render Closed = "Closed"
  28         render WaitClose = "Awaiting Close"
  29         render ConnectionError = "Connection Error"
  30
  31 /* input (received from client) */
  32 :: Input = InSYN | InACK | InDATA | InRST | InFIN
  33
  34 instance render Input where
  35         render InSYN = "SYN"
  36         render InACK = "ACK"
  37         render InDATA = "DATA"
  38         render InRST = "RST"
  39         render InFIN = "FIN"
  40
  41 /* output (sent to client) */
  42 :: Output = OutSYN | OutACK | OutDATA | OutFIN
  43
  44 instance render Output where
  45         render OutSYN = "SYN"
  46         render OutACK = "ACK"
  47         render OutDATA = "DATA"
  48         render OutFIN = "FIN"
  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 stateTrans Closed _ = [Pt [] Closed]
  77 stateTrans ConnectionError _ = [Pt [] ConnectionError]
  78
  79 /* state machine thingy */
  80 esm :: ESM State Input Output
  81 esm = {s_0 = Listen, d_F = stateTrans, out = \_ _ . [], pred = \_ . []}
  82
  83 /* build transitions */
  84 automaton = addTransitions 50 esm [Listen] [InSYN] {trans = [], issues = []}
  85
  86 /* build graph */
  87 graph = mkDigraph "TCPModel" (automaton, Listen, [], [Closed,ConnectionError], [], [])
  88
  89 /* write list of strings to file */
  90 instance <<< [String] where
  91         (<<<) file [] = file
  92         (<<<) file [x:xs] = file <<< x <<< xs
  93
  94 /* testing program */
  95 Start world
  96         # (_, file, world) = fopen "graph.dot" FWriteText world
  97         # file = file <<< printDigraph graph
  98         # (_, world) = fclose file world
  99         = world
 100