I-LaSer answers questions about regular languages and independent properties - prefix code property, suffix code property, ..., various error-detection and error-correction properties.
t(L) ∩ L = EmptySet
that is, the transducer t cannot take as input an L-word and also output an L-word. For example, the prefix code property can be
described via a transducer that, on input w, returns all proper prefixes
of w---see 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 input-preserving 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 1-subsitution-detection 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---see 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 1-subsitution-correction 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/)
Nelma Moreira & Rogerio Reis: as of version 3, LaSer's back end is based on FAdo
5: Matthew Rafuse (January 2018, current version)
Incorporating into LaSer satisfaction of DNA properties, introducing text areas for entering user input, and making the views.py code modular.
4: Abisola Adeniran (October 2016)
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: Input-preserving transducer, Error-detection, and Error-correction properties
1: Krystian Dudzinski (June 2010)
Deciding satisfaction of: Trajectory and Input-altering 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:
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)
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
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).
Theta Antimorphisms are used to answer questions about DNA properties.
Below is an example of an antimorphism describing the DNA antimorphism over the DNA alphabet. There is no need to add the inverses as LaSer does this automatically.
@Theta
a t
g c