From ac914c719d401c44cb2633127952b022bf563ff3 Mon Sep 17 00:00:00 2001
From: René den Hertog
Date: Thu, 26 Oct 2017 17:34:51 +0200
Subject: 'Bounded Retransmission Protocol' Blob

---
 assignments/assignment2/assignment2.tex | 104 ++++++++++++++++++++++++++++++++
 1 file changed, 104 insertions(+)

(limited to 'assignments/assignment2/assignment2.tex')

diff --git a/assignments/assignment2/assignment2.tex b/assignments/assignment2/assignment2.tex
index 9f843a7..65c6bbc 100644
--- a/assignments/assignment2/assignment2.tex
+++ b/assignments/assignment2/assignment2.tex
@@ -9,6 +9,11 @@
 \usepackage{cleveref}
 \usepackage{subfig}
 
+\usepackage{adjustbox}
+\usepackage{minted}
+
+\newenvironment{longlisting}{\captionsetup{type=listing}}{}
+
 \let\oldurl\url
 \def\url#1{{\small\oldurl{#1}}}
 
@@ -114,4 +119,103 @@
 
 \section{Bounded Retransmission Protocol}
 
+\subsection*{Q8}
+
+When running the learning system (a normal laptop computer and a common distribution of Linux) on the reference implementation with the default values for the settings of the random walk testing method to find counter examples, that is,
+\begin{minted}{java}
+    BasicLearner.randomWalk_chanceOfResetting = 0.1;
+    BasicLearner.randomWalk_numberOfSymbols = 300;
+\end{minted}
+it executes for about 5 minutes resulting in a final model \emph{without} the outputs \texttt{OCONF\_0} and \texttt{OCONF\_2}. \\
+When inspecting the visual form of the final model, we can see that most of the states only transition to another state on \emph{one} input, while ``looping" on itself on any \emph{other} input.
+See \texttt{Bounded Retransmission Protocol Tester/Out Put/Only "Reference.jar" With Default (300 : 0.1) Random Walk/Final Model Of Reference.pdf}.
+This leads to the state ``behaving'' almost like a ``dead end''.
+We call these states `stubborn'.
+Note that the resulting final model does differ from the real model, as some of the required outputs are missing.
+However, it is reasonable to assume that the models of the systems under test also include mostly stubborn states. \\
+In order to ``escape" stubborn states, the random walk must continuously try different inputs, until the ``escaping" input is chosen.
+Hence, we need to \emph{lower} the chance of resetting of the random walk to the initial state. \\
+
+When running the learning system on the reference implementation with the following settings,
+\begin{minted}{java}
+    BasicLearner.randomWalk_chanceOfResetting = 0.01;
+    BasicLearner.randomWalk_numberOfSymbols = 300;
+\end{minted}
+it executes for \emph{also} around 5 minutes \emph{as well as} resulting in a final model \emph{without} the outputs \texttt{OCONF\_0} and \texttt{OCONF\_2}. \\
+It is likely that the learning system requires a ``lengthier" testing method in order to result in the real model.
+Thus, we need to \emph{increase} the number of symbols random walk tries. \\
+
+When running the learning system on the reference implementation on the following settings,
+\begin{minted}{java}
+    BasicLearner.randomWalk_chanceOfResetting = 0.01;
+    BasicLearner.randomWalk_numberOfSymbols = 1001;
+\end{minted}
+it executes for \emph{30 minutes}. However, it definitely results in a final model containing \emph{all} the required outputs (\texttt{OCONF\_0}, \texttt{OCONF\_1} and \texttt{OCONF\_2}).
+Hence, we will use these last settings for the entire learning system. \\
+
+The learning system is ``backboned" by the Java program shown in listing \ref{L:BRPTM}.
+
+\subsection*{Q9}
+
+Only for the 5\textsuperscript{th} implementation did the learning system not result in a final model containing all the required outputs: it is missing \texttt{OCONF\_2}. \\
+
+One probable reason why this model is lacking outputs is simple: the implementation contains a fault which prevents it from ever outputting \texttt{OCONF\_2}. \\
+
+Another likely reason is the fact that random walk does not guarantee to show that a given hypothesis model differs from the real model.
+Due to the fact that a counter example may exist which is not found by this testing method.
+Either because the randomness lead it to not occur or because it contains more inputs than the current settings allow to ``visit''. \\
+The solution to this problem is changing the random walk parameters to test the given hypothesis more strictly.
+By lowering the chance of resetting and/or increasing the number of input symbols tried.
+Even though the 5\textsuperscript{th} final model may be different from the real model, we did not continue testing this implementation.
+Because the execution already took around 30 minutes and it is still possible that a bug in the implementation prevents \texttt{OCONF\_2} from even outputting. \\
+
+All the other implementations (Reference, 1, 2, 3, 4 and 6) resulted in final models which contained the required outputs \texttt{OCONF\_0}, \texttt{OCONF\_1} and \texttt{OCONF\_2}.
+
+\subsection*{Q10}
+
+\begin{adjustbox}{center, width=\textwidth}
+    \begin{tabular}{c|l}
+        \textbf{Implementation} & \textbf{Equivalent To Reference?}                              \\
+                                & (\textbf{Counter Example})                                     \\
+        \hline
+        \hline
+        1                       & No                                                             \\
+                                & \footnotesize{\verb|IREQ_0_0_0 ITIMEOUT|}                      \\
+        \hline
+        2                       & No                                                             \\
+                                & \footnotesize{
+            \verb|IREQ_0_0_0 ITIMEOUT ITIMEOUT ITIMEOUT ITIMEOUT ITIMEOUT|
+                                  } \\
+        \hline
+        3                       & Yes                                                            \\
+                                & -                                                              \\
+        \hline
+        4                       & No                                                             \\
+                                & \footnotesize{\verb|IREQ_0_0_0 IACK IACK|}                     \\
+        \hline
+        5                       & No                                                             \\
+                                & \footnotesize{
+            \verb|IREQ_0_0_0 IACK IACK ITIMEOUT ITIMEOUT ITIMEOUT ITIMEOUT ITIMEOUT ITIMEOUT|
+                                  } \\
+        \hline
+        6                       & No                                                             \\
+                                & \footnotesize{\verb|IREQ_0_0_1 IACK IACK|}
+    \end{tabular}
+\end{adjustbox}
+
+\pagebreak
+
+\appendix
+
+\section*{Source : Bounded Retransmission Protocol}
+
+\begin{longlisting}
+    \inputminted[fontsize=\footnotesize]
+                {java}
+                {Bounded Retransmission Protocol Tester/Source/Main.java}
+    \caption{
+            \texttt{Bounded Retransmission Protocol Tester} Learning System's \texttt{Main.java}
+    } \label{L:BRPTM}
+\end{longlisting}
+
 \end{document}
-- 
cgit v1.2.3

