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 = "127.0.0.1"
hostPort = 1203

/* states */
:: State = Listen | ReceivedSYN | Established | Waiting | Closed

/* input (received from client) */
:: Input = InSYN | InACK | InRST | InFIN | InUserData

instance toString Input where
	toString InSYN = "SYN"
	toString InACK = "ACK"
	toString InRST = "RST"
	toString InFIN = "FIN"
	toString InUserData = "DATA <some data here>"

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

toOutput :: String -> [Output]
toOutput "SYN-ACK" = [OutSYN, OutACK]
toOutput _ = []

/* state transitions */
stateTrans :: State Input -> [Trans Output State]
stateTrans Listen InSYN = [Pt [OutSYN, OutACK] ReceivedSYN]
stateTrans Listen _ = [Pt [] Listen]

stateTrans ReceivedSYN InRST = [Pt [] Listen]
stateTrans ReceivedSYN InACK = [Pt [] Established]
stateTrans ReceivedSYN _ = [Pt [] ReceivedSYN]

stateTrans Established InACK = [Pt [OutACK] Established]
stateTrans Established InUserData = [Pt [OutACK] Waiting]
stateTrans Established InFIN = [Pt [OutACK] Closed]
stateTrans Established _ = [Pt [] Established]

stateTrans Waiting InACK = [Pt [] Established]
stateTrans Waiting _ = [Pt [] Waiting]

/* 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)

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 [] stateTrans Listen adapter st reset console file
	/* close connection */
	/* close files */
	# (_, world) = fclose file world
	# (_, world) = fclose console world
	/* done */
	= world