\section{Modeling TCP}
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, in which the interactions would be initiated by the
remote client, 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 an extension of LTS in which each label is a tuple of input
and output. For our SUT this means that is is not just possible to model the
behaviour of the SUT regarding its internal state, but also its behaviour 
regarding its output. 

For simplicity however we have chosen to model the SUT with the assumption that
it is only handed correct input and will then generate correct output (assuming 
that the internal state transition function is correct). Therefore the extra
functionality provided by modeling our SUT as a Mealy Machine is not necessary.