From a3a6397bfd8a80bc49374ba168d8b8437c5de8a0 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Mon, 23 Oct 2017 14:24:06 +0200
Subject: Add hypotheses
---
assignments/assignment2/.latexmkrc | 2 +-
assignments/assignment2/LStar_hypothesis5.dot | 66 +++++++++++++++++++++++
assignments/assignment2/LStar_hypothesis6.dot | 72 ++++++++++++++++++++++++++
assignments/assignment2/LStar_learnedModel.dot | 61 +---------------------
assignments/assignment2/assignment2.tex | 50 +++++++++++++-----
5 files changed, 178 insertions(+), 73 deletions(-)
create mode 100644 assignments/assignment2/LStar_hypothesis5.dot
create mode 100644 assignments/assignment2/LStar_hypothesis6.dot
mode change 100644 => 120000 assignments/assignment2/LStar_learnedModel.dot
(limited to 'assignments/assignment2')
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
deleted file mode 100644
index abcbc95..0000000
--- a/assignments/assignment2/LStar_learnedModel.dot
+++ /dev/null
@@ -1,60 +0,0 @@
-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;
-}
diff --git a/assignments/assignment2/LStar_learnedModel.dot b/assignments/assignment2/LStar_learnedModel.dot
new file mode 120000
index 0000000..132a49d
--- /dev/null
+++ b/assignments/assignment2/LStar_learnedModel.dot
@@ -0,0 +1 @@
+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}
--
cgit v1.2.3