In previous assignments our group has viewed the SUT as a stateful input-output
system. 

\subsection{Behaviour of the SUT}
When considering the behaviour of the SUT we will only consider it's behaviour 
with regards to correct input and output. In this case some models are more
fitting than others. 

\paragraph{Labeled Transition System} A Labeled Transition System (LTS) would 
be a fitting model for our SUT as the 
behaviour of TCP is such that a TCP client is in a certain state (connection 
closed, listening, connection established, etc.) and the TCP client transitions
between those states based upon input coming from another connected client.
In this case an LTS, would be a fitting model for our SUT. 

An LTS would not be a fitting model in case it would be desirable to model the
behaviour when wrong input (such as wrong sequence numbers) is given to the SUT.

\paragraph{Mealy Machines} 
Mealy Machines are a variant of LTS in which each label is a tuple of input
and output. This forces each state transition to consume both input and 
produce output. The model for the SUT (see Section~\ref{subsec:sut_model}) 
however contains state transitions with sequences of output which do not
require new input.

Due to this limitation Mealy Machines are not a very suitable model to model
the SUT. Instead we choose to model the SUT as a LTS. Since LTSs provide the 
functionality to express the desired properties of the SUT, that is, that the
SUT transitions through states depending on input as described in the TCP
specification and produces the output described by the TCP specification.