490 case (r1s, r2s) => ASEQ(bs1, r1s, r2s) |
490 case (r1s, r2s) => ASEQ(bs1, r1s, r2s) |
491 } |
491 } |
492 case AALTS(bs1, rs) => { |
492 case AALTS(bs1, rs) => { |
493 // println("alts case") |
493 // println("alts case") |
494 val rs_simp = rs.map(strongBsimp5(_)) |
494 val rs_simp = rs.map(strongBsimp5(_)) |
495 |
|
496 val flat_res = flats(rs_simp) |
495 val flat_res = flats(rs_simp) |
497 |
496 var dist_res = distinctBy5(flat_res)//distinctBy(flat_res, erase) |
498 val dist_res = distinctBy5(flat_res)//distinctBy(flat_res, erase) |
497 var dist2_res = distinctBy5(dist_res) |
499 |
498 while(dist_res != dist2_res){ |
500 dist_res match { |
499 dist_res = dist2_res |
|
500 dist2_res = distinctBy5(dist_res) |
|
501 } |
|
502 (dist2_res) match { |
501 case Nil => AZERO |
503 case Nil => AZERO |
502 case s :: Nil => fuse(bs1, s) |
504 case s :: Nil => fuse(bs1, s) |
503 case rs => AALTS(bs1, rs) |
505 case rs => AALTS(bs1, rs) |
504 } |
506 } |
505 |
|
506 } |
507 } |
507 case r => r |
508 case r => r |
508 } |
509 } |
509 } |
510 } |
510 |
511 |
602 |
603 |
603 //the "fake" Language interpretation: just concatenates! |
604 //the "fake" Language interpretation: just concatenates! |
604 def L(acc: Rexp, rs: List[Rexp]) : Rexp = rs match { |
605 def L(acc: Rexp, rs: List[Rexp]) : Rexp = rs match { |
605 case Nil => acc |
606 case Nil => acc |
606 case r :: rs1 => |
607 case r :: rs1 => |
607 if(acc == ONE) |
608 // if(acc == ONE) |
608 L(r, rs1) |
609 // L(r, rs1) |
609 else |
610 // else |
610 L(SEQ(acc, r), rs1) |
611 L(SEQ(acc, r), rs1) |
611 } |
612 } |
612 |
613 |
613 def pAKC(rs: List[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = { |
614 def rprint(r: Rexp) : Unit = println(shortRexpOutput(r)) |
614 if (breakIntoTerms(L(erase(r), ctx)).map(oneSimp).forall(rs.contains)) {//rs.flatMap(breakIntoTerms |
615 def rsprint(rs: List[Rexp]) = rs.foreach(r => println(shortRexpOutput(r))) |
|
616 def aprint(a: ARexp) = println(shortRexpOutput(erase(a))) |
|
617 def asprint(as: List[ARexp]) = as.foreach(a => println(shortRexpOutput(erase(a)))) |
|
618 |
|
619 def pAKC(acc: List[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = { |
|
620 // println("pakc") |
|
621 // println(shortRexpOutput(erase(r))) |
|
622 // println("acc") |
|
623 // rsprint(acc) |
|
624 // println("ctx---------") |
|
625 // rsprint(ctx) |
|
626 // println("ctx---------end") |
|
627 // rsprint(breakIntoTerms(L(erase(r), ctx)).map(oneSimp)) |
|
628 |
|
629 if (breakIntoTerms(L(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms |
615 AZERO |
630 AZERO |
616 } |
631 } |
617 else{ |
632 else{ |
618 r match { |
633 r match { |
619 case ASEQ(bs, r1, r2) => |
634 case ASEQ(bs, r1, r2) => |
620 (pAKC(rs, r1, erase(r2) :: ctx)) match{ |
635 (pAKC(acc, r1, erase(r2) :: ctx)) match{ |
621 case AZERO => |
636 case AZERO => |
622 AZERO |
637 AZERO |
623 case AONE(bs1) => |
638 case AONE(bs1) => |
624 fuse(bs1, r2) |
639 fuse(bs1, r2) |
625 case r1p => |
640 case r1p => |
629 // println("before pruning") |
644 // println("before pruning") |
630 // println(s"ctx is ") |
645 // println(s"ctx is ") |
631 // ctx.foreach(r => println(shortRexpOutput(r))) |
646 // ctx.foreach(r => println(shortRexpOutput(r))) |
632 // println(s"rs0 is ") |
647 // println(s"rs0 is ") |
633 // rs0.foreach(r => println(shortRexpOutput(erase(r)))) |
648 // rs0.foreach(r => println(shortRexpOutput(erase(r)))) |
634 // println(s"rs is ") |
649 // println(s"acc is ") |
635 // rs.foreach(r => println(shortRexpOutput(r))) |
650 // acc.foreach(r => println(shortRexpOutput(r))) |
636 rs0.map(r => pAKC(rs, r, ctx)).filter(_ != AZERO) match { |
651 rs0.map(r => pAKC(acc, r, ctx)).filter(_ != AZERO) match { |
637 case Nil => |
652 case Nil => |
638 // println("after pruning Nil") |
653 // println("after pruning Nil") |
639 AZERO |
654 AZERO |
640 case r :: Nil => |
655 case r :: Nil => |
641 // println("after pruning singleton") |
656 // println("after pruning singleton") |
1089 // } |
1104 // } |
1090 // asize(bdStrong5) <= asize(bdStrong) |
1105 // asize(bdStrong5) <= asize(bdStrong) |
1091 // }) |
1106 // }) |
1092 // !boolList.exists(b => b == false) |
1107 // !boolList.exists(b => b == false) |
1093 // } |
1108 // } |
1094 //test(rexp(3), 10000000) { (r: Rexp) => |
1109 //*** example where bdStrong5 has a smaller size than bdStrong |
1095 test(single(STAR(SEQ(SEQ(ALTS(CHAR('b'),STAR(CHAR('b'))),CHAR('b')),ALTS(ALTS(STAR(CHAR('c')),SEQ(CHAR('a'),CHAR('c'))),ALTS(ZERO,ONE))))), 1) {(r: Rexp) => |
1110 // test(single(STAR(SEQ(ALTS(SEQ(STAR(CHAR('a')),ALTS(ALTS(ONE,ZERO),SEQ(ONE,ONE))),CHAR('a')),ONE))), 1) { (r: Rexp) => |
|
1111 //*** depth 5 example bdStrong5 larger size than bdStrong |
|
1112 // test(single(STAR(SEQ(SEQ(ALTS(CHAR('b'),STAR(CHAR('b'))),CHAR('b')),(ALTS(STAR(CHAR('c')), ONE))))), 1) {(r: Rexp) => |
|
1113 |
|
1114 |
|
1115 |
|
1116 //sanity check from Christian's request |
|
1117 // val r = ("a" | "ab") ~ ("bc" | "c") |
|
1118 // val a = internalise(r) |
|
1119 // val aval = blexing_simp(r, "abc") |
|
1120 // println(aval) |
|
1121 |
|
1122 //sample counterexample:(depth 7) |
|
1123 //STAR(SEQ(ALTS(STAR(STAR(STAR(STAR(CHAR(c))))),ALTS(CHAR(c),CHAR(b))),ALTS(ZERO,SEQ(ALTS(ALTS(STAR(CHAR(c)),SEQ(CHAR(b),CHAR(a))),CHAR(c)),STAR(ALTS(ALTS(ONE,CHAR(a)),STAR(CHAR(c)))))))) |
|
1124 //(depth5) |
|
1125 //STAR(SEQ(ALTS(ALTS(STAR(CHAR(b)),SEQ(ONE,CHAR(b))),SEQ(STAR(CHAR(a)),CHAR(b))),ALTS(ZERO,ALTS(STAR(CHAR(b)),STAR(CHAR(a)))))) |
|
1126 test(rexp(4), 10000000) { (r: Rexp) => |
|
1127 // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => |
1096 val ss = stringsFromRexp(r) |
1128 val ss = stringsFromRexp(r) |
1097 val boolList = ss.map(s => { |
1129 val boolList = ss.map(s => { |
1098 val bdStrong = bdersStrong(s.toList, internalise(r)) |
1130 val bdStrong = bdersStrong(s.toList, internalise(r)) |
1099 val bdStrong5 = bdersStrong5(s.toList, internalise(r)) |
1131 val bdStrong5 = bdersStrong5(s.toList, internalise(r)) |
|
1132 val bdFurther5 = strongBsimp5(bdStrong5) |
|
1133 val sizeFurther5 = asize(bdFurther5) |
|
1134 val pdersSet = pderUNIV(r) |
1100 val size5 = asize(bdStrong5) |
1135 val size5 = asize(bdStrong5) |
1101 val size0 = asize(bdStrong) |
1136 val size0 = asize(bdStrong) |
1102 println(s) |
|
1103 println(shortRexpOutput(erase(bdStrong5))) |
|
1104 println(shortRexpOutput(erase(bdStrong))) |
|
1105 println(size5, size0) |
|
1106 // println(s) |
1137 // println(s) |
1107 size5 <= size0 |
1138 // println("pdersSet size") |
|
1139 // println(pdersSet.size) |
|
1140 // pdersSet.foreach(r => println(shortRexpOutput(r))) |
|
1141 // println("after bdStrong5") |
|
1142 |
|
1143 // println(shortRexpOutput(erase(bdStrong5))) |
|
1144 // println(breakIntoTerms(erase(bdStrong5)).size) |
|
1145 |
|
1146 // println("after bdStrong") |
|
1147 // println(shortRexpOutput(erase(bdStrong))) |
|
1148 // println(breakIntoTerms(erase(bdStrong)).size) |
|
1149 // println(size5, size0, sizeFurther5) |
|
1150 // aprint(strongBsimp5(bdStrong)) |
|
1151 // println(asize(strongBsimp5(bdStrong5))) |
|
1152 // println(s) |
|
1153 size5 <= size0 |
1108 }) |
1154 }) |
1109 // println(boolList) |
1155 // println(boolList) |
|
1156 //!boolList.exists(b => b == false) |
1110 !boolList.exists(b => b == false) |
1157 !boolList.exists(b => b == false) |
1111 } |
1158 } |
1112 |
1159 |
1113 |
1160 |
1114 } |
1161 } |