joshua/phd-thesis
Archived
1
Fork 0
Code Activity

Figures and small things

Browse source
This commit is contained in:
Joshua Moerman 2018-10-08 17:11:56 +02:00
parent 48c3a9bccf
commit f87889cacc
6 changed files with 87 additions and 108 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
content/introduction.tex
View file

@ -97,7 +97,7 @@ Fix a countable, infinite set $\atoms = \{ a, b, \ldots \}$ of \emph{names} (som
The elements of $\atoms$ bare no relationship to natural numbers, or other standard mathematical entities.
Define $\Pm = \{ \pi \colon \atoms \to \atoms \mid \pi \text{ is bijective} \}$ to be the set of permutations of names.
Together with function composition, $\Pm$ forms a group.
Together with function composition, $\Pm$ forms a \emph{group}.
For two elements $a$ and $b$ we define a particular bijection $\swap{a}{b} \in \Pm$ which swaps $a$ and $b$ and leaves all other elements fixed.
\stopdefinition
@ -107,12 +107,13 @@ The names are abstract entities which can be compared for equality, but nothing
This also means that although $a$ and $b$ are distinct names, they are interchangeable.
If we write $a \in \atoms$, then $a$ can stand for any of the names.
So if we write $a, b \in \atoms$, then $a$ and $b$ can refer to the same name, i.e., $a = b$.
In other words, we do not adapt the permutative convention by \cite[].
In other words, we do not adapt the permutative convention by \citet[?].
As noted before, we want to let permutations act on objects constructed from names, such as lambda terms, tuples, and words.
As alluded to before, we want to have permutations act on objects constructed from names, such as words, states in an automaton and languages.
The notion of a group action captures exactly this.
In most cases we are interested in the group $\Pm$.
However, in order to be general enough for the next chapters, we introduce group actions for an arbitrary group $G$.
\todo{Notatie $1$ is groepseenheid, ${\cdot}$ is vermenigvuldiging en werking.}
\startdefinition
Let $X$ be a set.
@ -165,11 +166,11 @@ Such an action is called \emph{trivial}.
Note that the action on $\emptyset$ and $\{*\}$ are trivial, but the $\Pm$-actions on $\atoms$, $\atoms^{*}$ and $\atoms^{\omega}$ are not trivial.
\item
Another interesting non-trivial example is the set $\Pm$ itself.
There are three different actions which are natural:
There are three different interesting actions one can define:
\startformula\startalign
\NC \pi \cdot_1 \sigma \NC = \pi \sigma \NR
\NC \pi \cdot_2 \sigma \NC = \sigma \pi^{-1} \NR
\NC \pi \cdot_3 \sigma \NC = \pi \sigma \pi^{-1} \NR
\NC \pi \cdot_{l} \sigma \NC = \pi \sigma \NR
\NC \pi \cdot_{r} \sigma \NC = \sigma \pi^{-1} \NR
\NC \pi \cdot_{c} \sigma \NC = \pi \sigma \pi^{-1} \NR
\stopalign\stopformula
Here the group multiplication is written by juxtaposition.
The first two actions are left-multiplication and right-multiplication respectively.
@ -178,7 +179,7 @@ For each of them, one can verify the requirements.
\stopitemize
\stopexample
In the above examples, the non trivial $\Pm$-sets are all infinite.
In the above examples, the non-trivial $\Pm$-sets are all infinite.
Yet, in a sense, the set $\atoms^{*}$ is bigger than the set $\atoms$.
To be able to quantify this, we introduce the notion of an orbit.

144
content/minimal-separating-sequences.tex
View file

@ -13,7 +13,7 @@ is a classic problem in automata theory. Sets of minimal separating sequences, f
central role in many conformance testing methods. Moore has already outlined a partition refinement
algorithm that constructs such a set of sequences in $\bigO(mn)$ time, where $m$ is the number of
transitions and $n$ is the number of states. In this paper, we present an improved algorithm based
on the minimization algorithm of Hopcroft that runs in $\bigO(m \log n)$ time. The efficiency of our
on the minimisation algorithm of Hopcroft that runs in $\bigO(m \log n)$ time. The efficiency of our
algorithm is empirically verified and compared to the traditional algorithm.
\stopabstract
@ -22,7 +22,7 @@ algorithm is empirically verified and compared to the traditional algorithm.
[title={Introduction}]
In diverse areas of computer science and engineering, systems can be modelled by \emph{finite state machines} (FSMs).
One of the cornerstones of automata theory is minimization of such machines (and many variation thereof).
One of the cornerstones of automata theory is minimisation of such machines (and many variation thereof).
In this process one obtains an equivalent minimal FSM, where states are different if and only if they have different behaviour.
The first to develop an algorithm for minimisation was \citet[Moore56].
His algorithm has a time complexity of $\bigO(mn)$, where $m$ is the number of transitions, and $n$ is the number of states of the FSM.
@ -92,7 +92,7 @@ A partition is \emph{valid} if equivalent states are in the same block.
\stopdefinition
Partition refinement algorithms for FSMs start with the trivial partition $P = \{S\}$, and iteratively refine $P$ until it is the finest valid partition (where all states in a block are equivalent).
The blocks of such a \emph{complete} partition form the states of the minimized FSM, whose transition and output functions are well-defined because states in the same block are equivalent.
The blocks of such a \emph{complete} partition form the states of the minimised FSM, whose transition and output functions are well-defined because states in the same block are equivalent.
Let $B$ be a block and $a$ be an input.
There are two possible reasons to split $B$ (and hence refine the partition).
@ -207,10 +207,10 @@ We continue until $T$ is complete.
\stopexample
\startplacefigure
[title={A FSM (a) and a complete splitting tree for it (b)},
[title={A FSM (a) and a complete splitting tree for it (b).},
reference=fig:automaton-tree]
\starttikzpicture
\startcombination[2*1]
{\hbox{\starttikzpicture
\node[state] (0) {$s_0$};
\node[state] (1) [above right of=0] {$s_1$};
\node[state] (2) [right of=1] {$s_2$};
@ -230,12 +230,11 @@ We continue until $T$ is complete.
(4) edge node [below] {${b}/1$} (5)
(5) edge node [below left] {${b}/0$} (0)
(5) edge node [left] {${a}/1$} (0);
\stoptikzpicture
\todo{monotone-tree}
% \subfloat[\label{fig:monotone-tree}]{
% \includegraphics[width=0.45\textwidth]{monotone-tree.pdf}
% }
% This is for alignment
\path (3) edge [loop right, draw=none] node [right] {\phantom{${b}/0$}} (3);
\stoptikzpicture}} {(a)}
{\externalfigure[monotone-tree.pdf][width=0.5\textwidth]} {(b)}
\stopcombination
\stopplacefigure
@ -363,7 +362,7 @@ In both cases we have shown that $|x| \geq k+1$ as required.
\stopplacealgorithm
\startexample
\in{Figure}[fig:splitting-tree-only] shows a stable and minimal splitting tree $T$ for the machine in \in{Figure}[fig:automaton].
\in{Figure}{(a)}[fig:splitting-tree] shows a stable and minimal splitting tree $T$ for the machine in \in{Figure}[fig:automaton-tree].
This tree is constructed by \in{Algorithm}[alg:minimaltree] as follows.
It executes the same as \in{Algorithm}[alg:tree] until we consider the node labelled $\{s_0, s_2\}$.
At this point $k = 1$.
@ -371,61 +370,55 @@ We observe that the sequence of $\lca(\delta(\{s_0,s_2\}, a))$ has length $2$, w
We find that we can indeed split w.r.t. the state after $b$, so the associated sequence is $ba$.
Continuing, we obtain the same partition as before, but with smaller witnesses.
The internal data structure (a refinable partition) is shown in \in{Figure}[fig:internal-data-structure]:
The internal data structure (a refinable partition) is shown in \in{Figure}{(b)}[fig:splitting-tree]:
the array with the permutation of the states is at the bottom,
and every block includes an indication of the slice containing its label and a pointer to its parent (as our final algorithm needs to find the parent block, but never the child blocks).
\stopexample
\todo{Figure: splitting tree + internal representation}
%\begin{figure}
% \centering
% \subfloat[\label{fig:splitting-tree-only}]{
% \includegraphics[width=0.43\textwidth]{splitting-tree.pdf}
% }
% \subfloat[\label{fig:internal-data-structure}]{
% \setcounter{maxdepth}{3}
% \begin{tikzpicture}[scale=1.0,>=stealth']
% \gasblock{0}{6}{0}{2}{\makebox[0pt][r]{\tiny\textcolor{gray}{$\sigma(B_2) = \mbox{}$}} a}
% \gasblock{0}{3}{1}{4}{b}
% \gasblock{3}{6}{1}{8}{a \sigma(B_4)}
% \gasblock{0}{2}{2}{6}{b \sigma(B_2)}
% \gasblock{2}{3}{2}{3}{}
% \gasblock{3}{5}{2}{10}{a \sigma(B_6)}
% \gasblock{5}{6}{2}{7}{}
% \gasblock{0}{1}{3}{0}{}
% \gasblock{1}{2}{3}{5}{}
% \gasblock{3}{4}{3}{1}{}
% \gasblock{4}{5}{3}{9}{}
% \draw (0,0) node[shape=rectangle,minimum width=1cm,draw] (s2) {\footnotesize $s_2$};
% \draw (1,0) node[shape=rectangle,minimum width=1cm,draw] (s0) {\footnotesize $s_0$};
% \draw (2,0) node[shape=rectangle,minimum width=1cm,draw] (s4) {\footnotesize $s_4$};
% \draw (3,0) node[shape=rectangle,minimum width=1cm,draw] (s5) {\footnotesize $s_5$};
% \draw (4,0) node[shape=rectangle,minimum width=1cm,draw] (s1) {\footnotesize $s_1$};
% \draw (5,0) node[shape=rectangle,minimum width=1cm,draw] (s3) {\footnotesize $s_3$};
% \draw[->]
% (s2) edge (B0)
% (B0) edge (B6)
% (B6) edge (B4)
% (B4) edge (B2)
% (s0) edge (B5)
% (B5) edge (B6)
% (s4) edge (B3)
% (B3) edge (B4)
% (s5) edge (B1)
% (B1) edge (B10)
% (B10) edge (B8)
% (B8) edge (B2)
% (s1) edge (B9)
% (B9) edge (B10)
% (s3) edge (B7)
% (B7) edge (B8);
% \end{tikzpicture}
% }
% \caption{A complete and minimal splitting tree for the FSM in \in{Figure}[fig:automaton] (a) and its
% internal refinable partition data structure (b)}
% \label{fig:splitting-tree}
%\end{figure}
\startplacefigure
[title={(a) A complete and minimal splitting tree for the FSM in \in{Figure}[fig:automaton-tree] and (b) its internal refinable partition data structure.},
list={A minimal splitting tree and internal data structure.},
reference=fig:splitting-tree]
\startcombination[2*1]
{\externalfigure[splitting-tree.pdf][width=0.5\textwidth]} {(a)}
{\hbox{\starttikzpicture[scale=1.0,>=stealth']
\gasblock{0}{6}{0}{2}{\sigma = a}
\gasblock{0}{3}{1}{4}{\sigma = b}
\gasblock{3}{6}{1}{8}{\sigma = a \sigma(B_4)}
\gasblock{0}{2}{2}{6}{\sigma = b \sigma(B_2)}
\gasblock{2}{3}{2}{3}{}
\gasblock{3}{5}{2}{10}{\sigma = a \sigma(B_6)}
\gasblock{5}{6}{2}{7}{}
\gasblock{0}{1}{3}{0}{}
\gasblock{1}{2}{3}{5}{}
\gasblock{3}{4}{3}{1}{}
\gasblock{4}{5}{3}{9}{}
\draw (0,0) node[shape=rectangle,minimum width=1cm,draw] (s2) {\tfx $s_2$};
\draw (1,0) node[shape=rectangle,minimum width=1cm,draw] (s0) {\tfx $s_0$};
\draw (2,0) node[shape=rectangle,minimum width=1cm,draw] (s4) {\tfx $s_4$};
\draw (3,0) node[shape=rectangle,minimum width=1cm,draw] (s5) {\tfx $s_5$};
\draw (4,0) node[shape=rectangle,minimum width=1cm,draw] (s1) {\tfx $s_1$};
\draw (5,0) node[shape=rectangle,minimum width=1cm,draw] (s3) {\tfx $s_3$};
\draw[->]
(s2) edge (B0)
(B0) edge (B6)
(B6) edge (B4)
(B4) edge (B2)
(s0) edge (B5)
(B5) edge (B6)
(s4) edge (B3)
(B3) edge (B4)
(s5) edge (B1)
(B1) edge (B10)
(B10) edge (B8)
(B8) edge (B2)
(s1) edge (B9)
(B9) edge (B10)
(s3) edge (B7)
(B7) edge (B8);
\stoptikzpicture}} {(b)}
\stopcombination
\stopplacefigure
\stopsection
@ -464,7 +457,7 @@ The key idea is that, when we fix a $k$-candidate $v$, all leaves are split with
Instead of iterating over of all leaves to refine them, we iterate over $s \in \delta^{-1}(l(w), a)$ for all $w$ in $C(v)$ and look up in which leaf it is contained to move $s$ out of it.
From Lemma 8 by \citet[DBLP:journals/tcs/Knuutila01] it follows that we can skip one of the children of $v$.
This lowers the time complexity to $\bigO(m \log n)$.
In order to move $s$ out of its leaf, each leaf $u$ is associated with a set of temporary children $C'(u)$ that is initially empty, and will be finalized after iterating over all $s$ and $w$.
In order to move $s$ out of its leaf, each leaf $u$ is associated with a set of temporary children $C'(u)$ that is initially empty, and will be finalised after iterating over all $s$ and $w$.
\startplacealgorithm
[title={A better step towards the stability of a splitting tree.},
@ -511,7 +504,7 @@ For each $k$-candidate $v$ and input $a$, we consider all children $w$ of $v$, e
For each state $s \in \delta^{-1}(l(w), a)$ we consider the leaf $u$ containing it.
If this leaf does not have an associated temporary child for $w$ we create such a child (\inline[line:add-temp-child]), if this child exists we move $s$ into that child (\inline[line:move-to-temp-child]).
Once we have done the simultaneous splitting for the candidate $v$ and input $a$, we finalize the temporary children.
Once we have done the simultaneous splitting for the candidate $v$ and input $a$, we finalise the temporary children.
This is done at \inline[line:finalize].
If there is only one temporary child with all the states, no split has been made and we recover this node (\inline[line:recover]). In the other case we make the temporary children permanent.
@ -556,7 +549,7 @@ The important observation is that when using \in{Algorithm}[alg:increase-k-v3] w
\starttheorem[reference=th:complexity]
\in{Algorithm}[alg:minimaltree] using \in{Algorithm}[alg:increase-k-v3] runs in $\bigO(m \log n)$ time.
\stoptheorem
\startproof
\startproofnoqed
We prove that bookkeeping does not increase time complexity by discussing the implementation.
\startdescription{Inverse transition.}
@ -581,8 +574,9 @@ On finalizing the temporary children we store (a reference to) the biggest child
\stopdescription
\startdescription{Storing sequences.}
The operation on \inline[line:prepend] is done in constant time by using a linked list.
\QED
\stopdescription
\stopproof
\stopproofnoqed
\stopsection
@ -590,15 +584,15 @@ The operation on \inline[line:prepend] is done in constant time by using a linke
[title=Application in Conformance Testing]
A splitting tree can be used to extract relevant information for two classical test generation methods:
a \emph{characterization set} for the W-method and a \emph{separating family} for the HSI-method.
a \emph{characterisation set} for the W-method and a \emph{separating family} for the HSI-method.
For an introduction and comparison of FSM-based test generation methods we refer to \citet[DBLP:journals/infsof/DorofeevaEMCY10].
\startdefinition[def:cset]
A set $W \subset I^{\ast}$ is called a \emph{characterization set} if for every pair of inequivalent states $s, t$ there is a sequence $w \in W$ such that $\lambda(s, w) \neq \lambda(t, w)$.
A set $W \subset I^{\ast}$ is called a \emph{characterisation set} if for every pair of inequivalent states $s, t$ there is a sequence $w \in W$ such that $\lambda(s, w) \neq \lambda(t, w)$.
\stopdefinition
\startlemma[reference=lem:cset]
Let $T$ be a complete splitting tree, then $\{\sigma(u)|u \in T\}$ is a characterization set.
Let $T$ be a complete splitting tree, then $\{\sigma(u)|u \in T\}$ is a characterisation set.
\stoplemma
\startproof
Let $W = \{\sigma(u) \mid u \in T\}$.
@ -609,12 +603,12 @@ This shows that $W$ is a characterisation set.
\stopproof
\startlemma
A characterization set with minimal length sequences can be constructed in time $\bigO(m \log n)$.
A characterisation set with minimal length sequences can be constructed in time $\bigO(m \log n)$.
\stoplemma
\startproof
By \in{Lemma}[lem:cset] the sequences associated with the inner nodes of a splitting tree form a characterization set.
By \in{Lemma}[lem:cset] the sequences associated with the inner nodes of a splitting tree form a characterisation set.
By \in{Theorem}[th:complexity], such a tree can be constructed in time $\bigO(m \log n)$.
Traversing the tree to obtain the characterization set is linear in the number of nodes (and hence linear in the number of states).
Traversing the tree to obtain the characterisation set is linear in the number of nodes (and hence linear in the number of states).
\stopproof
\startdefinition[reference=def:separating_fam]
@ -654,7 +648,7 @@ This can be done in $\bigO(n^2)$ time using a trie data structure.
[title={Experimental Results}]
We have implemented \in{Algorithms}[alg:increase-k, alg:increase-k-v3] in Go, and we have compared their running time on two sets of FSMs.
\footnote{Available at \todo{https://gitlab.science.ru.nl/rick/partition/}.}
\footnote{Available at \href{https://gitlab.science.ru.nl/rick/partition/}.}
The first set is from \citet[DBLP:conf/icfem/SmeenkMVJ15], where FSMs for embedded control software were automatically constructed.
These FSMs are of increasing size, varying from 546 to 3~410 states, with 78 inputs and up to 151 outputs.
The second set is inferred from \citet[Hopcroft71], where two classes of finite automata, $A$ and $B$, are described that serve as a worst case for \in{Algorithms}[alg:increase-k, alg:increase-k-v3] respectively.

4
environment.tex
View file

@ -27,7 +27,9 @@
\defineenumeration[corollary][text=Corollary]
\setupenumeration[definition,example,lemma,proposition,theorem,corollary][alternative=serried,width=fit,right=.]
\definestartstop[proof][before={{\it Proof. }}, after={\hfill$\square$}]
\define\QED{\hfill$\square$}
\definestartstop[proof][before={{\it Proof. }}, after={\QED}]
\definestartstop[proofnoqed][before={{\it Proof. }}, after={}]
\definefloat[algorithm][algorithms]

28
environment/tikz.tex
View file

@ -13,28 +13,10 @@
% observation table
\tikzset{obs table/.style={matrix of math nodes, ampersand replacement=\&, column 1/.style={anchor=base west}}}
\stopenvironment
% This command is used to draw the internal data structure for the minimal separating sequences paper
% this is not used yet.
\newcounter{maxdepth}
\newcommand{\gasblock}[5]{
\fill (#1-0.495,{(\themaxdepth-#3)*0.75+0.5}) [rounded corners=0.2cm] -- (#1-0.495,{(\themaxdepth-#3)*0.75+0.655}) -- (#2-0.505,{(\themaxdepth-#3)*0.75+0.655}) [sharp corners] -- (#2-0.505,{(\themaxdepth-#3)*0.75+0.5}) [rounded corners=0.2cm] -- (#2-0.505,{(\themaxdepth-#3)*0.75+0.645}) -- (#1-0.495,{(\themaxdepth-#3)*0.75+0.645}) [sharp corners] -- cycle;
%\draw[rounded corners=0.225cm] (#1-0.45,{(\themaxdepth-#3)*0.75+0.5}) -- (#1-0.45,{(\themaxdepth-#3)*0.75+0.65}) -- (#2-0.55,{(\themaxdepth-#3)*0.75+0.65}) -- (#2-0.55,{(\themaxdepth-#3)*0.75+0.5});
\draw ({(#1+#2)/2-0.5},{(\themaxdepth-#3)*0.75+0.65}) node[fill=white] (B#4) {\footnotesize $B_{#4}$};
%\draw (#1-0.5,{(\themaxdepth-#3)*0.75+0.3}) node {\tiny $#1$};
%\draw (#2-0.5,{(\themaxdepth-#3)*0.75+0.3}) node {\tiny $#2$};
%\draw ({(#1+#2)/2-0.5},{(\themaxdepth-#3)*0.75+0.3}) node {\scriptsize \smash{$#5$}};
%\begin{scope}
% \clip[overlay] (-0.55,{(\themaxdepth-#3)*0.75+0.6}) rectangle (#2-3.45,0);
% \draw (#1-0.5,{(\themaxdepth-#3)*0.75+0.3}) node{\tiny $\phantom{#1}$\makebox[0pt][l]{\textcolor{gray}{$\mbox{} = \smash{#4.\mathit{begin}}$}}};
%\end{scope}
%\begin{scope}
% \clip[overlay] (#1+2.45,{(\themaxdepth-#3)*0.75+0.6}) rectangle (#2-0.45,0);
% \draw (#2-0.5,{(\themaxdepth-#3)*0.75+0.3}) node{\tiny\makebox[0pt][r]{\textcolor{gray}{$\smash{#4.\mathit{end}} = \mbox{}$}}$\phantom{#2}$};
%\end{scope}
%% \begin{scope}
%% \clip[overlay] (#1*2-1.7,{(\themaxdepth-#3)*0.75+0.8}) rectangle (-0.5,0);
%% \draw[overlay] (-0.5,{(\themaxdepth-#3)*0.75+0.65}) node{\tiny\makebox[0pt][r]{\textcolor{gray}{$#4.\mathit{level} = #3$}~~\quad}};
%% \end{scope}
\define[5]\gasblock{
\fill (#1-0.495,{(3-#3)*0.75+0.5}) [rounded corners=0.2cm] -- (#1-0.495,{(3-#3)*0.75+0.655}) -- (#2-0.505,{(3-#3)*0.75+0.655}) [sharp corners] -- (#2-0.505,{(3-#3)*0.75+0.5}) [rounded corners=0.2cm] -- (#2-0.505,{(3-#3)*0.75+0.645}) -- (#1-0.495,{(3-#3)*0.75+0.645}) [sharp corners] -- cycle;
\draw ({(#1+#2)/2-0.5},{(3-#3)*0.75+0.65}) node[fill=white] (B#4) {{$B_{#4}$} {$\scriptscriptstyle #5$}};
}
\stopenvironment

BIN
images/monotone-tree.pdf Normal file
View file

Binary file not shown.

BIN
images/splitting-tree.pdf Normal file
View file

Binary file not shown.