Typesetted the algs. in sep seqs

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}
+\startplacealgorithm
-
+  [title={Constructing a stable splitting tree.},
-%\begin{algorithm}[t]
+   reference=alg:tree]
-%    \DontPrintSemicolon
+\startalgorithmic
-%    \KwIn{A FSM $M$}
+\REQUIRE An FSM $M$
-%    \KwResult{A valid and stable splitting tree $T$}
+\ENSURE A valid and stable splitting tree $T$
-%    initialize $T$ to be a tree with a single node labeled $S$\;
+\startlinenumbering
-%    \Repeat{$P(T)$ is acceptable}{
+\STATE initialise $T$ to be a tree with a single node labelled $S$
-%        find $a \in I, B \in P(T)$ such that we can split $B$ w.r.t.\@ output $\lambda(\cdot, a)$\;
+\REPEAT
-%        expand the $u \in T$ with $l(u)=B$ as described in (split-output)\;
+	\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)
-%    \Repeat{$P(T)$ is stable}{
+\UNTIL{$P(T)$ is acceptable}
-%        find $a \in I, B \in P(T)$ such that we can split $B$ w.r.t.\@ state $\delta(\cdot, a)$\;
+\REPEAT
-%        expand the $u \in T$ with $l(u)=B$ as described in (split-state)\;
+	\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)
-%    \caption{Constructing a stable splitting tree}
+\UNTIL{$P(T)$ is stable}
-%    \label{alg:tree}
+\stoplinenumbering
-%\end{algorithm}
+\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]
+\startplacealgorithm
-%    \DontPrintSemicolon
+  [title={A step towards the stability of a splitting tree.},
-%    \KwIn{A FSM $M$ with $n$ states}
+   reference=alg:increase-k]
-%    \KwResult{A stable, minimal splitting tree $T$}
+\startalgorithmic
-%    initialize $T$ to be a tree with a single node labeled $S$\;
+\REQUIRE A $k$-stable and minimal splitting tree $T$
-%    \Repeat{$P(T)$ is acceptable}{
+\ENSURE $T$ is a $(k+1)$-stable, minimal splitting tree
-%        find $a \in I, B \in P(T)$ such that we can split $B$ w.r.t.\@ output $\lambda(\cdot, a)$\;
+\startlinenumbering
-%        expand the $u \in T$ with $l(u)=B$ as described in (split-output)\; 
+\FORALL{leaves $u \in T$ and all inputs $a \in I$}
-%    }
+	\STATE $v \gets \lca(\delta(l(u), a))$
-%    \For{$k=1$ to $n-1$}{
+	\IF{$v$ is an inner node and $|\sigma(v)| = k$}
-%        perform Algorithm~\ref{alg:increase-k} or Algorithm~\ref{alg:increase-k-v3} on $T$ for
+		\STATE expand $u$ as described in (split-state) (this generates new leaves)
-%        $k$\; 
+	\ENDIF
-%    }
+\ENDFOR
-%    \caption{Constructing a stable and minimal splitting tree}
+\stoplinenumbering
-%    \label{alg:minimaltree}
+\stopalgorithmic
-%\end{algorithm}
+\stopplacealgorithm
-
-%\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}
 
 \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?}
+\startplacealgorithm
-
+  [title={A better step towards the stability of a splitting tree.},
-%\begin{algorithm}[t]
+   reference=alg:increase-k-v3]
-%    \LinesNumbered
+\startalgorithmic
-%    \DontPrintSemicolon
+\REQUIRE A $k$-stable and minimal splitting tree $T$, and a list $L_k$
-%    \SetKw{KwContinue}{continue}
+\ENSURE $T$ is a $(k+1)$-stable and minimal splitting tree, and a list $L_{k+1}$
-%    \KwIn{a $k$-stable and minimal splitting tree $T$, and a list $L_k$}
+\startlinenumbering
-%    \KwResult{$T$ is a $(k+1)$-stable and minimal splitting tree, and a list $L_{k+1}$}
+\STATE $L_{k+1} \gets \emptyset$
-%    $L_{k+1} \gets \emptyset$\;
+\FORALL{$k$-candidates $v$ in $L_{k}$ in order}
-%    \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)$
-%        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{inputs $a$ in $I$}{
+		\FORALL{nodes $w$ in $C(v) \setminus \{ w' \}$}
-%            \ForAll{nodes $w$ in $C(v) \setminus w'$}{
+			\FORALL{states $s$ in $\delta^{-1}(l(w), a)$}
-%                \ForAll{states $s$ in $\delta^{-1}(l(w), a)$}{
+				\STATE locate leaf $u$ such that $s \in l(u)$
-%                    locate leaf $u$ such that $s \in l(u)$\;
+				\IF{$C'(u)$ does not contain node $u_{w}$}
-%                    \If{$C'(u)$ does not contain node $u_{w}$}{
+					\STATE add a new node $u_{w}$ to $C'(u)$ \someline[line:add-temp-child]
-%                        add a new node $u_{w}$ to $C'(u)$\;\label{line:add-temp-child}
+				\ENDIF
-%                    }
+				\STATE move $s$ from $l(u)$ to $l(u_{w})$ \someline[line:move-to-temp-child]
-%                    move $s$ from $l(u)$ to $l(u_{w})$\;\label{line:move-to-temp-child}
+			\ENDFOR
-%                }
+		\ENDFOR
-%            }
+		\FORALL{leaves $u$ with $C'(u) \neq \emptyset$\startline[line:finalize]}
-%            \ForEach{leaf $u$ with $C'(u) \neq \emptyset$}{\label{line:finalize}
+			\IF{$|l(u)| = 0$}
-%                \eIf{$|l(u)| = 0$}{
+				\IF{$|C'(u)| = 1$}
-%                    \If{$|C'(u)| = 1$}{
+					\STATE recover $u$ by moving its elements back and clear $C'(u)$ \someline[line:recover]
-%                        recover $u$ by moving its elements back and clear
+					\STATE {\bf continue} with the next leaf
-%                        $C'(u)$\;\label{line:recover}
+				\ENDIF
-%                        \KwContinue with the next leaf\;
+				\STATE set $p=u$ and $C(u)=C'(u)$ \someline[line:setptou]
-%                    }
+			\ELSE
-%                    set $p=u$ and $C(u)=C'(u)$\;\label{line:setptou}
+				\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
-%                    construct a new node $p$ and set $C(p) = C'(u) \cup \{ u \}$\;
+			\ENDIF
-%                    insert $p$ in the tree in the place where $u$ was\;
+			\STATE set $\sigma(p) = a \sigma(v)$ \someline[line:prepend]
-%                }
+			\STATE append $p$ to $L_{k+1}$ and clear $C'(u)$ \stopline[line:finalize]
-%                set $\sigma(p) = a \sigma(v)$\;\label{line:prepend}
+		\ENDFOR
-%                append $p$ to $L_{k+1}$ and clear $C'(u)$\;\label{line:finalize-end}
+	\ENDFOR
-%            }
+\ENDFOR
-%        }
+\stoplinenumbering
-%    }
+\stopalgorithmic
-%    \caption{A better step towards the stability of a splitting tree}
+\stopplacealgorithm
-%    \label{alg:increase-k-v3}
-%\end{algorithm}
 
 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}.
+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 (line~\ref{line:recover}). In the other case we make the temporary children permanent.
+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