t(L) ∩ L = EmptySet
that is, the transducer t cannot take as input an Lword and also output an Lword. For example, the prefix code property can be
described via a transducer that, on input w, returns all proper prefixes
of wsee Format
for transducers for more details.
y in t(x) implies y=x,
for any words x, y in L
; that is, on any input word x from L, the
transducer t will never output another word in L.
An inputpreserving transducer, also called channel, is a transducer t
that, on any input word w for which t(w) is nonempty, the set t(w) includes w; thus, t acts as a communication channel that receives a word w and can always return w (case of no error) or posiibly a word other than w (case of error). For example, the 1subsitutiondetection property can be
described by a transducer that, on input w, returns either w or any word that obtains by changing 1 symbol of wsee Format
for transducers for examples.
w in t(x) and w in t(y) implies y=x,
for any words x, y in L
and any word w; that is, the transducer cannot turn two different input words x, y from L into the same word. For example, the 1subsitutioncorrection property can be
described by a transducer that, on input w, returns either w or any word that obtains by changing 1 symbol of w.
Project initiator: Stavros Konstantinidis
(http://cs.smu.ca/~stavros/)

Significant contributors:
Nelma Moreira &
Rogerio Reis: as of version 3, LaSer's back end is based on
FAdo

4: Abisola Adeniran (October 2016, current version)
Incorporating into LaSer the construction problem.

3: Casey Meijer (June 2014)
Deciding maximality of all available properties, generation of executable code

2: Meng Yang (June 2012)
Deciding satisfaction of: Inputpreserving transducer, Errordetection,
and Errorcorrection properties

1: Krystian Dudzinski (June 2010)
Deciding satisfaction of: Trajectory and Inputaltering transducer properties
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:
1. '#' begins a comment
2. @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
3. Transitions are written one per line and consist of three fields separated by blanks:
"state" "symbol" "new state"
4. The source state of the first transition is the initial state.
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)
@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
Inputpreserving transducer describing the 1substitutiondetecting property over the alphabet {0, 1}. On input w, the transducer outputs either w, or any word resulting by substituting 1 bit of w with a different bit.

@Transducer 0 1
0 0 0 0
0 1 1 0
0 0 1 1
0 1 0 1
1 0 0 1
1 1 1 1
Inputpreserving transducer describing the 1siddetecting property over the alphabet {a, b}. On input w, the transducer outputs any word 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
Inputaltering transducer describing the thin property (= all languages whose words are of different lengths). On input w, the transducer outputs any word 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 properties can be described by regular expressions in the
FAdo format. For example,
the regular expression 1*0*
describes the suffix code property;
the regular expression 1*0*1* describes the infix code property;
the regular expression 0*1* + 1*0* describes the bifix code property
(being prefix and suffix code).