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