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:
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.
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)