(* val hasBad2 : str -> bool

   hasBad2 x tests whether x has one or more of 02, 10 and 21 as a
   substring *)

fun hasBad2 x =
      Str.substr(Str.fromString "02", x) orelse
      Str.substr(Str.fromString "10", x) orelse
      Str.substr(Str.fromString "21", x)

(* val hasSym sym * str -> bool

   hasSym(a, x) tests whether a is a symbol in x *)

fun hasSym(a, x) = Str.substr([a], x);

(* val hasAllSyms : str -> bool

   hasAllSyms x tests whether x has at least one occurrence of
   all of 0, 1 and 2 *)

fun hasAllSyms x =
     hasSym(Sym.fromString "0", x) andalso
     hasSym(Sym.fromString "1", x) andalso
     hasSym(Sym.fromString "2", x)

(* val inX : int -> str -> bool

   if m >= 0 and x is in {0, 1, 2}^*, inX m x tests whether x is in X_m *)

fun inX m x =
      not(hasBad2 x) andalso
      Set.all
      (fn y => if length y = m then hasAllSyms y else true)
      (StrSet.substrings x);

(* val upto : int -> str set

   if n >= 0, then upto n returns all strings over alphabet {0, 1, 2} 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, 2", ys))
      end;

(* val partition : int -> int -> str set * str set

   if m >= 0 and n >= 0, then partition m n returns (xs, ys) where:

   xs is all elements of upto n that are in X_m; and

   ys is all elements of upto n that are not in X_m *)

fun partition m n = Set.partition (inX m) (upto n);

(* val test : int -> int -> dfa -> str option * str option

   if m >= 0 and n >= 0, then test m 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, 2}^* of length no more than n that
     is in X_m 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, 2}^* of length no more than n that
     is not in X_m but is accepted by dfa, then yOpt = SOME y for some
     such y; otherwise, yOpt = NONE. *)

fun test m n =
      let val (goods, bads) = partition m n
      in fn dfa =>
              let val determAccepted = DFA.determAccepted dfa
                  val goodNotAccOpt  = Set.position (not o determAccepted) goods
                  val badAccOpt      = Set.position determAccepted 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;

(* doit m prints the required information about ansDFA m *)

fun doit m =
      let val dfa = ansDFA m
          val bs  = DFA.alphabet dfa
          val n   = DFA.numStates dfa
          val res =
                case test m 12 dfa of
                     (NONE, NONE) => "test succeeded"
                   |  _           => "test failed"
      in print "m = "; print(Int.toString m); print ": ";
         print "alphabet is {"; print(SymSet.toString bs); print "}; ";
         print "number of states is "; print(Int.toString n); print "; ";
         print res; print "\n"
      end;