(* val inX : str -> bool

   tests whether a string over the alphabet {0, 1} is in X *)

fun inX x =
      Set.all
      (fn y => not(Str.equal(y, Str.fromString "010")))
      (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 inX (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 FAs
   fa, f fa 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 fa, 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 fa, then yOpt = SOME y for some
     such y; otherwise, yOpt = NONE. *)

fun test n =
      let val (goods, bads) = partition n
      in fn fa =>
              let val accepted      = FA.accepted fa
                  val goodNotAccOpt = Set.position (not o accepted) goods
                  val badAccOpt     = Set.position accepted bads
              in ((case goodNotAccOpt of
                        NONE   => NONE
                      | SOME i => SOME(ListAux.sub(Set.toList goods, i))),
                  (case badAccOpt of
                        NONE   => NONE
                      | SOME i => SOME(ListAux.sub(Set.toList bads, i))))
              end
      end;