(* val zero : sym *)
val zero = Sym.fromString "0";
(* val one : sym *)
val one = Sym.fromString "1";
(* val minAndRen : dfa -> dfa *)
val minAndRen =
DFA.renameStatesCanonically o DFA.minimize o DFA.renameStatesCanonically;
(* val efaToDFA : efa -> dfa *)
val efaToDFA = nfaToDFA o efaToNFA;
(* val allStrDFA : dfa
allStrDFA accepts {0, 1}* *)
val allStrDFA =
minAndRen(efaToDFA(EFA.closure(EFA.union(EFA.fromSym zero,
EFA.fromSym one))));
(* val swapRel : sym_rel *)
val swapRel = SymRel.fromString "(0, 1), (1, 0)";
(* val zeroAllPrefPosEFA : int -> efa
if n >= 0, then zeroAllPrefPosEFA n returns an efa that accepts all
w in {0, 1}* such that diff w = 0 and all prefixes of w have diff's
between 0 and n *)
fun zeroAllPrefPosEFA 0 = EFA.emptyStr
| zeroAllPrefPosEFA n =
EFA.closure(EFA.concat(EFA.fromSym one,
EFA.concat(zeroAllPrefPosEFA(n - 1),
EFA.fromSym zero)));
(* val zeroAllPrefPosDFA : int -> dfa
if n >= 0, then zeroAllPrefPosDFA n returns a dfa that accepts
all w in {0, 1}* such that diff w = 0 and all prefixes of w
have diff's between 0 and n *)
fun zeroAllPrefPosDFA n = minAndRen(efaToDFA(zeroAllPrefPosEFA n));
(* val justBadPosEFA : int -> efa
if n >= 0, then justBadPosEFA n returns an efa that accepts all w
in {0, 1}* such that diff w = n + 1 and all proper prefixes of w
have diff's between 0 and n *)
fun justBadPosEFA 0 = EFA.fromSym one
| justBadPosEFA n =
EFA.concat(injDFAToEFA(zeroAllPrefPosDFA n),
EFA.concat(EFA.fromSym one, justBadPosEFA(n - 1)));
(* val justBadPosDFA : int -> dfa
if n >= 0, then justBadPosDFA n returns a dfa that accepts all w in
{0, 1}* such that diff w = n + 1 and all proper prefixes of w have
diff's between 0 and n *)
fun justBadPosDFA n = minAndRen(efaToDFA(justBadPosEFA n));
(* val justBadNegDFA : int -> dfa
if n >= 0, then justBadNegDFA n returns a dfa that accepts all w in
{0, 1}* such that diff w = ~(n + 1) and all proper prefixes of w
have diff's between 0 and ~n *)
fun justBadNegDFA n = DFA.renameAlphabet(justBadPosDFA n, swapRel);
(* val justBadPosOrNegDFA : int -> dfa
if n >= 0, then justBadPosOrNegDFA n returns a dfa accepting all w
in {0, 1}* such that either:
diff w = n + 1 and all proper prefixes of w have diff's between 0
and n; or
diff w = ~(n + 1) and all proper prefixes of w have diff's
between 0 and ~n *)
fun justBadPosOrNegDFA n =
minAndRen(efaToDFA(EFA.union(injDFAToEFA(justBadPosDFA n),
injDFAToEFA(justBadNegDFA n))));
(* val someSubBadEFA : int -> efa
if n >= 0, then someSubBadEFA n returns an efa that accepts all w in
{0, 1}* such that some substring of w has a diff that is < ~n or > n *)
fun someSubBadEFA n =
EFA.concat(injDFAToEFA allStrDFA,
EFA.concat(injDFAToEFA(justBadPosOrNegDFA n),
injDFAToEFA allStrDFA));
(* val someSubBadDFA : int -> dfa
if n >= 0, then someSubBadDFA n returns a dfa that accepts all w in
{0, 1}* such that some substring of w has a diff that is < ~n or > n *)
fun someSubBadDFA n = minAndRen(efaToDFA(someSubBadEFA n));
(* val allSubGoodDFA : int -> dfa
if n >= 0, then allSubGoodDFA n returns a minimized dfa that
accepts all w in {0, 1}* such that all substrings of w have diff's
between ~n and n *)
fun allSubGoodDFA n = minAndRen(DFA.minus(allStrDFA, someSubBadDFA n));