439 case r => r |
439 case r => r |
440 } |
440 } |
441 def correctness_proof_convenient_path(){ |
441 def correctness_proof_convenient_path(){ |
442 for(i <- 1 to 10000) |
442 for(i <- 1 to 10000) |
443 { |
443 { |
444 val s = rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3) |
444 val s = "abab"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3) |
445 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) |
445 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) |
446 for(j <- 0 to s.length - 1){ |
446 for(j <- 0 to s.length - 1){ |
447 val ss = s.slice(0, j+ 1) |
447 val ss = s.slice(0, j+ 1) |
448 val nangao = ders_simp(r, ss.toList) |
448 val nangao = ders_simp(r, ss.toList) |
449 val easy = bsimp(bders(ss.toList, r)) |
449 val easy = bsimp(bders(ss.toList, r)) |
450 if(!(nangao == easy || pushbits(nangao) == (easy))){ |
450 if(!(nangao == easy || pushbits(nangao) == (easy))){ |
488 println("frect v = ") |
488 println("frect v = ") |
489 println(frectv) |
489 println(frectv) |
490 } |
490 } |
491 */ |
491 */ |
492 def retrieve_experience(){ |
492 def retrieve_experience(){ |
493 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")))) |
493 for(i <- 1 to 100){ |
494 val st = "abaab" |
494 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")))) |
495 val r_der_s = ders(st.toList, erase(rg)) |
495 val st = "ab"//"abaab" |
496 val unsimplified_vl = mkeps(r_der_s) |
496 val r_der_s = ders(st.toList, erase(rg)) |
497 val r_bder_s = bders( st.toList, rg) |
497 if(nullable(r_der_s)){ |
498 val s_r_bder_s = bsimp(r_bder_s) |
498 val unsimplified_vl = mkeps(r_der_s) |
499 val bits1 = retrieve(r_bder_s, unsimplified_vl) |
499 val r_bder_s = bders( st.toList, rg) |
500 println(r_bder_s) |
500 val s_r_bder_s = bsimp(r_bder_s) |
501 println(erase(r_bder_s)) |
501 val bits1 = retrieve(internalise(r_der_s), unsimplified_vl) |
502 println(s_r_bder_s) |
502 println("The property: ") |
503 println(erase(s_r_bder_s)) |
503 println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r") |
504 println(code(unsimplified_vl)) |
504 println("does not hold.") |
505 val bits2 = retrieve(s_r_bder_s, decode(erase(s_r_bder_s), code(unsimplified_vl))) |
505 println("Here v == mkeps r\\s and r == r\\s") |
506 if(bits1 == bits2){ |
506 println("regular expression is") |
507 println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r") |
507 println(rg) |
508 println("Here v == mkeps r\\s and r == r\\s") |
508 println("string is") |
509 println(r_der_s, unsimplified_vl) |
509 println(st) |
510 println(s_r_bder_s, erase(s_r_bder_s), code(unsimplified_vl)) |
510 println("derivative without simplification is ") |
511 } |
511 |
512 } |
512 println(r_bder_s) |
|
513 |
|
514 println("after erase of this derivative") |
|
515 println(erase(r_bder_s)) |
|
516 println("simplification of derivative (bsimp(ar))") |
|
517 println(s_r_bder_s) |
|
518 println("after erase of simplified derivative (erase(bsimp(ar))") |
|
519 println(erase(s_r_bder_s)) |
|
520 println("decode says the above regex and the below bits(code(v)) are not decodable") |
|
521 println(unsimplified_vl) |
|
522 println(code(unsimplified_vl)) |
|
523 println(bits1) |
|
524 val bits2 = retrieve(s_r_bder_s, decode(erase(s_r_bder_s), code(unsimplified_vl))) |
|
525 if(bits1 == bits2){ |
|
526 println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r") |
|
527 println("Here v == mkeps r\\s and r == r\\s") |
|
528 println(r_der_s, unsimplified_vl) |
|
529 println(s_r_bder_s, erase(s_r_bder_s), code(unsimplified_vl)) |
|
530 } |
|
531 } |
|
532 } |
|
533 } |
513 def radical_correctness(){ |
534 def radical_correctness(){ |
514 enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet |
535 enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet |
515 random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet |
536 random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet |
|
537 } |
|
538 def christian_def(){ |
|
539 val r = ALTS(List(SEQ(ZERO,CHAR('b')), ONE)) |
|
540 val v = Right(Empty) |
|
541 val a = internalise(r) |
|
542 val as = bsimp(a) |
|
543 println(s"Testing ${r} and ${v}") |
|
544 println(s"internalise(r) = ${a}") |
|
545 val bs1 = retrieve(a, v) |
|
546 println(bs1) |
|
547 println(s"as = ${as}") |
|
548 //val bs2 = retrieve(as, decode(erase(as), bs1)) |
|
549 val bs3 = retrieve(as, decode(erase(as), bs1.tail)) |
|
550 println(decode(erase(as), bs1.tail)) |
|
551 println(bs3) |
|
552 } |
|
553 def essence_posix(){ |
|
554 val s = "abab"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3) |
|
555 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) |
|
556 ders(s.toList, r) |
516 } |
557 } |
517 def main(args: Array[String]) { |
558 def main(args: Array[String]) { |
518 //check_all() |
559 //check_all() |
519 //radical_correctness() |
560 //radical_correctness() |
520 //correctness_proof_convenient_path() |
561 //correctness_proof_convenient_path() |
521 retrieve_experience() |
562 //retrieve_experience() |
|
563 christian_def() |
522 } |
564 } |
523 } |
565 } |
524 |
566 |