--- a/Spiral.scala	Sat Apr 13 16:18:23 2019 +0100
+++ b/Spiral.scala	Sun May 05 22:02:29 2019 +0100
@@ -441,8 +441,8 @@
   def correctness_proof_convenient_path(){
     for(i <- 1 to 10000)
     {
-        val s = rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
-        val r = internalise(random_struct_gen(4))//ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
+        val s = "abab"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
+        val r = ("ab"| SEQ(ONE, "ab"))//internalise(random_struct_gen(4))//ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
         for(j <- 0 to s.length - 1){
           val ss = s.slice(0, j+ 1)
           val nangao = ders_simp(r, ss.toList)
@@ -490,35 +490,77 @@
     }
     */
   def retrieve_experience(){
-    val rg = ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) 
-    val st = "abaab"
-    val r_der_s = ders(st.toList, erase(rg))
-    val unsimplified_vl = mkeps(r_der_s)
-    val r_bder_s = bders( st.toList, rg)
-    val s_r_bder_s = bsimp(r_bder_s)
-    val bits1 = retrieve(r_bder_s, unsimplified_vl)
-    println(r_bder_s)
-    println(erase(r_bder_s))
-    println(s_r_bder_s)
-    println(erase(s_r_bder_s))
-    println(code(unsimplified_vl))
-    val bits2 = retrieve(s_r_bder_s, decode(erase(s_r_bder_s), code(unsimplified_vl)))
-    if(bits1 == bits2){
-      println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r")
-      println("Here v == mkeps r\\s and r == r\\s")
-      println(r_der_s, unsimplified_vl)
-      println(s_r_bder_s, erase(s_r_bder_s), code(unsimplified_vl))
+    for(i <- 1 to 100){
+      val rg = internalise(balanced_struct_gen(1))//ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) 
+      val st = "ab"//"abaab"
+      val r_der_s = ders(st.toList, erase(rg))
+      if(nullable(r_der_s)){
+        val unsimplified_vl = mkeps(r_der_s)
+        val r_bder_s = bders( st.toList, rg)
+        val s_r_bder_s = bsimp(r_bder_s)
+        val bits1 = retrieve(internalise(r_der_s), unsimplified_vl)
+        println("The property: ")
+        println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r")
+        println("does not hold.")
+        println("Here v == mkeps r\\s and r == r\\s")
+        println("regular expression is")
+        println(rg)
+        println("string is")
+        println(st)
+        println("derivative without simplification is ")
+        
+        println(r_bder_s)
+
+        println("after erase of this derivative")
+        println(erase(r_bder_s))
+        println("simplification of derivative (bsimp(ar))")
+        println(s_r_bder_s)
+        println("after erase of simplified derivative (erase(bsimp(ar))")
+        println(erase(s_r_bder_s))
+        println("decode says the above regex and the below bits(code(v)) are not decodable")
+        println(unsimplified_vl)
+        println(code(unsimplified_vl))
+        println(bits1)
+        val bits2 = retrieve(s_r_bder_s, decode(erase(s_r_bder_s), code(unsimplified_vl)))
+          if(bits1 == bits2){
+            println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r")
+            println("Here v == mkeps r\\s and r == r\\s")
+            println(r_der_s, unsimplified_vl)
+            println(s_r_bder_s, erase(s_r_bder_s), code(unsimplified_vl))
+          }
+        }
+      }
     }
-  }
   def radical_correctness(){
     enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet
     random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet
   }
+  def christian_def(){
+    val r = ALTS(List(SEQ(ZERO,CHAR('b')), ONE))
+    val v = Right(Empty)
+    val a = internalise(r)
+    val as = bsimp(a)
+    println(s"Testing ${r} and ${v}")
+    println(s"internalise(r) = ${a}")
+    val bs1 = retrieve(a, v)
+    println(bs1)
+    println(s"as = ${as}")
+    //val bs2 = retrieve(as, decode(erase(as), bs1))
+    val bs3 = retrieve(as, decode(erase(as), bs1.tail))
+    println(decode(erase(as), bs1.tail))
+    println(bs3)
+  }
+  def essence_posix(){
+    val s = "abab"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
+    val r = STAR("ab"| SEQ(ONE, "ab"))//internalise(random_struct_gen(4))//ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
+    ders(s.toList, r)
+  }
   def main(args: Array[String]) {
     //check_all()   
     //radical_correctness()
     //correctness_proof_convenient_path()
-    retrieve_experience()
+    //retrieve_experience()
+    christian_def()
   } 
 }