Skip to content

Commit

Permalink
test automata minimization
Browse files Browse the repository at this point in the history
  • Loading branch information
@breandan
breandan committed Jun 22, 2024
1 parent d5eaa09 commit 7a57c90
Show file tree
Hide file tree
Showing 4 changed files with 169 additions and 128 deletions.
1 change: 1 addition & 0 deletions build.gradle.kts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,7 @@ kotlin {
// implementation(files("$projectDir/libs/mpj-0.44.jar"))

implementation(files("$projectDir/jautomata-0.0.1-SNAPSHOT.jar"))
implementation("dk.brics:automaton:1.12-4")

implementation("org.sosy-lab:common:0.3000-529-g6152d88")
implementation("org.sosy-lab:java-smt:4.1.1")
Expand Down
Binary file modified latex/popl2025/popl.pdf
View file
Binary file not shown.
227 changes: 113 additions & 114 deletions latex/popl2025/popl.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -937,120 +937,119 @@

Constructively, let $+, *: \mathcal{M}\times \mathcal{M} \rightarrow \mathcal{M}$ be the automata operators corresponding to language union and concatenation satisfying $\mathcal{L}(A_1 + A_2) = \mathcal{L}(A_1)\cup\mathcal{L}(A_2)$, and $\mathcal{L}(A_1 * A_2) = \mathcal{L}(A_1)\times\mathcal{L}(A_2)$. This can be implemented using the standard textbook construction, recalling that NFA are closed under these operations. $\Lambda^* \circ S$ would then yield an NFA recognizing $\Sigma^n\cap\mathcal{L}(G)$, which can be determinized and decoded using k-best paths to obtain the top-k maximum likelihood repairs.


\definecolor{R}{RGB}{202,65,55}
\definecolor{G}{RGB}{151,216,56}
\definecolor{W}{RGB}{255,255,255}
\definecolor{X}{RGB}{65,65,65}

\newcommand{\TikZRubikFaceLeft}[9]{\def\myarrayL{#1,#2,#3,#4,#5,#6,#7,#8,#9}}
\newcommand{\TikZRubikFaceRight}[9]{\def\myarrayR{#1,#2,#3,#4,#5,#6,#7,#8,#9}}
\newcommand{\TikZRubikFaceTop}[9]{\def\myarrayT{#1,#2,#3,#4,#5,#6,#7,#8,#9}}
\newcommand{\BuildArray}{\foreach \X [count=\Y] in \myarrayL%
{\ifnum\Y=1%
\xdef\myarray{"\X"}%
\else%
\xdef\myarray{\myarray,"\X"}%
\fi}%
\foreach \X in \myarrayR%
{\xdef\myarray{\myarray,"\X"}}%
\foreach \X in \myarrayT%
{\xdef\myarray{\myarray,"\X"}}%
\xdef\myarray{{\myarray}}%
}
\TikZRubikFaceLeft
{LA}{W}{W}
{W}{LB}{LC}
{LD}{W}{W}
\TikZRubikFaceRight
{W}{LK}{W}
{LC}{W}{LG}
{W}{LH}{W}
\TikZRubikFaceTop
{LA}{W}{LI}
{W}{W}{LJ}
{W}{LK}{W}
\BuildArray
\pgfmathsetmacro\radius{0.1}
\tdplotsetmaincoords{55}{135}

\showcellnumberfalse

\bgroup
\newcommand\ddd{\Ddots}
\newcommand\vdd{\Vdots}
\newcommand\cdd{\Cdots}
\newcommand\lds{\ldots}
\newcommand\vno{\varnothing}
\newcommand{\ts}[1]{\textsuperscript{#1}}
\newcommand\non{1\ts{st}}
\newcommand\ntw{2\ts{nd}}
\newcommand\nth{3\ts{rd}}
\newcommand\nfo{4\ts{th}}
\newcommand\nfi{5\ts{th}}
\newcommand\nsi{6\ts{th}}
\newcommand\nse{7\ts{th}}
\newcommand{\vs}[1]{\shup\sigma_{#1}}
\newcommand\rcr{\rowcolor{black!15}}
\newcommand\rcw{\rowcolor{white}}
\newcommand\pcd{\cdot}
\newcommand\pcp{\phantom\cdot}
\newcommand\ppp{\phantom{\nse}}

\begin{wrapfigure}{r}{0.32\textwidth}
\vspace{-0.5cm}
\begin{minipage}[r]{4cm}
\begin{align*}
o &\rightarrow \hiliD{so} \mid \hiliC{rs} \mid \hiliB{rr}\hspace{0.5pt} \mid \hiliA{oo}\\
r &\rightarrow \hiliE{so} \mid \hiliH{ss}\hspace{0.4pt}\mid \hiliF{rr}\hspace{0.5pt} \mid \hiliK{os}\\
s &\rightarrow \hiliL{so} \mid \hiliG{rs} \mid \hiliJ{or} \mid \hiliI{oo}
\end{align*}
\end{minipage}
% \mathcal{J} = \begin{pmatrix}
% \pder{o}{o} & \pder{o}{r} & \pder{o}{s}\\
% \pder{r}{o} & \pder{r}{r} & \pder{r}{s}\\
% \pder{s}{o} & \pder{s}{r} & \pder{s}{s}
% \end{pmatrix}
\hspace{-0.1cm}\begin{minipage}[r]{4cm}
\scalebox{0.8}{\begin{tikzpicture}
\clip (-3,-2.5) rectangle (3,2.5);
\begin{scope}[tdplot_main_coords]
\filldraw [canvas is yz plane at x=1.5] (-1.5,-1.5) rectangle (1.5,1.5);
\filldraw [canvas is xz plane at y=1.5] (-1.5,-1.5) rectangle (1.5,1.5);
\filldraw [canvas is yx plane at z=1.5] (-1.5,-1.5) rectangle (1.5,1.5);
\foreach \X [count=\XX starting from 0] in {-1.5,-0.5,0.5}{
\foreach \Y [count=\YY starting from 0] in {-1.5,-0.5,0.5}{
\pgfmathtruncatemacro{\Z}{\XX+3*(2-\YY)}
\pgfmathsetmacro{\mycolor}{\myarray[\Z]}
\draw [thick,canvas is yz plane at x=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle;
\ifshowcellnumber
\node[canvas is yz plane at x=1.5,shift={(\X+0.5,\Y+0.5)}] {\Z};
\fi
\pgfmathtruncatemacro{\Z}{2-\XX+3*(2-\YY)+9}
\pgfmathsetmacro{\mycolor}{\myarray[\Z]}
\draw [thick,canvas is xz plane at y=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle;
\ifshowcellnumber
\node[canvas is xz plane at y=1.5,shift={(\X+0.5,\Y+0.5)},xscale=-1] {\Z};
\fi
\pgfmathtruncatemacro{\Z}{2-\YY+3*\XX+18}
\pgfmathsetmacro{\mycolor}{\myarray[\Z]}
\draw [thick,canvas is yx plane at z=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle;
\ifshowcellnumber
\node[canvas is yx plane at z=1.5,shift={(\X+0.5,\Y+0.5)},xscale=-1,rotate=-90] {\Z};
\fi
}
}
\draw [decorate,decoration={calligraphic brace,amplitude=10pt,mirror},yshift=0pt, line width=1.25pt]
(3,0) -- (3,3) node [black,midway,xshift=-8pt, yshift=-14pt] {\footnotesize $V_x$};
\draw [decorate,decoration={calligraphic brace,amplitude=10pt},yshift=0pt, line width=1.25pt]
(3,0) -- (0,-3) node [black,midway,xshift=-16pt, yshift=0pt] {\footnotesize $V_z$};
\draw [decorate,decoration={calligraphic brace,amplitude=10pt},yshift=0pt, line width=1.25pt]
(0,-3) -- (-3,-3) node [black,midway,xshift=-8pt, yshift=14pt] {\footnotesize $V_w$};
\end{scope}
\end{tikzpicture}}
\end{minipage}
\caption{CFGs are hypergraphs witnessed by a rank-3 tensor, whose nonempty inhabitants indicate CNF productions.\vspace{-10pt}}
\end{wrapfigure}
% \definecolor{R}{RGB}{202,65,55}
% \definecolor{G}{RGB}{151,216,56}
% \definecolor{W}{RGB}{255,255,255}
% \definecolor{X}{RGB}{65,65,65}
%
% \newcommand{\TikZRubikFaceLeft}[9]{\def\myarrayL{#1,#2,#3,#4,#5,#6,#7,#8,#9}}
% \newcommand{\TikZRubikFaceRight}[9]{\def\myarrayR{#1,#2,#3,#4,#5,#6,#7,#8,#9}}
% \newcommand{\TikZRubikFaceTop}[9]{\def\myarrayT{#1,#2,#3,#4,#5,#6,#7,#8,#9}}
% \newcommand{\BuildArray}{\foreach \X [count=\Y] in \myarrayL%
% {\ifnum\Y=1%
% \xdef\myarray{"\X"}%
% \else%
% \xdef\myarray{\myarray,"\X"}%
% \fi}%
% \foreach \X in \myarrayR%
% {\xdef\myarray{\myarray,"\X"}}%
% \foreach \X in \myarrayT%
% {\xdef\myarray{\myarray,"\X"}}%
% \xdef\myarray{{\myarray}}%
% }
% \TikZRubikFaceLeft
% {LA}{W}{W}
% {W}{LB}{LC}
% {LD}{W}{W}
% \TikZRubikFaceRight
% {W}{LK}{W}
% {LC}{W}{LG}
% {W}{LH}{W}
% \TikZRubikFaceTop
% {LA}{W}{LI}
% {W}{W}{LJ}
% {W}{LK}{W}
% \BuildArray
% \pgfmathsetmacro\radius{0.1}
% \tdplotsetmaincoords{55}{135}
%
% \showcellnumberfalse
%
% \bgroup
% \newcommand\ddd{\Ddots}
% \newcommand\vdd{\Vdots}
% \newcommand\cdd{\Cdots}
% \newcommand\lds{\ldots}
% \newcommand\vno{\varnothing}
% \newcommand{\ts}[1]{\textsuperscript{#1}}
% \newcommand\non{1\ts{st}}
% \newcommand\ntw{2\ts{nd}}
% \newcommand\nth{3\ts{rd}}
% \newcommand\nfo{4\ts{th}}
% \newcommand\nfi{5\ts{th}}
% \newcommand\nsi{6\ts{th}}
% \newcommand\nse{7\ts{th}}
% \newcommand{\vs}[1]{\shup\sigma_{#1}}
% \newcommand\rcr{\rowcolor{black!15}}
% \newcommand\rcw{\rowcolor{white}}
% \newcommand\pcd{\cdot}
% \newcommand\pcp{\phantom\cdot}
% \newcommand\ppp{\phantom{\nse}}
%
% \begin{wrapfigure}{r}{0.32\textwidth}
% \vspace{-0.5cm}
% \begin{minipage}[r]{4cm}
% \begin{align*}
% o &\rightarrow \hiliD{so} \mid \hiliC{rs} \mid \hiliB{rr}\hspace{0.5pt} \mid \hiliA{oo}\\
% r &\rightarrow \hiliE{so} \mid \hiliH{ss}\hspace{0.4pt}\mid \hiliF{rr}\hspace{0.5pt} \mid \hiliK{os}\\
% s &\rightarrow \hiliL{so} \mid \hiliG{rs} \mid \hiliJ{or} \mid \hiliI{oo}
% \end{align*}
% \end{minipage}
%% \mathcal{J} = \begin{pmatrix}
%% \pder{o}{o} & \pder{o}{r} & \pder{o}{s}\\
%% \pder{r}{o} & \pder{r}{r} & \pder{r}{s}\\
%% \pder{s}{o} & \pder{s}{r} & \pder{s}{s}
%% \end{pmatrix}
% \hspace{-0.1cm}\begin{minipage}[r]{4cm}
% \scalebox{0.8}{\begin{tikzpicture}
% \clip (-3,-2.5) rectangle (3,2.5);
% \begin{scope}[tdplot_main_coords]
% \filldraw [canvas is yz plane at x=1.5] (-1.5,-1.5) rectangle (1.5,1.5);
% \filldraw [canvas is xz plane at y=1.5] (-1.5,-1.5) rectangle (1.5,1.5);
% \filldraw [canvas is yx plane at z=1.5] (-1.5,-1.5) rectangle (1.5,1.5);
% \foreach \X [count=\XX starting from 0] in {-1.5,-0.5,0.5}{
% \foreach \Y [count=\YY starting from 0] in {-1.5,-0.5,0.5}{
% \pgfmathtruncatemacro{\Z}{\XX+3*(2-\YY)}
% \pgfmathsetmacro{\mycolor}{\myarray[\Z]}
% \draw [thick,canvas is yz plane at x=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle;
% \ifshowcellnumber
% \node[canvas is yz plane at x=1.5,shift={(\X+0.5,\Y+0.5)}] {\Z};
% \fi
% \pgfmathtruncatemacro{\Z}{2-\XX+3*(2-\YY)+9}
% \pgfmathsetmacro{\mycolor}{\myarray[\Z]}
% \draw [thick,canvas is xz plane at y=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle;
% \ifshowcellnumber
% \node[canvas is xz plane at y=1.5,shift={(\X+0.5,\Y+0.5)},xscale=-1] {\Z};
% \fi
% \pgfmathtruncatemacro{\Z}{2-\YY+3*\XX+18}
% \pgfmathsetmacro{\mycolor}{\myarray[\Z]}
% \draw [thick,canvas is yx plane at z=1.5,shift={(\X,\Y)},fill=\mycolor] (0.5,0) -- ({1-\radius},0) arc (-90:0:\radius) -- (1,{1-\radius}) arc (0:90:\radius) -- (\radius,1) arc (90:180:\radius) -- (0,\radius) arc (180:270:\radius) -- cycle;
% \ifshowcellnumber
% \node[canvas is yx plane at z=1.5,shift={(\X+0.5,\Y+0.5)},xscale=-1,rotate=-90] {\Z};
% \fi
% }
% }
% \draw [decorate,decoration={calligraphic brace,amplitude=10pt,mirror},yshift=0pt, line width=1.25pt]
% (3,0) -- (3,3) node [black,midway,xshift=-8pt, yshift=-14pt] {\footnotesize $V_x$};
% \draw [decorate,decoration={calligraphic brace,amplitude=10pt},yshift=0pt, line width=1.25pt]
% (3,0) -- (0,-3) node [black,midway,xshift=-16pt, yshift=0pt] {\footnotesize $V_z$};
% \draw [decorate,decoration={calligraphic brace,amplitude=10pt},yshift=0pt, line width=1.25pt]
% (0,-3) -- (-3,-3) node [black,midway,xshift=-8pt, yshift=14pt] {\footnotesize $V_w$};
% \end{scope}
% \end{tikzpicture}}
% \end{minipage}
% \caption{CFGs are hypergraphs witnessed by a rank-3 tensor, whose nonempty inhabitants indicate CNF productions.\vspace{-10pt}}
% \end{wrapfigure}

In the distributional setting, suppose we have a PCFG, $G$, such that $|\mathcal{L}(G)|<\infty$. This induces a distribution $F_G: \mathcal{L}(G) \rightarrow \mathbb{R}$ which can be bisimulated by a weighted automaton (WA), $A$, where $F_A: \mathcal{L}(A) \rightarrow \mathbb{R}$ such that $F_G \sim F_A$, i.e., sampling paths through $A$ yields members of $\mathcal{L}(G)$ equal probability as sampling the PCFG from the top, down. A key issue with this approach is that $|P_G| \ll |\delta_A|$ for bisimilar $G, A$, and renormalizing the transition weights can be computationally infeasible for large $\delta_A$.

Expand Down
69 changes: 55 additions & 14 deletions src/jvmTest/kotlin/ai/hypergraph/kaliningraph/automata/WFSATest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,22 +4,27 @@ import Grammars
import Grammars.shortS2PParikhMap
import ai.hypergraph.kaliningraph.graphs.LabeledGraph
import ai.hypergraph.kaliningraph.parsing.*
import ai.hypergraph.kaliningraph.visualization.alsoCopy
import ai.hypergraph.markovian.mcmc.MarkovChain
import net.jhoogland.jautomata.*
import net.jhoogland.jautomata.Automaton
import net.jhoogland.jautomata.operations.*
import net.jhoogland.jautomata.semirings.RealSemiring
import kotlin.random.Random
import kotlin.test.*
import kotlin.time.measureTimedValue
import kotlin.time.*

typealias BAutomaton = dk.brics.automaton.Automaton
typealias JAutomaton<S, K> = Automaton<S, K>

class WFSATest {

/*
./gradlew jvmTest --tests "ai.hypergraph.kaliningraph.automata.WFSATest.testWFSA"
*/
@Test
fun testWFSA() {
val a: Automaton<String, Double> =
val a: JAutomaton<String, Double> =
EditableAutomaton<String, Double>(RealSemiring()).apply {
val s1: Int = addState(1.0, 0.0) // Create initial state (initial weight 1.0, final weight 0.0)
val s2: Int = addState(0.0, 1.0) // Create final state (initial weight 0.0, final weight 1.0)
Expand All @@ -34,7 +39,22 @@ class WFSATest {
.also { println("Took ${it.duration} to decode ${it.value.size} best strings") }
}

fun Automaton<String, Double>.toDot(processed: MutableSet<Any> = mutableSetOf()) =
/*
./gradlew jvmTest --tests "ai.hypergraph.kaliningraph.automata.WFSATest.testBRICS"
*/
@Test
fun testBRICS() {
val ab = BAutomaton.makeString("a").concatenate(BAutomaton.makeString("b"))
val aa = BAutomaton.makeString("a").concatenate(BAutomaton.makeString("a"))
val a = ab.union(aa)
val ag = List(6) { a }.fold(a) { acc, automaton -> acc.concatenate(automaton) }

println(ag.getFiniteStrings(-1))
println()
println(BAutomaton.minimize(ag.also { it.determinize() }).toDot())
}

fun JAutomaton<String, Double>.toDot(processed: MutableSet<Any> = mutableSetOf()) =
LabeledGraph {
val stateQueue = mutableListOf<Any>()
initialStates().forEach { stateQueue.add(it) }
Expand Down Expand Up @@ -70,7 +90,7 @@ class WFSATest {
* previous n-1 transitions, i.e., q' ~ argmax_{q'} P(q' | q_{t-1}, ..., q_{t-n+1})
*/

fun <S, K> Automaton<S, K>.randomWalk(mc: MarkovChain<S>, topK: Int = 1000): Sequence<S> {
fun <S, K> JAutomaton<S, K>.randomWalk(mc: MarkovChain<S>, topK: Int = 1000): Sequence<S> {
val init = initialStates().first()
val padding = List(mc.memory - 1) { null }
val ts = transitionsOut(init).map { (it as BasicTransition<S, K>).label() }.map { it to mc.score(padding + it) }
Expand All @@ -85,27 +105,48 @@ class WFSATest {
val toRepair = "NAME : NEWLINE NAME = STRING NEWLINE NAME = NAME . NAME ( STRING ) NEWLINE"
val radius = 2
val pt = Grammars.seq2parsePythonCFG.makeLevPTree(toRepair, radius, shortS2PParikhMap)
fun Char.toUnicodeEscaped() = "\\u${code.toString(16).padStart(4, '0')}"

val ctbl = Grammars.seq2parsePythonCFG.terminals.associateBy { Random(it.hashCode()).nextInt().toChar() }
val stbl = Grammars.seq2parsePythonCFG.terminals.associateBy { Random(it.hashCode()).nextInt().toChar().toUnicodeEscaped() }
fun Σᐩ.replaceAll(tbl: Map<String, String>) = tbl.entries.fold(this) { acc, (k, v) -> acc.replace(k, v) }

println("Total trees: " + pt.totalTrees.toString())
val maxResults = 10_000
val ptreeRepairs = measureTimedValue {
pt.sampleStrWithoutReplacement().distinct().take(maxResults).toSet()
}
measureTimedValue {
pt.propagator<Automaton<String, Double>>(
both = { a, b -> if (a == null) b else if (b == null) a else Concatenation(a, b) },
either = { a, b -> if (a == null) b else if (b == null) a else Union(a, b) },
pt.propagator(
both = { a, b -> if (a == null) b else if (b == null) a else a.concatenate(b) },
either = { a, b -> if (a == null) b else if (b == null) a else a.union(b) },
unit = { a ->
if ("ε" in a.root) null
else EditableAutomaton<String, Double>(RealSemiring()).apply {
val s1 = addState(1.0, 0.0)
val s2 = addState(0.0, 1.0)
addTransition(s1, s2, a.root, 1.0)
}
else BAutomaton.makeChar(Random(a.root.hashCode()).nextInt().toChar())
// EditableAutomaton<String, Double>(RealSemiring()).apply {
// val s1 = addState(1.0, 0.0)
// val s2 = addState(0.0, 1.0)
// addTransition(s1, s2, a.root, 1.0)
// }
}
)
// ?.also { println("\n" + Operations.determinizeER(it).toDot().alsoCopy() + "\n") }
// .also { println("Total: ${Automata.transitions(it).size} arcs, ${Automata.states(it).size}") }
.let { Automata.bestStrings(it, maxResults).map { it.label.joinToString(" ") }.toSet() }
// .let { WAutomata.bestStrings(it, maxResults).map { it.label.joinToString(" ") }.toSet() }
?.also { println("Original automata had ${it
.let { "${it.numberOfStates} states and ${it.numberOfTransitions} transitions"}}") }
?.also {
measureTimedValue { BAutomaton.minimize(it) }
.also { println("Minimization took ${it.duration}") }.value
// .also { it.toDot().replaceAll(stbl).alsoCopy() }
.also {
// Minimal automata had 92 states and 707 transitions
println("Minimal automata had ${
it.let { "${it.numberOfStates} states and ${it.numberOfTransitions} transitions" }
}")
}
}
.let { it?.getFiniteStrings(-1) ?: emptySet() }
}.also {
// // Print side by side comparison of repairs
// repairs.sorted().forEach {
Expand All @@ -117,7 +158,7 @@ class WFSATest {
// }
assertEquals(it.value.size, ptreeRepairs.value.size)

it.value.forEach {
it.value.map { it.map { ctbl[it] }.joinToString(" ") }.forEach {
// println(levenshteinAlign(toRepair, it).paintANSIColors())
assertTrue(levenshtein(toRepair, it) <= radius)
assertTrue(it in Grammars.seq2parsePythonCFG.language)
Expand Down

0 comments on commit 7a57c90

Please sign in to comment.