519 r match { |
519 r match { |
520 case ASEQ(bs1, r1, r2) => (strongBsimp6(r1), strongBsimp6(r2)) match { |
520 case ASEQ(bs1, r1, r2) => (strongBsimp6(r1), strongBsimp6(r2)) match { |
521 case (AZERO, _) => AZERO |
521 case (AZERO, _) => AZERO |
522 case (_, AZERO) => AZERO |
522 case (_, AZERO) => AZERO |
523 case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s) |
523 case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s) |
|
524 case (r1s, AONE(bs2)) => fuse(bs1, r1s) //asserted bs2 == Nil |
524 case (r1s, r2s) => ASEQ(bs1, r1s, r2s) |
525 case (r1s, r2s) => ASEQ(bs1, r1s, r2s) |
525 } |
526 } |
526 case AALTS(bs1, rs) => { |
527 case AALTS(bs1, rs) => { |
527 // println("alts case") |
528 // println("alts case") |
528 val rs_simp = rs.map(strongBsimp6(_)) |
529 val rs_simp = rs.map(strongBsimp6(_)) |
730 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = { |
731 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = { |
731 val res = strongBreakIntoTerms((L(erase(r), ctx))).map(oneSimp) |
732 val res = strongBreakIntoTerms((L(erase(r), ctx))).map(oneSimp) |
732 res.toSet |
733 res.toSet |
733 } |
734 } |
734 |
735 |
735 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, inclusionPred: (C, C) => Boolean) : Boolean = { |
736 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, subseteqPred: (C, C) => Boolean) : Boolean = { |
736 |
737 |
737 inclusionPred(f(a, b), c) |
738 subseteqPred(f(a, b), c) |
738 } |
739 } |
739 def rexpListInclusion(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = { |
740 def rexpListInclusion(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = { |
740 // println("r+ctx---------") |
741 // println("r+ctx---------") |
741 // rsprint(rs1) |
742 // rsprint(rs1) |
742 // println("acc---------") |
743 // println("acc---------") |
745 val res = rs1.forall(rs2.contains) |
746 val res = rs1.forall(rs2.contains) |
746 // println(res) |
747 // println(res) |
747 // println("end------------------") |
748 // println("end------------------") |
748 res |
749 res |
749 } |
750 } |
750 def pAKC6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = { |
751 def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = { |
751 // println("pakc--------r") |
752 // println("pakc--------r") |
752 // println(shortRexpOutput(erase(r))) |
753 // println(shortRexpOutput(erase(r))) |
753 // println("ctx---------") |
754 // println("ctx---------") |
754 // rsprint(ctx) |
755 // rsprint(ctx) |
755 // println("pakc-------acc") |
756 // println("pakc-------acc") |
780 // ctx.foreach(r => println(shortRexpOutput(r))) |
781 // ctx.foreach(r => println(shortRexpOutput(r))) |
781 // println(s"rs0 is ") |
782 // println(s"rs0 is ") |
782 // rs0.foreach(r => println(shortRexpOutput(erase(r)))) |
783 // rs0.foreach(r => println(shortRexpOutput(erase(r)))) |
783 // println(s"acc is ") |
784 // println(s"acc is ") |
784 // acc.foreach(r => println(shortRexpOutput(r))) |
785 // acc.foreach(r => println(shortRexpOutput(r))) |
785 rs0.map(r => pAKC6(acc, r, ctx)).filter(_ != AZERO) match { |
786 rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match { |
786 case Nil => |
787 case Nil => |
787 // println("after pruning Nil") |
788 // println("after pruning Nil") |
788 AZERO |
789 AZERO |
789 case r :: Nil => |
790 case r :: Nil => |
790 // println("after pruning singleton") |
791 // println("after pruning singleton") |
807 val erased = erase(x) |
808 val erased = erase(x) |
808 if(acc.contains(erased)){ |
809 if(acc.contains(erased)){ |
809 distinctBy6(xs, acc) |
810 distinctBy6(xs, acc) |
810 } |
811 } |
811 else{ |
812 else{ |
812 val pruned = pAKC6(acc, x, Nil) |
813 val pruned = prune6(acc, x, Nil) |
813 val newTerms = strongBreakIntoTerms(erase(pruned)) |
814 val newTerms = strongBreakIntoTerms(erase(pruned)) |
814 pruned match { |
815 pruned match { |
815 case AZERO => |
816 case AZERO => |
816 distinctBy6(xs, acc) |
817 distinctBy6(xs, acc) |
817 case xPrime => |
818 case xPrime => |
1234 |
1235 |
1235 //sample counterexample:(depth 7) |
1236 //sample counterexample:(depth 7) |
1236 //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)))))))) |
1237 //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)))))))) |
1237 //(depth5) |
1238 //(depth5) |
1238 //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)))))) |
1239 //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)))))) |
1239 test(rexp(4), 100000) { (r: Rexp) => |
1240 test(rexp(8), 10000) { (r: Rexp) => |
1240 // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => |
1241 // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => |
1241 val ss = stringsFromRexp(r) |
1242 val ss = stringsFromRexp(r) |
1242 val boolList = ss.filter(s => s != "").map(s => { |
1243 val boolList = ss.filter(s => s != "").map(s => { |
1243 //val bdStrong = bdersStrong(s.toList, internalise(r)) |
1244 //val bdStrong = bdersStrong(s.toList, internalise(r)) |
1244 val bdStrong6 = bdersStrong6(s.toList, internalise(r)) |
1245 val bdStrong6 = bdersStrong6(s.toList, internalise(r)) |
1254 } |
1255 } |
1255 |
1256 |
1256 |
1257 |
1257 } |
1258 } |
1258 // small() |
1259 // small() |
1259 // generator_test() |
1260 generator_test() |
1260 |
1261 |
1261 def counterexample_check() { |
1262 def counterexample_check() { |
1262 val r = SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE)))//STAR(SEQ(ALTS(STAR(CHAR('c')),CHAR('c')),SEQ(ALTS(CHAR('c'),ONE),ONE))) |
1263 val r = SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE)))//STAR(SEQ(ALTS(STAR(CHAR('c')),CHAR('c')),SEQ(ALTS(CHAR('c'),ONE),ONE))) |
1263 val s = "ccc" |
1264 val s = "ccc" |
1264 val bdStrong5 = bdersStrong6(s.toList, internalise(r)) |
1265 val bdStrong5 = bdersStrong6(s.toList, internalise(r)) |
1273 println("after pderUNIV") |
1274 println("after pderUNIV") |
1274 rsprint(pdersSet.toList) |
1275 rsprint(pdersSet.toList) |
1275 } |
1276 } |
1276 // counterexample_check() |
1277 // counterexample_check() |
1277 def linform_test() { |
1278 def linform_test() { |
1278 val r = STAR(SEQ(STAR(CHAR('c')), ONE)) |
1279 val r = STAR(SEQ(STAR(CHAR('c')),ONE))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE))) // |
1279 val r_linforms = lf(r) |
1280 val r_linforms = lf(r) |
1280 println(r_linforms.size) |
1281 println(r_linforms.size) |
1281 } |
1282 val pderuniv = pderUNIV(r) |
1282 linform_test() |
1283 println(pderuniv.size) |
|
1284 } |
|
1285 // linform_test() |
1283 // 1 |
1286 // 1 |
1284 def newStrong_test() { |
1287 def newStrong_test() { |
1285 val r2 = (CHAR('b') | ONE) |
1288 val r2 = (CHAR('b') | ONE) |
1286 val r0 = CHAR('d') |
1289 val r0 = CHAR('d') |
1287 val r1 = (ONE | CHAR('c')) |
1290 val r1 = (ONE | CHAR('c')) |