diff options
author | 2021-01-26 22:04:28 +0100 | |
---|---|---|
committer | 2021-01-26 22:04:28 +0100 | |
commit | 48915afb6bd6bfb7c84533c0d4383c90e65dda33 (patch) | |
tree | b783bdebad102e078dc0975ebd23b5d99d71d2d5 | |
parent | temporary fix for Z3 usage on Linux VM (diff) | |
download | VIATRA-Generator-48915afb6bd6bfb7c84533c0d4383c90e65dda33.tar.gz VIATRA-Generator-48915afb6bd6bfb7c84533c0d4383c90e65dda33.tar.zst VIATRA-Generator-48915afb6bd6bfb7c84533c0d4383c90e65dda33.zip |
Improve crossingScenario queries + small ease-of-use adjustments
3 files changed, 133 insertions, 105 deletions
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index a26782ae..8eabfd05 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql | |||
@@ -90,12 +90,28 @@ pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { | |||
90 | pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { | 90 | pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { |
91 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | 91 | find helper_vert_getYAndBounds(cs, a, yMax, yP); |
92 | check(yP <= 0-yMax);} | 92 | check(yP <= 0-yMax);} |
93 | |||
94 | //Minimum Distances | ||
95 | private pattern helper_getCoords(a1:Actor, | ||
96 | a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | ||
97 | Actor.xPos(a1, x1); | ||
98 | Actor.yPos(a1, y1); | ||
99 | Actor.xPos(a2, x2); | ||
100 | Actor.yPos(a2, y2); | ||
101 | } | ||
102 | |||
103 | //INFO may remove? | ||
104 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
105 | pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { | ||
106 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
107 | a1 != a2; | ||
108 | //check(dx^2 + dy^2 < 5^2) | ||
109 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); | ||
110 | } | ||
93 | 111 | ||
94 | /////---------------- | 112 | /////---------------- |
95 | //Xspeed and Yspeed bounds | 113 | //Xspeed and Yspeed bounds |
96 | /////---------------- | 114 | /////---------------- |
97 | |||
98 | //TODO THIS IS HARD_CODED | ||
99 | 115 | ||
100 | /////////VERTICAL LANE | 116 | /////////VERTICAL LANE |
101 | @Constraint(severity="error", key={a}, message="7 Actor") | 117 | @Constraint(severity="error", key={a}, message="7 Actor") |
@@ -103,7 +119,7 @@ pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { | |||
103 | Actor.placedOn(a, vl); | 119 | Actor.placedOn(a, vl); |
104 | Lane_Vertical(vl); | 120 | Lane_Vertical(vl); |
105 | Actor.xSpeed(a, xSpeed); | 121 | Actor.xSpeed(a, xSpeed); |
106 | check(xSpeed != 0); | 122 | check(xSpeed != 0.0); |
107 | } | 123 | } |
108 | 124 | ||
109 | private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, | 125 | private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, |
@@ -118,7 +134,7 @@ private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, | |||
118 | @Constraint(severity="error", key={cs}, message="x") | 134 | @Constraint(severity="error", key={cs}, message="x") |
119 | pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { | 135 | pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { |
120 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | 136 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); |
121 | check(yS <= 0-ySMax); | 137 | check(yS <= 0.0-ySMax); |
122 | } | 138 | } |
123 | 139 | ||
124 | @Constraint(severity="error", key={cs}, message="x") | 140 | @Constraint(severity="error", key={cs}, message="x") |
@@ -133,7 +149,7 @@ pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { | |||
133 | Actor.placedOn(a, hl); | 149 | Actor.placedOn(a, hl); |
134 | Lane_Horizontal(hl); | 150 | Lane_Horizontal(hl); |
135 | Actor.ySpeed(a, ySpeed); | 151 | Actor.ySpeed(a, ySpeed); |
136 | check(ySpeed != 0); | 152 | check(ySpeed != 0.0); |
137 | } | 153 | } |
138 | 154 | ||
139 | private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, | 155 | private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, |
@@ -148,7 +164,7 @@ private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, | |||
148 | @Constraint(severity="error", key={cs}, message="x") | 164 | @Constraint(severity="error", key={cs}, message="x") |
149 | pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { | 165 | pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { |
150 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | 166 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); |
151 | check(xS <= 0-xSMax); | 167 | check(xS <= 0.0-xSMax); |
152 | } | 168 | } |
153 | 169 | ||
154 | @Constraint(severity="error", key={cs}, message="x") | 170 | @Constraint(severity="error", key={cs}, message="x") |
@@ -203,54 +219,46 @@ pattern define_actor_vehicleLength(v:Vehicle) { | |||
203 | check(l != 1.0); | 219 | check(l != 1.0); |
204 | } | 220 | } |
205 | 221 | ||
206 | /////---------------- | 222 | ///////---------------- |
207 | /////DERIVED FEATURES | 223 | ///////DERIVED FEATURES |
208 | /////---------------- | 224 | ///////---------------- |
209 | 225 | // | |
210 | private pattern helper_getCoords(a1:Actor, | 226 | //@QueryBasedFeature |
211 | a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | 227 | //pattern dist_near(a1: Actor, a2: Actor) { |
212 | Actor.xPos(a1, x1); | 228 | // find helper_actorsAreNear(a1, a2); |
213 | Actor.yPos(a1, y1); | 229 | // Actor.dist_near(a1, a2); |
214 | Actor.xPos(a2, x2); | 230 | //} |
215 | Actor.yPos(a2, y2); | 231 | // |
216 | } | 232 | //private pattern helper_actorsAreNear(a1: Actor, a2: Actor) { |
217 | 233 | // find helper_getCoords(a1, a2, x1, x2, y1, y2); | |
218 | @QueryBasedFeature | 234 | // //check(dx^2 + dy^2 < 10^2) |
219 | pattern dist_near(a1: Actor, a2: Actor) { | 235 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); |
220 | find helper_actorsAreNear(a1, a2); | 236 | //} |
221 | Actor.dist_near(a1, a2); | 237 | // |
222 | } | 238 | //@QueryBasedFeature |
223 | 239 | //pattern dist_med(a1: Actor, a2: Actor) { | |
224 | private pattern helper_actorsAreNear(a1: Actor, a2: Actor) { | 240 | // find helper_actorsAreMed(a1, a2); |
225 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | 241 | // Actor.dist_med(a1, a2); |
226 | //check(dx^2 + dy^2 < 10^2) | 242 | //} |
227 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | 243 | // |
228 | } | 244 | //private pattern helper_actorsAreMed(a1: Actor, a2: Actor) { |
229 | 245 | // find helper_getCoords(a1, a2, x1, x2, y1, y2); | |
230 | @QueryBasedFeature | 246 | // //check(10^2 < dx^2 + dy^2 < 15^2) |
231 | pattern dist_med(a1: Actor, a2: Actor) { | 247 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); |
232 | find helper_actorsAreMed(a1, a2); | 248 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); |
233 | Actor.dist_med(a1, a2); | 249 | //} |
234 | } | 250 | // |
235 | 251 | //@QueryBasedFeature | |
236 | private pattern helper_actorsAreMed(a1: Actor, a2: Actor) { | 252 | //pattern dist_far(a1: Actor, a2: Actor) { |
237 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | 253 | // find helper_actorsAreFar(a1, a2); |
238 | //check(10^2 < dx^2 + dy^2 < 15^2) | 254 | // Actor.dist_far(a1, a2); |
239 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | 255 | //} |
240 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | 256 | // |
241 | } | 257 | //private pattern helper_actorsAreFar(a1: Actor, a2: Actor) { |
242 | 258 | // find helper_getCoords(a1, a2, x1, x2, y1, y2); | |
243 | @QueryBasedFeature | 259 | // //check(dx^2 + dy^2 > 20^2) |
244 | pattern dist_far(a1: Actor, a2: Actor) { | 260 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); |
245 | find helper_actorsAreFar(a1, a2); | 261 | //} |
246 | Actor.dist_far(a1, a2); | ||
247 | } | ||
248 | |||
249 | private pattern helper_actorsAreFar(a1: Actor, a2: Actor) { | ||
250 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
251 | //check(dx^2 + dy^2 > 20^2) | ||
252 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); | ||
253 | } | ||
254 | 262 | ||
255 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | 263 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
256 | //Relation | 264 | //Relation |
@@ -527,10 +535,12 @@ pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocke | |||
527 | check(x1 == x2); | 535 | check(x1 == x2); |
528 | } | 536 | } |
529 | 537 | ||
530 | //TODO refactor? | 538 | private pattern helper_VB_getAllCoords(a1:Actor, a2: Actor, |
531 | @Constraint(severity="error", key={a1, vb}, message="x") | 539 | x1:java Double, y1:java Double, |
532 | pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { | 540 | x2:java Double, y2:java Double, |
533 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 541 | xBlocker:java Double, yBlocker:java Double, |
542 | lenBlocker:java Double, widBlocker:java Double) { | ||
543 | |||
534 | VisionBlocked.source(vb, a1); | 544 | VisionBlocked.source(vb, a1); |
535 | VisionBlocked.target(vb, a2); | 545 | VisionBlocked.target(vb, a2); |
536 | VisionBlocked.blockedBy(vb, aBlocker); | 546 | VisionBlocked.blockedBy(vb, aBlocker); |
@@ -543,6 +553,13 @@ pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { | |||
543 | Actor.yPos(aBlocker, yBlocker); | 553 | Actor.yPos(aBlocker, yBlocker); |
544 | Actor.length(aBlocker, lenBlocker); | 554 | Actor.length(aBlocker, lenBlocker); |
545 | Actor.width(aBlocker, widBlocker); | 555 | Actor.width(aBlocker, widBlocker); |
556 | } | ||
557 | |||
558 | @Constraint(severity="error", key={a1}, message="x") | ||
559 | pattern visionBlocked_ites_top(a1:Actor, a2:Actor) { | ||
560 | |||
561 | find helper_VB_getAllCoords(a1, a2, | ||
562 | x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); | ||
546 | 563 | ||
547 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | 564 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) |
548 | check( | 565 | check( |
@@ -551,22 +568,12 @@ pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { | |||
551 | < ((y1-y2)/(x1-x2))); | 568 | < ((y1-y2)/(x1-x2))); |
552 | } | 569 | } |
553 | 570 | ||
554 | //TODO refactor? | 571 | |
555 | @Constraint(severity="error", key={a1, vb}, message="x") | 572 | @Constraint(severity="error", key={a1}, message="x") |
556 | pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { | 573 | pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor) { |
557 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 574 | |
558 | VisionBlocked.source(vb, a1); | 575 | find helper_VB_getAllCoords(a1, a2, |
559 | VisionBlocked.target(vb, a2); | 576 | x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); |
560 | VisionBlocked.blockedBy(vb, aBlocker); | ||
561 | |||
562 | Actor.xPos(a1, x1); | ||
563 | Actor.yPos(a1, y1); | ||
564 | Actor.xPos(a2, x2); | ||
565 | Actor.yPos(a2, y2); | ||
566 | Actor.xPos(aBlocker, xBlocker); | ||
567 | Actor.yPos(aBlocker, yBlocker); | ||
568 | Actor.length(aBlocker, lenBlocker); | ||
569 | Actor.width(aBlocker, widBlocker); | ||
570 | 577 | ||
571 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | 578 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) |
572 | check( | 579 | check( |
@@ -575,44 +582,43 @@ pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { | |||
575 | > ((y1-y2)/(x1-x2))); | 582 | > ((y1-y2)/(x1-x2))); |
576 | } | 583 | } |
577 | 584 | ||
578 | //TODO refactor? | 585 | |
579 | //TODO CORNER CASES | 586 | private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, |
580 | @Constraint(severity="error", key={a1, vb}, message="x") | 587 | x1:java Double, y1:java Double, |
581 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor, vb:VisionBlocked) { | 588 | x2:java Double, y2:java Double, |
582 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 589 | xBlocker:java Double, yBlocker:java Double) { |
590 | |||
583 | VisionBlocked.source(vb, a1); | 591 | VisionBlocked.source(vb, a1); |
584 | VisionBlocked.target(vb, a2); | 592 | VisionBlocked.target(vb, a2); |
585 | VisionBlocked.blockedBy(vb, aBlocker); | 593 | VisionBlocked.blockedBy(vb, aBlocker); |
586 | 594 | ||
587 | Actor.xPos(a1, x1); | 595 | Actor.xPos(a1, x1); |
596 | Actor.yPos(a1, y1); | ||
588 | Actor.xPos(a2, x2); | 597 | Actor.xPos(a2, x2); |
598 | Actor.yPos(a2, y2); | ||
589 | Actor.xPos(aBlocker, xBlocker); | 599 | Actor.xPos(aBlocker, xBlocker); |
590 | 600 | Actor.yPos(aBlocker, yBlocker); | |
591 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | ||
592 | //TODO implement ABSOLUTE VALUE or MULTI-CHECK | ||
593 | //TODO do pythagoras | ||
594 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); | ||
595 | } | 601 | } |
596 | 602 | ||
597 | //TODO refactor? | 603 | //INFO may use approximation instead |
598 | //TODO CORNER CASES | 604 | @Constraint(severity="error", key={a1}, message="x") |
599 | @Constraint(severity="error", key={a1, vb}, message="x") | 605 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { |
600 | pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor, vb:VisionBlocked) { | 606 | |
601 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 607 | find helper_VB_getJustCoords(a1, a2, |
602 | VisionBlocked.source(vb, a2); | 608 | x1, y1, x2, y2, xBlocker, yBlocker); |
603 | VisionBlocked.target(vb, a1); | ||
604 | VisionBlocked.blockedBy(vb, aBlocker); | ||
605 | |||
606 | Actor.xPos(a1, x1); | ||
607 | Actor.xPos(a2, x2); | ||
608 | Actor.xPos(aBlocker, xBlocker); | ||
609 | 609 | ||
610 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | 610 | //check(dist(A1, ABlocker) > dist(A1, A2)) |
611 | //TODO implement ABSOLUTE VALUE or MULTI-CHECK | 611 | check((x1-xBlocker)*(x1-xBlocker) + (y1-yBlocker)*(y1-yBlocker) > (x1-x2)*(x1-x2) + (y1-y2)*(y1-y2)); |
612 | //TODO do pythagoras | ||
613 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); | ||
614 | } | 612 | } |
615 | 613 | ||
616 | //TODO same as above for Y??? | 614 | //INFO may use approximation instead |
617 | //TODO same as above for Y ???? | 615 | @Constraint(severity="error", key={a1}, message="x") |
616 | pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { | ||
617 | |||
618 | find helper_VB_getJustCoords(a1, a2, | ||
619 | x1, y1, x2, y2, xBlocker, yBlocker); | ||
620 | |||
621 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
622 | check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1)); | ||
623 | } | ||
618 | 624 | ||
diff --git a/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java b/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java index ed227f7a..5bf70b3a 100644 --- a/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java +++ b/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java | |||
@@ -30,13 +30,16 @@ public class CrossingScenarioMain { | |||
30 | } | 30 | } |
31 | 31 | ||
32 | Path pathStats = Paths.get("outputs/statistics.csv"); | 32 | Path pathStats = Paths.get("outputs/statistics.csv"); |
33 | String pathXmi = "outputs/models/1.xmi"; | 33 | // String pathXmi = "outputs/models/1.xmi"; |
34 | String savePath = "outputs/drawnModel1.png"; | 34 | // String savePath = "outputs/drawnModel1.png"; |
35 | // Path target = Paths.get("../..//Tests/MODELS2020-CaseStudies/case.study.pledge.run/measurements1/stats.csv"); | 35 | // Path target = Paths.get("../..//Tests/MODELS2020-CaseStudies/case.study.pledge.run/measurements1/stats.csv"); |
36 | // Files.copy(path, target, StandardCopyOption.REPLACE_EXISTING); | 36 | // Files.copy(path, target, StandardCopyOption.REPLACE_EXISTING); |
37 | 37 | ||
38 | printStats(pathStats); | 38 | printStats(pathStats); |
39 | DrawScenario.drawScenario(pathXmi, savePath); | 39 | for (int i = 1; i <= 10; i++) { |
40 | DrawScenario.drawScenario("outputs/models/"+i+".xmi", "outputs/drawnModel"+i+".png"); | ||
41 | System.out.println("DONE " + i); | ||
42 | } | ||
40 | 43 | ||
41 | // String p1 = "outputs/models/1.xmi"; | 44 | // String p1 = "outputs/models/1.xmi"; |
42 | // String p2 = "outputs/simplePrevLane.tgf"; | 45 | // String p2 = "outputs/simplePrevLane.tgf"; |
diff --git a/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java b/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java index 572fea68..daf294f4 100644 --- a/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java +++ b/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java | |||
@@ -135,6 +135,25 @@ public class DrawScenario { | |||
135 | 135 | ||
136 | } | 136 | } |
137 | } | 137 | } |
138 | |||
139 | g.setPaint(Color.GREEN); | ||
140 | for (Relation ce : cs.getRelations().stream(). | ||
141 | filter(r -> r instanceof VisionBlocked).collect(Collectors.toList())) { | ||
142 | Actor a1 = ce.getSource(); | ||
143 | Actor a2 = ce.getTarget(); | ||
144 | Actor b = ((VisionBlocked) ce).getBlockedBy(); | ||
145 | |||
146 | |||
147 | int x1 = (int) (a1.getXPos() * multiplier); | ||
148 | int y1 = (int) (a1.getYPos() * multiplier); | ||
149 | int x2 = (int) (a2.getXPos() * multiplier); | ||
150 | int y2 = (int) (a2.getYPos() * multiplier); | ||
151 | int xb = (int) (b.getXPos() * multiplier); | ||
152 | int yb = (int) (b.getYPos() * multiplier); | ||
153 | |||
154 | g.drawLine(x1, y1, xb, yb); | ||
155 | g.drawLine(x2, y2, xb, yb); | ||
156 | } | ||
138 | g.dispose(); | 157 | g.dispose(); |
139 | 158 | ||
140 | File f = new File(saveToPath); | 159 | File f = new File(saveToPath); |