Synthesizing Transducers from Complex Specifications

The transducer we are synthesizing has $k$ (part of the problem input) states $Q_{T}=\allowbreak{}\{q_{0},...,\allowbreak{}q_{k-1}\}$. We often use $q^{\mathit{init}}_{T}$ as an alternative for $q_{0}$, the initial state of $T$.

We illustrate how a transition $q_{1}\xrightarrow{\texttt{a}/\texttt{bc}}q_{2}$ is represented in our encoding. The target state is captured using an uninterpreted function ${\texttt{d}^{\texttt{st}}}:Q_{T}\times\Sigma\to Q_{T}$, e.g., ${\texttt{d}^{\texttt{st}}}(q_{1},\texttt{a})=q_{2}$. Representing the output of the transition is trickier because its length is not known a priori. The synthesis problem however provides an output bound $l$, which allows us to limit the number of characters that may appear in the output. We use an uninterpreted function ${\texttt{d}^{\texttt{out}}_{\texttt{ch}}}:Q_{T}\times\Sigma\times\{0,\ldots,l{-}1\}\to\Sigma$ to represent each character in the output string; in our example, ${\texttt{d}^{\texttt{out}}_{\texttt{ch}}}(q_{1},\texttt{a},0)=\texttt{b}$ and ${\texttt{d}^{\texttt{out}}_{\texttt{ch}}}(q_{1},\texttt{a},1)=\texttt{c}$. Since an output string’s length can be smaller than $l$, we use an additional uninterpreted function ${\texttt{d}^{\texttt{out}}_{\texttt{len}}}{}:Q_{T}\times\Sigma\to\{0,\ldots,l\}$ to model the length of a transition’s output; in our example ${\texttt{d}^{\texttt{out}}_{\texttt{len}}}(q_{1},\texttt{a})=2$.

We say an assignment to the above variables extends to a transducer $T$ for the transducer $T$ obtained by instantiating $\delta^{st}$ and $\delta^{out}$ as described above.

Goal: For each input output-example ${s\mapsto t}\in E$, $T$ should translate $s$ to $t$.

Translating $s$ to the correct output string means that $\delta_{T}^{\mathit{out*}}(q^{\mathit{init}}_{T},s)=t$. Generating constraints that capture this behavior of $T$ on an example is challenging because we do not know a priori what parts of $t$ are produced by what steps of the transducer’s run. Suppose that we need to translate $s=a_{0}a_{1}$ to $t=b_{0}b_{1}b_{2}$. A possible solution is for the transducer to have the run $q_{0}\xrightarrow{a_{0}/b_{0}}q1\xrightarrow{a_{1}/b_{1}b_{2}}q_{2}$. Another possible solution might be to instead have $q_{0}\xrightarrow{a_{0}/b_{0}b_{1}}q1\xrightarrow{a_{1}/b_{2}}q_{2}$. Notice that the two runs traverse the same states but produce different parts of the output strings at each step. Intuitively, we need a way to “track” how much output the transducer has produced before processing the $i$-th character in the input and what state it has landed in. For every input example ${s\mapsto t}$ such that $s=a_{0}\cdots a_{n}$ and $t=b_{0}\cdots b_{m}$, we introduce an uninterpreted function ${\texttt{config}}_{s}:\{0,\ldots,n\}\rightarrow\{0,\ldots,m\}\times Q_{T}$ such that ${\texttt{config}}_{s}(i)=(j,q_{T})$ iff after reading $a_{0}\cdots a_{i-1}$, the transducer $T$ has produced the output $b_{0}\cdots b_{j-1}$ and reached state $q_{T}$—i.e., $\delta_{T}^{\mathit{out*}}(q_{0},a_{0}\cdots a_{i-1})=b_{0}\cdots b_{j-1}$ and $\delta_{T}^{\mathit{st*}}(q_{0},a_{0}\cdots a_{i-1})=q_{T}$.

We describe the constraints that describe the behavior of ${\texttt{config}}_{s}$. Constraint 1 states that a configuration must start at the initial state and be at position 0 in the output.

Constraint 2 captures how the configuration is updated when reading the $i$-th character of the input. For every $0\leq i<n$, $0\leq j<m$, $c\in\Sigma$, and $q_{T}\in Q_{T}$:

Informally, if the $i$-th character is $c$ and the transducer has reached state $q_{T}$ and produced the characters $b_{0}\cdots b_{j-1}$ so far, the transition reading $c$ from state $q_{T}$ outputs characters $b_{j}\cdots b_{j+f-1}$, where $f$ is the output length of the transition. The next configuration is then $(j+f,{\texttt{d}^{\texttt{st}}}(q_{T},c))$.

Finally, Constraint 3 forces $T$ to be completely done with generating $t$ when $s$ has been entirely read. Recall that $\mathit{len}(s)=n$ and $\mathit{len}(t)=m$.

Goal: $T$ should satisfy the property $\{P\}T\{Q\}$.

Encoding this property using constraints is challenging because it requires enforcing that when $T$ reads one of the (potentially) infinitely many strings in $P$ it always outputs a string in $Q$. To solve this problem, we draw inspiration from how one proves that the property $\{P\}T\{Q\}$ holds—i.e., using a simulation relation that relates runs over $P$, $T$ and $Q$. Intuitively, if $P$ has read some string $w$, we need to be able to encode the behavior of $T$ in terms of $w$, i.e., what state of $T$ this transducer is in after reading $w$ and what output string $w^{\prime}$ it produced. Further, we also need to be able to encode in which state $Q$ would be after reading the output string $w^{\prime}$. We do this by introducing a function sim: $Q_{P}\times Q_{T}\times Q_{Q}\rightarrow\{0,1\}$, which preserves the following invariant: ${\texttt{sim}}(q_{P},q_{T},q_{Q})$ holds if there exist strings $w,w^{\prime}$ such that $\delta_{P}^{*}(q^{\mathit{init}}_{P},w)=q_{P}$, $\delta_{T}^{\mathit{st*}}(q^{\mathit{init}}_{T},w)=q_{T}$, $\delta_{T}^{\mathit{out*}}(q^{\mathit{init}}_{T},w)=w^{\prime}$, and $\delta_{Q}^{*}(q^{\mathit{init}}_{Q},w^{\prime})=q_{Q}$.

Constraint 4 states the initial condition of the simulation—i.e., $P$, $T$, and $Q$ are in their initial states.

Constraint 5 encodes how we advance the simulation relation for states $q_{P},q_{T},q_{Q}$ and for a character $c\in\Sigma$, using free variables $c_{0}\ldots,c_{l-1}$ and $q_{Q}^{0}\ldots,\allowbreak{}q_{Q}^{l}$ that are separate for each combination of $q_{P},q_{T},q_{Q}$, and $c$:

Intuitively, if ${\texttt{sim}}(q_{P},q_{T},q_{Q})$ and we read a character $c$, $P$ moves to $\delta_{P}(q_{P},\mathit{c})$ and $T$ moves to ${\texttt{d}^{\texttt{st}}}{}(q_{P},\mathit{c})$. However, we also need to advance $Q$ and the ${\texttt{d}^{\texttt{out}}_{\texttt{len}}}{}$ symbols produced by ${\texttt{d}^{\texttt{out}}_{\texttt{ch}}}{}$. We hard-code the transition relation $\delta_{Q}$ in an uninterpreted function ${\texttt{d}_{Q}}:Q_{Q}\times\Sigma\rightarrow Q_{Q}$, and apply it to compute the output state reached when reading the output string. E.g., if ${\texttt{d}^{\texttt{out}}_{\texttt{len}}}{}(q_{T},c)=2$ and ${\texttt{d}^{\texttt{out}}_{\texttt{ch}}}(q_{T},c,0)=c_{0}$ and ${\texttt{d}^{\texttt{out}}_{\texttt{ch}}}(q_{T},c,1)=c_{1}$, the next state in $Q$ is ${\texttt{d}_{Q}}({\texttt{d}_{Q}}(q_{Q},c_{0}),c_{1})$.

Lastly, Constraint 6 states that if we encounter a string in $\mathcal{L}(P)$—i.e., $P$ is in a state $q_{P}\in F_{P}$—the relation does not contain a state $q_{Q}\notin F_{Q}$. Since $Q$ is deterministic, this means that $Q$ accepts $T$’s output.

Goal: The mean edit distance between any input string $w$ in $\mathcal{L}(P)$ and the output string $T(w)$ should not exceed $d$.

Capturing the edit distance for all the possible inputs in the language of $P$ and the corresponding outputs produced by the transducer is challenging because these sets can be infinite. Furthermore, exactly computing the edit distance between an input and an output string may involve comparing characters appearing on different transitions in the transducer run. For example, consider the transducer shown in Figure 2(a) and suppose that we are only interested in strings in the input type $P=\texttt{a(ba)}{\ast}\texttt{a}$. The first transition from $q_{0}$ deletes the a, therefore making 1 edit. This transducer has a cycle between states $q_{1}$ and $q_{2}$, which can be taken any number of times. Each iteration, locally, would require that we make 2 edits: one to change the b to a, and the other to change the a to b. However, the total number of edits made over any string in the input type $P=\texttt{a(ab)}{\ast}\texttt{a}$ by this transducer is 1, because the transducer changes strings of the form $\texttt{a(ba)}^{n}\texttt{a}$ to be of the form $\texttt{(ab)}^{n}\texttt{a}$. Looking at the transitions in isolation, we are prevented from deducing that the edit distance is always 1 because the first transition delays outputting a character. If there was no such delay, as is the case for the transducer in Figure 2(b), which is equivalent on the relevant input type to the one in Figure 2(a), then this issue would not arise.

We take inspiration from Benedikt et al. [12] and focus on the simpler problem of synthesizing a transducer that has ‘aggregate cost’ that satisfies the given objective.¹¹1Benedikt et al. [12] studied a variant of the problem where the distance is bounded by some finite constant. Their work shows that when there is a transducer between two languages that has some bounded global edit distance, then there is also a transducer that is bounded (but with a different bound) under a local method of computing the edit distance—i.e., one where the computation of the edit distance is done transition by transition. For a transducer $T$ and string $s=a_{0}\ldots a_{n}$, let $q^{\mathit{init}}_{T}\xrightarrow{a_{0}/y_{0}}q_{T}^{1}\ldots q_{T}^{n}\xrightarrow{a_{n}/y_{n}}q_{T}^{n+1}$ be the run of $s$ on $T$. Then, the aggregate cost of $T$ on $s$ is the sum of the edit distances $\mathit{ed\!\_\!dist}(a_{i},y_{i})$ over all indices $0\leq i\leq n$. The mean aggregate cost of $T$ on $s$ is the aggregate cost divided by $\mathit{len}(s)$, the length of $s$. It follows that if $T$ has a mean aggregate cost lower than some specified $d$ for every string, then it also has a mean edit distance lower than $d$ for every string.

However, the mean aggregate cost overapproximates the edit distance, e.g., the transducer in Figure 2(a) has mean aggregate cost 1, while the mean edit distance when considering only strings in $P=\texttt{a(ab)}{\ast}\texttt{a}$ is less than $1/2$. For this reason, if the mean edit distance objective was set to $1/2$, our constraint encoding can only synthesize the transducer in Figure 2(b), and not the equivalent one in Figure 2(a).

Our encoding is complete for transducers in which the aggregate cost coincides with the actual edit distance. We leave the problem of being complete with regards to global edit distance as an open problem. In fact, we are not even aware of an algorithm for checking (instead of synthesizing) whether a transducer satisfies a mean edit distance objective.²²2The mean edit distance is similar to mean payoff [13], which discounts a cost by the length of a string and looks at the behavior of a transducer in the limit. Our distance is different because 1) it looks at finite-length strings, and 2) it requires computing the edit distance, which cannot be done one transition at a time. In Section 4.2, we present transducers with lookahead, which can mitigate this source of incompleteness. Furthermore, our evaluation shows that using the aggregate cost and enabling lookahead are both effective techniques in practice.

We can now present our constraints. First, we provide constraints for the edit distance of individual transitions (recall that transitions are being synthesized and we therefore need to compute their edit distances separately). Secondly, we provide constraints that implicitly compute state invariants to capture the aggregate cost between input and output strings at various points in the computation. We are given a rational number $d$ as an input to the problem, which is the allowed distance bound.

We still need to compute the weighted edit distance for every string in the possibly infinite language $\mathcal{L}(P)$. Building on the idea of simulation from the previous section, we introduce a new function called ${\texttt{en}}:Q_{P}\times Q_{T}\times Q_{Q}\rightarrow\mathbb{Q}$, which tracks an upper bound on the sum of the distances so far at that point in the simulation. This function is similar to a progress measure, which is a type of invariant used to solve energy games [14], a connection we expand on in Section 6. In particular, we already know that if there exist strings $w,w^{\prime}$ such that $\delta_{P}^{*}(q^{\mathit{init}}_{P},w)=q_{P}$, $\delta_{T}^{\mathit{st*}}(q^{\mathit{init}}_{T},w)=q_{T}$, $\delta_{T}^{\mathit{out*}}(q^{\mathit{init}}_{T},w)=w^{\prime}$, and $\delta_{Q}^{*}(q^{\mathit{init}}_{Q},w^{\prime})=q_{Q}$, then we have ${\texttt{sim}}(q_{P},q_{T},q_{Q})$. Let this run over $T$ be denoted by $q^{\mathit{init}}_{T}\xrightarrow{a_{0}/y_{0}}q_{T}^{1}\ldots q_{T}^{n-1}\xrightarrow{a_{n-1}/y_{n-1}}q_{T}$, where $w=a_{0}\cdots a_{n-1}$, $w^{\prime}=y_{0}\cdots y_{n-1}$, and $q_{T}=q_{T}^{n}$. We have that ${\texttt{en}}(q_{P},q_{T},q_{Q})\geq\sum_{i=0}^{n-1}{\texttt{wed}}(q_{T}^{i},a_{i})$.

The en function is a budget on the number of edits we can still perform. At the initial states, we start with no ‘initial credit’ and the energy is 0.

Constraint 10 bounds the energy budget according to the weighted edit distance of a transition by computing the minimum budget required at any point to still satisfy the distance bound. For each combination of $q_{P},q_{T},q_{Q}$, and $c\in\Sigma$, the constraint uses free variables $c_{0},\ldots,c_{l}$ and $q_{Q}^{0},\ldots,q_{Q}^{l-1}$:

In our example, Constraint 10 encodes that the energy at $q_{0}$ can be 1 less than that at $q_{1}$, but that the energy at $q_{1}$ needs to be $3$ greater than at $q_{2}$ since we need to spend 3 edit operations over the second transition.

At any point during a run, the transducer is allowed to go below the mean edit distance and then ‘catch up’ later because we only care about the edit distance when the transducer has finished reading a string in $\mathcal{L}(P)$. Therefore, when we reach a final state of $P$, the transducer should not be in ‘energy debt’.

Symbolic finite automata (s-FA) and transducers (s-FT) extend their non-symbolic counterparts by allowing transitions to carry predicates and functions to represent (potentially infinite) sets of input characters and output strings. Figure 3(a) shows an s-FT that extends the escapeQuotes transducer from Figure 1(a) to handle alphabetic characters. The bottom transition from $q_{0}$ reads a character " (bound to the variable $x$) and outputs the string \" (i.e., a \ followed by the character stored in $x$). Symbolic finite automata (s-FA) are s-FTs with no outputs. To simplify our exposition, we focus on s-FAs and s-FTs that only operate over ASCII characters that are ordered by their codes. In particular, all of our predicates are unions of intervals over characters (i.e., $x\neq\texttt{\textbackslash}$ is really the union of intervals [NUL-[] and []-DEL]); we often use the predicate notation instead of explicitly writing the intervals for ease of presentation. Furthermore, we only consider two types of output functions: constant characters and offset functions of the form $x+k$ that output the character obtained by taking the input $x$ and adding a constant $k$ to it—e.g., applying $x+(-32)$ to a lowercase alphabetic letter gives the corresponding uppercase letter.

In the rest of the section, we show how we can solve the transducer synthesis problem in the case where $P$ and $Q$ are s-FAs and the goal is to synthesize an s-FT (instead of an FT) that meets the given specification. Intuitively, we do this by ‘finitizing’ the alphabet of the now symbolic input-output types, synthesizing a finite transducer over this alphabet using the technique presented in Section 3, and then extracting an s-FT from the solution.

For an s-FA $M$, we denote its corresponding FA over the alphabet $\mathit{mterms}(M)$ with $\mathit{F}(M)$. Given an s-FA $M$, the set of transitions of $\mathit{F}(M)$ is defined as follows:

This algorithm replaces a transition guarded by a predicate $\phi$ in the given s-FA with a set of transitions consisting of the witnesses of the minterms where $\phi$ is satisfiable. In interval arithmetic this is the set of intervals that intersect with the interval specified by $\phi$. The transition from $q_{1}$ guarded by the predicate $[x\neq\texttt{\textbackslash}]$ in Figure 3(a) intersects with 2 minterms $[x\neq\texttt{"}\wedge x\neq\texttt{\textbackslash}]$ and $[x=\texttt{"}]$. As a result, we see that this transition is replaced by two transitions in Figure 3(b), one that reads " and another that reads a.

While our s-FT recovery algorithm is sound, it may apply case 3 more often than necessary and introduce many constants, therefore yielding a transducer that does not generalize well to unseen examples. However, our evaluation shows that our technique works well in practice. We provide a sketch of the proof of soundness of this algorithm in Appendix C.

Deterministic transducers cannot express functions where the output at a certain transition depends on future characters in the input. Consider the problem of extracting all substrings of the form <x> (where $\texttt{x}\neq\texttt{<}$) from an input string. This is the getTags problem from [15]. A deterministic transducer cannot express this transformation because when it reads < followed by x it has to output <x if the next character is a > and nothing otherwise. However, the transducer does not have access to the next character!

Instead, we extend our technique to handle deterministic transducers with lookahead, i.e., the ability to look at the string suffix when reading a symbol. Formally, a Transducer with Regular Lookahead is a pair $(T,R)$ where $T$ is an FT with $\Sigma_{T}=Q_{R}\times\Sigma$, and $R$ is a total DFA with $\Sigma_{R}=\Sigma$. The transducer $T$ now has another input in its transition function, although it still only outputs characters from $\Sigma$, i.e., $\delta_{T}^{\mathit{out}}:Q_{T}\times(Q_{R}\times\Sigma)\rightarrow\Sigma$, and $\delta_{T}^{\mathit{st}}:Q_{T}\times(Q_{R}\times\Sigma)\rightarrow Q_{T}$. The semantics is defined as follows. Given a string $w=a_{0}\cdots a_{n}$, we define a function $r_{w}$ such that $r_{w}(i)=\delta_{R}(q^{\mathit{init}}_{R},a_{n}\cdots a_{i+1})$. In other words, $r_{w}(i)$ gives the state reached by $R$ on the reversed suffix starting at $i+1$. At each step $i$, the transducer $T$ reads the symbol $(a_{i},r_{w}(i))$. The extended transition functions now take as input a lookahead word, which is a sequence of pairs of lookahead states and characters, i.e., from $(Q_{R}\times\Sigma)^{\ast}$.

To synthesize transducers with lookahead, we introduce uninterpreted functions ${\texttt{d}_{\texttt{R}}}$ for the transition function of $R$, and ${\texttt{look}}_{w}$ for the $r$-values of $w$ on $R$. Additionally, we introduce a bound $k_{R}$ on the number of states in the lookahead automaton $R$ as our synthesis algorithm has to synthesize both $T$ and $R$ at the same time. Appendix D provides the modified constraints needed to encode input-output types and input-output examples to use lookahead.

Part of the transducer with lookahead we synthesize for the getTags problem is shown in Figure 4. Notice that there are 2 transitions out of $q_{1}$ for the same input but different lookahead state: the string <x is outputted when the lookahead state is $r_{1}$.

In this section, we show how our synthesis technique can also be used to “repair” buggy transducers. The key idea is to use the closure properties of automata and transducers—e.g., closure under union and sequential compositions [8]—to reduce repair problems to synthesis ones. The ability to algebraically manipulate transducers and automata is one of the key aspects that distinguishes our work from other synthesis works that use domain-specific languages [1, 5].

We describe two settings in which we can repair an incorrect transducer $T_{\textit{bad}}$: 1. Let $\{P\}T_{\textit{bad}}\{Q\}$ be an input-output type violated by $T_{\textit{bad}}$ and let $\mathit{Out}_{P}(T_{\textit{bad}})$ be the finite automaton describing the set of strings $T_{\textit{bad}}$ can output when fed inputs in $P$ (this is computable thanks to closure properties of transducers). We are interested in the case where $\mathit{Out}_{P}(T_{\textit{bad}})\setminus Q\neq\emptyset$—i.e., $T_{\textit{bad}}$ can produce strings that are not in the output type.

We describe two ways in which we repair transducers.

Benchmarks. Our first set of benchmarks is obtained from Optician [5, 6], a tool for synthesizing lenses, which are bidirectional programs used for keeping files in different data formats synchronized. We adapted 11 of these benchmarks to work with astra (note that we only synthesize one-directional transformations), and added one additional benchmark extrAcronym2, which is a harder variation (with a larger input type) of extrAcronym. We excluded benchmarks that require some memory, e.g., swapping words in a sentence, as they cannot be modeled with transducers.

Our second set of benchmarks (Miscellaneous) consists of 6 problems we created based on file transformation tasks (unixToDos, dosToUnix and CSVSeparator), and s-FTs from the literature–escapeQuotes from [17], getTags and quicktimeMerger from [15]. All of the benchmarks require synthesizing s-FTs and getTags requires synthesizing an s-FT with lookahead (details in Table I).

To generate the sets of examples, we started with the examples that were used in the original source when available. In 5 cases, astra synthesized a transducer that was not equivalent to the one synthesized by Optician, even though it did meet the specification. In these cases, we used astra to synthesize two different transducers that met the specification, computed a string on which the two transducers differed, and added the desired output for that string as a new example. We repeated this task until astra yielded the desired transducer and we report the time for such sets of examples. The number of examples varies between 1 and 5. The ability to perform equivalence checks of two transducers is yet another reason why synthesizing transducers is useful and is in some ways preferable to synthesizing programs in a DSL. For each benchmark we chose a mean edit distance of 0.5 when the transformation could be synthesized with this distance and of 1 otherwise.

While the synthesized transducers have at most 3 states, we note that this is because astra synthesizes total transducers and then restricts their domains to the input type $P$. This is advantageous because synthesizing small total transducers is easier than synthesizing transducers that require more states to define the domain. For instance, when we restrict the solution of extrAcronym2 to its input type, the resulting transducer has 11 states instead of the 2 required by the original solution!

Optician is faster when the number of variables in the constraint encoding increases, while astra is faster on the normalizeSpaces benchmark. Optician, which uses regular expressions to express the input and output types, does not work so well with unstructured data. To confirm this trend, we wrote synthesis tasks for the escapeQuotes and getTags benchmarks in Optician and it was unable to synthesize those as well—e.g., escapeQuotes requires replacing every " character with \".

To further look at the reliance of Optician on regular expressions, we converted the regular expressions used in the lens synthesis benchmarks to automata and then back to regular expressions using a variant of the state elimination algorithm that acts on character intervals. This results in regular expressions that are not very concise and might have redundancies. Optician could only solve 4/11 benchmarks that it was previously synthesizing (Optician-re in Table I).

Answer to Q1: astra can solve real-world benchmarks and has performance comparable to that of Optician for similar tasks. Unlike Optician, astra does not suffer from variations in how the input and output types are specified.

Benchmarks. We considered the benchmarks in Table II. The only pre-existing benchmark that we found was escapeQuotes, through the interface of the Bek programming language used for verifying transducers [17]. We generated 11 additional faulty transducers to repair in the following two ways: (i) Introducing faults in our synthesis benchmarks: We either replaced the output string of a transition with a constant character, inserted an extra character, or deleted a transition altogether. (ii) Incorrect transducers: We intentionally provided fewer input-output examples and used only example-based constraints on some of our synthesis benchmarks.

All the benchmarks involve s-FTs. Three benchmarks are wrong on both input-output types and examples and the rest are only wrong on examples. Additionally, we note that to repair a transducer, we need the “right” set of minterms. Typically, the set of minterms extracted from the transducer predicates is the right one, but in the case of the escapeBrackets problems, astra needs a set of custom minterms we provide manually—i.e., repairing the transducer requires coming up with a new predicate. We are not aware of another tool that solves transducer repair problems and so do not show any comparisons.