meer gast verhaal in verslag

diff --git a/a3/2tools.tex b/a3/2tools.tex
index cf69a51..9276002 100644 (file)
--- a/a3/2tools.tex
+++ b/a3/2tools.tex
@@ -24,6 +24,8 @@ functions. \GAST supports two different types of testing. Standard model
 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.
+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.
 
 % Misschien hier iets over het feit dat we TCP gebruiken als communicatie

diff --git a/a3/4tests.tex b/a3/4tests.tex
index 03d25b1..126e7d6 100644 (file)
--- a/a3/4tests.tex
+++ b/a3/4tests.tex
@@ -5,6 +5,33 @@
 % 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.
+
+\begin{figure}[H]
+       \centering
+       \includegraphics[scale=.75]{gast.eps}
+       \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. 
+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}
+
 \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

diff --git a/a3/code/tcpmodel.icl b/a3/code/tcpmodel.icl
index cf9cd89..4623b41 100644 (file)
--- a/a3/code/tcpmodel.icl
+++ b/a3/code/tcpmodel.icl
@@ -94,7 +94,7 @@ endstate :: [State] -> Bool
 endstate sts = isMember Closed sts || isMember ConnectionError sts
 
 /* testing options */
-options = [Nsequences 10000, Stop endstate]
+options = [Nsequences 9000, Stop endstate]
 
 /* testing program */
 Start world