(* val zero : sym
val one : sym
the symbols 0 and 1 *)
val zero = Sym.fromString "0";
val one = Sym.fromString "1";
(* val diff : str -> int
the diff function, assuming input is a string over alphabet {0, 1}
*)
fun diff (nil : str) = 0
| diff (b :: bs) =
if Sym.equal(b, zero)
then ~1 + diff bs
else 1 + diff bs;
(* val allSubstringsGood : str -> bool
tests whether all substrings of a string over alphabet {0, 1} have
diff's between ~2 and 2, inclusive *)
fun allSubstringsGood x =
Set.all
(fn y =>
let val n = diff y
in ~2 <= n andalso n <= 2 end)
(StrSet.substrings x);
(* val upto : int -> str set
if n >= 0, then upto n returns all strings over alphabet {0, 1} of
length no more than n *)
fun upto 0 : str set = Set.sing nil
| upto n =
let val xs = upto(n - 1)
val ys = Set.filter (fn x => length x = n - 1) xs
in StrSet.union
(xs, StrSet.concat(StrSet.fromString "0, 1", ys))
end;
(* val partition : int -> str set * str set
if n >= 0, then partition n returns (xs, ys) where:
xs is all elements of upto n that are in X; and
ys is all elements of upto n that are not in X *)
fun partition n = Set.partition allSubstringsGood (upto n);
(* val test = fn : int -> dfa -> str option * str option
if n >= 0, then test n returns a function f such that, for all DFAs
dfa, f dfa returns a pair (xOpt, yOpt) such that:
If there is an element of {0, 1}* of length no more than n that
is in X but is not accepted by dfa, then xOpt = SOME x for some
such x; otherwise, xOpt = NONE.
If there is an element of {0, 1}* of length no more than n that
is not in X but is accepted by dfa, then yOpt = SOME y for some
such y; otherwise, yOpt = NONE. *)
fun test n =
let val (goods, bads) = partition n
in fn dfa =>
let val determAccepted = DFA.determAccepted dfa
val failAccOpt = Set.position (not o determAccepted) goods
val failNotAccOpt = Set.position determAccepted bads
in ((case failAccOpt of
NONE => NONE
| SOME i => SOME(ListAux.sub(Set.toList goods, i))),
(case failNotAccOpt of
NONE => NONE
| SOME i => SOME(ListAux.sub(Set.toList bads, i))))
end
end;