| changeset 11 | 9c1ca6d6e190 |
| parent 10 | 2b95bcd2ac73 |
| child 12 | 768b833d6230 |
| 10:2b95bcd2ac73 | 11:9c1ca6d6e190 |
|---|---|
432 weak_sub_check(big_panda, str_panda, 6, size_expansion_rate) |
432 weak_sub_check(big_panda, str_panda, 6, size_expansion_rate) |
433 |
433 |
434 } |
434 } |
435 //simplified regex size 291, so called pd_simp size 70 (did not do simplification to terms in the PD set) |
435 //simplified regex size 291, so called pd_simp size 70 (did not do simplification to terms in the PD set) |
436 def pushbits(r: ARexp): ARexp = r match { |
436 def pushbits(r: ARexp): ARexp = r match { |
437 case AALTS(bs, rs) => AALTS(Nil, rs.map(fuse(bs, _))) |
437 case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r)))) |
438 case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2)) |
|
438 case r => r |
439 case r => r |
439 } |
440 } |
440 def correctness_proof_convenient_path(){ |
441 def correctness_proof_convenient_path(){ |
441 for(i <- 1 to 1) |
442 for(i <- 1 to 10000) |
442 { |
443 { |
443 val s = "baa"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3) |
444 val s = rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3) |
444 val r = ASTAR(List(),ASEQ(List(),AALTS(List(),List(ACHAR(List(Z),'c'), ACHAR(List(S),'b'))),ASEQ(List(),ASTAR(List(),ACHAR(List(),'a')),AALTS(List(),List(ACHAR(List(Z),'a'), ACHAR(List(S),'a'))))))//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 = 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 for(j <- 0 to s.length - 1){ |
446 for(j <- 0 to s.length - 1){ |
446 val ss = s.slice(0, j+ 1) |
447 val ss = s.slice(0, j+ 1) |
447 val nangao = ders_simp(r, ss.toList) |
448 val nangao = ders_simp(r, ss.toList) |
448 val easy = bsimp(bders(ss.toList, r)) |
449 val easy = bsimp(bders(ss.toList, r)) |
449 if(!(nangao == easy || pushbits(nangao) == (easy))){ |
450 if(!(nangao == easy || pushbits(nangao) == (easy))){ |
461 println(annotated_tree(easy)) |
462 println(annotated_tree(easy)) |
462 } |
463 } |
463 } |
464 } |
464 } |
465 } |
465 } |
466 } |
467 def retrieve_experience(){ |
|
468 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")))) |
|
469 val st = "abaab" |
|
470 val vl = blexing_simp(erase(rg), st) |
|
471 val bts = retrieve(rg, vl) |
|
472 val cdbts = code(vl) |
|
473 if(bts != cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r |
|
474 println(bts) |
|
475 println(cdbts) |
|
476 println("NOoooooo.....!") |
|
477 } |
|
478 } |
|
466 def radical_correctness(){ |
479 def radical_correctness(){ |
467 enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet |
480 enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet |
468 random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet |
481 random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet |
469 } |
482 } |
470 def main(args: Array[String]) { |
483 def main(args: Array[String]) { |
471 //check_all() |
484 //check_all() |
472 //radical_correctness() |
485 //radical_correctness() |
473 correctness_proof_convenient_path() |
486 //correctness_proof_convenient_path() |
487 retrieve_experience() |
|
474 } |
488 } |
475 } |
489 } |
476 |
490 |