18 :: State = Listen | ReceivedSYN | Established | Waiting | Closed
20 /* input (received from client) */
21 :: Input = InSYN | InACK | InRST | InFIN | InUserData
23 /* output (sent to client) */
24 :: Output = OutSYN | OutACK | OutFIN
26 /* state transitions */
27 stateTrans :: State Input -> [Trans Output State]
28 stateTrans Listen InSYN = [Pt [OutSYN, OutACK] ReceivedSYN]
29 stateTrans Listen _ = [Pt [] Listen]
31 stateTrans ReceivedSYN InRST = [Pt [] Listen]
32 stateTrans ReceivedSYN InACK = [Pt [] Established]
33 stateTrans ReceivedSYN _ = [Pt [] ReceivedSYN]
35 stateTrans Established InACK = [Pt [OutACK] Established]
36 stateTrans Established InUserData = [Pt [OutACK] Waiting]
37 stateTrans Established InFIN = [Pt [OutACK] Closed]
38 stateTrans Established _ = [Pt [] Established]
40 stateTrans Waiting InACK = [Pt [] Established]
41 stateTrans Waiting _ = [Pt [] Waiting]
43 /* invalid test implementation of SUT */
44 m0 :: Int Input -> ([Output], Int)
45 m0 0 InSYN = ([OutSYN, OutACK], 1)
48 Start world = testConfSM [] stateTrans Listen m0 0 (\_ . 0) world