diff options
| -rw-r--r-- | assignments/assignment2/.latexmkrc | 2 | ||||
| -rw-r--r-- | assignments/assignment2/LStar_hypothesis5.dot | 66 | ||||
| -rw-r--r-- | assignments/assignment2/LStar_hypothesis6.dot | 72 | ||||
| l---------[-rw-r--r--] | assignments/assignment2/LStar_learnedModel.dot | 61 | ||||
| -rw-r--r-- | assignments/assignment2/assignment2.tex | 50 |
5 files changed, 178 insertions, 73 deletions
diff --git a/assignments/assignment2/.latexmkrc b/assignments/assignment2/.latexmkrc index a5c2a05..4eed047 100644 --- a/assignments/assignment2/.latexmkrc +++ b/assignments/assignment2/.latexmkrc @@ -2,7 +2,7 @@ $pdflatex = 'internal pdflatexwithdot %R %O %S'; sub pdflatexwithdot { - for (my $i = 0; $i <= 4; $i++) { + for (my $i = 0; $i <= 6; $i++) { system("dot -Tpng LStar_hypothesis" . $i . ".dot > LStar_hypothesis" . $i . ".png"); } return system("pdflatex -shell-escape @_"); diff --git a/assignments/assignment2/LStar_hypothesis5.dot b/assignments/assignment2/LStar_hypothesis5.dot new file mode 100644 index 0000000..fd9f681 --- /dev/null +++ b/assignments/assignment2/LStar_hypothesis5.dot @@ -0,0 +1,66 @@ +digraph g { +__start0 [label="" shape="none"]; + + s0 [shape="circle" label="0"]; + s1 [shape="circle" label="1"]; + s2 [shape="circle" label="2"]; + s3 [shape="circle" label="3"]; + s4 [shape="circle" label="4"]; + s5 [shape="circle" label="5"]; + s6 [shape="circle" label="6"]; + s7 [shape="circle" label="7"]; + s8 [shape="circle" label="8"]; + s9 [shape="circle" label="9"]; + s0 -> s7 [label="5ct / OK"]; + s0 -> s1 [label="10ct / OK"]; + s0 -> s0 [label="mars / NOK"]; + s0 -> s0 [label="snickers / NOK"]; + s0 -> s0 [label="twix / NOK"]; + s1 -> s2 [label="5ct / OK"]; + s1 -> s4 [label="10ct / OK"]; + s1 -> s0 [label="mars / OK"]; + s1 -> s1 [label="snickers / NOK"]; + s1 -> s1 [label="twix / NOK"]; + s2 -> s4 [label="5ct / OK"]; + s2 -> s3 [label="10ct / OK"]; + s2 -> s7 [label="mars / OK"]; + s2 -> s2 [label="snickers / NOK"]; + s2 -> s0 [label="twix / OK"]; + s3 -> s6 [label="5ct / OK"]; + s3 -> s9 [label="10ct / OK"]; + s3 -> s2 [label="mars / OK"]; + s3 -> s0 [label="snickers / OK"]; + s3 -> s1 [label="twix / OK"]; + s4 -> s3 [label="5ct / OK"]; + s4 -> s6 [label="10ct / OK"]; + s4 -> s1 [label="mars / OK"]; + s4 -> s4 [label="snickers / NOK"]; + s4 -> s7 [label="twix / OK"]; + s5 -> s5 [label="5ct / NOK"]; + s5 -> s5 [label="10ct / NOK"]; + s5 -> s6 [label="mars / OK"]; + s5 -> s2 [label="snickers / OK"]; + s5 -> s3 [label="twix / OK"]; + s6 -> s8 [label="5ct / OK"]; + s6 -> s5 [label="10ct / OK"]; + s6 -> s4 [label="mars / OK"]; + s6 -> s7 [label="snickers / OK"]; + s6 -> s2 [label="twix / OK"]; + s7 -> s1 [label="5ct / OK"]; + s7 -> s2 [label="10ct / OK"]; + s7 -> s7 [label="mars / NOK"]; + s7 -> s7 [label="snickers / NOK"]; + s7 -> s7 [label="twix / NOK"]; + s8 -> s8 [label="5ct / NOK"]; + s8 -> s8 [label="10ct / NOK"]; + s8 -> s3 [label="mars / OK"]; + s8 -> s1 [label="snickers / OK"]; + s8 -> s4 [label="twix / OK"]; + s9 -> s5 [label="5ct / OK"]; + s9 -> s5 [label="10ct / OK"]; + s9 -> s3 [label="mars / OK"]; + s9 -> s1 [label="snickers / OK"]; + s9 -> s4 [label="twix / OK"]; + +__start0 -> s0; +} diff --git a/assignments/assignment2/LStar_hypothesis6.dot b/assignments/assignment2/LStar_hypothesis6.dot new file mode 100644 index 0000000..3c0ce6e --- /dev/null +++ b/assignments/assignment2/LStar_hypothesis6.dot @@ -0,0 +1,72 @@ +digraph g { +__start0 [label="" shape="none"]; + + s0 [shape="circle" label="0"]; + s1 [shape="circle" label="1"]; + s2 [shape="circle" label="2"]; + s3 [shape="circle" label="3"]; + s4 [shape="circle" label="4"]; + s5 [shape="circle" label="5"]; + s6 [shape="circle" label="6"]; + s7 [shape="circle" label="7"]; + s8 [shape="circle" label="8"]; + s9 [shape="circle" label="9"]; + s10 [shape="circle" label="10"]; + s0 -> s7 [label="5ct / OK"]; + s0 -> s1 [label="10ct / OK"]; + s0 -> s0 [label="mars / NOK"]; + s0 -> s0 [label="snickers / NOK"]; + s0 -> s0 [label="twix / NOK"]; + s1 -> s2 [label="5ct / OK"]; + s1 -> s4 [label="10ct / OK"]; + s1 -> s0 [label="mars / OK"]; + s1 -> s1 [label="snickers / NOK"]; + s1 -> s1 [label="twix / NOK"]; + s2 -> s4 [label="5ct / OK"]; + s2 -> s3 [label="10ct / OK"]; + s2 -> s7 [label="mars / OK"]; + s2 -> s2 [label="snickers / NOK"]; + s2 -> s0 [label="twix / OK"]; + s3 -> s6 [label="5ct / OK"]; + s3 -> s9 [label="10ct / OK"]; + s3 -> s2 [label="mars / OK"]; + s3 -> s0 [label="snickers / OK"]; + s3 -> s1 [label="twix / OK"]; + s4 -> s3 [label="5ct / OK"]; + s4 -> s6 [label="10ct / OK"]; + s4 -> s1 [label="mars / OK"]; + s4 -> s4 [label="snickers / NOK"]; + s4 -> s7 [label="twix / OK"]; + s5 -> s5 [label="5ct / NOK"]; + s5 -> s5 [label="10ct / NOK"]; + s5 -> s6 [label="mars / OK"]; + s5 -> s2 [label="snickers / OK"]; + s5 -> s3 [label="twix / OK"]; + s6 -> s8 [label="5ct / OK"]; + s6 -> s5 [label="10ct / OK"]; + s6 -> s4 [label="mars / OK"]; + s6 -> s7 [label="snickers / OK"]; + s6 -> s2 [label="twix / OK"]; + s7 -> s1 [label="5ct / OK"]; + s7 -> s2 [label="10ct / OK"]; + s7 -> s7 [label="mars / NOK"]; + s7 -> s7 [label="snickers / NOK"]; + s7 -> s7 [label="twix / NOK"]; + s8 -> s8 [label="5ct / NOK"]; + s8 -> s8 [label="10ct / NOK"]; + s8 -> s3 [label="mars / OK"]; + s8 -> s1 [label="snickers / OK"]; + s8 -> s4 [label="twix / OK"]; + s9 -> s5 [label="5ct / OK"]; + s9 -> s10 [label="10ct / OK"]; + s9 -> s3 [label="mars / OK"]; + s9 -> s1 [label="snickers / OK"]; + s9 -> s4 [label="twix / OK"]; + s10 -> s10 [label="5ct / NOK"]; + s10 -> s10 [label="10ct / NOK"]; + s10 -> s9 [label="mars / OK"]; + s10 -> s4 [label="snickers / OK"]; + s10 -> s6 [label="twix / OK"]; + +__start0 -> s0; +} diff --git a/assignments/assignment2/LStar_learnedModel.dot b/assignments/assignment2/LStar_learnedModel.dot index abcbc95..132a49d 100644..120000 --- a/assignments/assignment2/LStar_learnedModel.dot +++ b/assignments/assignment2/LStar_learnedModel.dot @@ -1,60 +1 @@ -digraph g { -__start0 [label="" shape="none"]; - - s0 [shape="circle" label="0"]; - s1 [shape="circle" label="1"]; - s2 [shape="circle" label="2"]; - s3 [shape="circle" label="3"]; - s4 [shape="circle" label="4"]; - s5 [shape="circle" label="5"]; - s6 [shape="circle" label="6"]; - s7 [shape="circle" label="7"]; - s8 [shape="circle" label="8"]; - s0 -> s7 [label="5ct / OK"]; - s0 -> s1 [label="10ct / OK"]; - s0 -> s0 [label="mars / NOK"]; - s0 -> s0 [label="snickers / NOK"]; - s0 -> s0 [label="twix / NOK"]; - s1 -> s2 [label="5ct / OK"]; - s1 -> s4 [label="10ct / OK"]; - s1 -> s0 [label="mars / OK"]; - s1 -> s1 [label="snickers / NOK"]; - s1 -> s1 [label="twix / NOK"]; - s2 -> s4 [label="5ct / OK"]; - s2 -> s3 [label="10ct / OK"]; - s2 -> s7 [label="mars / OK"]; - s2 -> s2 [label="snickers / NOK"]; - s2 -> s0 [label="twix / OK"]; - s3 -> s6 [label="5ct / OK"]; - s3 -> s6 [label="10ct / OK"]; - s3 -> s2 [label="mars / OK"]; - s3 -> s0 [label="snickers / OK"]; - s3 -> s1 [label="twix / OK"]; - s4 -> s3 [label="5ct / OK"]; - s4 -> s6 [label="10ct / OK"]; - s4 -> s1 [label="mars / OK"]; - s4 -> s4 [label="snickers / NOK"]; - s4 -> s7 [label="twix / OK"]; - s5 -> s5 [label="5ct / NOK"]; - s5 -> s5 [label="10ct / NOK"]; - s5 -> s6 [label="mars / OK"]; - s5 -> s2 [label="snickers / OK"]; - s5 -> s3 [label="twix / OK"]; - s6 -> s8 [label="5ct / OK"]; - s6 -> s5 [label="10ct / OK"]; - s6 -> s4 [label="mars / OK"]; - s6 -> s7 [label="snickers / OK"]; - s6 -> s2 [label="twix / OK"]; - s7 -> s1 [label="5ct / OK"]; - s7 -> s2 [label="10ct / OK"]; - s7 -> s7 [label="mars / NOK"]; - s7 -> s7 [label="snickers / NOK"]; - s7 -> s7 [label="twix / NOK"]; - s8 -> s8 [label="5ct / NOK"]; - s8 -> s8 [label="10ct / NOK"]; - s8 -> s3 [label="mars / OK"]; - s8 -> s1 [label="snickers / OK"]; - s8 -> s4 [label="twix / OK"]; - -__start0 -> s0; -} +LStar_hypothesis6.dot
\ No newline at end of file diff --git a/assignments/assignment2/assignment2.tex b/assignments/assignment2/assignment2.tex index 26e964e..655179b 100644 --- a/assignments/assignment2/assignment2.tex +++ b/assignments/assignment2/assignment2.tex @@ -7,6 +7,7 @@ \usepackage{graphicx} \usepackage{caption} \usepackage{cleveref} +\usepackage{subfig} \let\oldurl\url \def\url#1{{\small\oldurl{#1}}} @@ -44,23 +45,22 @@ \item 10ct 10ct 10ct 10ct 10ct snickers snickers \item 10ct 10ct 10ct snickers 10ct twix \item 10ct 10ct 10ct 5ct snickers twix + \item 10ct 10ct 5ct 10ct snickers mars + \item 10ct 10ct 5ct 10ct 10ct mars mars snickers \end{itemize} The hypotheses are given in \cref{fig:lstar-run} (p.~\pageref{fig:lstar-run}). - \begin{figure}[p] - \includegraphics[width=.5\textwidth]{LStar_hypothesis0} - \includegraphics[width=.5\textwidth]{LStar_hypothesis1} - \includegraphics[width=.5\textwidth]{LStar_hypothesis2} - \includegraphics[width=.5\textwidth]{LStar_hypothesis3} - \caption{Learning the chocolate bar machine with L* (top to bottom, left to right).\label{fig:lstar-run}} - \end{figure} - \item - States are uniquely identified by the amount injected in the machine. - The machine does not accept more than 40ct, and the granularity is 5ct. - Hence, there are $\frac{40}{5}+1=9$ states. - The learned model also contains states, therefore they must be equivalent. + States are in principle uniquely identified by the amount injected in the machine. + The machine does not accept more than 45ct, and the granularity is 5ct. + Hence, there are $\frac{45}{5}+1=10$ states. + However, there are two states in which we have 35ct, namely one where we can still insert money + (accessed through \enquote{10ct 10ct 5ct 10ct}) + and one where we cannot (e.g. \enquote{10ct 10ct 10ct 5ct}). + Hence, the complete model has 11 states. + + The learned model also contains 11 states, therefore they must be equivalent. \item A counter-example $\pi$ consists of a prefix, an input where an inconsistency appears and a suffix showing the inconsistency: @@ -77,8 +77,34 @@ \item \item + The method with user queries worked very efficiently in combination with L*. + It allows the user to insert cleverly chosen counter-examples, + but does not ask him as often as other learning methods would do. + However, we realise that for more complex systems it may be difficult for the user to provide counter-examples. + + As for the testing method, + on our small example a random walk appears to be the fasted. + However, as noted in the source code (\texttt{BasicLearner.java}), + it may perform worse than the others on large models. + \end{enumerate} +\begin{figure}[p] + \includegraphics[width=.5\textwidth]{LStar_hypothesis0} + \includegraphics[width=.5\textwidth]{LStar_hypothesis1} + \includegraphics[width=.5\textwidth]{LStar_hypothesis2} + \includegraphics[width=.5\textwidth]{LStar_hypothesis3} + \includegraphics[width=.5\textwidth]{LStar_hypothesis4} + \includegraphics[width=.5\textwidth]{LStar_hypothesis5} + \caption{Learning the chocolate bar machine with L* (top to bottom, left to right).\label{fig:lstar-run}} +\end{figure} +\begin{figure}[p] + \ContinuedFloat + \includegraphics[width=.5\textwidth]{LStar_hypothesis6} + \caption[]{Learning the chocolate bar machine with L* (top to bottom, left to right).\label{fig:lstar-run}} +\end{figure} +\thispagestyle{empty} + \section{Bounded Retransmission Protocol} \end{document} |