a4/question4.tex

   1 When checking the conformance of the learned models with the specification from
   2 assignment 3 some changes had to be made to the model from assignment 3. Since
   3 we could not detect timeouts we have replaced those with errors in the model
   4 and in the TCP adapter. Also we have removed the ability to open a new
   5 connection after closing a connection to simplify the model.
   6 Figure~\ref{fig:newTCPmodel} shows this new model.
   7
   8 \begin{figure}[H]
   9         \includegraphics[width=0.5\textwidth,natwidth=732,natheight=1016]{4newmodel.png}
  10         \caption{Simplified specification of TCP}
  11         \label{fig:newTCPmodel}
  12 \end{figure}
  13
  14 As was discussed in Section~\ref{sec:q2}, Learnlib does not support
  15 non determinism. However, since TCP is inherently non deterministic we have
  16 changed our adapter to be deterministic. Due to this determinism however none
  17 of the learned models are ioco-conforming to our specification. To accommodate
  18 for this more deterministic behaviour we need to update our specification
  19 slightly more. This updates specification can be seen in
  20 Figure~\ref{fig:newerTCPmodel}.
  21
  22 \begin{figure}[H]
  23         \includegraphics[width=0.5\textwidth,natwidth=710,natheight=1114]{4newermodel.png}
  24         \caption{Adapted simplified specification of TCP}
  25         \label{fig:newerTCPmodel}
  26 \end{figure}
  27
  28 When using JTorX to check the models learned with the full alphabet we see that
  29 these are ioco-conforming the the specification of
  30 Figure~\ref{fig:newerTCPmodel}. The models constructed with the smaller
  31 alphabets are not ioco-conforming as they miss required traces, such as:
  32 \texttt{SYN? . SYN-ACK! . RST?} which requires an output of \texttt{Reset!} but
  33 for both alphabets is not specified (which due to input completeness results in
  34 quiescence).
  35
  36 When restricting our specification to states reachable with inputs from the
  37 alphabet with which the model was learned (these models are trivially
  38 constructed by removing states form the model in Figure~\ref{fig:newerTCPmodel})
  39 then also these learned models are ioco-conforming to the (restricted)
  40 specifications.
  41