(* 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;