(* written so that the string length upper bound is a parameter; this
generality was not required *)
(* val zeroOne : str set
zeroOne = {0, 1} *)
val zeroOne = StrSet.fromString "0, 1";
(* val unwanted : int -> str set
if n >= 0, then unwanted n returns all length-n elements of {0, 1}*
with an occurrence of either 000/111 *)
fun unwanted n =
if n < 3
then Set.empty
else let (* val bad : str set
bad = {000, 111} *)
val bad = StrSet.fromString "000, 111"
(* val unwant : int -> str set
if 1 <= m <= n - 2, then unwant m is all length n
elements of {0, 1}* with an occurrence of 000/111
beginning at one of the positions 1, ..., m *)
fun unwant 1 = StrSet.concat(bad, StrSet.power(zeroOne, n - 3))
| unwant m =
StrSet.union
(StrSet.concat
(StrSet.power(zeroOne, m - 1),
StrSet.concat(bad,
StrSet.power(zeroOne, n - 3 - (m - 1)))),
unwant(m - 1))
in unwant(n - 2) end;
(* val atMost : int -> str set
if n >= 0, then atMost n returns all elements of {0, 1}* that have
length at most n and have no occurrences of 000/111 *)
fun atMost 0 = StrSet.minus(StrSet.power(zeroOne, 0), unwanted 0)
| atMost n =
StrSet.union(StrSet.minus(StrSet.power(zeroOne, n), unwanted n),
atMost(n - 1));
(* val atMostReg : int -> reg
if n >= 0, then atMostReg n returns a Reg.weakSubset-simplified
regular expression whose meaning is the set of all elements of {0,
1}* that have length at most n and have no occurrences of 000/111 *)
fun atMostReg n = Reg.simplify Reg.weakSubset (Reg.fromStrSet(atMost n));