Command:reg - Walnut-Theorem-Prover/Walnut GitHub Wiki

The "reg" command creates an automaton based on a specified regular expression. The syntax for the "reg" command is:

reg <name> <number system/alphabet> � <number system/alphabet> "<regular expression>"

Results saved in: Result/, Automata Library/.

Regular expressions consist of regular operations such as: - OR (|) - AND (&) - concatenation - Kleene star (*)

The alphabet for the regular expressions are arbitrary tuples of integers. One may define regular expressions on an alphabet of 0-9, but can also specify, for example, [1, -1, 1][0, 1, -1]* to mean 10* in the first coordinate, -11* in the second, and 1-1* in the third. In particular, one can specify numbers above 9 and below 0, provided brackets are used (e.g. 1[10]* is 1 followed by an arbitrary number of 10s and similar for 1[-1]*). Brackets may also be used for numbers 0-9 (e.g. [1][10]*) but are not mandatory in this case. A number system or alphabet must be supplied for each coordinate in the expression's tuples.

Sample usages of the "reg" command:

reg foo {-1,0,1} "(1[-1])*0*|(1[-1])*10*"

reg bar msd_2 msd_2 "[1, 0][0, 0]*"

reg tmp msd_3 "((012)*2*)|((012)*01)"