540 case r => r |
540 case r => r |
541 } |
541 } |
542 } |
542 } |
543 |
543 |
544 def distinctWith(rs: List[ARexp], |
544 def distinctWith(rs: List[ARexp], |
545 f: (ARexp, Set[Rexp]) => ARexp, |
545 pruneFunction: (ARexp, Set[Rexp]) => ARexp, |
546 acc: Set[Rexp] = Set()) : List[ARexp] = |
546 acc: Set[Rexp] = Set()) : List[ARexp] = |
547 rs match{ |
547 rs match{ |
548 case Nil => Nil |
548 case Nil => Nil |
549 case r :: rs => |
549 case r :: rs => |
550 if(acc(erase(r))) |
550 if(acc(erase(r))) |
551 distinctWith(rs, f, acc) |
551 distinctWith(rs, pruneFunction, acc) |
552 else { |
552 else { |
553 val pruned_r = f(r, acc) |
553 val pruned_r = pruneFunction(r, acc) |
554 pruned_r :: distinctWith(rs, f, strongBreakIntoTerms(erase(pruned_r)) ++: acc) |
554 pruned_r :: |
|
555 distinctWith(rs, |
|
556 pruneFunction, |
|
557 turnIntoTerms(erase(pruned_r)) ++: acc |
|
558 ) |
555 } |
559 } |
556 } |
560 } |
|
561 |
|
562 // def distinctByPlus(rs: List[ARexp], acc: Set[Rexp] = Set()) : |
|
563 // List[ARexp] = rs match { |
|
564 // case Nil => Nil |
|
565 // case r :: rs => |
|
566 // if(acc.contains(erase(r))) |
|
567 // distinctByPlus(rs, acc) |
|
568 // else |
|
569 // prune(r, acc) :: distinctByPlus(rs, prune(r, acc) +: acc) |
|
570 // } |
557 |
571 |
558 //r = r' ~ tail => returns r' |
572 //r = r' ~ tail => returns r' |
559 def removeSeqTail(r: Rexp, tail: Rexp) : Rexp = r match { |
573 def removeSeqTail(r: Rexp, tail: Rexp) : Rexp = r match { |
560 case SEQ(r1, r2) => |
574 case SEQ(r1, r2) => |
561 if(r2 == tail) |
575 if(r2 == tail) |
803 case CHAR(c) => false |
817 case CHAR(c) => false |
804 case ZERO => false |
818 case ZERO => false |
805 |
819 |
806 } |
820 } |
807 |
821 |
808 def strongBreakIntoTerms(r: Rexp): List[Rexp] = r match { |
822 def turnIntoTerms(r: Rexp): List[Rexp] = r match { |
809 case SEQ(r1, r2) => if(isOne(r1)) |
823 case SEQ(r1, r2) => if(isOne(r1)) |
810 //strongBreakIntoTerms(r1).map(r11 => SEQ(r11, r2)) ::: |
824 turnIntoTerms(r2) |
811 strongBreakIntoTerms(r2) |
|
812 else |
825 else |
813 strongBreakIntoTerms(r1).map(r11 => SEQ(r11, r2)) |
826 turnIntoTerms(r1).map(r11 => SEQ(r11, r2)) |
814 case ALTS(r1, r2) => strongBreakIntoTerms(r1) ::: strongBreakIntoTerms(r2) |
827 case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2) |
815 case ZERO => Nil |
828 case ZERO => Nil |
816 case _ => r :: Nil |
829 case _ => r :: Nil |
817 } |
830 } |
818 |
831 |
819 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = { |
832 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = { |
820 val res = strongBreakIntoTerms((L(erase(r), ctx))).map(oneSimp) |
833 val res = turnIntoTerms((L(erase(r), ctx))).map(oneSimp) |
821 res.toSet |
834 res.toSet |
822 } |
835 } |
823 |
836 |
824 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, subseteqPred: (C, C) => Boolean) : Boolean = { |
837 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, subseteqPred: (C, C) => Boolean) : Boolean = { |
825 subseteqPred(f(a, b), c) |
838 subseteqPred(f(a, b), c) |
866 if(acc.contains(erased)){ |
879 if(acc.contains(erased)){ |
867 distinctBy6(xs, acc) |
880 distinctBy6(xs, acc) |
868 } |
881 } |
869 else{ |
882 else{ |
870 val pruned = prune6(acc, x, Nil) |
883 val pruned = prune6(acc, x, Nil) |
871 val newTerms = strongBreakIntoTerms(erase(pruned)) |
884 val newTerms = turnIntoTerms(erase(pruned)) |
872 pruned match { |
885 pruned match { |
873 case AZERO => |
886 case AZERO => |
874 distinctBy6(xs, acc) |
887 distinctBy6(xs, acc) |
875 case xPrime => |
888 case xPrime => |
876 xPrime :: distinctBy6(xs, newTerms.map(oneSimp) ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc) |
889 xPrime :: distinctBy6(xs, newTerms.map(oneSimp) ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc) |
1199 else ALTS(STAR("a" * d), n_astar_list(d - 1)) |
1212 else ALTS(STAR("a" * d), n_astar_list(d - 1)) |
1200 } |
1213 } |
1201 def n_astar_alts(d: Int) : Rexp = d match { |
1214 def n_astar_alts(d: Int) : Rexp = d match { |
1202 case 0 => n_astar_list(0) |
1215 case 0 => n_astar_list(0) |
1203 case d => STAR(n_astar_list(d)) |
1216 case d => STAR(n_astar_list(d)) |
1204 // case r1 :: r2 :: Nil => ALTS(r1, r2) |
1217 } |
1205 // case r1 :: Nil => r1 |
1218 def n_astar_alts2(d: Int) : Rexp = d match { |
1206 // case r :: rs => ALTS(r, n_astar_alts(rs)) |
1219 case 0 => n_astar_list(0) |
1207 // case Nil => throw new Error("should give at least 1 elem") |
1220 case d => STAR(STAR(n_astar_list(d))) |
1208 } |
1221 } |
1209 def n_astar_aux(d: Int) = { |
1222 def n_astar_aux(d: Int) = { |
1210 if(d == 0) n_astar_alts(0) |
1223 if(d == 0) n_astar_alts(0) |
1211 else ALTS(n_astar_alts(d), n_astar_alts(d - 1)) |
1224 else ALTS(n_astar_alts(d), n_astar_alts(d - 1)) |
1212 } |
1225 } |
1213 |
1226 |
1231 def small() = { |
1244 def small() = { |
1232 //val pderSTAR = pderUNIV(STARREG) |
1245 //val pderSTAR = pderUNIV(STARREG) |
1233 |
1246 |
1234 //val refSize = pderSTAR.map(size(_)).sum |
1247 //val refSize = pderSTAR.map(size(_)).sum |
1235 for(n <- 5 to 5){ |
1248 for(n <- 5 to 5){ |
1236 val STARREG = n_astar(n) |
1249 val STARREG = n_astar_alts2(n) |
1237 val iMax = (lcm((1 to n).toList)) |
1250 val iMax = (lcm((1 to n).toList)) |
1238 for(i <- 1 to iMax + 2){// 100, 400, 800, 840, 841, 900 |
1251 for(i <- 0 to iMax ){// 100, 400, 800, 840, 841, 900 |
1239 val prog0 = "a" * i |
1252 val prog0 = "a" * i |
1240 //println(s"test: $prog0") |
1253 //println(s"test: $prog0") |
1241 print(i) |
1254 print(i) |
1242 print(" ") |
1255 print(" ") |
1243 // print(i) |
1256 // print(i) |
1244 // print(" ") |
1257 // print(" ") |
1245 println(asize(bders_simp(prog0.toList, internalise(STARREG)))) |
1258 println(asize(bders_simp(prog0.toList, internalise(STARREG)))) |
1246 } |
1259 // println(asize(bdersStrong7(prog0.toList, internalise(STARREG)))) |
1247 } |
1260 } |
1248 } |
1261 } |
1249 |
1262 } |
|
1263 small() |
1250 def generator_test() { |
1264 def generator_test() { |
1251 |
1265 |
1252 test(rexp(4), 1000000) { (r: Rexp) => |
1266 test(rexp(4), 1000000) { (r: Rexp) => |
1253 // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => |
1267 // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => |
1254 val ss = Set("b")//stringsFromRexp(r) |
1268 val ss = Set("b")//stringsFromRexp(r) |
1255 val boolList = ss.filter(s => s != "").map(s => { |
1269 val boolList = ss.filter(s => s != "").map(s => { |
1256 //val bdStrong = bdersStrong(s.toList, internalise(r)) |
1270 //val bdStrong = bdersStrong(s.toList, internalise(r)) |
1257 val bdStrong6 = bdersStrong7(s.toList, internalise(r)) |
1271 val bdStrong6 = bdersStrong7(s.toList, internalise(r)) |
1258 val bdStrong6Set = strongBreakIntoTerms(erase(bdStrong6)) |
1272 val bdStrong6Set = turnIntoTerms(erase(bdStrong6)) |
1259 val pdersSet = pderUNIV(r)//.flatMap(r => strongBreakIntoTerms(r)) |
1273 val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r)) |
1260 val pdersSetBroken = pdersSet.flatMap(r => strongBreakIntoTerms(r)) |
1274 val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r)) |
1261 bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size |
1275 bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size |
1262 }) |
1276 }) |
1263 //println(boolList) |
1277 //println(boolList) |
1264 //!boolList.exists(b => b == false) |
1278 //!boolList.exists(b => b == false) |
1265 !boolList.exists(b => b == false) |
1279 !boolList.exists(b => b == false) |
1278 val r = SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))), |
1292 val r = SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))), |
1279 ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b'))) |
1293 ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b'))) |
1280 val s = "b" |
1294 val s = "b" |
1281 val bdStrong5 = bdersStrong7(s.toList, internalise(r)) |
1295 val bdStrong5 = bdersStrong7(s.toList, internalise(r)) |
1282 val bdStrong5Set = breakIntoTerms(erase(bdStrong5)) |
1296 val bdStrong5Set = breakIntoTerms(erase(bdStrong5)) |
1283 val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => strongBreakIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r)) |
1297 val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r)) |
1284 println("original regex ") |
1298 println("original regex ") |
1285 rprint(r) |
1299 rprint(r) |
1286 println("after strong bsimp") |
1300 println("after strong bsimp") |
1287 aprint(bdStrong5) |
1301 aprint(bdStrong5) |
1288 println("turned into a set %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ") |
1302 println("turned into a set %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ") |
1289 rsprint(bdStrong5Set) |
1303 rsprint(bdStrong5Set) |
1290 println("after pderUNIV") |
1304 println("after pderUNIV") |
1291 rsprint(pdersSet.toList) |
1305 rsprint(pdersSet.toList) |
1292 |
1306 |
1293 } |
1307 } |
1294 counterexample_check() |
1308 // counterexample_check() |
1295 |
1309 |
1296 def linform_test() { |
1310 def linform_test() { |
1297 val r = STAR(SEQ(STAR(CHAR('c')),ONE))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE))) // |
1311 val r = STAR(SEQ(STAR(CHAR('c')),ONE))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE))) // |
1298 val r_linforms = lf(r) |
1312 val r_linforms = lf(r) |
1299 println(r_linforms.size) |
1313 println(r_linforms.size) |