Replaced hrefs with cites. Fixed some todos.

biblio-web.bib

@@ -1,8 +1,8 @@
 @misc{nlambda-code,
 	author    = {Michal Szynwelski},
 	title     = {{N}\lambda},
-	note      = {Website},
+	note      = {Website & Source code},
-	url       = {http://www.mimuw.edu.pl/~szynwelski/nlambda/},
+	url       = {https://www.mimuw.edu.pl/~szynwelski/nlambda/},
 	urldate   = {2018-08-14}
 }
 
@@ -36,7 +36,7 @@
 	author    = {Rick Smetsers and
 	             Joshua Moerman},
 	title     = {Partition},
-	note      = {Website},
+	note      = {Source code},
 	url       = {https://gitlab.science.ru.nl/rick/partition/}
 }
 
@@ -44,21 +44,36 @@
 	author    = {David Venhoek and
 	             Joshua Moerman},
 	title     = {ONS},
-	note      = {Website},
+	note      = {Source code},
 	url       = {https://github.com/davidv1992/ONS}
 }
 
 @misc{hybrid-ads-code,
 	author    = {Joshua Moerman},
 	title     = {Hybrid {ADS}},
-	note      = {Website},
+	note      = {Source code},
 	url       = {https://gitlab.science.ru.nl/moerman/hybrid-ads}
 }
 
 @misc{lois-lstar-code,
-	url       = {github.com/eryxcc/lois/blob/master/tests/learning.cpp}
+	author    = {Eryk Kopczynski},
+	title     = {Nominal LStar in LOIS},
+	note      = {Source code},
+	url       = {https://github.com/eryxcc/lois/blob/master/tests/learning.cpp}
 }
 
 @misc{nominal-lstar-conjecture,
-	url       = {joshuamoerman.nl/papers/2017/17popl-learning-nominal-automata.html}
+	author    = {Joshua Moerman},
+	title     = {Nominal LStar in polynomial time?},
+	note      = {Online note},
+	url       = {https://joshuamoerman.nl/papers/2017/17popl-learning-nominal-automata.html}
+}
+
+@misc{nominal-lstar-code,
+	author    = {Joshua Moerman and
+	             Michal Szynwelski and
+	             Bartek Klin},
+	title     = {Nominal LStar},
+	note      = {Source code},
+	url       = {https://github.com/Jaxan/nominal-lstar}
 }

biblio.bib

@@ -665,6 +665,21 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{Clouston13,
+	author    = {Ranald Clouston},
+	title     = {Generalised Name Abstraction for Nominal Sets},
+	booktitle = {Foundations of Software Science and Computation Structures - 16th
+	             International Conference, {FOSSACS} 2013. Proceedings},
+	pages     = {434--449},
+	year      = {2013},
+	crossref  = {DBLP:conf/fossacs/2013},
+	url       = {https://doi.org/10.1007/978-3-642-37075-5\_28},
+	doi       = {10.1007/978-3-642-37075-5\_28},
+	timestamp = {Tue, 26 Jun 2018 14:10:47 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/fossacs/Clouston13},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DavidMY02,
 	author    = {Alexandre David and
 	             M. Oliver M{\"{o}}ller and
@@ -1855,6 +1870,26 @@
 	year={2013}
 }
 
+@inproceedings{Pitts14,
+	author    = {Andrew M. Pitts},
+	editor    = {Hugo Herbelin and
+	             Pierre Letouzey and
+	             Matthieu Sozeau},
+	title     = {Nominal Presentation of Cubical Sets Models of Type Theory},
+	booktitle = {20th International Conference on Types for Proofs and Programs, {TYPES}
+	             2014, May 12-15, 2014, Paris, France},
+	series    = {LIPIcs},
+	volume    = {39},
+	pages     = {202--220},
+	publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
+	year      = {2014},
+	url       = {https://doi.org/10.4230/LIPIcs.TYPES.2014.202},
+	doi       = {10.4230/LIPIcs.TYPES.2014.202},
+	timestamp = {Thu, 23 Aug 2018 15:56:39 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/types/Pitts14},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{Pitts16,
 	author    = {Andrew M. Pitts},
 	title     = {Nominal techniques},

content/applying-automata-learning.tex

@@ -92,7 +92,7 @@ During recent years most researchers working on active automata learning focused
 Our work shows that if we want to further scale automata learning to industrial applications, we also need better algorithms for finding counterexamples for incorrect hypotheses.
 Following \citet[BergGJLRS05], our work shows that the context of automata learning provides both new challenges and new opportunities for the application of testing algorithms.
 All the models for the ESM case study together with the learning and testing statistics are available at \href{http://www.mbsd.cs.ru.nl/publications/papers/fvaan/ESM/}, as a benchmark for both the automata learning and testing communities.
-It is now also included in the automata wiki at \href{http://automata.cs.ru.nl/}.
+It is now also included in the automata wiki at \citeurl[automata-wiki].
 
 
 \startsection

content/learning-nominal-automata.tex

@@ -187,7 +187,7 @@ The table is closed and consistent, so we construct the hypothesis $\autom_1$,
 where $q_0 = row(\epsilon) = \{ \epsilon \mapsto 0 \}$:
 
 \placefigure[force, none]{}{
-\startcombination[nx=2, ny=1, location=middle]
+\startcombination[nx=2, ny=1, location=middle, distance=1cm]
 {\hbox{\starttikzpicture
 \matrix[obs table](tab)
 {
@@ -219,7 +219,7 @@ Therefore, \inline{line}[line:cons-witness] is triggered and an extra column $a$
 The new table is closed and consistent and a new hypothesis $\autom_2$ is constructed.
 
 \placefigure[force, none]{}{
-\startcombination[nx=3, ny=1, location=middle]
+\startcombination[nx=3, ny=1, location=middle, distance=1cm]
 {\hbox{\starttikzpicture[bend angle=45]
 \matrix[obs table](tab)
 {
@@ -283,7 +283,7 @@ Therefore we add the column $b$ and we get the table on the right, which is clos
 The new hypothesis is $\autom_3$.
 
 \placefigure[force, none]{}{
-\startcombination[nx=3, ny=1, location=middle]
+\startcombination[nx=3, ny=1, location=middle, distance=1cm]
 {\hbox{\starttikzpicture[bend angle=45]
 \matrix[obs table](tab)
 {
@@ -486,7 +486,7 @@ In fact, for any $a \in A$, we have $A = \{ \pi(a) \mid \text{$\pi$ is a permuta
 Then, by {\bf (P2)}, $row(\pi(a))(\epsilon) = row(a)(\epsilon) = 0$, for all $\pi$, so the first table can be written as:
 
 \placefigure[force, none]{}{
-\startcombination[nx=2, ny=1, location=middle]
+\startcombination[nx=2, ny=1, location=middle, distance=1cm]
 {\hbox{\starttikzpicture
 \matrix[obs table](tab)
 {
@@ -509,13 +509,8 @@ Our hypothesis is $\autom_1'$, where $\delta_{\autom_1'}(row(\epsilon),x) = row(
 As in {\bf Step 1}, the Teacher replies with the counterexample $aa$.
 \stopstep
 
-\startstep{2'} 
+\placefigure[right, none]{}{
-By equivariance of $\lang_1$, the counterexample tells us that \emph{all} words of length 2 with two repeated letters are accepted.
+\framed[frame=off]{\hbox{\starttikzpicture
-Therefore we extend $S$ with the (infinite!) set of such words.
-The new symbolic table is:
-
-\placefigure[force, none]{}{
-\hbox{\starttikzpicture
 \matrix[obs table](tab)
 {
  \phantom{\epsilon} \& \epsilon \\
@@ -529,7 +524,12 @@ The new symbolic table is:
 \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}}
+\stoptikzpicture}}}
+
+\startstep{2'}
+By equivariance of $\lang_1$, the counterexample tells us that \emph{all} words of length 2 with two repeated letters are accepted.
+Therefore we extend $S$ with the (infinite!) set of such words.
+The new symbolic table is depcited on the right.
 
 The lower part stands for elements of $S \Lext A$.
 For instance, $ab$ stands for words obtained by appending a fresh letter to words of length 1 (row $a$).
@@ -911,9 +911,8 @@ Second, the new hypothesis does not necessarily have more states, again it might
 
 From the proof \in{Theorem}[thm:termination] we observe moreover that the way we handle counterexamples is not crucial.
 Any other method which ensures a nonequivalent hypothesis will work.
-In particular our algorithm is easily adapted to include optimisations such as the ones by \cite[authoryears][RivestS93, MalerP95], where counterexamples are added as columns.
+In particular our algorithm is easily adapted to include optimisations such as the ones by \citet[RivestS93, MalerP95], where counterexamples are added as columns.
-
+\footnote{The additional optimisation of omitting the consistency check \citep[RivestS93] cannot be done: we always add a whole orbit to $S$ (to keep the set equivariant) and inconsistencies can arise within an orbit.}
-\todo{Consistentie is nodig?}
 
 
 \stopsubsection
@@ -1034,6 +1033,9 @@ We will use $\log$ in base two.
 	This is bounded by the number of divisors of $k!$, as each subgroup divides the order of the group.
 	We can easily bound the number of divisors of any $m$ by $\log m$ and so
 	one can at take a subgroup at most $k \log k$ times when starting with $S_k$.
+	\footnote{After publication we found a better bound by \citet[CameronST89]:
+	the length of the longest chain of subgroups of $S_k$ is $\left\lceil \frac{3}{2} k \right\rceil - b(k) - 1$, where $b(k)$ is the number of ones in the binary representation of $k$.
+	This gives a linear bound in $k$, instead of the \quote{linearithmic} bound.}
 	
 	Since the hypothesis will grow monotonically in the number of orbits and for each orbit will grow monotonically w.r.t. the remaining two dimensions, the number of equivalence queries is bound by $n + n (k + k \log k)$.
 \stopproof
@@ -1055,8 +1057,6 @@ Next we will give a bound for the size of the table.
 	Since they are suffix closed, the length is at most $n (k + k \log k + 1)$.
 \stopproof
 
-\todo{Betere bound \citet[CameronST89] = $ceil \frac{3}{2} n - b(n) - 1$.}
-
 Let $p$ and $l$ denote respectively the dimension and the number of orbits of $A$.
 
 \startlemma
@@ -1234,7 +1234,8 @@ It is immediate to verify that $\rowunion$ and $\rowincl$ are equivariant.
 
 Our algorithm is a simple modification of the algorithm in \in{Algorithm}[alg:nfa-alg], where a few lines are replaced:
 \startformula[interlinespace=small]\startmathmatrix[n=2, align={middle, left}, distance=1cm]
-\NC \text{\color[darkgray]{6'}}   \NC S \gets S \cup \orb(sa)       \NR
+\NC \reference[alg:nlstar-line6]{}
+    \text{\color[darkgray]{6'}}   \NC S \gets S \cup \orb(sa)       \NR
 \NC \text{\color[darkgray]{11'}}  \NC E \gets E \cup \orb(ae)       \NR
 \NC \text{\color[darkgray]{16'}}  \NC E \gets E \cup \suff(\orb(t)) \NR
 \stopmathmatrix\stopformula
@@ -1425,7 +1426,7 @@ Then the table has:
 \startproof
 By \in{Lemma}[lem:rows-min-dfa], the number of orbits of rows indexed by $S$ is at most $n$.
 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 \todo{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 \goto{line 6'}[alg:nlstar-line6] 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$.
@@ -1539,7 +1540,7 @@ For example, to evaluate the expression $\kw{isEmpty}\ \kw{distPairs}$,
 NLambda makes a system call to the SMT solver to check whether the formula $a \neq b$ is satisfiable in the first-order theory of equality and, after receiving the affirmative answer, returns the value \kw{False}.
 
 For more details about the semantics and implementation of NLambda, see \citet[KlinS16].
-The library itself can be downloaded from \cite[url][nlambda-code].
+The library itself can be downloaded from \citeurl[nlambda-code].
 
 
 \stopsubsection
@@ -1563,6 +1564,7 @@ As an optimisation, we use bisimulation up to congruence as described by \cite[a
 Having an approximate teacher is a minor issue since in many applications no complete teacher can be implemented and one relies on testing \cite[AartsFKV15, BolligHLM13].
 For the experiments listed here the bound was chosen large enough for the learner to terminate with the correct automaton.
 
+The code can be found at \citeurl[nominal-lstar-code].
 %We remark that our algorithms seamlessly merge with teachers written in NLambda, but the current version of the library does not allow generating concrete membership queries for external teachers.
 %We are currently working on a new version of the library in which this will be possible.
 %\todo{Dit kan nu al}

content/minimal-separating-sequences.tex

@@ -654,7 +654,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 \href{https://gitlab.science.ru.nl/rick/partition/}.}
+\footnote{Available at \citeurl[minimal-separating-sequences-code].}
 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.

content/ordered-nominal-sets.tex

@@ -417,7 +417,7 @@ As a base case we can represent single orbits by their dimension.
    reference=sec:impl]
 
 The ideas outlined above have been implemented in the \cpp{} library \ONS{}
-\footnote{\ONS{} can be found at \href{https://github.com/davidv1992/ONS}.}
+\footnote{\ONS{} can be found at \citeurl[ons-code].}
 The library can represent orbit-finite nominal sets and their products, (disjoint) unions, and maps.
 A full description of the possibilities is given in the documentation included with \ONS{}.
 
@@ -773,8 +773,7 @@ In particular, it learns a nominal DFA (over an infinite alphabet) using only fi
 We implement \nLStar{} in the presented library and compare it to its previous implementation in \NLambda{}.
 The algorithm is not polynomial, unlike the minimisation algorithm described above.
 However, the authors conjecture that there is a polynomial algorithm.
-\footnote{See \href{joshuamoerman.nl/papers/2017/17popl-learning-nominal-automata.html} for a sketch of the polynomial algorithm.}
+\footnote{See \citeurl[nominal-lstar-conjecture] for a sketch of the polynomial algorithm.}
-\todo{\emph{The authors} ben ik...}
 For the correctness, termination, and comparison with other learning algorithms see \in{Chapter}[chap:learning-nominal-automata].
 
 
@@ -783,7 +782,7 @@ For the correctness, termination, and comparison with other learning algorithms
 
 Both implementations in \NLambda{} and \ONS{} are direct implementations of the pseudocode for \nLStar{} with no further optimisations.
 The authors of \LOIS{} implemented \nLStar{} in their library as well.
-\footnote{Can be found on \href{github.com/eryxcc/lois/blob/master/tests/learning.cpp}.}
+\footnote{Can be found on \citeurl[lois-lstar-code].}
 They reported similar performance as the implementation in \NLambda{} (private communication).
 Hence we focus our comparison on \NLambda{} and \ONS{}.
 We use the variant of \nLStar{} where counterexamples are added as columns instead of prefixes.
@@ -888,13 +887,13 @@ Hence they are not suited for our applications.
 
 On the theoretical side, there are many complexity results for register automata \citep[GrigoreT16, MurawskiRT15].
 In particular, we note that problems such as emptiness and equivalence are NP-hard depending on the type of register automaton.
-This does not easily compare to our complexity results for minimisation.
+Recently, \citet[MurawskiRT18] showed that equivalence of unique-valued deterministic register automata can be decided in polynomial time.
+These results do not easily compare to our complexity results for minimisation.
 One difference is that we use the total order symmetry, where the local symmetries are always trivial (\in{Lemma}[group_trivial]).
 As a consequence, all the complexity required to deal with groups vanishes.
 Rather, the complexity is transferred to the input of our algorithms, because automata over the equality symmetry require more orbits when expressed over the total order symmetry.
 Another difference is that register automata allow for duplicate values in the registers.
 In nominal automata, such configurations will be encoded in different orbits.
-\todo{Equivalentie is polynomiaal: \cite[MurawskiRT18].}
 
 Orthogonal to nominal automata, there is the notion of symbolic automata \citep[DAntoniV17, MalerM17].
 These automata are also defined over infinite alphabets but they use predicates on transitions, instead of relying on symmetries.

content/test-methods.tex

@@ -953,7 +953,7 @@ We also observe that one of the state identifiers grew in length: $\{ aa, c \}$
   [title={Implementation}]
 
 All the algorithms concerning the hybrid ADS-method have been implemented and can be found at
-\href{https://gitlab.science.ru.nl/moerman/hybrid-ads}.
+\citeurl[hybrid-ads-code].
 We note that \in{Algorithm}[alg:hybrid] is implemented a bit more efficiently, as we can walk the splitting trees in a particular order.
 For constructing the splitting trees in the first place, we use Moore's minimisation algorithm and the algorithms by \citet[LeeY94].
 We keep all relevant sets prefix-closed by maintaining a \emph{trie data structure}.

environment.tex

@@ -18,7 +18,7 @@
 
 \mainlanguage[en]
 
-\setupindenting[yes, medium]
+%\setupindenting[yes, medium]
 \setupwhitespace[medium]
 
 \definefloat[algorithm][algorithms]