Question 4 answered

[tt2015.git] / a4 / question4.tex

diff --git a/a4/question4.tex b/a4/question4.tex
index e69de29..3d3bc39 100644 (file)
--- a/a4/question4.tex
+++ b/a4/question4.tex
@@ -0,0 +1,41 @@
+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.
+