diff options
Diffstat (limited to 'Domains/crossingScenario/queries')
-rw-r--r-- | Domains/crossingScenario/queries/crossingScenarioQueries.vql | 325 | ||||
-rw-r--r-- | Domains/crossingScenario/queries/moreCompleteQueries2._v_q_l | 891 |
2 files changed, 932 insertions, 284 deletions
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index c009e031..a26782ae 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql | |||
@@ -3,180 +3,6 @@ package queries | |||
3 | import "http://www.example.com/crossingScenario" | 3 | import "http://www.example.com/crossingScenario" |
4 | import "http://www.eclipse.org/emf/2002/Ecore" | 4 | import "http://www.eclipse.org/emf/2002/Ecore" |
5 | 5 | ||
6 | //////Minimal Failing Example | ||
7 | //@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation") | ||
8 | //pattern patterThatOnlyWorksWithInt(l : Lane) { | ||
9 | // Lane.referenceCoord(l, w); | ||
10 | // check(w <= 0-10.0); | ||
11 | //} | ||
12 | |||
13 | ////////////// | ||
14 | //CrossingScenario | ||
15 | ///////////// | ||
16 | |||
17 | /* | ||
18 | //TODO Hard-code xSize? | ||
19 | //TODO Hard-code ySize? | ||
20 | |||
21 | //TODO Hard-code maxTime? | ||
22 | @Constraint(severity="error", key={l}, message="3 CrossingScenari") | ||
23 | pattern define_cs_maxTime(cs:CrossingScenario) { | ||
24 | CrossingScenario.maxTime(cs, mt); | ||
25 | check(mt != 60.0); | ||
26 | } | ||
27 | */ | ||
28 | |||
29 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
30 | //Lane | ||
31 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
32 | /* | ||
33 | |||
34 | ////<<<<OLD>>>> | ||
35 | ////Width: Different Lanes | ||
36 | //@Constraint(severity="error", key={l}, message="1 Lane") | ||
37 | //pattern define_numWidth_small(l : Lane) { | ||
38 | // Lane.width(l, Size::S_Small); | ||
39 | // Lane.numWidth(l, nw); | ||
40 | // check(nw <= 5.0); | ||
41 | //} or { | ||
42 | // Lane.width(l, Size::S_Small); | ||
43 | // Lane.numWidth(l, nw); | ||
44 | // check(nw >= 10.0); | ||
45 | //} | ||
46 | // | ||
47 | //@Constraint(severity="error", key={l}, message="2 Lane") | ||
48 | //pattern define_numWidth_medium(l : Lane) { | ||
49 | // Lane.width(l, ::S_Med); | ||
50 | // Lane.numWidth(l, nw); | ||
51 | // check(nw <= 10.0); | ||
52 | //} | ||
53 | //or { | ||
54 | // Lane.width(l, Size::S_Med); | ||
55 | // Lane.numWidth(l, nw); | ||
56 | // check(nw >= 15.0); | ||
57 | //} | ||
58 | // | ||
59 | //@Constraint(severity="error", key={l}, message="3 Lane") | ||
60 | //pattern define_numWidth_large(l : Lane) { | ||
61 | // Lane.width(l, Size::S_Large); | ||
62 | // Lane.numWidth(l, nw); | ||
63 | // check(nw <= 15.0); | ||
64 | //} | ||
65 | //or { | ||
66 | // Lane.width(l, Size::S_Large); | ||
67 | // Lane.numWidth(l, nw); | ||
68 | // check(nw >= 20.0); | ||
69 | //} | ||
70 | |||
71 | //<<<<NEW>>>> | ||
72 | //Width is FIXED: always 5 | ||
73 | |||
74 | /////////////Prevlane | ||
75 | |||
76 | ////<<<<OLD>>>> | ||
77 | ////Generating 2 linkedlists (1 for horizontal, 1 for vertical lanes) | ||
78 | //////////head lanes do not have prevLane | ||
79 | //@Constraint(severity="error", key={l}, message="6.1 Lane") | ||
80 | //pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) { | ||
81 | // CrossingScenario.vertical_head(cs, l); | ||
82 | // Lane.prevLane(l, _); | ||
83 | //} | ||
84 | // | ||
85 | //@Constraint(severity="error", key={l}, message="6.2 Lane") | ||
86 | //pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) { | ||
87 | // CrossingScenario.horizontal_head(cs, l); | ||
88 | // Lane.prevLane(l, _); | ||
89 | //} | ||
90 | // | ||
91 | //////////Non-head lanes must have prevLane | ||
92 | //@Constraint(severity="error", key={l}, message="6.1 Lane") | ||
93 | //pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) { | ||
94 | // neg find find_headVertLane(l); | ||
95 | // neg find find_laneWithPrevLane(l); | ||
96 | //} | ||
97 | // | ||
98 | //@Constraint(severity="error", key={l}, message="6.1 Lane") | ||
99 | //pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) { | ||
100 | // neg find find_headHoriLane(l); | ||
101 | // neg find find_laneWithPrevLane(l); | ||
102 | //} | ||
103 | // | ||
104 | //private pattern find_headVertLane(l:Lane_Vertical) { | ||
105 | // CrossingScenario.vertical_head(_, l); | ||
106 | //} | ||
107 | //private pattern find_headHoriLane(l:Lane_Horizontal) { | ||
108 | // CrossingScenario.horizontal_head(_, l); | ||
109 | //} | ||
110 | //private pattern find_laneWithPrevLane(l:Lane) { | ||
111 | // Lane.prevLane(l, _); | ||
112 | //} | ||
113 | // | ||
114 | ///////////Lane cannot be its own recursive prevLane | ||
115 | //@Constraint(severity="error", key={l}, message="6.1 Lane") | ||
116 | //pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) { | ||
117 | // Lane.prevLane(l, l); | ||
118 | //} | ||
119 | // | ||
120 | //@Constraint(severity="error", key={l}, message="6.2 Lane") | ||
121 | //pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) { | ||
122 | // find find_prevLane+(l, l); | ||
123 | //} | ||
124 | //private pattern find_prevLane(l1:Lane, l2:Lane) { | ||
125 | // Lane.prevLane(l1, l2); | ||
126 | //} | ||
127 | // | ||
128 | ////////Lane cannot be prevLane of >1 other lane | ||
129 | //@Constraint(severity="error", key={l1, l2}, message="7 Lane") | ||
130 | //pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) { | ||
131 | // Lane.prevLane(l1, l); | ||
132 | // Lane.prevLane(l2, l); | ||
133 | // l1 != l2; | ||
134 | //} | ||
135 | // | ||
136 | ////////consecutive lanes must have same orientation | ||
137 | //@Constraint(severity="error", key={l1, l2}, message="8 Lane") | ||
138 | //pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) { | ||
139 | // Lane.prevLane(l1, l2); | ||
140 | //} | ||
141 | // | ||
142 | //@Constraint(severity="error", key={l1, l2}, message="8 Lane") | ||
143 | //pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) { | ||
144 | // Lane.prevLane(l1, l2); | ||
145 | //} | ||
146 | // | ||
147 | ///////////////ReferenceCoord | ||
148 | // | ||
149 | ///////refCoord of head lanes must be 0 | ||
150 | //@Constraint(severity="error", key={l}, message="6.2 Lane") | ||
151 | //pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) { | ||
152 | // CrossingScenario.horizontal_head(cs, l); | ||
153 | // Lane.referenceCoord(l, rc); | ||
154 | // check(rc != 0.0); | ||
155 | //} | ||
156 | // | ||
157 | //@Constraint(severity="error", key={l}, message="6.2 Lane") | ||
158 | //pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) { | ||
159 | // CrossingScenario.vertical_head(cs, l); | ||
160 | // Lane.referenceCoord(l, rc); | ||
161 | // check(rc != 0.0); | ||
162 | //} | ||
163 | // | ||
164 | ////////refCoord of a lane is prevLane.rc + curLane.numWidth | ||
165 | // | ||
166 | //@Constraint(severity="error", key={l}, message="6.2 Lane") | ||
167 | //pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) { | ||
168 | // Lane.prevLane(l, prev); | ||
169 | // Lane.referenceCoord(l, rcCur); | ||
170 | // | ||
171 | // Lane.numWidth(prev, wPrev); | ||
172 | // Lane.referenceCoord(prev, rcPrev); | ||
173 | // check(rcCur != rcPrev + wPrev); | ||
174 | //} | ||
175 | |||
176 | //<<<<NEW>>>> | ||
177 | //Lanes are all predefind | ||
178 | */ | ||
179 | |||
180 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | 6 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
181 | //Lane+Actor | 7 | //Lane+Actor |
182 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | 8 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
@@ -430,12 +256,12 @@ private pattern helper_actorsAreFar(a1: Actor, a2: Actor) { | |||
430 | //Relation | 256 | //Relation |
431 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | 257 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
432 | 258 | ||
433 | @Constraint(severity="error", key={a1, a2}, message="1 Relation") | 259 | //@Constraint(severity="error", key={a1, a2}, message="1 Relation") |
434 | pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { | 260 | //pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { |
435 | Relation.source(r, a1); | 261 | // Relation.source(r, a1); |
436 | Relation.target(r, a2); | 262 | // Relation.target(r, a2); |
437 | a1 == a2; | 263 | // a1 == a2; |
438 | } | 264 | //} |
439 | 265 | ||
440 | //TODO do above but transitively?/ | 266 | //TODO do above but transitively?/ |
441 | //////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | 267 | //////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
@@ -462,7 +288,7 @@ pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { | |||
462 | Lane_Horizontal(hl2); | 288 | Lane_Horizontal(hl2); |
463 | } | 289 | } |
464 | 290 | ||
465 | //<<END QUALITATIF ABSTRACTION>> | 291 | //<<END TEMP QUALITATIF ABSTRACTION>> |
466 | 292 | ||
467 | //// | 293 | //// |
468 | //VS VisionBlocked | 294 | //VS VisionBlocked |
@@ -470,6 +296,36 @@ pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { | |||
470 | //TODO Very prone to corner cases | 296 | //TODO Very prone to corner cases |
471 | /* | 297 | /* |
472 | @Constraint(severity="error", key={a1}, message="x") | 298 | @Constraint(severity="error", key={a1}, message="x") |
299 | pattern collisionExists_vsVisionBlockedX1(a1:Actor) { | ||
300 | VisionBlocked.blockedBy(_, a1); | ||
301 | CollisionExists.target(_, a1); | ||
302 | } | ||
303 | @Constraint(severity="error", key={a1}, message="x") | ||
304 | pattern collisionExists_vsVisionBlockedX2(a1:Actor) { | ||
305 | VisionBlocked.blockedBy(_, a1); | ||
306 | CollisionExists.source(_, a1); | ||
307 | } | ||
308 | |||
309 | @Constraint(severity="error", key={a1}, message="x") | ||
310 | pattern collisionExists_vsVisionBlocked1(a1:Actor) { | ||
311 | VisionBlocked.source(_, a1); | ||
312 | neg find helper_source(a1); | ||
313 | } | ||
314 | private pattern helper_source(a1:Actor) { | ||
315 | CollisionExists.source(_, a1); | ||
316 | } | ||
317 | |||
318 | @Constraint(severity="error", key={a1}, message="x") | ||
319 | pattern collisionExists_vsVisionBlocked2(a1:Actor) { | ||
320 | VisionBlocked.target(_, a1); | ||
321 | neg find helper_target(a1); | ||
322 | } | ||
323 | private pattern helper_target(a1:Actor) { | ||
324 | CollisionExists.target(_, a1); | ||
325 | } | ||
326 | */ | ||
327 | /* | ||
328 | @Constraint(severity="error", key={a1}, message="x") | ||
473 | pattern collisionExists_vsVisionBlocked(a1:Actor) { | 329 | pattern collisionExists_vsVisionBlocked(a1:Actor) { |
474 | VisionBlocked.source(vb, a1); | 330 | VisionBlocked.source(vb, a1); |
475 | VisionBlocked.target(vb, a2); | 331 | VisionBlocked.target(vb, a2); |
@@ -610,7 +466,7 @@ pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { | |||
610 | 466 | ||
611 | //<<QUALTATIF ABSTRACTION>> | 467 | //<<QUALTATIF ABSTRACTION>> |
612 | 468 | ||
613 | @Constraint(severity="error", key={a1, a2}, message="x") | 469 | @Constraint(severity="error", key={a1, a2}, message="on 3 different lanes") |
614 | pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { | 470 | pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { |
615 | VisionBlocked.source(vb, a1); | 471 | VisionBlocked.source(vb, a1); |
616 | VisionBlocked.target(vb, a2); | 472 | VisionBlocked.target(vb, a2); |
@@ -628,7 +484,7 @@ pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { | |||
628 | Actor.placedOn(a2, l); | 484 | Actor.placedOn(a2, l); |
629 | } | 485 | } |
630 | 486 | ||
631 | @Constraint(severity="error", key={a1, a2}, message="x") | 487 | @Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation") |
632 | pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { | 488 | pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { |
633 | VisionBlocked.source(ce, a1); | 489 | VisionBlocked.source(ce, a1); |
634 | VisionBlocked.target(ce, a2); | 490 | VisionBlocked.target(ce, a2); |
@@ -734,6 +590,7 @@ pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor, vb:VisionBloc | |||
734 | 590 | ||
735 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | 591 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) |
736 | //TODO implement ABSOLUTE VALUE or MULTI-CHECK | 592 | //TODO implement ABSOLUTE VALUE or MULTI-CHECK |
593 | //TODO do pythagoras | ||
737 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); | 594 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); |
738 | } | 595 | } |
739 | 596 | ||
@@ -752,110 +609,10 @@ pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor, vb:VisionBloc | |||
752 | 609 | ||
753 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | 610 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) |
754 | //TODO implement ABSOLUTE VALUE or MULTI-CHECK | 611 | //TODO implement ABSOLUTE VALUE or MULTI-CHECK |
612 | //TODO do pythagoras | ||
755 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); | 613 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); |
756 | } | 614 | } |
757 | 615 | ||
758 | //TODO same as above for Y??? | 616 | //TODO same as above for Y??? |
759 | //TODO same as above for Y ???? | 617 | //TODO same as above for Y ???? |
760 | 618 | ||
761 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
762 | //SeparationDistance | ||
763 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
764 | /* | ||
765 | private pattern helper_getSeperateActorsCoords(a1:Actor, | ||
766 | a2: Actor, sd:SeparationDistance, | ||
767 | x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | ||
768 | SeperationDistance.source(sd, a1); | ||
769 | SeparationDistance.target(sd, a2); | ||
770 | |||
771 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
772 | } | ||
773 | |||
774 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
775 | pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
776 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
777 | |||
778 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
779 | SeparationDistance.distance(sd, Distance::D_Near); | ||
780 | |||
781 | //check(dx^2 + dy^2 < 5^2) | ||
782 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); | ||
783 | } | ||
784 | |||
785 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
786 | pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
787 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
788 | |||
789 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
790 | SeparationDistance.distance(sd, Distance::D_Near); | ||
791 | |||
792 | //check(dx^2 + dy^2 > 10^2) | ||
793 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | ||
794 | } | ||
795 | |||
796 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
797 | pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
798 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
799 | |||
800 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
801 | SeparationDistance.distance(sd, Distance::D_Med); | ||
802 | |||
803 | //check(dx^2 + dy^2 < 10^2) | ||
804 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | ||
805 | } | ||
806 | |||
807 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
808 | pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
809 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
810 | |||
811 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
812 | SeparationDistance.distance(sd, Distance::D_Med); | ||
813 | |||
814 | //check(dx^2 + dy^2 > 1^2) | ||
815 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); | ||
816 | } | ||
817 | |||
818 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
819 | pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
820 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
821 | |||
822 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
823 | SeparationDistance.distance(sd, Distance::D_Far); | ||
824 | |||
825 | //check(dx^2 + dy^2 < 15^2) | ||
826 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
827 | } | ||
828 | */ | ||
829 | |||
830 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
831 | //CollisionDoesNotExist | ||
832 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
833 | /* | ||
834 | //TODO | ||
835 | @Constraint(severity="error", key={a1, cdne}, message="x") | ||
836 | pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) { | ||
837 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
838 | |||
839 | CrossingScenario.actors(ss, a1); | ||
840 | CrossingScenario.actors(ss, a2); | ||
841 | Actor.relations(a1, cdne); | ||
842 | CollisionDoesNotExist.target(cdne, a2); | ||
843 | CrossingScenario.maxTime(ss, maxTime); | ||
844 | |||
845 | Actor.width(a1, w1); | ||
846 | Actor.length(a1, l1); | ||
847 | Actor.xPos(a1, xPos1); | ||
848 | Actor.yPos(a1, yPos1); | ||
849 | Actor.xSpeed(a1, xSpeed1); | ||
850 | Actor.ySpeed(a1, ySpeed1); | ||
851 | |||
852 | Actor.width(a2, w2); | ||
853 | Actor.length(a2, l2); | ||
854 | Actor.xPos(a2, xPos2); | ||
855 | Actor.yPos(a2, yPos2); | ||
856 | Actor.xSpeed(a2, xSpeed2); | ||
857 | Actor.ySpeed(a2, ySpeed2); | ||
858 | //check(dx^2 + dy^2 < 15^2) | ||
859 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
860 | } | ||
861 | */ \ No newline at end of file | ||
diff --git a/Domains/crossingScenario/queries/moreCompleteQueries2._v_q_l b/Domains/crossingScenario/queries/moreCompleteQueries2._v_q_l new file mode 100644 index 00000000..51e1bf00 --- /dev/null +++ b/Domains/crossingScenario/queries/moreCompleteQueries2._v_q_l | |||
@@ -0,0 +1,891 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http://www.example.com/crossingScenario" | ||
4 | import "http://www.eclipse.org/emf/2002/Ecore" | ||
5 | |||
6 | //////Minimal Failing Example | ||
7 | //@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation") | ||
8 | //pattern patterThatOnlyWorksWithInt(l : Lane) { | ||
9 | // Lane.referenceCoord(l, w); | ||
10 | // check(w <= 0-10.0); | ||
11 | //} | ||
12 | |||
13 | ////////////// | ||
14 | //CrossingScenario | ||
15 | ///////////// | ||
16 | |||
17 | /* | ||
18 | //TODO Hard-code xSize? | ||
19 | //TODO Hard-code ySize? | ||
20 | |||
21 | //TODO Hard-code maxTime? | ||
22 | @Constraint(severity="error", key={l}, message="3 CrossingScenari") | ||
23 | pattern define_cs_maxTime(cs:CrossingScenario) { | ||
24 | CrossingScenario.maxTime(cs, mt); | ||
25 | check(mt != 60.0); | ||
26 | } | ||
27 | */ | ||
28 | |||
29 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
30 | //Lane | ||
31 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
32 | /* | ||
33 | |||
34 | ////<<<<OLD>>>> | ||
35 | ////Width: Different Lanes | ||
36 | //@Constraint(severity="error", key={l}, message="1 Lane") | ||
37 | //pattern define_numWidth_small(l : Lane) { | ||
38 | // Lane.width(l, Size::S_Small); | ||
39 | // Lane.numWidth(l, nw); | ||
40 | // check(nw <= 5.0); | ||
41 | //} or { | ||
42 | // Lane.width(l, Size::S_Small); | ||
43 | // Lane.numWidth(l, nw); | ||
44 | // check(nw >= 10.0); | ||
45 | //} | ||
46 | // | ||
47 | //@Constraint(severity="error", key={l}, message="2 Lane") | ||
48 | //pattern define_numWidth_medium(l : Lane) { | ||
49 | // Lane.width(l, ::S_Med); | ||
50 | // Lane.numWidth(l, nw); | ||
51 | // check(nw <= 10.0); | ||
52 | //} | ||
53 | //or { | ||
54 | // Lane.width(l, Size::S_Med); | ||
55 | // Lane.numWidth(l, nw); | ||
56 | // check(nw >= 15.0); | ||
57 | //} | ||
58 | // | ||
59 | //@Constraint(severity="error", key={l}, message="3 Lane") | ||
60 | //pattern define_numWidth_large(l : Lane) { | ||
61 | // Lane.width(l, Size::S_Large); | ||
62 | // Lane.numWidth(l, nw); | ||
63 | // check(nw <= 15.0); | ||
64 | //} | ||
65 | //or { | ||
66 | // Lane.width(l, Size::S_Large); | ||
67 | // Lane.numWidth(l, nw); | ||
68 | // check(nw >= 20.0); | ||
69 | //} | ||
70 | |||
71 | //<<<<NEW>>>> | ||
72 | //Width is FIXED: always 5 | ||
73 | |||
74 | /////////////Prevlane | ||
75 | |||
76 | ////<<<<OLD>>>> | ||
77 | ////Generating 2 linkedlists (1 for horizontal, 1 for vertical lanes) | ||
78 | //////////head lanes do not have prevLane | ||
79 | //@Constraint(severity="error", key={l}, message="6.1 Lane") | ||
80 | //pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) { | ||
81 | // CrossingScenario.vertical_head(cs, l); | ||
82 | // Lane.prevLane(l, _); | ||
83 | //} | ||
84 | // | ||
85 | //@Constraint(severity="error", key={l}, message="6.2 Lane") | ||
86 | //pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) { | ||
87 | // CrossingScenario.horizontal_head(cs, l); | ||
88 | // Lane.prevLane(l, _); | ||
89 | //} | ||
90 | // | ||
91 | //////////Non-head lanes must have prevLane | ||
92 | //@Constraint(severity="error", key={l}, message="6.1 Lane") | ||
93 | //pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) { | ||
94 | // neg find find_headVertLane(l); | ||
95 | // neg find find_laneWithPrevLane(l); | ||
96 | //} | ||
97 | // | ||
98 | //@Constraint(severity="error", key={l}, message="6.1 Lane") | ||
99 | //pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) { | ||
100 | // neg find find_headHoriLane(l); | ||
101 | // neg find find_laneWithPrevLane(l); | ||
102 | //} | ||
103 | // | ||
104 | //private pattern find_headVertLane(l:Lane_Vertical) { | ||
105 | // CrossingScenario.vertical_head(_, l); | ||
106 | //} | ||
107 | //private pattern find_headHoriLane(l:Lane_Horizontal) { | ||
108 | // CrossingScenario.horizontal_head(_, l); | ||
109 | //} | ||
110 | //private pattern find_laneWithPrevLane(l:Lane) { | ||
111 | // Lane.prevLane(l, _); | ||
112 | //} | ||
113 | // | ||
114 | ///////////Lane cannot be its own recursive prevLane | ||
115 | //@Constraint(severity="error", key={l}, message="6.1 Lane") | ||
116 | //pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) { | ||
117 | // Lane.prevLane(l, l); | ||
118 | //} | ||
119 | // | ||
120 | //@Constraint(severity="error", key={l}, message="6.2 Lane") | ||
121 | //pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) { | ||
122 | // find find_prevLane+(l, l); | ||
123 | //} | ||
124 | //private pattern find_prevLane(l1:Lane, l2:Lane) { | ||
125 | // Lane.prevLane(l1, l2); | ||
126 | //} | ||
127 | // | ||
128 | ////////Lane cannot be prevLane of >1 other lane | ||
129 | //@Constraint(severity="error", key={l1, l2}, message="7 Lane") | ||
130 | //pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) { | ||
131 | // Lane.prevLane(l1, l); | ||
132 | // Lane.prevLane(l2, l); | ||
133 | // l1 != l2; | ||
134 | //} | ||
135 | // | ||
136 | ////////consecutive lanes must have same orientation | ||
137 | //@Constraint(severity="error", key={l1, l2}, message="8 Lane") | ||
138 | //pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) { | ||
139 | // Lane.prevLane(l1, l2); | ||
140 | //} | ||
141 | // | ||
142 | //@Constraint(severity="error", key={l1, l2}, message="8 Lane") | ||
143 | //pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) { | ||
144 | // Lane.prevLane(l1, l2); | ||
145 | //} | ||
146 | // | ||
147 | ///////////////ReferenceCoord | ||
148 | // | ||
149 | ///////refCoord of head lanes must be 0 | ||
150 | //@Constraint(severity="error", key={l}, message="6.2 Lane") | ||
151 | //pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) { | ||
152 | // CrossingScenario.horizontal_head(cs, l); | ||
153 | // Lane.referenceCoord(l, rc); | ||
154 | // check(rc != 0.0); | ||
155 | //} | ||
156 | // | ||
157 | //@Constraint(severity="error", key={l}, message="6.2 Lane") | ||
158 | //pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) { | ||
159 | // CrossingScenario.vertical_head(cs, l); | ||
160 | // Lane.referenceCoord(l, rc); | ||
161 | // check(rc != 0.0); | ||
162 | //} | ||
163 | // | ||
164 | ////////refCoord of a lane is prevLane.rc + curLane.numWidth | ||
165 | // | ||
166 | //@Constraint(severity="error", key={l}, message="6.2 Lane") | ||
167 | //pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) { | ||
168 | // Lane.prevLane(l, prev); | ||
169 | // Lane.referenceCoord(l, rcCur); | ||
170 | // | ||
171 | // Lane.numWidth(prev, wPrev); | ||
172 | // Lane.referenceCoord(prev, rcPrev); | ||
173 | // check(rcCur != rcPrev + wPrev); | ||
174 | //} | ||
175 | |||
176 | //<<<<NEW>>>> | ||
177 | //Lanes are all predefind | ||
178 | */ | ||
179 | |||
180 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
181 | //Lane+Actor | ||
182 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
183 | |||
184 | /////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] | ||
185 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
186 | pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { | ||
187 | Actor.placedOn(a, vl); | ||
188 | Actor.xPos(a, x); | ||
189 | Lane.referenceCoord(vl, r); | ||
190 | check(x <= r); | ||
191 | } or { | ||
192 | Actor.placedOn(a, vl); | ||
193 | Actor.xPos(a, x); | ||
194 | Lane.referenceCoord(vl, r); | ||
195 | // //<<<<OLD>>>> | ||
196 | // Lane.numWidth(vl, w); | ||
197 | // check(x >= (r + w)); | ||
198 | |||
199 | //<<<<NEW>>>>: lanes all have width=5 | ||
200 | check(x >= (r + 5.0)); | ||
201 | } | ||
202 | |||
203 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
204 | pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { | ||
205 | Actor.placedOn(a, hl); | ||
206 | Actor.yPos(a, y); | ||
207 | Lane.referenceCoord(hl, r); | ||
208 | check(y <= r); | ||
209 | } or { | ||
210 | Actor.placedOn(a, hl); | ||
211 | Actor.yPos(a, y); | ||
212 | Lane.referenceCoord(hl, r); | ||
213 | // //<<OLD>> | ||
214 | // Lane.numWidth(hl, w); | ||
215 | // check(y >= (r + w)); | ||
216 | |||
217 | //<<NEW>> | ||
218 | check(y >= (r + 5.0)); | ||
219 | |||
220 | } | ||
221 | |||
222 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
223 | //Actor | ||
224 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
225 | |||
226 | /////---------------- | ||
227 | //Xpos and Ypos Bounds | ||
228 | /////---------------- | ||
229 | |||
230 | private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor, | ||
231 | xMax:java Double, xP:java Double) { | ||
232 | Actor.placedOn(a, hl); | ||
233 | Lane_Horizontal(hl); | ||
234 | CrossingScenario.actors(cs, a); | ||
235 | CrossingScenario.xSize(cs, xMax); | ||
236 | Actor.xPos(a, xP); | ||
237 | } | ||
238 | |||
239 | private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor, | ||
240 | yMax:java Double, yP:java Double) { | ||
241 | Actor.placedOn(a, vl); | ||
242 | Lane_Vertical(vl); | ||
243 | CrossingScenario.actors(cs, a); | ||
244 | CrossingScenario.ySize(cs, yMax); | ||
245 | Actor.yPos(a, yP); | ||
246 | } | ||
247 | |||
248 | @Constraint(severity="error", key={cs}, message="x") | ||
249 | pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { | ||
250 | find helper_horiz_getXAndBounds(cs, a, xMax, xP); | ||
251 | check(xP >= xMax);} | ||
252 | |||
253 | @Constraint(severity="error", key={cs}, message="x") | ||
254 | pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { | ||
255 | find helper_horiz_getXAndBounds(cs, a, xMax, xP); | ||
256 | check(xP <= 0-xMax);} | ||
257 | |||
258 | @Constraint(severity="error", key={cs}, message="x") | ||
259 | pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { | ||
260 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | ||
261 | check(yP >= yMax);} | ||
262 | |||
263 | @Constraint(severity="error", key={cs}, message="x") | ||
264 | pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { | ||
265 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | ||
266 | check(yP <= 0-yMax);} | ||
267 | |||
268 | /////---------------- | ||
269 | //Xspeed and Yspeed bounds | ||
270 | /////---------------- | ||
271 | |||
272 | //TODO THIS IS HARD_CODED | ||
273 | |||
274 | /////////VERTICAL LANE | ||
275 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
276 | pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { | ||
277 | Actor.placedOn(a, vl); | ||
278 | Lane_Vertical(vl); | ||
279 | Actor.xSpeed(a, xSpeed); | ||
280 | check(xSpeed != 0); | ||
281 | } | ||
282 | |||
283 | private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, | ||
284 | ySpeedMax:java Double, ySpeed:java Double) { | ||
285 | Actor.placedOn(a, vl); | ||
286 | Lane_Vertical(vl); | ||
287 | CrossingScenario.actors(cs, a); | ||
288 | CrossingScenario.maxYSpeed(cs, ySpeedMax); | ||
289 | Actor.ySpeed(a, ySpeed); | ||
290 | } | ||
291 | |||
292 | @Constraint(severity="error", key={cs}, message="x") | ||
293 | pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { | ||
294 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | ||
295 | check(yS <= 0-ySMax); | ||
296 | } | ||
297 | |||
298 | @Constraint(severity="error", key={cs}, message="x") | ||
299 | pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) { | ||
300 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | ||
301 | check(yS >= ySMax); | ||
302 | } | ||
303 | |||
304 | /////////HORIZONTAL LANE | ||
305 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
306 | pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { | ||
307 | Actor.placedOn(a, hl); | ||
308 | Lane_Horizontal(hl); | ||
309 | Actor.ySpeed(a, ySpeed); | ||
310 | check(ySpeed != 0); | ||
311 | } | ||
312 | |||
313 | private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, | ||
314 | xSpeedMax:java Double, xSpeed:java Double) { | ||
315 | Actor.placedOn(a, hl); | ||
316 | Lane_Horizontal(hl); | ||
317 | CrossingScenario.actors(cs, a); | ||
318 | CrossingScenario.maxXSpeed(cs, xSpeedMax); | ||
319 | Actor.xSpeed(a, xSpeed); | ||
320 | } | ||
321 | |||
322 | @Constraint(severity="error", key={cs}, message="x") | ||
323 | pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { | ||
324 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | ||
325 | check(xS <= 0-xSMax); | ||
326 | } | ||
327 | |||
328 | @Constraint(severity="error", key={cs}, message="x") | ||
329 | pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) { | ||
330 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | ||
331 | check(xS >= xSMax); | ||
332 | } | ||
333 | |||
334 | /////---------------- | ||
335 | /////WIDTH and LENGTH | ||
336 | /////---------------- | ||
337 | |||
338 | ///////pedestrian-width (3) | ||
339 | @Constraint(severity="error", key={p}, message="3 Actor") | ||
340 | pattern define_actor_pedestrianWidth(p:Pedestrian) { | ||
341 | Pedestrian.width(p, w); | ||
342 | check(w != 1.0); | ||
343 | } | ||
344 | |||
345 | /////////pedestrian-width (4) | ||
346 | @Constraint(severity="error", key={p}, message="4 Actor") | ||
347 | pattern define_actor_pedestrianLength(p:Pedestrian) { | ||
348 | Pedestrian.length(p, l); | ||
349 | check(l != 1.0); | ||
350 | } | ||
351 | |||
352 | /////////actor-width (5) | ||
353 | @Constraint(severity="error", key={v}, message="5 Actor") | ||
354 | pattern define_actor_vehicleWidth(v:Vehicle) { | ||
355 | Vehicle.placedOn(v, lane); | ||
356 | Lane_Vertical(lane); | ||
357 | Vehicle.width(v, w); | ||
358 | check(w != 1.0); | ||
359 | } or { | ||
360 | Vehicle.placedOn(v, lane); | ||
361 | Lane_Horizontal(lane); | ||
362 | Vehicle.width(v, w); | ||
363 | check(w != 3.0); | ||
364 | } | ||
365 | |||
366 | /////////actor-width (6) | ||
367 | @Constraint(severity="error", key={v}, message="6 Actor") | ||
368 | pattern define_actor_vehicleLength(v:Vehicle) { | ||
369 | Vehicle.placedOn(v, lane); | ||
370 | Lane_Vertical(lane); | ||
371 | Vehicle.length(v, l); | ||
372 | check(l != 3.0); | ||
373 | } or { | ||
374 | Vehicle.placedOn(v, lane); | ||
375 | Lane_Horizontal(lane); | ||
376 | Vehicle.length(v, l); | ||
377 | check(l != 1.0); | ||
378 | } | ||
379 | |||
380 | /////---------------- | ||
381 | /////DERIVED FEATURES | ||
382 | /////---------------- | ||
383 | |||
384 | private pattern helper_getCoords(a1:Actor, | ||
385 | a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | ||
386 | Actor.xPos(a1, x1); | ||
387 | Actor.yPos(a1, y1); | ||
388 | Actor.xPos(a2, x2); | ||
389 | Actor.yPos(a2, y2); | ||
390 | } | ||
391 | |||
392 | @QueryBasedFeature | ||
393 | pattern dist_near(a1: Actor, a2: Actor) { | ||
394 | find helper_actorsAreNear(a1, a2); | ||
395 | Actor.dist_near(a1, a2); | ||
396 | } | ||
397 | |||
398 | private pattern helper_actorsAreNear(a1: Actor, a2: Actor) { | ||
399 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
400 | //check(dx^2 + dy^2 < 10^2) | ||
401 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | ||
402 | } | ||
403 | |||
404 | @QueryBasedFeature | ||
405 | pattern dist_med(a1: Actor, a2: Actor) { | ||
406 | find helper_actorsAreMed(a1, a2); | ||
407 | Actor.dist_med(a1, a2); | ||
408 | } | ||
409 | |||
410 | private pattern helper_actorsAreMed(a1: Actor, a2: Actor) { | ||
411 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
412 | //check(10^2 < dx^2 + dy^2 < 15^2) | ||
413 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | ||
414 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
415 | } | ||
416 | |||
417 | @QueryBasedFeature | ||
418 | pattern dist_far(a1: Actor, a2: Actor) { | ||
419 | find helper_actorsAreFar(a1, a2); | ||
420 | Actor.dist_far(a1, a2); | ||
421 | } | ||
422 | |||
423 | private pattern helper_actorsAreFar(a1: Actor, a2: Actor) { | ||
424 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
425 | //check(dx^2 + dy^2 > 20^2) | ||
426 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); | ||
427 | } | ||
428 | |||
429 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
430 | //Relation | ||
431 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
432 | |||
433 | @Constraint(severity="error", key={a1, a2}, message="1 Relation") | ||
434 | pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { | ||
435 | Relation.source(r, a1); | ||
436 | Relation.target(r, a2); | ||
437 | a1 == a2; | ||
438 | } | ||
439 | |||
440 | //TODO do above but transitively?/ | ||
441 | //////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
442 | //CollisionExists | ||
443 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
444 | |||
445 | |||
446 | //<<QUALTATIF ABSTRACTION>> | ||
447 | |||
448 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
449 | pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { | ||
450 | CollisionExists.source(ce, a1); | ||
451 | CollisionExists.target(ce, a2); | ||
452 | Actor.placedOn(a1, vl1); | ||
453 | Lane_Vertical(vl1); | ||
454 | Actor.placedOn(a2, vl2); | ||
455 | Lane_Vertical(vl2); | ||
456 | } or { | ||
457 | CollisionExists.source(ce, a1); | ||
458 | CollisionExists.target(ce, a2); | ||
459 | Actor.placedOn(a1, hl1); | ||
460 | Lane_Horizontal(hl1); | ||
461 | Actor.placedOn(a2, hl2); | ||
462 | Lane_Horizontal(hl2); | ||
463 | } | ||
464 | |||
465 | //<<END TEMP QUALITATIF ABSTRACTION>> | ||
466 | |||
467 | //// | ||
468 | //VS VisionBlocked | ||
469 | //// | ||
470 | //TODO Very prone to corner cases | ||
471 | /* | ||
472 | @Constraint(severity="error", key={a1}, message="x") | ||
473 | pattern collisionExists_vsVisionBlockedX1(a1:Actor) { | ||
474 | VisionBlocked.blockedBy(_, a1); | ||
475 | CollisionExists.target(_, a1); | ||
476 | } | ||
477 | @Constraint(severity="error", key={a1}, message="x") | ||
478 | pattern collisionExists_vsVisionBlockedX2(a1:Actor) { | ||
479 | VisionBlocked.blockedBy(_, a1); | ||
480 | CollisionExists.source(_, a1); | ||
481 | } | ||
482 | |||
483 | @Constraint(severity="error", key={a1}, message="x") | ||
484 | pattern collisionExists_vsVisionBlocked1(a1:Actor) { | ||
485 | VisionBlocked.source(_, a1); | ||
486 | neg find helper_source(a1); | ||
487 | } | ||
488 | private pattern helper_source(a1:Actor) { | ||
489 | CollisionExists.source(_, a1); | ||
490 | } | ||
491 | |||
492 | @Constraint(severity="error", key={a1}, message="x") | ||
493 | pattern collisionExists_vsVisionBlocked2(a1:Actor) { | ||
494 | VisionBlocked.target(_, a1); | ||
495 | neg find helper_target(a1); | ||
496 | } | ||
497 | private pattern helper_target(a1:Actor) { | ||
498 | CollisionExists.target(_, a1); | ||
499 | } | ||
500 | */ | ||
501 | /* | ||
502 | @Constraint(severity="error", key={a1}, message="x") | ||
503 | pattern collisionExists_vsVisionBlocked(a1:Actor) { | ||
504 | VisionBlocked.source(vb, a1); | ||
505 | VisionBlocked.target(vb, a2); | ||
506 | CollisionExists.source(ce, a1); | ||
507 | CollisionExists.target(ce, a3); | ||
508 | a2 != a3; | ||
509 | } or { | ||
510 | VisionBlocked.source(vb, a1); | ||
511 | VisionBlocked.target(vb, a2); | ||
512 | CollisionExists.source(ce, a3); | ||
513 | CollisionExists.target(ce, a1); | ||
514 | a2 != a3; | ||
515 | } or { | ||
516 | VisionBlocked.source(vb, a2); | ||
517 | VisionBlocked.target(vb, a1); | ||
518 | CollisionExists.source(ce, a3); | ||
519 | CollisionExists.target(ce, a1); | ||
520 | a2 != a3; | ||
521 | } or { | ||
522 | VisionBlocked.source(vb, a2); | ||
523 | VisionBlocked.target(vb, a1); | ||
524 | CollisionExists.source(ce, a1); | ||
525 | CollisionExists.target(ce, a3); | ||
526 | a2 != a3; | ||
527 | } | ||
528 | */ | ||
529 | //<<END QUALITATIF ABSTRACTION>> | ||
530 | |||
531 | //// | ||
532 | //CollisionExists - Time | ||
533 | //// | ||
534 | |||
535 | |||
536 | @Constraint(severity="error", key={c}, message="x") | ||
537 | pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { | ||
538 | CrossingScenario.relations(ss, c); | ||
539 | CrossingScenario.maxTime(ss, maxTime); | ||
540 | CollisionExists.collisionTime(c, cTime); | ||
541 | check(cTime >= maxTime);} | ||
542 | |||
543 | @Constraint(severity="error", key={c}, message="x") | ||
544 | pattern collisionExists_timeNotNegative(c:CollisionExists) { | ||
545 | CollisionExists. collisionTime(c, cTime); | ||
546 | check(cTime <= 0.0);} | ||
547 | |||
548 | //// | ||
549 | //CollisionExists - Physical Positioniung | ||
550 | //// | ||
551 | |||
552 | private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) { | ||
553 | CollisionExists.source(c, a1); | ||
554 | CollisionExists.target(c, a2); | ||
555 | CollisionExists. collisionTime(c, cTime); | ||
556 | } | ||
557 | |||
558 | private pattern helper_getYCoords(a:Actor, l:java Double, | ||
559 | yPos:java Double, ySpeed:java Double) { | ||
560 | |||
561 | Actor.length(a, l); | ||
562 | Actor.yPos(a, yPos); | ||
563 | Actor.ySpeed(a, ySpeed); | ||
564 | } | ||
565 | |||
566 | private pattern helper_getAllYCoords(a1:Actor, a2: Actor, | ||
567 | l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double, | ||
568 | ySpeed1:java Double, ySpeed2:java Double) { | ||
569 | |||
570 | CollisionExists.source(c, a1); | ||
571 | CollisionExists.target(c, a2); | ||
572 | find helper_getYCoords(a1, l1, yPos1, ySpeed1); | ||
573 | find helper_getYCoords(a2, l2, yPos2, ySpeed2); | ||
574 | } | ||
575 | |||
576 | private pattern helper_getXCoords(a:Actor, l:java Double, | ||
577 | xPos:java Double, xSpeed:java Double) { | ||
578 | |||
579 | Actor.length(a, l); | ||
580 | Actor.xPos(a, xPos); | ||
581 | Actor.xSpeed(a, xSpeed); | ||
582 | } | ||
583 | |||
584 | private pattern helper_getAllXCoords(a1:Actor, a2: Actor, | ||
585 | w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double, | ||
586 | xSpeed1:java Double, xSpeed2:java Double) { | ||
587 | |||
588 | CollisionExists.source(c, a1); | ||
589 | CollisionExists.target(c, a2); | ||
590 | find helper_getXCoords(a1, w1, xPos1, xSpeed1); | ||
591 | find helper_getXCoords(a2, w2, xPos2, xSpeed2); | ||
592 | } | ||
593 | |||
594 | @Constraint(severity="error", key={a1}, message="x") | ||
595 | pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) { | ||
596 | |||
597 | find helper_getCollExistsTime(a1, a2, cTime); | ||
598 | find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | ||
599 | |||
600 | //check(y_1_bottom > y_2_top | ||
601 | check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); | ||
602 | } | ||
603 | |||
604 | @Constraint(severity="error", key={a1}, message="x") | ||
605 | pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) { | ||
606 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
607 | |||
608 | find helper_getCollExistsTime(a1, a2, cTime); | ||
609 | find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | ||
610 | |||
611 | //check(y_1_top < y_2_bottom) | ||
612 | check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); | ||
613 | } | ||
614 | |||
615 | @Constraint(severity="error", key={a1}, message="x") | ||
616 | pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) { | ||
617 | |||
618 | find helper_getCollExistsTime(a1, a2, cTime); | ||
619 | find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | ||
620 | |||
621 | //check(x_1_left > x_2_right) | ||
622 | check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); | ||
623 | } | ||
624 | |||
625 | @Constraint(severity="error", key={a1}, message="x") | ||
626 | pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { | ||
627 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
628 | |||
629 | find helper_getCollExistsTime(a1, a2, cTime); | ||
630 | find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | ||
631 | |||
632 | //check(x_1_right < x_2_left) | ||
633 | check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | ||
634 | } | ||
635 | |||
636 | |||
637 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
638 | //VisionBlocked | ||
639 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
640 | |||
641 | //<<QUALTATIF ABSTRACTION>> | ||
642 | |||
643 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
644 | pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { | ||
645 | VisionBlocked.source(vb, a1); | ||
646 | VisionBlocked.target(vb, a2); | ||
647 | Actor.placedOn(a1, l); | ||
648 | Actor.placedOn(a2, l); | ||
649 | } or { | ||
650 | VisionBlocked.source(vb, a1); | ||
651 | VisionBlocked.blockedBy(vb, a2); | ||
652 | Actor.placedOn(a1, l); | ||
653 | Actor.placedOn(a2, l); | ||
654 | } or { | ||
655 | VisionBlocked.blockedBy(vb, a1); | ||
656 | VisionBlocked.target(vb, a2); | ||
657 | Actor.placedOn(a1, l); | ||
658 | Actor.placedOn(a2, l); | ||
659 | } | ||
660 | |||
661 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
662 | pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { | ||
663 | VisionBlocked.source(ce, a1); | ||
664 | VisionBlocked.target(ce, a2); | ||
665 | Actor.placedOn(a1, vl1); | ||
666 | Lane_Vertical(vl1); | ||
667 | Actor.placedOn(a2, vl2); | ||
668 | Lane_Vertical(vl2); | ||
669 | } or { | ||
670 | VisionBlocked.source(ce, a1); | ||
671 | VisionBlocked.target(ce, a2); | ||
672 | Actor.placedOn(a1, hl1); | ||
673 | Lane_Horizontal(hl1); | ||
674 | Actor.placedOn(a2, hl2); | ||
675 | Lane_Horizontal(hl2); | ||
676 | } | ||
677 | |||
678 | //<<END QUALITATIF ABSTRACTION>> | ||
679 | |||
680 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
681 | pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) { | ||
682 | VisionBlocked.source(vb, a1); | ||
683 | VisionBlocked.target(vb, a2); | ||
684 | VisionBlocked.blockedBy(vb, a2); | ||
685 | } or { | ||
686 | VisionBlocked.source(vb, a1); | ||
687 | VisionBlocked.target(vb, a2); | ||
688 | VisionBlocked.blockedBy(vb, a1); | ||
689 | } | ||
690 | |||
691 | @Constraint(severity="error", key={a1, vb}, message="x") | ||
692 | pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
693 | //REQUIRED to avoid division by 0 in next 2 queries | ||
694 | VisionBlocked.source(vb, a1); | ||
695 | VisionBlocked.target(vb, a2); | ||
696 | |||
697 | Actor.xPos(a1, x1); | ||
698 | Actor.xPos(a2, x2); | ||
699 | |||
700 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | ||
701 | check(x1 == x2); | ||
702 | } | ||
703 | |||
704 | //TODO refactor? | ||
705 | @Constraint(severity="error", key={a1, vb}, message="x") | ||
706 | pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
707 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
708 | VisionBlocked.source(vb, a1); | ||
709 | VisionBlocked.target(vb, a2); | ||
710 | VisionBlocked.blockedBy(vb, aBlocker); | ||
711 | |||
712 | Actor.xPos(a1, x1); | ||
713 | Actor.yPos(a1, y1); | ||
714 | Actor.xPos(a2, x2); | ||
715 | Actor.yPos(a2, y2); | ||
716 | Actor.xPos(aBlocker, xBlocker); | ||
717 | Actor.yPos(aBlocker, yBlocker); | ||
718 | Actor.length(aBlocker, lenBlocker); | ||
719 | Actor.width(aBlocker, widBlocker); | ||
720 | |||
721 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | ||
722 | check( | ||
723 | ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / | ||
724 | ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) | ||
725 | < ((y1-y2)/(x1-x2))); | ||
726 | } | ||
727 | |||
728 | //TODO refactor? | ||
729 | @Constraint(severity="error", key={a1, vb}, message="x") | ||
730 | pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
731 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
732 | VisionBlocked.source(vb, a1); | ||
733 | VisionBlocked.target(vb, a2); | ||
734 | VisionBlocked.blockedBy(vb, aBlocker); | ||
735 | |||
736 | Actor.xPos(a1, x1); | ||
737 | Actor.yPos(a1, y1); | ||
738 | Actor.xPos(a2, x2); | ||
739 | Actor.yPos(a2, y2); | ||
740 | Actor.xPos(aBlocker, xBlocker); | ||
741 | Actor.yPos(aBlocker, yBlocker); | ||
742 | Actor.length(aBlocker, lenBlocker); | ||
743 | Actor.width(aBlocker, widBlocker); | ||
744 | |||
745 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | ||
746 | check( | ||
747 | ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / | ||
748 | ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) | ||
749 | > ((y1-y2)/(x1-x2))); | ||
750 | } | ||
751 | |||
752 | //TODO refactor? | ||
753 | //TODO CORNER CASES | ||
754 | @Constraint(severity="error", key={a1, vb}, message="x") | ||
755 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
756 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
757 | VisionBlocked.source(vb, a1); | ||
758 | VisionBlocked.target(vb, a2); | ||
759 | VisionBlocked.blockedBy(vb, aBlocker); | ||
760 | |||
761 | Actor.xPos(a1, x1); | ||
762 | Actor.xPos(a2, x2); | ||
763 | Actor.xPos(aBlocker, xBlocker); | ||
764 | |||
765 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | ||
766 | //TODO implement ABSOLUTE VALUE or MULTI-CHECK | ||
767 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); | ||
768 | } | ||
769 | |||
770 | //TODO refactor? | ||
771 | //TODO CORNER CASES | ||
772 | @Constraint(severity="error", key={a1, vb}, message="x") | ||
773 | pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
774 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
775 | VisionBlocked.source(vb, a2); | ||
776 | VisionBlocked.target(vb, a1); | ||
777 | VisionBlocked.blockedBy(vb, aBlocker); | ||
778 | |||
779 | Actor.xPos(a1, x1); | ||
780 | Actor.xPos(a2, x2); | ||
781 | Actor.xPos(aBlocker, xBlocker); | ||
782 | |||
783 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | ||
784 | //TODO implement ABSOLUTE VALUE or MULTI-CHECK | ||
785 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); | ||
786 | } | ||
787 | |||
788 | //TODO same as above for Y??? | ||
789 | //TODO same as above for Y ???? | ||
790 | |||
791 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
792 | //SeparationDistance | ||
793 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
794 | /* | ||
795 | private pattern helper_getSeperateActorsCoords(a1:Actor, | ||
796 | a2: Actor, sd:SeparationDistance, | ||
797 | x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | ||
798 | SeperationDistance.source(sd, a1); | ||
799 | SeparationDistance.target(sd, a2); | ||
800 | |||
801 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
802 | } | ||
803 | |||
804 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
805 | pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
806 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
807 | |||
808 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
809 | SeparationDistance.distance(sd, Distance::D_Near); | ||
810 | |||
811 | //check(dx^2 + dy^2 < 5^2) | ||
812 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); | ||
813 | } | ||
814 | |||
815 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
816 | pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
817 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
818 | |||
819 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
820 | SeparationDistance.distance(sd, Distance::D_Near); | ||
821 | |||
822 | //check(dx^2 + dy^2 > 10^2) | ||
823 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | ||
824 | } | ||
825 | |||
826 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
827 | pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
828 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
829 | |||
830 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
831 | SeparationDistance.distance(sd, Distance::D_Med); | ||
832 | |||
833 | //check(dx^2 + dy^2 < 10^2) | ||
834 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | ||
835 | } | ||
836 | |||
837 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
838 | pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
839 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
840 | |||
841 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
842 | SeparationDistance.distance(sd, Distance::D_Med); | ||
843 | |||
844 | //check(dx^2 + dy^2 > 1^2) | ||
845 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); | ||
846 | } | ||
847 | |||
848 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
849 | pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
850 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
851 | |||
852 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
853 | SeparationDistance.distance(sd, Distance::D_Far); | ||
854 | |||
855 | //check(dx^2 + dy^2 < 15^2) | ||
856 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
857 | } | ||
858 | */ | ||
859 | |||
860 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
861 | //CollisionDoesNotExist | ||
862 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
863 | /* | ||
864 | //TODO | ||
865 | @Constraint(severity="error", key={a1, cdne}, message="x") | ||
866 | pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) { | ||
867 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
868 | |||
869 | CrossingScenario.actors(ss, a1); | ||
870 | CrossingScenario.actors(ss, a2); | ||
871 | Actor.relations(a1, cdne); | ||
872 | CollisionDoesNotExist.target(cdne, a2); | ||
873 | CrossingScenario.maxTime(ss, maxTime); | ||
874 | |||
875 | Actor.width(a1, w1); | ||
876 | Actor.length(a1, l1); | ||
877 | Actor.xPos(a1, xPos1); | ||
878 | Actor.yPos(a1, yPos1); | ||
879 | Actor.xSpeed(a1, xSpeed1); | ||
880 | Actor.ySpeed(a1, ySpeed1); | ||
881 | |||
882 | Actor.width(a2, w2); | ||
883 | Actor.length(a2, l2); | ||
884 | Actor.xPos(a2, xPos2); | ||
885 | Actor.yPos(a2, yPos2); | ||
886 | Actor.xSpeed(a2, xSpeed2); | ||
887 | Actor.ySpeed(a2, ySpeed2); | ||
888 | //check(dx^2 + dy^2 < 15^2) | ||
889 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
890 | } | ||
891 | */ \ No newline at end of file | ||