diff -r 61eff2abb0b6 -r 1481f465e6ea thys2/blexer2.sc
--- a/thys2/blexer2.sc	Tue Apr 19 09:08:01 2022 +0100
+++ b/thys2/blexer2.sc	Thu Apr 21 14:58:51 2022 +0100
@@ -137,7 +137,7 @@
   if(len <= 0) single(Nil)
   else{
     for { 
-      c <- chars
+      c <- chars_range('a', 'd')
       tail <- char_list(len - 1)
     } yield c :: tail
   }
@@ -145,6 +145,19 @@
 
 def strings(len: Int): Generator[String] = for(cs <- char_list(len)) yield cs.toString
 
+def sampleString(r: Rexp) : List[String] = r match {
+  case STAR(r) => stringsFromRexp(r).flatMap(s => List("", s, s ++ s))//only generate 0, 1, 2 reptitions
+  case SEQ(r1, r2) => stringsFromRexp(r1).flatMap(s1 => stringsFromRexp(r2).map(s2 => s1 ++ s2) )
+  case ALTS(r1, r2) => throw new Error(s" Rexp ${r} not expected: all alternatives are supposed to have been opened up")
+  case ONE => "" :: Nil
+  case ZERO => Nil
+  case CHAR(c) => c.toString :: Nil
+
+}
+
+def stringsFromRexp(r: Rexp) : List[String] = 
+  breakIntoTerms(r).flatMap(r => sampleString(r))
+
 
 // (simple) binary trees
 trait Tree[T]
@@ -682,7 +695,6 @@
   def blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
       case Nil => {
         if (bnullable(r)) {
-          //println(asize(r))
           val bits = mkepsBC(r)
           bits
         }
@@ -923,11 +935,51 @@
   // test(rexp(10), 1000) { r => height(r) <= size(r) }
   // println("XXX faulty test")
   // test(rexp(10), 100) { r => height(r) <= size_faulty(r) }
-  println("testing strongbsimp against bsimp")
-  test2(rexp(10), strings(2), 100) { (r : Rexp, s: String) => 
-    (simpBlexer(r, s) == strongBlexer(r, s)) 
+
+
+  /* For inspection of counterexamples should they arise*/
+//   println("testing strongbsimp against bsimp")
+//   val r = SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))),
+// SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))),
+// STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))),
+// SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE))
+
+//     val ss = stringsFromRexp(r)
+//     val boolList = ss.map(s => {
+//       val simpVal = simpBlexer(r, s)
+//       val strongVal = strongBlexer(r, s)
+//       println(simpVal)
+//       println(strongVal)
+//       (simpVal == strongVal) && (simpVal != None) 
+//     })
+//     println(boolList)
+//     println(boolList.exists(b => b == false))
+
+
+  test(rexp(9), 100000) { (r: Rexp) => 
+    val ss = stringsFromRexp(r)
+    val boolList = ss.map(s => {
+      val simpVal = simpBlexer(r, s)
+      val strongVal = strongBlexer(r, s)
+      // println(simpVal)
+      // println(strongVal)
+      (simpVal == strongVal) && (simpVal != None) 
+    })
+    !boolList.exists(b => b == false)
   }
-  
+
+
 }
 // small()
 generator_test()
+
+1
+
+SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))),
+SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))),
+STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))),
+SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE))
+
+
+// Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
+// Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
\ No newline at end of file