When checking the conformance of the learned models with the specification from 
assignment 3 some changes had to be made to the model from assignment 3. Since
we could not detect timeouts we have replaced those with errors in the model 
and in the TCP adapter. Also we have removed the ability to open a new 
connection after closing a connection to simplify the model. 
Figure~\ref{fig:newTCPmodel} shows this new model. 

\begin{figure}[H]
	\includegraphics[width=0.5\textwidth,natwidth=732,natheight=1016]{4newmodel.png} 
	\caption{Simplified specification of TCP}
	\label{fig:newTCPmodel}
\end{figure}

As was discussed in Section~\ref{sec:q2}, Learnlib does not support 
non determinism. However, since TCP is inherently non deterministic we have
changed our adapter to be deterministic. Due to this determinism however none
of the learned models are ioco-conforming to our specification. To accommodate 
for this more deterministic behaviour we need to update our specification 
slightly more. This updates specification can be seen in 
Figure~\ref{fig:newerTCPmodel}.

\begin{figure}[H]
	\includegraphics[width=0.5\textwidth,natwidth=710,natheight=1114]{4newermodel.png} 
	\caption{Adapted simplified specification of TCP}
	\label{fig:newerTCPmodel}
\end{figure}

When using JTorX to check the models learned with the full alphabet we see that
these are ioco-conforming the the specification of 
Figure~\ref{fig:newerTCPmodel}. The models constructed with the smaller
alphabets are not ioco-conforming as they miss required traces, such as:
\texttt{SYN? . SYN-ACK! . RST?} which requires an output of \texttt{Reset!} but
for both alphabets is not specified (which due to input completeness results in
quiescence). 

When restricting our specification to states reachable with inputs from the 
alphabet with which the model was learned (these models are trivially 
constructed by removing states form the model in Figure~\ref{fig:newerTCPmodel})
then also these learned models are ioco-conforming to the (restricted) 
specifications.

