checking and property based testing. As discussed earlier we are not using
property based testing. \GAST can communicate with the SUT via TCP or embedded
C code. In our setup we use TCP as the desired communication method between the
-SUT and the tool. In order to enable \GAST to communicate with our adapter (written in Python)
-we needed to slightly modify the \GAST source. The modified source is provided in combination with
-this paper.
+SUT and the tool. In order to enable \GAST to communicate with our adapter
+(written in Python)
+we needed to slightly modify the \GAST source. The modified source is provided
+with this report.
% Misschien hier iets over het feit dat we TCP gebruiken als communicatie
% 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{\GAST}
-Since \GAST requires a input enabled model, the actual specification is a bit different compared to the other tools.
-Luckily \GAST is capable of generating a graphical representation of the model from source.
+\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
\caption{Model generated by \GAST}\label{fig:model}
\end{figure}
-Because of the input enabled model it was necessary to include the \emph{ConnectionError} state.
+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}.
+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.
+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
\begin{lstlisting}[caption={Gast testOut.txt output}]
TODO: gast testOut.txt copy paste
\end{lstlisting}
-
-\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}