O-LaSer answers questions about regular languages, __O__ther than
independence properties questions.

[KaKoKoYa:2013] Lila Kari, Stavros Konstantinidis, Steffen Kopecki, Meng Yang: An efficient algorithm for computing the edit distance of a regular language via input-altering transducers.

One can use the Grail and FAdo formats for nondeterministic finite automata (those with nonempty transitions).

The format of FAdo files must be as follows:

- '#' begins a comment
**@NFA**, or**@DFA**, begins a new automaton (and determines its type) and must be followed by the list of the final states separated by blanks- Transitions are written one per line and consist of three fields separated by blanks: "state" "symbol" "new state"
- The source state of the first transition is the initial state.

Here is an example of an automaton accepting ab* using both, Grail and FAdo formats:

```
Grail: FAdo:
(START) |- 1 @NFA 2
1 a 2 1 a 2
2 b 2 2 b 2
2 -| (FINAL)
```

**More examples follow:**

Automaton accepting aaa(aaa)*b + aa(ba)*a(aa(ba)*a)*b:

```
Grail: FAdo:
(START) |- 1 @NFA 8
1 a 2 1 a 2
2 a 3 2 a 3
3 b 2 3 b 2
3 a 4 3 a 4
4 a 2 4 a 2
4 b 8 4 b 8
1 a 5 1 a 5
5 a 6 5 a 6
6 a 7 6 a 7
7 a 5 7 a 5
7 b 8 7 b 8
8 -| (FINAL)
```

Automaton accepting ab + bba:

```
Grail: FAdo:
(START) |- 1 @NFA 3
1 a 2 1 a 2
2 b 3 2 b 3
1 b 4 1 b 4
4 b 5 4 b 5
5 a 3 5 a 3
3 -| (FINAL)
```

In the new version of I-LaSer (as of June 2014), only the FAdo format of transducers is accepted, as the Grail-like format is not generally supported. Transducers must be in standard form, that is, having *transitions of the form p x y q*, where p and q are states, and each of x and y is either a single alphabet symbol or the empty word. The empty word is written as *@epsilon*.

The format of transducer FAdo files must be as follows:

- '#' begins a comment.
**@Transducer**begins a new transducer and must be followed by the list of the final states separated by blanks.- Transitions are written one per line and must be in standard form as noted above.
- The source state of the first transition is the initial state.

Please see the FAdo documentation for the full description of Transducer format.

Here is an example of an input-altering transducer defining the *suffix code* property. The transducer returns the set of all *proper* suffixes of a given input word.

```
@Transducer 2 3
1 a @epsilon 2
1 b @epsilon 2
2 a @epsilon 2
2 b @epsilon 2
2 a a 3
2 b b 3
3 a a 3
3 b b 3
```

Input-preserving transducer defining the *1-sid error-detecting* property. On input *w*, the transducer returns all words resulting by performing at most one symbol substitution/insertion/deletion operation on *w*.

```
@Transducer 0 1
0 a a 0
0 b b 0
0 a b 1
0 b a 1
0 a @epsilon 1
0 b @epsilon 1
0 @epsilon a 1
0 @epsilon b 1
1 a a 1
1 b b 1
```

Input-altering transducer defining the *thin* property (those languages whose words are of different lengths). On input *w*, the transducer returns all words of the same length as *w*, but different from *w*.

```
@Transducer 2
1 a a 1
1 b b 1
1 a b 2
1 b a 2
2 a a 2
2 b b 2
2 a b 2
2 b a 2
```

Regular trajectory sets can be described via regular expressions or automata over {0,1}. For regular expressions, one can use FAdo format. For finite automata (those with nonempty transitions), one can use the Grail or FAdo format.

Here is an example of an automaton accepting the language described by the regular expression 1*0*, which defines the *suffix code* property.

```
Grail: FAdo:
(START) |- 1 @NFA 1 2
1 0 1 1 0 1
1 1 2 1 1 2
2 1 2 2 1 2
1 -| (FINAL)
2 -| (FINAL)
```

Automaton accepting 1*0*1*, which defines the *infix code* property.

```
Grail: FAdo:
(START) |- 1 @NFA 1 2 3
1 1 1 1 1 1
1 0 2 1 0 2
2 0 2 2 0 2
2 1 3 2 1 3
3 1 3 3 1 3
1 -| (FINAL)
2 -| (FINAL)
3 -| (FINAL)
```