module tcpmodel

import gast

derive bimap []

derive gEq State
derive gLess State
derive genShow State

derive ggen Input
derive genShow Input

derive gEq Output
derive genShow Output

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

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

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

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

/* invalid test implementation of SUT */
m0 :: Int Input -> ([Output], Int)
m0 0 InSYN = ([OutSYN, OutACK], 1)
m0 n _ = ([], n)

Start world = testConfSM [] stateTrans Listen m0 0 (\_ . 0) world