figures for nom aut

content.tex

@@ -11,12 +11,18 @@
 \completelistofalgorithms
 
 \component content/introduction
+
+\startpart[title={Testing}]
 \component content/test-methods
 \component content/applying-automata-learning
 \component content/minimal-separating-sequences
+\stoppart
+
+\startpart[title={Nominal Automata}]
 \component content/learning-nominal-automata
 \component content/ordered-nominal-sets
 \chapter{Succinct Nominal Automata?}
+\stoppart
 
 \title{References}
 \placelistofpublications

content/introduction.tex

@@ -240,8 +240,7 @@ More importantly, their orbits $\orb(x^{\sigma})$ and $\orb(x^{\tau})$ are diffe
 This shows that there is an injective map from $2^{\omega}$ to the orbits of $\atoms^{\omega}$.
 This concludes that $\atoms^{\omega}$ has uncountably many orbits.
 \stopitemize
-
+\stopexample
-
 
 
 \stopsubsection

content/learning-nominal-automata.tex

@@ -83,7 +83,8 @@ The learning algorithm works by incrementally building an {\em observation table
 The algorithm is able to fill the table with membership queries.
 As an example, and to set notation, consider the following table (over $A=\{a, b\}$).
 
-\starttikzpicture
+\placefigure[force, none]{}{
+\hbox{\starttikzpicture
 \matrix[obs table](tab)
 {
  \phantom{\epsilon} \& \epsilon \& a \& aa \\
@@ -107,7 +108,7 @@ As an example, and to set notation, consider the following table (over $A=\{a, b
 \draw[->, shorten >=10pt, dotted] (r1.east) -- (row.west);
 \draw[->, shorten >=10pt, dotted] (r2.east) -- (row.west);
 \draw[->, shorten >=10pt, dotted] (r3.east) -- (row.west);
-\stoptikzpicture
+\stoptikzpicture}}
 
 This table indicates that $\lang$ contains at least $aa$ and definitely does not contain the words $\epsilon, a, b, ba, baa, aaa$.
 Since $row$ is fully determined by the language $\lang$, we will from now on refer to an observation table as a pair $(S,E)$, leaving the language $\lang$ implicit.
@@ -695,6 +696,7 @@ We fix a target language $\lang$, which is assumed to be a nominal regular langu
 
 The learning algorithm for nominal automata, \nLStar{}, will be very similar to \LStar{} in \in{Algorithm}[alg:alg].
 In fact, we only change the following lines:
+\todo{In Alg environment?}
 \placeformula[eq:changes]
 \startformula[interlinespace=small]\startmathmatrix[n=2, align={middle, left}, distance=1cm]
 \NC \text{\color[darkgray]{7'}}   \NC S \gets S \cup \orb(sa)       \NR
@@ -878,7 +880,77 @@ In particular our algorithm is easily adapted to include optimizations such as t
 \startsubsection
   [title={Example}]
 
-\todo{Figure \tt 186-257}
+\startplacefigure
+  [title={Example automaton to be learnt and three subsequent tables computed by \nLStar{}.
+          In the automaton, $x,y,z$ denote distinct atoms.},
+   list={Example automaton with three subsequent tables computed by \nLStar{}.},
+   reference=fig:ex,
+   location=page]
+\startcombination[nx=3,ny=1,location=middle,distance=.5cm]
+{\starttikzpicture
+	\node[initial, state] (q0) {$q_0$};
+	\node[state, right of=q0] (q1) {$q_{1,x}$};
+	\node[state, accepting, below of=q1] (q2) {$q_{2, x, y}$};
+
+	\path[->]
+	(q0) edge [bend left] node [above] {$x$} (q1)
+	(q1) edge [bend left] node [above] {$x$} (q0)
+	(q1) edge [bend left] node [right] {$y$} (q2)
+	(q2) edge [bend left] node [right] {$y$} (q1)
+	(q2) edge             node [below left] {$x$} (q0)
+	(q2) edge [loop left] node [left]  {$z$} (q2);
+\stoptikzpicture}{}
+{\starttikzpicture
+\matrix[obs table](tab)
+{
+ T_1      \& \epsilon \\
+ \epsilon \& 0        \\
+ a        \& 0        \\
+ ab       \& 1        \\
+ aa       \& 0        \\
+ aba      \& 0        \\
+ abb      \& 0        \\
+ abc      \& 1        \\
+};
+\draw (tab-2-2.north -| tab.west) -- (tab-2-2.north -| tab.east);
+\draw (tab-5-2.north -| tab.west) -- (tab-5-2.north -| tab.east);
+\draw (tab-2-2.west |- tab.north) -- (tab-2-2.west |- tab.south);
+\stoptikzpicture}{}
+{\starttikzpicture
+\matrix[obs table, nodes={anchor=west}](tab)
+{
+ T_2      \& \epsilon \& a'                       \\
+ \epsilon \& 0        \& 0                        \\
+ a        \& 0        \& \NomCell{a' \neq a}      \\
+ ab       \& 1        \& \NomCell{a' \neq a{,} b} \\
+ aa       \& 0        \& 0                        \\
+ aba      \& 0        \& 0                        \\
+ abb      \& 0        \& \NomCell{a' \neq a}      \\
+ abc      \& 1        \& \NomCell{a' \neq a{,} b} \\
+};
+\draw (tab-2-2.north -| tab.west) -- (tab-2-2.north -| tab.east);
+\draw (tab-5-2.north -| tab.west) -- (tab-5-2.north -| tab.east);
+\draw (tab-2-2.west |- tab.north) -- (tab-2-2.west |- tab.south);
+\stoptikzpicture}{}
+\stopcombination
+
+\hbox{\starttikzpicture
+\matrix[obs table, nodes={anchor=west}](tab)
+{
+ T_3      \& \epsilon \& a'                       \& b'a'                                                                          \\
+ \epsilon \& 0        \& 0                        \& 1                                                                             \\
+ a        \& 0        \& \NomCell{a' \neq a}      \& \NomCell{a \neq a'{,}b'}                                                      \\
+ ab       \& 1        \& \NomCell{a' \neq a{,} b} \& \NomCell{(b' \neq a{,}b \wedge a' \neq a{,}b) \vee (b' = b \wedge a' \neq a)} \\
+ aa       \& 0        \& 0                        \& 1                                                                             \\
+ aba      \& 0        \& 0                        \& 1                                                                             \\
+ abb      \& 0        \& \NomCell{a' \neq a}      \& \NomCell{a \neq a'{,}b'}                                                      \\
+ abc      \& 1        \& \NomCell{a' \neq a{,} b} \& \NomCell{(b' \neq a{,}b \wedge a' \neq a{,}b) \vee (b' = b \wedge a' \neq a)} \\
+};
+\draw (tab-2-2.north -| tab.west) -- (tab-2-2.north -| tab.east);
+\draw (tab-5-2.north -| tab.west) -- (tab-5-2.north -| tab.east);
+\draw (tab-2-2.west |- tab.north) -- (tab-2-2.west |- tab.south);
+\stoptikzpicture}
+\stopplacefigure
 
 Consider the target automaton in \in{Figure}[fig:ex] and an observation table $T_1$ at some stage during the algorithm.
 We remind the reader that the table is represented in a symbolic way:
@@ -976,7 +1048,34 @@ We first illustrate \NLStar{}, then we discuss its extension to nominal automata
 The states of this automaton correspond to Myhill-Nerode right-congruence classes, but can be exponentially smaller than the corresponding minimal DFA:
 \emph{Composed} states, language-equivalent to sets of other states, can be dropped.
 
-\todo{alg \tt 9-39}
+\startplacealgorithm
+  [title={Algorithm for learning NFAs by \citet[DBLP:conf/ijcai/BolligHKL09].},
+   reference=alg:nfa-alg]
+\startalgorithmic
+\startlinenumbering
+\STATE $S,E \gets \{\epsilon\}$
+\REPEAT
+	\WHILE{$(S, E)$ is not RFSA-closed or not RFSA-consistent\someline[line:nfa-checks]}
+		\IF{$(S, E)$ is not RFSA-closed \startline[line:nfa-closed]}
+		\STATE find $s \in S, a \in A$ such that $row(s a) \in PR(S, E) \setminus PR^{\top}(S, E)$ \someline[line:nfa-clos-witness]
+		\STATE $S\gets S \cup \{sa\}$ \someline[line:nfa-addrow-clos]
+		\ENDIF\stopline[line:nfa-closed]
+		\IF{$(S, E)$ is not RFSA-consistent \startline[line:nfa-const]}
+		\STATE find $s_1,s_2 \in S$, $a \in A$, and $e \in E$ such that
+		\STATE \hfill $row(s_1) \rowincl row(s_2)$ and $\lang(s_1 a e) = 1$, $\lang(s_2 a e) = 0$ \someline[line:nfa-cons-witness]
+		\STATE $E\gets E\cup \{ae\}$ \someline[line:nfa-addcol-cons]
+		\ENDIF\stopline[line:nfa-const]
+	\ENDWHILE
+	\STATE Make the conjecture $N(S,E)$ \someline[line:nfa-conj]
+	\IF{the Teacher replies {\bf no}, with a counter-example $t$\someline[line:nfa-counter-ex]}
+	\STATE $E \gets E \cup \suff(t)$ \someline[line:nfa-addcol-ex]
+	\ENDIF
+\UNTIL{the Teacher replies {\bf yes} to the conjecture $N(S, E)$}
+\RETURN $N(S, E)$
+\stoplinenumbering
+\stopalgorithmic
+\stopplacealgorithm
+
 
 The algorithm \NLStar{} equips the observation table $(S, E)$ with a union operation, allowing for the detection of \emph{composed} and \emph{prime} rows.
 
@@ -1002,10 +1101,10 @@ A table $(S, E)$ is:
 \stopdefinition
 
 If $(S, E)$ is not RFSA-closed, then there is a row in the bottom part of the table which is prime, but not contained in the top part.
-This row is then added to $S$ (line \ref{line:nfa-clos-witness}).
+This row is then added to $S$ (\inline[line:nfa-clos-witness]).
 If $(S,E)$ is not RFSA-consistent, then there is a suffix which does not preserve the containment of two existing rows, so those rows are actually incomparable.
-A new column is added to distinguish those rows (line \ref{line:nfa-cons-witness}).
+A new column is added to distinguish those rows (\inline[line:nfa-cons-witness]).
-Notice that counterexamples supplied by the teacher are added \emph{to columns} (line \ref{line:nfa-addcol-ex}).
+Notice that counterexamples supplied by the teacher are added \emph{to columns} (\inline[line:nfa-addcol-ex]).
 Indeed, it is shown by \cite[authoryears][DBLP:conf/ijcai/BolligHKL09] that treating the counterexamples as in the original \LStar{}, namely adding them to rows, does not lead to a terminating algorithm.
 
 \startdefinition[reference=def:nfa-conj]
@@ -1054,7 +1153,7 @@ Intuitively, all states of a nominal RSFA recognize residuals, but not all resid
 There may be a residual $\lang'$ and a set of states $Q'$ such that $\lang' = \bigcup_{q \in Q'} \lang(q)$, but no state $q'$ is such that $\lang(q') = \lang'$.
 A residual $\lang'$ is called \emph{composed} if it is equal to the union of the components it strictly contains, explicitly
 \startformula
-\lang' = \Union \{ \lang'' \in R(\lang) \mid \lang'' \subsetneqq \lang' \} ;
+\lang' = \Union \{ \lang'' \in R(\lang) \mid \lang'' \subsetneq \lang' \} ;
 \stopformula
 otherwise it is called \emph{prime}.
 In an ordinary RSFA, composed residuals have finitely-many components.
@@ -1085,12 +1184,12 @@ Our nominal version of \NLStar{} again makes use of an observation table $(S, E)
 As in the basic algorithm, we equip $(S, E)$ with a union operation $\rowunion$ and row containment relation $\rowincl$, defined as in \in{Definition}[def:rows-jsl].
 It is immediate to verify that $\rowunion$ and $\rowincl$ are equivariant.
 
-Our algorithm is a simple modification of the algorithm in \in{Algorithm}[fig:nfa-alg], where a few lines are replaced:
+Our algorithm is a simple modification of the algorithm in \in{Algorithm}[alg:nfa-alg], where a few lines are replaced:
-\startformula
+\startformula[interlinespace=small]\startmathmatrix[n=2, align={middle, left}, distance=1cm]
-6'    S \gets S \cup \orb(sa)        \qquad
+\NC \text{\color[darkgray]{6'}}   \NC S \gets S \cup \orb(sa)       \NR
-9'    E \gets E \cup \orb(ae)        \qquad
+\NC \text{\color[darkgray]{11'}}  \NC E \gets E \cup \orb(ae)       \NR
-12'   E \gets E \cup \suff(\orb(t))
+\NC \text{\color[darkgray]{16'}}  \NC S \gets S \cup \suff(\orb(t)) \NR
-\stopformula
+\stopmathmatrix\stopformula
 Switching to nominal sets, several decidability issues arise.
 The most critical one is that rows may be the union of infinitely many component rows, as happens for residuals of nominal languages, so finding all such components can be challenging.
 We adapt the notion of composed to rows: $row(t)$ is composed whenever
@@ -1104,7 +1203,7 @@ We now check that relevant parts of our algorithm terminate.
 {\bf Row Containment Check.}
 The basic containment check $row(s) \rowincl row(t)$ is decidable, as $row(s)$ and $row(t)$ are supported by the finite supports of $s$ and $t$ respectively.
 
-{\bf Line \ref{line:nfa-checks}.}
+{\bf \inline{Line}[line:nfa-checks].}
 RFSA-Closedness and RFSA-Consistency Checks.
 
 We first show that prime rows form orbit-finite nominal sets.
@@ -1119,13 +1218,12 @@ This may not be equivariant under permutations $Perm(\EAlph)$, but it is if we p
 \startlemma[reference=lem:comp-prop]
 The set $C(row(t))$ has the following properties:
 \startitemize
-\item $\supp(C(row(t))) \subseteq \supp(row(t))$. \label{supp}
+\item $\supp(C(row(t))) \subseteq \supp(row(t))$.
 \item it is equivariant and orbit-finite under the action of the group
 \startformula
 G_t = \{ \pi \in Perm(\EAlph) \mid \restr{\pi}{\supp(row(t))} = \id \}
 \stopformula
 of permutations fixing $\supp(row(t))$.
-\label{orb-fin}
 \stopitemize
 \stoplemma
 
@@ -1134,16 +1232,16 @@ In fact, $\Rowunion$ is equivariant w.r.t the whole $Perm(\EAlph)$ and then, in
 Now, to check $row(t) = \Rowunion C(row(t))$, we can just pick one representative of every orbit of $S \Lext A$, because we have $C(\pi \cdot row(t)) = \pi \cdot C(row(t))$ and permutations distribute over $\rowunion$, so permuting both sides of the equation gives again a valid equation.
 
 For RFSA-consistency, consider the two sets:
-\startformula
+\startformula\startalign
-N = \{ (s_1, s_2) \in S \times S \mid row(s_1) \rowincl row(s_2) \} \\
+\NC N \NC = \{ (s_1, s_2) \in S \times S \mid row(s_1) \rowincl row(s_2) \}                    \NR
-M = \{ (s_1, s_2) \in S \times S \mid \forall a \in A : row(s_1a) \rowincl row(s_2a) \}
+\NC M \NC = \{ (s_1, s_2) \in S \times S \mid \forall a \in A : row(s_1a) \rowincl row(s_2a) \} \NR
-\stopformula
+\stopalign\stopformula
 They are both orbit-finite nominal sets, by equivariance of $row$, $\rowincl$ and $A$.
 We can check RFSA-consistency in finite time by picking orbit representatives from $N$ and $M$.
 For each representative $n \in N$, we look for a representative $m \in M$ and a permutation $\pi$ such that $n = \pi \cdot m$.
 If no such $m$ and $\pi$ exist, then $n$ does not belong to any orbit of $M$, so it violates RFSA-consistency.
 
-{\bf Lines \ref{line:nfa-clos-witness} and \ref{line:nfa-cons-witness}: Finding Witnesses for Violations.}
+{\bf \inline{Lines}[line:nfa-clos-witness] and \inlinerange[line:nfa-cons-witness]: Finding Witnesses for Violations.}
 We can find witnesses by comparing orbit representatives of orbit-finite sets, as we did with RFSA-consistency.
 Specifically, we can pick representatives in $S \times A$ and $S \times S \times A \times E$ and check them against the following orbit-finite nominal sets:
 \startitemize
@@ -1217,7 +1315,7 @@ Therefore the orbit of $(row'(s_1), row'(s_2))$ is not in $I$.
 Moreover, $row'(s) \rowincls row'(t)$ implies $row(s) \rowincls row(t)$ (as no new rows are added), so no new pairs are added to $I$.
 Overall, $I$ has less orbits ({\bf C2}).
 \item
-If $row(s_1) = row(s_2)$, then we must have $row(s_1) = \pi \cdot row(s_1)$, for some $\pi$, because line~\ref{line:begin-nfa-closed} forbids equal rows in different orbits.
+If $row(s_1) = row(s_2)$, then we must have $row(s_1) = \pi \cdot row(s_1)$, for some $\pi$, because \inline[line:nfa-closed] forbids equal rows in different orbits.
 In this case $row'(s_1) \neq \pi \cdot row'(s_1)$ and we can use part of the proof of \in{Theorem}[thm:termination] to see that the orbit of $row'(s_1)$ has bigger dimension or less local symmetries than that of $row(s_1)$ ({\bf C3}).
 \stopitemize
 Orbits of $(S \cup S \Lext A)/{\sim}$ and of $I$ are finitely-many, by \in{Lemma}[lem:rows-min-dfa] and what we proved above.
@@ -1276,8 +1374,8 @@ Then the table has:
 \stoplemma
 \startproof
 By \in{Lemma}[lem:rows-min-dfa], the number of orbits of rows indexed by $S$ is at most $n$.
-Now, notice that line~\ref{line:nfa-clos-witness} does not add $\orb(sa)$ to $S$ if $sa \in S$, and lines~\ref{line:nfa-addcol-ex}~and~\ref{line:nfa-addcol-cons} cannot identify rows, so $S$ has at most $n$ orbits.
+Now, notice that \inline[line:nfa-clos-witness] does not add $\orb(sa)$ to $S$ if $sa \in S$, and \inline{lines}[line:nfa-addcol-ex] and \inlinerange[line:nfa-addcol-cons] cannot identify rows, so $S$ has at most $n$ orbits.
-The length of the longest word in $S$ must be at most $n$, as $S = \{ \epsilon \}$ when the algorithm starts, and line~$6'$ adds words with one additional symbol than those in $S$.
+The length of the longest word in $S$ must be at most $n$, as $S = \{ \epsilon \}$ when the algorithm starts, and \todo{line} $6'$ adds words with one additional symbol than those in $S$.
 
 For columns, we note that both fixing RFSA-consistency and adding counterexamples increase the number of columns, but this can happen at most $E'_{n,k}$ times (see proof of \in{Lemma}[lem:nfa-eq-queries]).
 Each time at most $m$ suffixes are added to $E$.
@@ -1415,6 +1513,7 @@ We remark that our algorithms seamlessly merge with teachers written in NLambda,
 We are currently working on a new version of the library in which this will be possible.
 \todo{Dit kan nu al}
 
+
 \stopsubsection
 \startsubsection
   [title={Test Cases},
@@ -1422,7 +1521,33 @@ We are currently working on a new version of the library in which this will be p
 
 To provide a benchmark for future improvements, we tested our algorithms on a few simple automata described below. We report results in \in{Table}[tab:results].
 The experiments were performed on a machine with an Intel Core i5 (Skylake, 2.4 GHz) and 8 GB RAM.
-\todo{Tabel \tt 110-134}
+
+\placetable[here][tab:results]
+{Results of experiments.
+The column DFA (resp. RFSA) shows the number of orbits (left sub-column) and dimension (right sub-column) of the learnt minimal DFA (resp. canonical RFSA).
+We use $\infty$ when the running time is too high.
+\todo{Getallen in mathmode?}}
+\starttabulate[|l|c|c|cg{.}|cg{.}|c|c|cg{.}|][distance=none]
+\NC Model \NC \NC \VL \nLStar{} (s) \NC \nLStar{}$_{\text{col}}$ (s) \VL \NC \VL \nNLStar{} (s) \NC\NR
+\HL
+\NC FIFO$_0$   \NC  2 \NC 0 \VL 1.9  \NC 1.9  \VL 2        \NC 0        \VL 2.4      \NC\NR
+\NC FIFO$_1$   \NC  3 \NC 1 \VL 12.9 \NC 7.4  \VL 3        \NC 1        \VL 17.3     \NC\NR
+\NC FIFO$_2$   \NC  5 \NC 2 \VL 45.6 \NC 22.6 \VL 5        \NC 2        \VL 70.3     \NC\NR
+\NC FIFO$_3$   \NC 10 \NC 3 \VL 189  \NC 107  \VL 10       \NC 3        \VL 476      \NC\NR
+\NC FIFO$_4$   \NC 25 \NC 4 \VL 370  \NC 267  \VL 25       \NC 4        \VL 1230     \NC\NR
+\NC FIFO$_5$   \NC 77 \NC 5 \VL 1337 \NC 697  \VL $\infty$ \NC $\infty$ \VL $\infty$ \NC\NR
+\HL
+\NC $\lang_0$  \NC  2 \NC 0 \VL 1.3  \NC 1.4  \VL 2 \NC 0 \VL 1.4    \NC\NR
+\NC $\lang_1$  \NC  4 \NC 1 \VL 29.6 \NC 4.7  \VL 4 \NC 1 \VL 8.9    \NC\NR
+\NC $\lang_2$  \NC  7 \NC 2 \VL 229  \NC 23.1 \VL 7 \NC 2 \VL 84.7   \NC\NR
+\HL
+\NC $\lang'_0$ \NC  3 \NC 1 \VL 4.4  \NC 4.9  \VL 3 \NC 1 \VL 11.3   \NC\NR
+\NC $\lang'_1$ \NC  5 \NC 1 \VL 15.4 \NC 15.4 \VL 4 \NC 1 \VL 66.4   \NC\NR
+\NC $\lang'_2$ \NC  9 \NC 1 \VL 46.3 \NC 40.5 \VL 5 \NC 1 \VL 210    \NC\NR
+\NC $\lang'_3$ \NC 17 \NC 1 \VL 89.0 \NC 66.8 \VL 6 \NC 1 \VL 566    \NC\NR
+\HL
+\NC $\lang_{eq}$ \NC n/a \NC n/a \VL n/a \NC n/a \VL 3 \NC 1 \VL 16.3 \NC\NR
+\stoptabulate
 
 {\bf Queue Data Structure.}
 A queue is a data structure to store elements which can later be retrieved in a first-in, first-out order.
@@ -1430,9 +1555,25 @@ It has two operations: \kw{push} and \kw{pop}.
 We define the alphabet $\Sigma_{\text{FIFO}} = \{ \kw{push}(a), \kw{pop}(a) \mid a \in \EAlph \}$.
 The language $\text{FIFO}_n$ contains all valid traces of \kw{push} and \kw{pop} using a bounded queue of size $n$.
 The minimal nominal DFA for $\text{FIFO}_2$ is
-\todo{tikz \tt 143-160}
 
-The state reached from $q_{1,x}$ via $\xrightarrow{push(x)}$ is omitted:
+\starttikzpicture[node distance=4cm]
+	\node[state, initial, accepting] (q0) {$q_0$};
+	\node[state, accepting, right of=q0] (q1) {$q_{1,x}$};
+	\node[state, accepting, right of=q1] (q2) {$q_{2, x, y}$};
+	\node[state, below=1cm of q0] (bot) {$\bot$};
+
+	\path[->]
+	(q0) edge[bend left=15] node[above] {$\kw{push}(x)$} (q1)
+	(q1) edge[bend left=15] node[below] {$\kw{pop}(x)$} (q0)
+	(q1) edge[bend left=15] node[above] {$\kw{push}(y)$} (q2)
+	(q2) edge[bend left=15] node[below,xshift=-5pt] {$\kw{pop}(x)$ to $q_{1,y}$} (q1)
+	(q0) edge node[left] {$\kw{pop}(\EAlph)$} (bot)
+	(q1) edge[bend left] node[right] {$\kw{pop}(\neq x)$} (bot)
+	(q2) edge[bend left] node[below, align=center] {$\kw{pop}(\neq x)$ \\ $\kw{push}(\EAlph)$} (bot)
+	(bot) edge[loop left] node {$\ast$} (bot);
+\stoptikzpicture
+
+The state reached from $q_{1,x}$ via $\kw{push}(x)$ is omitted:
 Its outgoing transitions are those of $q_{2,x,y}$, where $y$ is replaced by $x$.
 Similar benchmarks appear in \cite[DBLP:conf/ictac/AartsFKV15, DBLP:journals/ml/IsbernerHS14].
 
@@ -1445,7 +1586,24 @@ Consider the language $\lang_{eq} = \bigcup_{a \in \EAlph} \EAlph^{\ast} a \EAlp
 This is accepted by an NFA which guesses the position of the first occurrence of a repeated letter $a$ and then waits for the second $a$ to appear.
 The language is not accepted by a DFA \cite[DBLP:journals/corr/BojanczykKL14].
 Despite this \nNLStar{} is able to learn the automaton:
-\todo{tikz \tt 173-190}
+
+\starttikzpicture[node distance=4cm]
+	\node[state, initial] (q0) {$q_0'$};
+	\node[state, right of=q0] (q1) {$q_{1,x}'$};
+	\node[state, accepting, right of=q1] (q2) {$q_{2}'$};
+
+	\path[->]
+	(q0) edge[bend left=15] node[above] {$x$} (q1)
+	(q1) edge[bend left=15] node[below] {$\EAlph$} (q0)
+	(q1) edge[bend left=15] node[above] {$x$} (q2)
+	(q2) edge[bend left=15] node[below] {$\EAlph$ to any $q_{2,x}'$} (q1)
+	(q2) edge[bend left=45] node[below] {$\EAlph$} (q0)
+	(q0) edge[loop above] node[above] {$\EAlph$} (q0)
+	(q1) edge[loop above] node[above] {$\EAlph$} (q1)
+	(q1) edge[loop below] node[below] {$y$ to $q_{2,y}'$} (q1)
+	(q2) edge[loop above] node[above] {$\EAlph$} (q2);
+\stoptikzpicture
+
 where the transition from $q_2'$ to $q_{1,x}'$ is defined as $\delta(q_2', a) = \{ q_{1,b}' \mid b \in \EAlph \}$.
 
 {\bf $n$-last Position.}
@@ -1507,6 +1665,7 @@ We implemented our algorithms in the nominal library NLambda as sketched before.
 Other implementation options include Fresh OCaml \cite[DBLP:journals/entcs/Shinwell06], a functional programming language designed for programming over nominal data structures with binding, and \LOIS{} by \cite[authoryears][DBLP:conf/cade/KopczynskiT16, DBLP:conf/popl/KopczynskiT17], a C++ library for imperative nominal programming.
 We chose NLambda for its convenient set-theoretic primitives, but the other options remain to be explored, in particular the low-level \LOIS{} could be expected to provide more efficient implementations.
 
+
 \stopsection
 \startsection
   [title={Discussion and Future Work}]
@@ -1531,17 +1690,37 @@ Our algorithm \nNLStar{} is based on the \emph{powerset} monad, representing cla
 We are currently investigating a \emph{substitution} monad, where the operation is \quotation{applying a (possibly non-injective) substitution of atoms in the support}.
 A minimal automaton over this monad, akin to a RFSA, will have states that can generate all the states of the associated minimal DFA via a substitution, but cannot be generated by other states (they are prime).
 For instance, we can give an automaton over the substitution monad that recognizes $\lang_2$ from \in{Section}[sec:overview]:
-\todo{tikz \tt 16-37}
+
+\placefigure[force, none]{}{
+\hbox{\starttikzpicture
+	\node[state, initial] (q0) {$q_0$};
+	\node[state, right of=q0] (qxp) {$q_x$};
+	\node[state, right of=qxp] (qxyp) {$q_{xy}$};
+	\node[state, right of=qxyp] (qys) {$q_{y}$};
+	\node[state, accepting, right of=qys] (q1) {$q_1$};
+	\node[state, right of=q1] (q2) {$q_2$};
+
+	\path[->]
+	(q0)   edge node[above] {$x$} (qxp)
+	(qxp)  edge[bend right] node[above] {$y$} (qxyp)
+	(qxp)  edge[bend left] node[above] {$x,[y \mapsto x]$} (qxyp)
+	(qxyp) edge node[above] {$x$} (qys)
+	(qxyp) edge[bend left,out=45,in=135] node[above] {$\neq x$} (q2)
+	(qys)  edge node[above] {$y$} (q1)
+	(qys)  edge[bend left] node[above] {$\neq y$} (q2)
+	(q1)   edge node[above] {$A$} (q2)
+	(q2)   edge[loop right] node[right] {$A$} (q2);
+\stoptikzpicture}}
 
 Here $[y \mapsto x]$ means that, if that transition is taken, $q_{xy}$ (hence its language) is subject to $y \mapsto x$.
 In general, the size of the minimal DFA for $\lang_n$ grows more than exponentially with $n$, but an automaton with substitutions on transitions, like the one above, only needs $\bigO(n)$ states.
 
-In principle, thanks to the generic approach we have taken, all our algorithms should work for various kinds of atoms with more structure than just equality, as advocated by \cite[authoryears][DBLP:journals/corr/BojanczykKL14].
+In principle, thanks to the generic approach we have taken, all our algorithms should work for various kinds of atoms with more structure than just equality, as advocated by \citet[DBLP:journals/corr/BojanczykKL14].
 Details, such as precise assumptions on the underlying structure of atoms necessary for proofs to go through, remain to be checked.
 For an implementation of automata learning over other kinds of atoms without compromising the generic approach, an extension of NLambda to those atoms will be needed, as the current version of the library only supports equality and totally ordered atoms.
 
 The efficiency of our current implementation, as measured in \in{Section}[sec:tests], leaves much to be desired.
-There is plenty of potential for running time optimization, ranging from improvements in the learning algorithms itself, to optimizations in the NLambda library (such as replacing the external and general-purpose SMT solver with a purpose-built, internal one, or a tighter integration of nominal mechanisms with the underlying Haskell language as it was done by \cite[authoryears][DBLP:journals/entcs/Shinwell06]), to giving up the functional programming paradigm for an imperative language such as LOIS \cite[DBLP:conf/cade/KopczynskiT16, DBLP:conf/popl/KopczynskiT17].
+There is plenty of potential for running time optimization, ranging from improvements in the learning algorithms itself, to optimizations in the NLambda library (such as replacing the external and general-purpose SMT solver with a purpose-built, internal one, or a tighter integration of nominal mechanisms with the underlying Haskell language as it was done by \citenp[DBLP:journals/entcs/Shinwell06]), to giving up the functional programming paradigm for an imperative language such as LOIS \cite[DBLP:conf/cade/KopczynskiT16, DBLP:conf/popl/KopczynskiT17].
 
 
 \stopsection

content/ordered-nominal-sets.tex

@@ -130,13 +130,14 @@ For instance, the set $\mathbb{Z} \in \mathcal{P}(\Q)$ of integers has no finite
 
 
 If $S \subseteq \mathcal{D}$ is a support of an element $x \in X$, then any set $S' \subseteq \mathcal{D}$ such that $S \subseteq S'$ is also a support of $x$.
-A set $S \subseteq \mathcal{D}$ is a \emph{least support} of $x \in X$ if it is a support of $x$ and $S \subseteq S'$ for any support $S'$ of $x$.
+A set $S \subseteq \mathcal{D}$ is a \emph{least finite support} of $x \in X$ if it is a support of $x$ and $S \subseteq S'$ for any support $S'$ of $x$.
-The existence of least supports is crucial for representing orbits. 
+The existence of least finite supports is crucial for representing orbits.
-Unfortunately, even when elements have a finite support, in general they do not always have a least support.
+Unfortunately, even when elements have a finite support, in general they do not always have a least finite support.
-A data symmetry $(\mathcal{D}, G)$ is said to \emph{admit least supports} if every element of every nominal set 
+A data symmetry $(\mathcal{D}, G)$ is said to \emph{admit least supports} if every element of every nominal set has a least finite support.
-has a least support. Both the equality and the total order symmetry admit least supports.
+Both the equality and the total order symmetry admit least supports.
 (\citenp[DBLP:journals/corr/BojanczykKL14] give additional (counter)examples of data symmetries admitting least supports.)
-Having least supports is useful for a finite representation.
+Having least finite supports is useful for a finite representation.
+Henceforth, we will write \emph{least support} to mean least finite support.
 
 Given a nominal set $X$, the size of the least support of an element $x \in X$ is denoted by $\dim(x)$, the \emph{dimension} of $x$.
 We note that all elements in the orbit of $x$ have the same dimension.

environment/font.tex

@@ -19,6 +19,8 @@
 \definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range=0x0266D-0x0266F,rscale=0.95] % sharp and flat
 \definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range={0x025A1,0x025B3}] % triangle, square
 \definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range={0x022EE, 0x02254}] % vdots, assignment
+\definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range=0x0228F-0x02294] % square cup etc
+\definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range={0x02A05, 0x02A06}] % big sq cup
 % \definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range={0x02713,0x02717}] % checkmark
 % Neo Euler voor wiskunde. Merk op dat dit niet cursief is!
 \definefontfamily[mainfamily] [mm] [Neo Euler] [rscale=0.95]

environment/tikz.tex

@@ -19,4 +19,12 @@
 \draw ({(#1+#2)/2-0.5},{(3-#3)*0.75+0.65}) node[fill=white] (B#4) {{$B_{#4}$} {$\scriptscriptstyle #5$}};
 }
 
+% Used to draw extended cells in observation tables for the learning nominal automata paper
+\define[1]\NomCell{
+\startmathcases
+   \NC 1 \NC if $#1$   \NR
+   \NC 0 \NC else \NR
+\stopmathcases
+}
+
 \stopenvironment