% testcases, results and discussion on results:

% Write your model in the input language of the selected MBT tools, generate
%  tests, and execute
% them on your SUT. Explain your observations and analyse the test results.

\subsection{JTorX}
The model in itself was usable in JTorX since the model was written in
Graphviz' DOT language which is readable by JTorX. JTorX itself generates all
the testcases and after over $8000$ state changes we stopped the testing. There
are an infinite number of traces possible because there are several loops in
the model. The logfile generated by JTorX is $6.7MB$ long and contains indepth
detail about the trace. 

\begin{lstlisting}[caption={Last lines of JTorX' log saying the sut has passed}]
2015-12-20T21:17:32.370+0100 VERDICT 8500 pass
2015-12-20T21:17:32.370+0100 EOT 8500
2015-12-20T21:17:32.371+0100 LOG 8500 (tcpclient-label-Adapter) streamreader io exception: Socket closed
\end{lstlisting}

\subsection{\GAST}
\GAST requires an input enabled model, therefore the actual specification is a
bit different compared to the other tools. This model, generated by \GAST can be
seen in Figure~\ref{fig:model}.

\begin{figure}[H]
	\centering
	\includegraphics[scale=.75]{gast.eps}
	\caption{Model generated by \GAST}\label{fig:model}
\end{figure}

The \texttt{ConnectionError} state is added to make the model input enabled.
All inputs (packets sent from \emph{SUT}) which the original TCP specification 
deems illegal in a given state are redirected to this state which is also
defined as one of the final states together with \emph{Closed}.
When \GAST will end up in this state the SUT is reset and a new path is tried.

Because of time constraints we decided to allow \GAST to evaluate $9000$ paths.
None of the paths where rejected by \GAST. The output generated by \GAST is
listed below.

\begin{lstlisting}[caption={Gast commandline output}]
TODO: gast commandline output
\end{lstlisting}


\begin{lstlisting}[caption={Gast testOut.txt output}]
TODO: gast testOut.txt copy paste
\end{lstlisting}
