From: pimjager <pim@pimjager.nl>
Date: Mon, 21 Dec 2015 11:05:26 +0000 (+0100)
Subject: spellcheck
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=4a4b1f6b4381b60d4aa2c27c2c859fc24e6c371f;p=tt2015.git

spellcheck
---

diff --git a/a3/2tools.tex b/a3/2tools.tex
index 9276002..1f4e61f 100644
--- a/a3/2tools.tex
+++ b/a3/2tools.tex
@@ -24,8 +24,9 @@ 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. 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
diff --git a/a3/4tests.tex b/a3/4tests.tex
index 126e7d6..e10cfb8 100644
--- a/a3/4tests.tex
+++ b/a3/4tests.tex
@@ -3,10 +3,25 @@
 % 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
@@ -14,14 +29,15 @@ Luckily \GAST is capable of generating a graphical representation of the model f
 	\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
@@ -31,17 +47,3 @@ 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}