(* standard definitions *)
val regToDFA = nfaToDFA o efaToNFA o faToEFA o regToFA;
val minAndRen = DFA.renameStatesCanonically o DFA.minimize;
(* the alphabet {0, 1, 2, 3} *)
val syms0123 = SymSet.fromString "0, 1, 2, 3";
(* regular expression and DFA generating/accepting {0, 1, 2, 3}* *)
val allStrReg = Reg.closure(Reg.allSym syms0123);
val allStrDFA = minAndRen(regToDFA allStrReg);
(* symbolic relation on {0, 1, 2, 3} swapping 0 and 1 *)
val swap01 = SymRel.fromString "(0, 1), (1, 0), (2, 2), (3, 3)";
(* symbolic relation on {0, 1, 2, 3} swapping 0 and 2 *)
val swap02 = SymRel.fromString "(0, 2), (2, 0), (1, 1), (3, 3)";
(* symbolic relation on {0, 1, 2, 3} swapping 0 and 3 *)
val swap03 = SymRel.fromString "(0, 3), (3, 0), (1, 1), (2, 2)";
(* DFA accepting all elements of {0, 1, 2, 3}* with odd number of 1s *)
val odd1sDFA =
minAndRen
(DFA.minus
(allStrDFA,
DFA.renameAlphabet(even0sDFA, swap01)));
(* DFA accepting all elements of {0, 1, 2, 3}* with even number of 2s *)
val even2sDFA = DFA.renameAlphabet(even0sDFA, swap02);
(* DFA accepting all elements of {0, 1, 2, 3}* with odd number of 3s *)
val odd3sDFA =
minAndRen
(DFA.minus
(allStrDFA,
DFA.renameAlphabet(even0sDFA, swap03)));
(* DFA accepting all elements of {0, 1, 2, 3}* in which the
number of 0s is even and the number of 1s is odd and the
number of 2s is even and the number of 3s is odd *)
val paritiesDFA =
minAndRen
(DFA.genInter
[even0sDFA, odd1sDFA, even2sDFA, odd3sDFA]);
(* grammar generating X *)
val gram0 =
Gram.renameVariablesCanonically
(Gram.inter(origGram, injDFAToEFA paritiesDFA));