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:
Please see the FAdo documentation for the full description of Transducer format.
Below is an example of an input-altering transducer describing the suffix code property over the alphabet {a, b}. The transducer outputs any proper suffix 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 describing the 1-substitution-detecting 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
Input-preserving transducer describing the 1-sid-detecting 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
Input-altering 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