regular expression | v ----------- | mk_auto | ----------- | deterministic automaton | v ---------------- string --> | auto_chopper | --> chopped up string ----------------A chopped up string is a pair of
The auto_chopper is implemented in theory AutoChopper. An alternative (more efficient) version is defined in AutoChopper1. However, no properties have been proved for it yet. The top part of the diagram, i.e. the translation of regular expressions into deterministic finite automata is still missing (although we have some bits and pieces).
The directory also contains Regset_of_auto, a theory describing the translation of deterministic automata into regular sets.