From: pimjager Date: Wed, 27 Jan 2016 00:13:41 +0000 (+0100) Subject: Question 4 answered X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=556e4662a10985ad185d8f20bf2eaca516924ab4;p=tt2015.git Question 4 answered --- diff --git a/a4/4newermodel.png b/a4/4newermodel.png new file mode 100644 index 0000000..efd8995 Binary files /dev/null and b/a4/4newermodel.png differ diff --git a/a4/4newmodel.png b/a4/4newmodel.png new file mode 100644 index 0000000..e5e44f1 Binary files /dev/null and b/a4/4newmodel.png differ diff --git a/a4/question4.tex b/a4/question4.tex index e69de29..3d3bc39 100644 --- 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. + diff --git a/a4/tcp/tcp_model.graphml b/a4/tcp/tcp_model.graphml index 0810f57..d896b82 100644 --- a/a4/tcp/tcp_model.graphml +++ b/a4/tcp/tcp_model.graphml @@ -93,10 +93,10 @@ - + - Established + Established' @@ -110,10 +110,10 @@ - + - Established' + Syn recv'' @@ -125,12 +125,49 @@ + - + - Syn recv'' + CloseWait + + + + + + + + + + + + + + + + + + Last ACK + + + + + + + + + + + + + + + + + + Data @@ -182,7 +219,7 @@ - + @@ -202,77 +239,75 @@ - + - + - ACK? + ERR! - + - + - + - + - ERR! + SYN? - + - + - + - - - - + + - SYN? + Reset! - + - - + + - + - ERR! + ACK? - + @@ -280,17 +315,18 @@ - + + - Reset! + FIN? - + @@ -298,14 +334,14 @@ - + - ACK? + ACK! @@ -317,6 +353,48 @@ + + + + + + + + + + DAT? + + + + + + + + + + + + + + + + + + + + + ACK! + + + + + + + + + + + diff --git a/a4/tcp/tcp_model_det.graphml b/a4/tcp/tcp_model_det.graphml new file mode 100644 index 0000000..4d9bff0 --- /dev/null +++ b/a4/tcp/tcp_model_det.graphml @@ -0,0 +1,454 @@ + + + + + + + + + + + + + + + + + + + + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + Listen + + + + + + + + + + + + + + + + + Syn Recv' + + + + + + + + + + + + + + + + + Syn Recv + + + + + + + + + + + + + + + + + Established' + + + + + + + + + + + + + + + + + Syn recv'' + + + + + + + + + + + + + + + + + CloseWait + + + + + + + + + + + + + + + + + Last ACK + + + + + + + + + + + + + + + + + Data + + + + + + + + + + + + + + + + + + Esablished + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + SYN-ACK! + + + + + + + + + + + + + + + + + + + + RST? + + + + + + + + + + + + + + + + + + + + ERR! + + + + + + + + + + + + + + + + + + + + SYN? + + + + + + + + + + + + + + + + + + Reset! + + + + + + + + + + + + + + + + + + FIN? + + + + + + + + + + + + + + + + + + ACK! + + + + + + + + + + + + + + + + + + + + DAT? + + + + + + + + + + + + + + + + + + + + ACK! + + + + + + + + + + + + + + + + + + + DAT? + + + + + + + + + + + + + + + + + + + ACK! + + + + + + + + + + + + + + + + + + + + + DATA! + + + + + + + + + + + + + + + + diff --git a/a4/tcp/tcp_model_part.graphml b/a4/tcp/tcp_model_part.graphml new file mode 100644 index 0000000..d99558f --- /dev/null +++ b/a4/tcp/tcp_model_part.graphml @@ -0,0 +1,178 @@ + + + + + + + + + + + + + + + + + + + + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + Listen + + + + + + + + + + + + + + + + + Syn Recv' + + + + + + + + + + + + + + + + + Syn Recv + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + SYN-ACK! + + + + + + + + + + + + + + + + + + + + ERR! + + + + + + + + + + + + + + + + + + + + SYN? + + + + + + + + + + + + + + + + diff --git a/a4/tt4.tex b/a4/tt4.tex index a9ec7f3..c1bc678 100644 --- a/a4/tt4.tex +++ b/a4/tt4.tex @@ -7,7 +7,7 @@ \section{Question 1} \input{question1.tex} -\section{Question 2} +\section{Question 2} \label{sec:q2} \input{question2.tex} \section{Question 3} @@ -17,7 +17,7 @@ \input{question4.tex} \appendix -\section{Models} +\section{Models} \label{app:models} \input{models.tex} \nocite{*}