module tcpmodel

import gast, TCPIP

derive bimap []
derive gEq State
derive gLess State
derive genShow State
derive ggen Input
derive genShow Input
derive gEq Output
derive genShow Output

/* connection settings */
hostIP = "192.168.0.14"
hostPort = 1203

/* states */
:: 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 | InDATA | InRST | InFIN

instance toString Input where
	toString InSYN = "SYN"
	toString InACK = "ACK"
	toString InRST = "RST"
	toString InFIN = "FIN"
	toString InDATA = "DATA"

/* output (sent to client) */
:: Output = OutSYN | OutACK | OutDATA | OutFIN

toOutput :: String -> [Output]
toOutput "SYN-ACK" = [OutSYN, OutACK]
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 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 InFIN = [Pt [OutACK] Closed]
stateTrans ReceivedSYN InDATA = [Pt [OutACK] 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 [] ConnectionError, Pt [OutACK] ConnectionError, Pt [OutDATA] ConnectionError]

stateTrans WaitClose InACK = [Pt [OutACK] Closed]
stateTrans WaitClose _ = [Pt [] ConnectionError]

/* sut state */
:: *SutState :== (StringSChannel, StringRChannel, *World)

/* adapter for SUT communication */
adapter :: *SutState Input -> ([Output], *SutState)
adapter (s, r, world) i
	# (s, world) = send (toString i) s world
	# (cmd, r, world) = receive r world
	= (toOutput cmd, (s, r, world))

/* reset SUT */
reset :: *SutState -> *SutState
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
	/* setup connection with adapter */
	# (Just adr, world) = lookupIPAddress hostIP world
	# (to, mcon, world) = connectTCP_MT Nothing (adr, hostPort) world
	| to <> TR_Success
		# console = console <<< "ERROR: can't connect to SUT!\n"
		# (_, world) = fclose console world
		= world
	# (Just con) = mcon
	/* open files */
	# (_, file, world) = fopen "testOut.txt" FWriteText world
	/* perform testing */
	# st = (toStringSChannel con.sChannel, toStringRChannel con.rChannel, world)
	# ((_, _, world), console, file) = testConfSM options stateTrans Listen adapter st reset console file
	/* close connection */
	/* close files */
	# (_, world) = fclose file world
	# (_, world) = fclose console world
	/* done */
	= world