diff --git a/content/learning-nominal-automata.tex b/content/learning-nominal-automata.tex index 2da5224..2b17361 100644 --- a/content/learning-nominal-automata.tex +++ b/content/learning-nominal-automata.tex @@ -129,7 +129,7 @@ It terminates when the answer is {\bf yes}, otherwise it extends the table with \startplacealgorithm[title={The \LStar{} learning algorithm from \cite[authoryears][DBLP:journals/iandc/Angluin87].}, reference=alg:alg] \startalgorithmic \startlinenumbering -\STATE $S,E \gets \{\epsilon\}$ +\STATE $S,E \gets \{\epsilon\}$ \REPEAT \WHILE{$(S, E)$ is not closed or not consistent\someline[line:checks]} \IF{$(S, E)$ is not closed\someline[line:begin-closed]} diff --git a/content/minimal-separating-sequences.tex b/content/minimal-separating-sequences.tex index a6d92df..648ecc2 100644 --- a/content/minimal-separating-sequences.tex +++ b/content/minimal-separating-sequences.tex @@ -173,24 +173,25 @@ A straight-forward adaptation of partition refinement for constructing a stable The termination and the correctness of the algorithm outlined in \in{Section}[sec:partition] are preserved. It follows directly that states are equivalent if and only if they are in the same label of a leaf node. -\todo{algorithm 1} - -%\begin{algorithm}[t] -% \DontPrintSemicolon -% \KwIn{A FSM $M$} -% \KwResult{A valid and stable splitting tree $T$} -% initialize $T$ to be a tree with a single node labeled $S$\; -% \Repeat{$P(T)$ is acceptable}{ -% find $a \in I, B \in P(T)$ such that we can split $B$ w.r.t.\@ output $\lambda(\cdot, a)$\; -% expand the $u \in T$ with $l(u)=B$ as described in (split-output)\; -% } -% \Repeat{$P(T)$ is stable}{ -% find $a \in I, B \in P(T)$ such that we can split $B$ w.r.t.\@ state $\delta(\cdot, a)$\; -% expand the $u \in T$ with $l(u)=B$ as described in (split-state)\; -% } -% \caption{Constructing a stable splitting tree} -% \label{alg:tree} -%\end{algorithm} +\startplacealgorithm + [title={Constructing a stable splitting tree.}, + reference=alg:tree] +\startalgorithmic +\REQUIRE An FSM $M$ +\ENSURE A valid and stable splitting tree $T$ +\startlinenumbering +\STATE initialise $T$ to be a tree with a single node labelled $S$ +\REPEAT + \STATE find $a \in I, B \in P(T)$ such that we can split $B$ w.r.t. output $\lambda(\cdot, a)$ + \STATE expand the $u \in T$ with $l(u)=B$ as described in (split-output) +\UNTIL{$P(T)$ is acceptable} +\REPEAT + \STATE find $a \in I, B \in P(T)$ such that we can split $B$ w.r.t. state $\delta(\cdot, a)$ + \STATE expand the $u \in T$ with $l(u)=B$ as described in (split-state) +\UNTIL{$P(T)$ is stable} +\stoplinenumbering +\stopalgorithmic +\stopplacealgorithm \startexample[reference=ex:tree] \in{Figure}[fig:automaton-tree] shows a FSM and a complete splitting tree for it. @@ -231,6 +232,7 @@ We continue until $T$ is complete. (5) edge node [left] {${a}/1$} (0); \stoptikzpicture +\todo{monotone-tree} % \subfloat[\label{fig:monotone-tree}]{ % \includegraphics[width=0.45\textwidth]{monotone-tree.pdf} % } @@ -324,38 +326,41 @@ This means that $|\sigma(u)| \geq k$ and by minimality of $T$ we get $|x'| \geq In both cases we have shown that $|x| \geq k+1$ as required. \stopproof -\todo{algorithms 2 and 3} +\startplacealgorithm + [title={Constructing a stable and minimal splitting tree.}, + reference=alg:minimaltree] +\startalgorithmic +\REQUIRE An FSM $M$ with $n$ states +\ENSURE A stable, minimal splitting tree $T$ +\startlinenumbering +\STATE initialise $T$ to be a tree with a single node labelled $S$ +\REPEAT + \STATE find $a \in I, B \in P(T)$ such that we can split $B$ w.r.t. output $\lambda(\cdot, a)$ + \STATE expand the $u \in T$ with $l(u)=B$ as described in (split-output) +\UNTIL{$P(T)$ is acceptable} +\FOR{$k = 1$ {\bf to} $n-1$} + \STATE invoke \in{Algorithm}[alg:increase-k] or \in{Algorithm}[alg:increase-k-v3] on $T$ for $k$ +\ENDFOR +\stoplinenumbering +\stopalgorithmic +\stopplacealgorithm -%\begin{algorithm}[t] -% \DontPrintSemicolon -% \KwIn{A FSM $M$ with $n$ states} -% \KwResult{A stable, minimal splitting tree $T$} -% initialize $T$ to be a tree with a single node labeled $S$\; -% \Repeat{$P(T)$ is acceptable}{ -% find $a \in I, B \in P(T)$ such that we can split $B$ w.r.t.\@ output $\lambda(\cdot, a)$\; -% expand the $u \in T$ with $l(u)=B$ as described in (split-output)\; -% } -% \For{$k=1$ to $n-1$}{ -% perform Algorithm~\ref{alg:increase-k} or Algorithm~\ref{alg:increase-k-v3} on $T$ for -% $k$\; -% } -% \caption{Constructing a stable and minimal splitting tree} -% \label{alg:minimaltree} -%\end{algorithm} - -%\begin{algorithm}[t] -% \DontPrintSemicolon -% \KwIn{a $k$-stable and minimal splitting tree $T$} -% \KwResult{$T$ is a $(k+1)$-stable, minimal splitting tree} -% \ForAll{leaves $u \in T$ and all inputs $a$}{ -% locate $v=\lca(\delta(l(u), a))$\; -% \If{$v$ is an inner node and $|\sigma(v)| = k$}{\label{sigma-k} -% expand $u$ as described in (split-state) (which generates new leaves)\; -% } -% } -% \caption{A step towards the stability of a splitting tree} -% \label{alg:increase-k} -%\end{algorithm} +\startplacealgorithm + [title={A step towards the stability of a splitting tree.}, + reference=alg:increase-k] +\startalgorithmic +\REQUIRE A $k$-stable and minimal splitting tree $T$ +\ENSURE $T$ is a $(k+1)$-stable, minimal splitting tree +\startlinenumbering +\FORALL{leaves $u \in T$ and all inputs $a \in I$} + \STATE $v \gets \lca(\delta(l(u), a))$ + \IF{$v$ is an inner node and $|\sigma(v)| = k$} + \STATE expand $u$ as described in (split-state) (this generates new leaves) + \ENDIF +\ENDFOR +\stoplinenumbering +\stopalgorithmic +\stopplacealgorithm \startexample \in{Figure}[fig:splitting-tree-only] shows a stable and minimal splitting tree $T$ for the machine in \in{Figure}[fig:automaton]. @@ -417,7 +422,7 @@ and every block includes an indication of the slice containing its label and a p % (B7) edge (B8); % \end{tikzpicture} % } -% \caption{A complete and minimal splitting tree for the FSM in Fig.~\ref{fig:automaton} (a) and its +% \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} @@ -461,60 +466,58 @@ From Lemma 8 by \citet[Knuutila2001] it follows that we can skip one of the chil 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$. -\todo{algorithm 4?} - -%\begin{algorithm}[t] -% \LinesNumbered -% \DontPrintSemicolon -% \SetKw{KwContinue}{continue} -% \KwIn{a $k$-stable and minimal splitting tree $T$, and a list $L_k$} -% \KwResult{$T$ is a $(k+1)$-stable and minimal splitting tree, and a list $L_{k+1}$} -% $L_{k+1} \gets \emptyset$\; -% \ForAll{$k$-candidates $v$ in $L_{k}$ in order}{ -% let $w'$ be a node in $C(v)$ such that $|l(w')| \geq |l(w)|$ for all nodes $w$ in $C(v)$\; -% \ForAll{inputs $a$ in $I$}{ -% \ForAll{nodes $w$ in $C(v) \setminus w'$}{ -% \ForAll{states $s$ in $\delta^{-1}(l(w), a)$}{ -% locate leaf $u$ such that $s \in l(u)$\; -% \If{$C'(u)$ does not contain node $u_{w}$}{ -% add a new node $u_{w}$ to $C'(u)$\;\label{line:add-temp-child} -% } -% move $s$ from $l(u)$ to $l(u_{w})$\;\label{line:move-to-temp-child} -% } -% } -% \ForEach{leaf $u$ with $C'(u) \neq \emptyset$}{\label{line:finalize} -% \eIf{$|l(u)| = 0$}{ -% \If{$|C'(u)| = 1$}{ -% recover $u$ by moving its elements back and clear -% $C'(u)$\;\label{line:recover} -% \KwContinue with the next leaf\; -% } -% set $p=u$ and $C(u)=C'(u)$\;\label{line:setptou} -% }{ -% construct a new node $p$ and set $C(p) = C'(u) \cup \{ u \}$\; -% insert $p$ in the tree in the place where $u$ was\; -% } -% set $\sigma(p) = a \sigma(v)$\;\label{line:prepend} -% append $p$ to $L_{k+1}$ and clear $C'(u)$\;\label{line:finalize-end} -% } -% } -% } -% \caption{A better step towards the stability of a splitting tree} -% \label{alg:increase-k-v3} -%\end{algorithm} +\startplacealgorithm + [title={A better step towards the stability of a splitting tree.}, + reference=alg:increase-k-v3] +\startalgorithmic +\REQUIRE A $k$-stable and minimal splitting tree $T$, and a list $L_k$ +\ENSURE $T$ is a $(k+1)$-stable and minimal splitting tree, and a list $L_{k+1}$ +\startlinenumbering +\STATE $L_{k+1} \gets \emptyset$ +\FORALL{$k$-candidates $v$ in $L_{k}$ in order} + \STATE let $w'$ be a node in $C(v)$ with $|l(w')| \geq |l(w)|$ for all nodes $w \in C(v)$ + \FORALL{inputs $a$ in $I$} + \FORALL{nodes $w$ in $C(v) \setminus \{ w' \}$} + \FORALL{states $s$ in $\delta^{-1}(l(w), a)$} + \STATE locate leaf $u$ such that $s \in l(u)$ + \IF{$C'(u)$ does not contain node $u_{w}$} + \STATE add a new node $u_{w}$ to $C'(u)$ \someline[line:add-temp-child] + \ENDIF + \STATE move $s$ from $l(u)$ to $l(u_{w})$ \someline[line:move-to-temp-child] + \ENDFOR + \ENDFOR + \FORALL{leaves $u$ with $C'(u) \neq \emptyset$\startline[line:finalize]} + \IF{$|l(u)| = 0$} + \IF{$|C'(u)| = 1$} + \STATE recover $u$ by moving its elements back and clear $C'(u)$ \someline[line:recover] + \STATE {\bf continue} with the next leaf + \ENDIF + \STATE set $p=u$ and $C(u)=C'(u)$ \someline[line:setptou] + \ELSE + \STATE construct a new node $p$ and set $C(p) = C'(u) \cup \{ u \}$ + \STATE insert $p$ in the tree in the place where $u$ was + \ENDIF + \STATE set $\sigma(p) = a \sigma(v)$ \someline[line:prepend] + \STATE append $p$ to $L_{k+1}$ and clear $C'(u)$ \stopline[line:finalize] + \ENDFOR + \ENDFOR +\ENDFOR +\stoplinenumbering +\stopalgorithmic +\stopplacealgorithm In \in{Algorithm}[alg:increase-k-v3] we use the ideas described above. For each $k$-candidate $v$ and input $a$, we consider all children $w$ of $v$, except for the largest one (in case of multiple largest children, we skip one of these arbitrarily). 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 (line~\ref{line:add-temp-child}), if this child exists we move $s$ into that child (line~\ref{line:move-to-temp-child}). +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. -This is done at lines~\ref{line:finalize}--\ref{line:finalize-end}. -If there is only one temporary child with all the states, no split has been made and we recover this node (line~\ref{line:recover}). In the other case we make the temporary children permanent. +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. The states remaining in $u$ are those for which $\delta(s, a)$ is in the child of $v$ that we have skipped; therefore we will call it the \emph{implicit child}. We should not touch these states to keep the theoretical time bound. -Therefore, we construct a new parent node $p$ that will \quotation{adopt} the children in $C'(u)$ together with $u$ (line~\ref{line:setptou}). +Therefore, we construct a new parent node $p$ that will \quotation{adopt} the children in $C'(u)$ together with $u$ (\inline[line:setptou]). We will now explain why considering all but the largest children of a node lowers the algorithm's time complexity. Let $T$ be a splitting tree in which we color all children of each node blue, except for the largest one. @@ -577,7 +580,7 @@ For finding the largest child, we maintain counts for the temporary children and On finalizing the temporary children we store (a reference to) the biggest child in the node, so that we can skip this node later in the algorithm. \stopdescription \startdescription{Storing sequences.} -The operation on line~\ref{line:prepend} is done in constant time by using a linked list. +The operation on \inline[line:prepend] is done in constant time by using a linked list. \stopdescription \stopproof