final

[tt2015.git] / a3 / code / tcpmodel.icl

diff --git a/a3/code/tcpmodel.icl b/a3/code/tcpmodel.icl
index 439dde8..4623b41 100644 (file)
--- a/a3/code/tcpmodel.icl
+++ b/a3/code/tcpmodel.icl
@@ -12,45 +12,66 @@ derive gEq Output
 derive genShow Output
 
 /* connection settings */
-hostIP = "127.0.0.1"
+hostIP = "192.168.0.14"
 hostPort = 1203
 
 /* states */
-:: State = Listen | ReceivedSYN | Established | Waiting | Closed
+:: State = Listen | ReceivedSYN | Established | Waiting | Closed | WaitClose | ConnectionError
+
+instance == State where
+       (==) Listen Listen = True
+       (==) ReceivedSYN ReceivedSYN = True
+       (==) Established Established = True
+       (==) Waiting Waiting = True
+       (==) Closed Closed = True
+       (==) WaitClose WaitClose = True
+       (==) ConnectionError ConnectionError = True
+       (==) _ _ = False
 
 /* input (received from client) */
-:: Input = InSYN | InACK | InRST | InFIN | InUserData
+:: Input = InSYN | InACK | InDATA | InRST | InFIN
 
 instance toString Input where
        toString InSYN = "SYN"
        toString InACK = "ACK"
        toString InRST = "RST"
        toString InFIN = "FIN"
-       toString InUserData = "DATA <some data here>"
+       toString InDATA = "DATA"
 
 /* output (sent to client) */
-:: Output = OutSYN | OutACK | OutFIN
+:: Output = OutSYN | OutACK | OutDATA | OutFIN
 
 toOutput :: String -> [Output]
 toOutput "SYN-ACK" = [OutSYN, OutACK]
-toOutput _ = []
+toOutput "ACK" = [OutACK]
+toOutput "DATA" = [OutDATA]
+toOutput "TO" = []
 
 /* state transitions */
 stateTrans :: State Input -> [Trans Output State]
 stateTrans Listen InSYN = [Pt [OutSYN, OutACK] ReceivedSYN]
-stateTrans Listen _ = [Pt [] Listen]
+stateTrans Listen InFIN = [Pt [] ConnectionError]
+stateTrans Listen InACK = [Pt [] ConnectionError]
+stateTrans Listen InDATA = [Pt [] ConnectionError]
+stateTrans Listen InRST = [Pt [] ConnectionError]
 
+stateTrans ReceivedSYN InSYN = [Pt [OutSYN,OutACK] ConnectionError]
 stateTrans ReceivedSYN InRST = [Pt [] Listen]
 stateTrans ReceivedSYN InACK = [Pt [] Established]
-stateTrans ReceivedSYN _ = [Pt [] ReceivedSYN]
+stateTrans ReceivedSYN InFIN = [Pt [OutACK] Closed]
+stateTrans ReceivedSYN InDATA = [Pt [OutACK] Established]
 
-stateTrans Established InACK = [Pt [OutACK] Established]
-stateTrans Established InUserData = [Pt [OutACK] Waiting]
-stateTrans Established InFIN = [Pt [OutACK] Closed]
-stateTrans Established _ = [Pt [] Established]
+stateTrans Established InSYN = [Pt [] ConnectionError, Pt [OutACK] ConnectionError, Pt [OutDATA] ConnectionError] // connection error returns whatever it wants?
+stateTrans Established InDATA = [Pt [OutACK] Waiting, Pt [OutDATA] Established, Pt [] Established] // last one resend?
+stateTrans Established InRST = [Pt [] ConnectionError, Pt [OutACK] ConnectionError, Pt [OutDATA] ConnectionError] // connection error returns whatever it wants?
+stateTrans Established InFIN = [Pt [OutACK] Closed, Pt [] WaitClose]
+stateTrans Established InACK = [Pt [] ConnectionError]
 
 stateTrans Waiting InACK = [Pt [] Established]
-stateTrans Waiting _ = [Pt [] Waiting]
+stateTrans Waiting _ = [Pt [] ConnectionError, Pt [OutACK] ConnectionError, Pt [OutDATA] ConnectionError]
+
+stateTrans WaitClose InACK = [Pt [OutACK] Closed]
+stateTrans WaitClose _ = [Pt [] ConnectionError]
 
 /* sut state */
 :: *SutState :== (StringSChannel, StringRChannel, *World)
@@ -68,6 +89,14 @@ reset (s, r, world)
        # (s, world) = send "SUT-RESET" s world
        = (s, r, world)
 
+/* all endstates */
+endstate :: [State] -> Bool
+endstate sts = isMember Closed sts || isMember ConnectionError sts
+
+/* testing options */
+options = [Nsequences 9000, Stop endstate]
+
+/* testing program */
 Start world
        /* open console */
        # (console, world) = stdio world
@@ -83,7 +112,7 @@ Start world
        # (_, file, world) = fopen "testOut.txt" FWriteText world
        /* perform testing */
        # st = (toStringSChannel con.sChannel, toStringRChannel con.rChannel, world)
-       # ((_, _, world), console, file) = testConfSM [] stateTrans Listen adapter st reset console file
+       # ((_, _, world), console, file) = testConfSM options stateTrans Listen adapter st reset console file
        /* close connection */
        /* close files */
        # (_, world) = fclose file world