Added figures to ONS
This commit is contained in:
Joshua Moerman
parent
41421deeb6
commit
85a736df0b
3 changed files with 125 additions and 128 deletions
|
|
@ -889,7 +889,7 @@
|
|||
author = {Gian Luigi Ferrari and
|
||||
Ugo Montanari and
|
||||
Emilio Tuosto},
|
||||
title = {Coalgebraic minimization of HD-automata for the Pi-calculus using
|
||||
title = {Coalgebraic minimization of {HD}-automata for the $\pi$-calculus using
|
||||
polymorphic types},
|
||||
journal = {Theor. Comput. Sci.},
|
||||
volume = {331},
|
||||
|
|
|
|||
|
|
@ -379,19 +379,19 @@ Combining this, we find that the orbit is $\{(a,(a,b)) \mid a,b \in \Q, a < b\}$
|
|||
We summarise our concrete representation in the following table.
|
||||
\in{Propositions}[thm:pres-nom], \in{}[eqimap_rep] and \in{}[orbstring] correspond to the three rows in the table.
|
||||
|
||||
\todo{Table}
|
||||
% \starttabular}{l|p{5.7cm}
|
||||
% \emph{Object} & \emph{Representation} \\
|
||||
% \hline
|
||||
% Single orbit $O$ & Natural number $n = \dim(O)$ \\
|
||||
% Nominal set $X = \bigcup_i O_i$ & Multiset of these numbers \\
|
||||
% \hline
|
||||
% Map from single orbit $f \colon O \to Y$ & The orbit $f(O)$ and a bit string $F$ \\
|
||||
% Equivariant map $f \colon X \to Y$ & Set of tuples $(O, F, f(O))$, one for each orbit \\
|
||||
% \hline
|
||||
% Orbit in a product $O \subseteq X \times Y$ & The corresponding orbits of $X$ and $Y$, and a string $P$ relating their supports \\
|
||||
% Product $X \times Y$ & Set of tuples $(P, O_X, O_Y)$, one for each orbit \\
|
||||
% \stoptabular
|
||||
\placetable[here][tab:overview]{Overview of representation.}
|
||||
\starttabulate[|l|p|]
|
||||
\NC \emph{Object} \NC \emph{Representation} \NC\NR
|
||||
\HL %----------------------------------------
|
||||
\NC Single orbit $O$ \NC Natural number $n = \dim(O)$ \NC\NR
|
||||
\NC Nominal set $X = \bigcup_i O_i$ \NC Multiset of these numbers \NC\NR
|
||||
\HL %----------------------------------------
|
||||
\NC Map from single orbit $f \colon O \to Y$ \NC The orbit $f(O)$ and a bit string $F$ \NC\NR
|
||||
\NC Equivariant map $f \colon X \to Y$ \NC Set of tuples $(O, F, f(O))$, one for each orbit \NC\NR
|
||||
\HL %----------------------------------------
|
||||
\NC Orbit in a product $O \subseteq X \times Y$ \NC The corresponding orbits of $X$ and $Y$, and a string $P$ relating their supports \NC\NR
|
||||
\NC Product $X \times Y$ \NC Set of tuples $(P, O_X, O_Y)$, one for each orbit \NC\NR
|
||||
\stoptabulate
|
||||
|
||||
Notice that in the case of maps and products, the orbits are inductively represented using the concrete representation.
|
||||
As a base case we can represent single orbits by their dimension.
|
||||
|
|
@ -404,7 +404,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 \todo{https://github.com/davidv1992/ONS}.}
|
||||
\footnote{\ONS{} can be found at \href{https://github.com/davidv1992/ONS}.}
|
||||
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{}.
|
||||
|
||||
|
|
@ -463,20 +463,18 @@ Recall that $\Nsize(X)$ denotes the number of orbits of $X$.
|
|||
We use $p$ and $f$ to denote functions implemented in whatever way the user wants, which we assume to take $O(1)$ time.
|
||||
The software assumes these are equivariant, but this is not verified.
|
||||
|
||||
\todo{Table}
|
||||
% \startcenter
|
||||
% \starttabular}{r|l
|
||||
% Operation & Complexity\\
|
||||
% \hline
|
||||
% Test $x \in X$ & $O(\log \Nsize(X))$\\
|
||||
% Test $X\subseteq Y$ & $O(\min(\Nsize(X)+\Nsize(Y), \Nsize(X)\log \Nsize(Y)))$\\
|
||||
% Calculate $X \cup Y$ & $O(\Nsize(X)+\Nsize(Y))$\\
|
||||
% Calculate $X \cap Y$ & $O(\Nsize(X)+\Nsize(Y))$\\
|
||||
% Calculate $\{x \in X \mid p(x)\}$ & $O(\Nsize(X))$\\
|
||||
% Calculate $\{f(x) \mid x \in X\}$ & $O(\Nsize(X)\log \Nsize(X))$\\
|
||||
% Calculate $X\times Y$ & $O(\Nsize(X\times Y)) \,\subseteq\, O(3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y))$\\
|
||||
% \stoptabular
|
||||
% \stopcenter
|
||||
\placetable[here][tab:complexity]{Time complexity of operations on nominal sets.}
|
||||
\starttabulate[|r|l|]
|
||||
\NC \emph{Operation} \VL \emph{Complexity} \NC\NR
|
||||
\HL
|
||||
\NC Test $x \in X$ \VL $O(\log \Nsize(X))$ \NC\NR
|
||||
\NC Test $X\subseteq Y$ \VL $O(\min(\Nsize(X)+\Nsize(Y), \Nsize(X)\log \Nsize(Y)))$ \NC\NR
|
||||
\NC Calculate $X \cup Y$ \VL $O(\Nsize(X)+\Nsize(Y))$ \NC\NR
|
||||
\NC Calculate $X \cap Y$ \VL $O(\Nsize(X)+\Nsize(Y))$ \NC\NR
|
||||
\NC Calculate $\{x \in X \mid p(x)\}$ \VL $O(\Nsize(X))$ \NC\NR
|
||||
\NC Calculate $\{f(x) \mid x \in X\}$ \VL $O(\Nsize(X)\log \Nsize(X))$ \NC\NR
|
||||
\NC Calculate $X\times Y$ \VL $O(\Nsize(X\times Y)) \,\subseteq\, O(3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y))$ \NC\NR
|
||||
\stoptabulate
|
||||
\stoptheorem
|
||||
|
||||
\startproof
|
||||
|
|
@ -535,27 +533,25 @@ Such a transition structure is made precise by the notion of nominal automata.
|
|||
\startplacefigure
|
||||
[title={Example automaton that accepts the language $\Lint$.},
|
||||
reference=fig:lint-minimal]
|
||||
\todo{Plaatje}
|
||||
% \starttikzpicture
|
||||
% \node (S 0) at (0,0) [state, minimum size=1.5cm] {$q_0$};
|
||||
% \node (S 1) at (3,0) [state, minimum size=1.5cm] {$q_1(a)$};
|
||||
% \node (S 2) at (7,0) [state, minimum size=1.5cm, accepting] {$q_2(a,b)$};
|
||||
% \node (S 3) at (11,0) [state, minimum size=1.5cm] {$q_3(a,b)$};
|
||||
% \node (S 4) at (7,-2.5) [state, minimum size=1.5cm] {$q_4$};
|
||||
% \node (S 5) at (11,-2.5) [state,minimum size=1.5cm,draw=none] {};
|
||||
\starttikzpicture[node distance=3.5cm]
|
||||
\node (S 0) [state] {$q_0$};
|
||||
\node (S 1) [state, right of=S 0] {$q_1(a)$};
|
||||
\node (S 2) [state, accepting, right of=S 1] {$q_2(a,b)$};
|
||||
\node (S 3) [state, right of=S 2] {$q_3(a,b)$};
|
||||
\node (S 4) [state, below=1.5cm of S 2] {$q_4$};
|
||||
|
||||
% \path
|
||||
% (S 0) edge node[above] {$a$} (S 1)
|
||||
% (S 1) edge node[above] {$b > a$} (S 2)
|
||||
% (S 1) edge[bend right] node[below left] {$b \le a$} (S 4)
|
||||
% (S 2) edge[bend left=10] node[above,align=center] {$a<c<b$\\$a\leftarrow c$} (S 3)
|
||||
% (S 3) edge[bend left=10] node[below,align=center] {$a<c<b$\\$b\leftarrow c$} (S 2)
|
||||
% (S 2) edge[bend right=15] node[left] {$c\le a$} (S 4)
|
||||
% (S 2) edge[bend left=15] node[right] {$c\ge b$} (S 4)
|
||||
% (S 3) edge[bend left] node[above left] {$c\le a$} (S 4)
|
||||
% (S 3) edge[bend left=60] node[below right] {$c\ge b$} (S 4);
|
||||
% \draw[-{Latex},rounded corners=5] (S 4.south west) -- ([yshift=-.5cm]S 4.south west) -- node[midway,below]{$a$} ([yshift=-.5cm]S 4.south east) -- (S 4.south east);
|
||||
% \stoptikzpicture
|
||||
\path[->]
|
||||
(S 0) edge node[above] {$a$} (S 1)
|
||||
(S 1) edge node[above] {$b > a$} (S 2)
|
||||
(S 1) edge[bend right] node[below left] {$b \le a$} (S 4)
|
||||
(S 2) edge[bend left=10] node[above,align=center] {$a<c<b$\\$a \leftarrow c$} (S 3)
|
||||
(S 3) edge[bend left=10] node[below,align=center] {$a<c<b$\\$b \leftarrow c$} (S 2)
|
||||
(S 2) edge[bend right=10] node[left] {$c \le a$} (S 4)
|
||||
(S 2) edge[bend left=10] node[right] {$c \ge b$} (S 4)
|
||||
(S 3) edge[bend left] node[above left] {$c \le a$} (S 4)
|
||||
(S 3) edge[bend left=60] node[below right] {$c \ge b$} (S 4)
|
||||
(S 4) edge[loop below] node [below] {$a$} (S 4);
|
||||
\stoptikzpicture
|
||||
\stopplacefigure
|
||||
|
||||
\startdefinition
|
||||
|
|
@ -636,22 +632,27 @@ We say an automaton is \emph{minimal} if its set of states has the least number
|
|||
Minimal deterministic automata are unique up to isomorphism.}
|
||||
We generalise Moore's minimisation algorithm to nominal DFAs (\in{Algorithm}[alg:moore]) and analyse its time complexity using the bounds from \in{Section}[sec:impl].
|
||||
|
||||
\todo{algoritme}
|
||||
% \startalgorithm
|
||||
% \caption{Moore's minimisation algorithm for nominal DFAs}\label{alg:moore}
|
||||
% \startalgorithmic[1]
|
||||
% \Require{ Nominal automaton $(S,A,F,\delta)$.}
|
||||
% \State{$i \leftarrow 0$, ${\equiv_{-1}} \leftarrow S\times S$, ${\equiv_{0}} \leftarrow F\times F \cup (S\backslash F)\times (S\backslash F)$}
|
||||
% \While{${\equiv_i} \ne {\equiv_{i-1}}$}
|
||||
% \State{${\equiv_{i+1}} = \{(q_1, q_2) \mid (q_1, q_2) \in {\equiv_i} \wedge \forall a\in A, (\delta(q_1,a), \delta(q_2,a))\in {\equiv_i} \}$}
|
||||
% \State{$i \leftarrow i+1$}
|
||||
% \EndWhile
|
||||
% \State{$E\leftarrow S/_{\equiv_i}$}
|
||||
% \State{$F_E \leftarrow \{e\in E \mid \forall s\in e, s\in F\}$}
|
||||
% \State{Let $\delta_E$ be the map such that, if $s\in e$ and $\delta(s,a)\in e'$, then $\delta_E(e,a) = e'$.}
|
||||
% \State{\Return{$(E,A,F_E,\delta_E)$.}}
|
||||
% \stopalgorithmic
|
||||
% \stopalgorithm
|
||||
\startplacealgorithm
|
||||
[title={Moore's minimisation algorithm for nominal DFAs.},
|
||||
reference=alg:moore]
|
||||
\startalgorithmic
|
||||
\REQUIRE{Nominal automaton $M = (S,A,F,\delta)$}
|
||||
\ENSURE{Minimal nominal automaton equivalent to $M$}
|
||||
\startlinenumbering
|
||||
\STATE $i \gets 0$
|
||||
\STATE ${\equiv_{-1}} \gets S \times S$
|
||||
\STATE ${\equiv_{0}} \gets F \times F \cup (S\backslash F)\times (S\backslash F)$
|
||||
\WHILE{${\equiv_i} \ne {\equiv_{i-1}}$\startline[line:loop]}
|
||||
\STATE ${\equiv_{i+1}} \gets \{ (q_1, q_2) \mid (q_1, q_2) \in {\equiv_i} \wedge \forall a \in A, (\delta(q_1, a), \delta(q_2, a)) \in {\equiv_i} \}$\someline[line:main-work]
|
||||
\STATE $i \gets i+1$
|
||||
\ENDWHILE\stopline[line:loop]
|
||||
\STATE $E \gets S/_{\equiv_i}$
|
||||
\STATE $F_E \gets \{e \in E \mid \forall s \in e, s \in F\}$
|
||||
\STATE Let $\delta_E$ be the map such that, if $s \in e$ and $\delta(s, a) \in e'$, then $\delta_E(e, a) = e'$
|
||||
\RETURN $(E,A,F_E,\delta_E)$
|
||||
\stoplinenumbering
|
||||
\stopalgorithmic
|
||||
\stopplacealgorithm
|
||||
|
||||
\starttheorem[reference=thm:moore]
|
||||
The runtime complexity of Moore's algorithm on nominal deterministic automata is $O(3^{5k} k \Nsize(S)^3 \Nsize(A))$, where $k=\dim(S\cup A)$.
|
||||
|
|
@ -659,8 +660,8 @@ The runtime complexity of Moore's algorithm on nominal deterministic automata is
|
|||
|
||||
\startproof
|
||||
This is shown by counting operations, using the complexity results of set operations stated in \in{Theorem}[thmcomplexity].
|
||||
We first focus on the while loop on \todo{lines 2 through 5}.
|
||||
The runtime of an iteration of the loop is determined by \todo{line 3}, as this is the most expensive step.
|
||||
We first focus on the while loop on \inline[line:loop].
|
||||
The runtime of an iteration of the loop is determined by \inline[line:main-work], as this is the most expensive step.
|
||||
Since the dimensions of $S$ and $A$ are at most $k$, computing $S \times S \times A$ takes $O(\Nsize(S)^2 \Nsize(A) 3^{5k})$.
|
||||
Filtering $S \times S$ using that then takes $O(\Nsize(S)^2 3^{2k})$.
|
||||
The time to compute $S \times S \times A$ dominates, hence each iteration of the loop takes $O(\Nsize(S)^2 \Nsize(A) 3^{5k})$.
|
||||
|
|
@ -702,38 +703,33 @@ The output of these programs was manually checked to see if the minimisation was
|
|||
The results (shown in \in{Table}[minimize_results]) for random automata show a clear advantage for \ONS{}, which is capable of running all supplied testcases in less than one second.
|
||||
This in contrast to both \LOIS{} and \NLambda{}, which take more than $2$ hours on the largest random automata.
|
||||
|
||||
\todo{Table}
|
||||
% \starttable
|
||||
% \centering
|
||||
% \starttabular}{l|l|l|r|r|r|r
|
||||
% Type & $\Nsize(S)$ & $\Nsize(S^\text{min})$ & \multicolumn{2}{l|}{\ONS{}} & \NLambda{} & \LOIS{} \\
|
||||
% & & & & \color{black!70} Gen. & &\\
|
||||
% \hline
|
||||
% rand$_{5,1}$ (x10) & $5$ & n/a & $0.02$s & \color{black!70} n/a & $0.82$s & $3.14$s \\
|
||||
% rand$_{10,1}$ (x10) & $10$ & n/a & $0.03$s & \color{black!70} n/a & $17.03$s & $1$m $32$s \\
|
||||
% rand$_{10,2}$ (x10) & $10$ & n/a & $0.09$s & \color{black!70} n/a & $35$m $14$s & $> 60$m \\
|
||||
% rand$_{15,1}$ (x10) & $15$ & n/a & $0.04$s & \color{black!70} n/a & $1$m $27$s & $10$m $20$s \\
|
||||
% rand$_{15,2}$ (x10) & $15$ & n/a & $0.11$s & \color{black!70} n/a & $55$m $46$s & $> 60$m \\
|
||||
% rand$_{15,3}$ (x10) & $15$ & n/a & $0.46$s & \color{black!70} n/a & $> 60$m & $> 60$m \\
|
||||
% \hline
|
||||
% FIFO($2$) & $13$ & $6$ & $0.01$s & \color{black!70} $0.01$s & $1.37$s & $0.24$s \\
|
||||
% FIFO($3$) & $65$ & $19$ & $0.38$s & \color{black!70} $0.09$s & $11.59$s & $2.4$s \\
|
||||
% FIFO($4$) & $440$ & $94$ & $39.11$s & \color{black!70} $1.60$s & $1$m $16$s & $14.95$s \\
|
||||
% FIFO($5$) & $3686$ & $635$ & $> 60$m & \color{black!70} $39.78$s & $6$m $42$s & $1$m $11$s \\
|
||||
% \hline
|
||||
% $ww(2)$ & $8$ & $8$ & $0.00$s & \color{black!70} $0.00$s & $0.14$s & $0.03$s \\
|
||||
% $ww(3)$ & $24$ & $24$ & $0.19$s & \color{black!70} $0.02$s & $0.88$s & $0.16$s \\
|
||||
% $ww(4)$ & $112$ & $112$ & $26.44$s & \color{black!70} $0.25$s & $3.41$s & $0.61$s \\
|
||||
% $ww(5)$ & $728$ & $728$ & $> 60$m & \color{black!70} $6.37$s & $10.54$s & $1.80$s \\
|
||||
% \hline
|
||||
% $\Lmax$ & $5$ & $3$ & $0.00$s & \color{black!70} $0.00$s & $2.06$s & $0.03$s \\
|
||||
% $\Lint$ & $5$ & $5$ & $0.00$s & \color{black!70} $0.00$s & $1.55$s & $0.03$s
|
||||
% \stoptabular
|
||||
% \caption{Running times for \in{Algorithm}[alg:moore] implemented in the three libraries.
|
||||
% $N(S)$ is the size of the input and $N(S^\text{min})$ the size of the minimal automaton.
|
||||
% For \ONS{}, the time used to generate the automaton is reported separately (in grey).}
|
||||
% \label{minimize_results}
|
||||
% \stoptable
|
||||
\placetable[here][minimize_results]
|
||||
{Running times for \in{Algorithm}[alg:moore] implemented in the three libraries.
|
||||
$N(S)$ is the size of the input and $N(S^{\text{min}})$ the size of the minimal automaton.
|
||||
For \ONS{}, the time used to generate the automaton is reported separately (in grey).}
|
||||
\starttabulate[|l|l|l|r|r|r|r|][distance=none]
|
||||
\NC Type \NC $\Nsize(S)$ \NC $\Nsize(S^{\text{min}})$ \VL \ONS{} \NC \color[darkgray]{(Gen.)} \VL \NLambda{} \VL \LOIS{} \NC\NR
|
||||
\HL
|
||||
\NC rand$_{5,1}$ (x10) \NC $5$ \NC n/a \VL $0.02$s \NC \color[darkgray]{n/a} \VL $0.82$s \VL $3.14$s \NC\NR
|
||||
\NC rand$_{10,1}$ (x10) \NC $10$ \NC n/a \VL $0.03$s \NC \color[darkgray]{n/a} \VL $17.03$s \VL $1$m $32$s \NC\NR
|
||||
\NC rand$_{10,2}$ (x10) \NC $10$ \NC n/a \VL $0.09$s \NC \color[darkgray]{n/a} \VL $35$m $14$s \VL $> 60$m \NC\NR
|
||||
\NC rand$_{15,1}$ (x10) \NC $15$ \NC n/a \VL $0.04$s \NC \color[darkgray]{n/a} \VL $1$m $27$s \VL $10$m $20$s \NC\NR
|
||||
\NC rand$_{15,2}$ (x10) \NC $15$ \NC n/a \VL $0.11$s \NC \color[darkgray]{n/a} \VL $55$m $46$s \VL $> 60$m \NC\NR
|
||||
\NC rand$_{15,3}$ (x10) \NC $15$ \NC n/a \VL $0.46$s \NC \color[darkgray]{n/a} \VL $> 60$m \VL $> 60$m \NC\NR
|
||||
\HL
|
||||
\NC FIFO($2$) \NC $13$ \NC $6$ \VL $0.01$s \NC \color[darkgray]{$0.01$s} \VL $1.37$s \VL $0.24$s \NC\NR
|
||||
\NC FIFO($3$) \NC $65$ \NC $19$ \VL $0.38$s \NC \color[darkgray]{$0.09$s} \VL $11.59$s \VL $2.4$s \NC\NR
|
||||
\NC FIFO($4$) \NC $440$ \NC $94$ \VL $39.11$s \NC \color[darkgray]{$1.60$s} \VL $1$m $16$s \VL $14.95$s \NC\NR
|
||||
\NC FIFO($5$) \NC $3686$ \NC $635$ \VL $> 60$m \NC \color[darkgray]{$39.78$s} \VL $6$m $42$s \VL $1$m $11$s \NC\NR
|
||||
\HL
|
||||
\NC $ww(2)$ \NC $8$ \NC $8$ \VL $0.00$s \NC \color[darkgray]{$0.00$s} \VL $0.14$s \VL $0.03$s \NC\NR
|
||||
\NC $ww(3)$ \NC $24$ \NC $24$ \VL $0.19$s \NC \color[darkgray]{$0.02$s} \VL $0.88$s \VL $0.16$s \NC\NR
|
||||
\NC $ww(4)$ \NC $112$ \NC $112$ \VL $26.44$s \NC \color[darkgray]{$0.25$s} \VL $3.41$s \VL $0.61$s \NC\NR
|
||||
\NC $ww(5)$ \NC $728$ \NC $728$ \VL $> 60$m \NC \color[darkgray]{$6.37$s} \VL $10.54$s \VL $1.80$s \NC\NR
|
||||
\HL
|
||||
\NC $\Lmax$ \NC $5$ \NC $3$ \VL $0.00$s \NC \color[darkgray]{$0.00$s} \VL $2.06$s \VL $0.03$s \NC\NR
|
||||
\NC $\Lint$ \NC $5$ \NC $5$ \VL $0.00$s \NC \color[darkgray]{$0.00$s} \VL $1.55$s \VL $0.03$s \NC\NR
|
||||
\stoptabulate
|
||||
|
||||
The results for structured automata show a clear effect of the extra structure.
|
||||
Both \NLambda{} and \LOIS{} remain capable of minimising the automata in reasonable amounts of time for larger sizes.
|
||||
|
|
@ -762,7 +758,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 \todo{joshuamoerman.nl/papers/2017/17popl-learning-nominal-automata.html} for a sketch of the polynomial algorithm.}
|
||||
\footnote{See \href{joshuamoerman.nl/papers/2017/17popl-learning-nominal-automata.html} for a sketch of the polynomial algorithm.}
|
||||
For the correctness, termination, and comparison with other learning algorithms see \in{Chapter}[chap:learning-nominal-automata].
|
||||
|
||||
|
||||
|
|
@ -771,7 +767,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 \todo{github.com/eryxcc/lois/blob/master/tests/learning.cpp}.}
|
||||
\footnote{Can be found on \href{github.com/eryxcc/lois/blob/master/tests/learning.cpp}.}
|
||||
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.
|
||||
|
|
@ -804,33 +800,30 @@ For languages which are equivariant for the equality symmetry, the \NLambda{} im
|
|||
This is expected as the automata themselves have fewer orbits.
|
||||
It is interesting to see that these languages can be learned more efficiently by choosing the right symmetry.
|
||||
|
||||
\todo{Table}
|
||||
% \starttable
|
||||
% \centering
|
||||
% \starttabular}{l l l|r r|r r|r r
|
||||
% & & & \multicolumn{2}{l|}{\ONS{}} & \multicolumn{2}{l|}{\NLambda{}$^{\mathit{ord}}$} & \multicolumn{2}{l}{\NLambda{}$^{\mathit{eq}}$} \\
|
||||
% Model & $\Nsize(S)$ & $\dim(S)$ & time & MQs & time & MQs & time& MQs \\
|
||||
% \hline
|
||||
% rand$_{5,1}$ & $4$ & $1$ & $2$m $7$s & $2321$ & $39$m $51$s & $1243$ & & \\
|
||||
% rand$_{5,1}$ & $5$ & $1$ & $0.12$s & $404$ & $40$m $34$s & $435$ & & \\
|
||||
% rand$_{5,1}$ & $3$ & $0$ & $0.86$s & $499$ & $30$m $19$s & $422$ & & \\
|
||||
% rand$_{5,1}$ & $5$ & $1$ & $> 60$m & n/a & $> 60$m & n/a & & \\
|
||||
% rand$_{5,1}$ & $4$ & $1$ & $0.08$s & $387$ & $34$m $57$s & $387$ & & \\
|
||||
% \hline
|
||||
% FIFO$(1)$ & $3$ & $1$ & $0.04$s & $119$ & $3.17$s & $119$ & $1.76$s & $51$ \\
|
||||
% FIFO$(2)$ & $6$ & $2$ & $1.73$s & $2655$ & $6$m $32$s & $3818$ & $40.00$s & $434$ \\
|
||||
% FIFO$(3)$ & $19$ & $3$ & $46$m $34$s & $298400$ & $> 60$m & n/a & $34$m $7$s & $8151$ \\
|
||||
% \hline
|
||||
% $ww(1)$ & $4$ & $1$ & $0.42$s & $134$ & $2.49$s & $77$ & $1.47$s & $30$ \\
|
||||
% $ww(2)$ & $8$ & $2$ & $4$m $26$s & $3671$ & $3$m $48$s & $2140$ & $30.58$s & $237$ \\
|
||||
% $ww(3)$ & $24$ & $3$ & $> 60$m & n/a & $> 60$m & n/a & $> 60$m & n/a \\
|
||||
% \hline
|
||||
% $\Lmax$ & $3$ & $1$ & $0.01$s & $54$ & $3.58$s & $54$ & & \\
|
||||
% $\Lint$ & $5$ & $2$ & $0.59$s & $478$ & $1$m $23$s & $478$ & &
|
||||
% \stoptabular
|
||||
% \caption{Running times and number of membership queries for the \nLStar{} algorithm. For \NLambda{} we used two version: \NLambda{}$^{\mathit{ord}}$ uses the total order symmetry \NLambda{}$^{\mathit{eq}}$ uses the equality symmetry.}
|
||||
% \label{learning_results}
|
||||
% \stoptable
|
||||
\placetable[here][learning_results]
|
||||
{Running times and number of membership queries for the \nLStar{} algorithm.
|
||||
For \NLambda{} we used two version: \NLambda{}$^{\mathit{ord}}$ uses the total order symmetry \NLambda{}$^{\mathit{eq}}$ uses the equality symmetry.}
|
||||
\starttabulate[|l|l|l|r|r|r|r|r|r|][distance=none]
|
||||
\NC \NC \NC \VL \NC \ONS{} \VL \NC \NLambda{}$^{\mathit{ord}}$ \VL \NC \NLambda{}$^{\mathit{eq}}$ \NC\NR
|
||||
\NC Model \NC $\Nsize(S)$ \NC $\dim(S)$ \VL time \NC MQs \VL time \NC MQs \VL time \NC MQs \NC\NR
|
||||
\HL
|
||||
\NC rand$_{5,1}$ \NC $4$ \NC $1$ \VL $2$m $7$s \NC $2321$ \VL $39$m $51$s \NC $1243$ \VL \NC \NC\NR
|
||||
\NC rand$_{5,1}$ \NC $5$ \NC $1$ \VL $0.12$s \NC $404$ \VL $40$m $34$s \NC $435$ \VL \NC \NC\NR
|
||||
\NC rand$_{5,1}$ \NC $3$ \NC $0$ \VL $0.86$s \NC $499$ \VL $30$m $19$s \NC $422$ \VL \NC \NC\NR
|
||||
\NC rand$_{5,1}$ \NC $5$ \NC $1$ \VL $> 60$m \NC n/a \VL $> 60$m \NC n/a \VL \NC \NC\NR
|
||||
\NC rand$_{5,1}$ \NC $4$ \NC $1$ \VL $0.08$s \NC $387$ \VL $34$m $57$s \NC $387$ \VL \NC \NC\NR
|
||||
\HL
|
||||
\NC FIFO$(1)$ \NC $3$ \NC $1$ \VL $0.04$s \NC $119$ \VL $3.17$s \NC $119$ \VL $1.76$s \NC $51$ \NC\NR
|
||||
\NC FIFO$(2)$ \NC $6$ \NC $2$ \VL $1.73$s \NC $2655$ \VL $6$m $32$s \NC $3818$ \VL $40.00$s \NC $434$ \NC\NR
|
||||
\NC FIFO$(3)$ \NC $19$ \NC $3$ \VL $46$m $34$s\NC $298400$ \VL $> 60$m \NC n/a \VL $34$m $7$s \NC $8151$ \NC\NR
|
||||
\HL
|
||||
\NC $ww(1)$ \NC $4$ \NC $1$ \VL $0.42$s \NC $134$ \VL $2.49$s \NC $77$ \VL $1.47$s \NC $30$ \NC\NR
|
||||
\NC $ww(2)$ \NC $8$ \NC $2$ \VL $4$m $26$s \NC $3671$ \VL $3$m $48$s \NC $2140$ \VL $30.58$s \NC $237$ \NC\NR
|
||||
\NC $ww(3)$ \NC $24$ \NC $3$ \VL $> 60$m \NC n/a \VL $> 60$m \NC n/a \VL $> 60$m \NC n/a \NC\NR
|
||||
\HL
|
||||
\NC $\Lmax$ \NC $3$ \NC $1$ \VL $0.01$s \NC $54$ \VL $3.58$s \NC $54$ \VL \NC \NC\NR
|
||||
\NC $\Lint$ \NC $5$ \NC $2$ \VL $0.59$s \NC $478$ \VL $1$m $23$s \NC $478$ \VL \NC \NC\NR
|
||||
\stoptabulate
|
||||
|
||||
|
||||
\stopsubsubsection
|
||||
|
|
|
|||
|
|
@ -63,6 +63,10 @@
|
|||
\setupalgorithmic[before={\startframedtext[width=0.85\textwidth,offset=none,frame=off]},after={\stopframedtext}] % To enable linenumbers in a float
|
||||
|
||||
|
||||
\def\href#1{\useURL[#1][{#1}]{\tt\goto{\url[#1]}[url(#1)]}}
|
||||
|
||||
|
||||
|
||||
% Debugging
|
||||
%\enabletrackers[references.references, visualizers.justification]
|
||||
%\showmakeup
|
||||
|
|
|
|||
Reference in a new issue