diff options
Diffstat (limited to 'Domains/crossingScenario/queries/crossingScenarioQueries.vql')
-rw-r--r-- | Domains/crossingScenario/queries/crossingScenarioQueries.vql | 900 |
1 files changed, 506 insertions, 394 deletions
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index 34eff55c..179da874 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql | |||
@@ -14,160 +14,172 @@ import "http://www.eclipse.org/emf/2002/Ecore" | |||
14 | //CrossingScenario | 14 | //CrossingScenario |
15 | ///////////// | 15 | ///////////// |
16 | 16 | ||
17 | /* | ||
17 | //TODO Hard-code xSize? | 18 | //TODO Hard-code xSize? |
18 | //TODO Hard-code ySize? | 19 | //TODO Hard-code ySize? |
19 | 20 | ||
20 | //TODO Hard-code maxTime? | 21 | //TODO Hard-code maxTime? |
21 | //@Constraint(severity="error", key={l}, message="3 CrossingScenari") | 22 | @Constraint(severity="error", key={l}, message="3 CrossingScenari") |
22 | //pattern define_cs_maxTime(cs:CrossingScenario) { | 23 | pattern define_cs_maxTime(cs:CrossingScenario) { |
23 | // CrossingScenario.maxTime(cs, mt); | 24 | CrossingScenario.maxTime(cs, mt); |
24 | // check(mt != 60.0); | 25 | check(mt != 60.0); |
25 | //} | ||
26 | |||
27 | |||
28 | ////////////// | ||
29 | //Lane | ||
30 | ////////////// | ||
31 | |||
32 | @Constraint(severity="error", key={l}, message="1 Lane") | ||
33 | pattern define_numWidth_small(l : Lane) { | ||
34 | Lane.width(l, Size::S_Small); | ||
35 | Lane.numWidth(l, nw); | ||
36 | check(nw <= 5.0); | ||
37 | } or { | ||
38 | Lane.width(l, Size::S_Small); | ||
39 | Lane.numWidth(l, nw); | ||
40 | check(nw >= 10.0); | ||
41 | } | 26 | } |
27 | */ | ||
42 | 28 | ||
43 | @Constraint(severity="error", key={l}, message="2 Lane") | 29 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
44 | pattern define_numWidth_medium(l : Lane) { | 30 | //Lane |
45 | Lane.width(l, ::S_Med); | 31 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
46 | Lane.numWidth(l, nw); | 32 | /* |
47 | check(nw <= 10.0); | 33 | |
48 | } | 34 | ////<<<<OLD>>>> |
49 | or { | 35 | ////Width: Different Lanes |
50 | Lane.width(l, Size::S_Med); | 36 | //@Constraint(severity="error", key={l}, message="1 Lane") |
51 | Lane.numWidth(l, nw); | 37 | //pattern define_numWidth_small(l : Lane) { |
52 | check(nw >= 15.0); | 38 | // Lane.width(l, Size::S_Small); |
53 | } | 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 | //} | ||
54 | 70 | ||
55 | @Constraint(severity="error", key={l}, message="3 Lane") | 71 | //<<<<NEW>>>> |
56 | pattern define_numWidth_large(l : Lane) { | 72 | //Width is FIXED: always 5 |
57 | Lane.width(l, Size::S_Large); | ||
58 | Lane.numWidth(l, nw); | ||
59 | check(nw <= 15.0); | ||
60 | } | ||
61 | or { | ||
62 | Lane.width(l, Size::S_Large); | ||
63 | Lane.numWidth(l, nw); | ||
64 | check(nw >= 20.0); | ||
65 | } | ||
66 | 73 | ||
67 | /////////////Prevlane | 74 | /////////////Prevlane |
68 | 75 | ||
69 | ////////head lanes do not have prevLane | 76 | ////<<<<OLD>>>> |
70 | @Constraint(severity="error", key={l}, message="6.1 Lane") | 77 | ////Generating 2 linkedlists (1 for horizontal, 1 for vertical lanes) |
71 | pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) { | 78 | //////////head lanes do not have prevLane |
72 | CrossingScenario.vertical_head(cs, l); | 79 | //@Constraint(severity="error", key={l}, message="6.1 Lane") |
73 | Lane.prevLane(l, _); | 80 | //pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) { |
74 | } | 81 | // CrossingScenario.vertical_head(cs, l); |
75 | 82 | // Lane.prevLane(l, _); | |
76 | @Constraint(severity="error", key={l}, message="6.2 Lane") | 83 | //} |
77 | pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) { | 84 | // |
78 | CrossingScenario.horizontal_head(cs, l); | 85 | //@Constraint(severity="error", key={l}, message="6.2 Lane") |
79 | Lane.prevLane(l, _); | 86 | //pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) { |
80 | } | 87 | // CrossingScenario.horizontal_head(cs, l); |
81 | 88 | // Lane.prevLane(l, _); | |
82 | ////////Non-head lanes must have prevLane | 89 | //} |
83 | @Constraint(severity="error", key={l}, message="6.1 Lane") | 90 | // |
84 | pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) { | 91 | //////////Non-head lanes must have prevLane |
85 | neg find find_headVertLane(l); | 92 | //@Constraint(severity="error", key={l}, message="6.1 Lane") |
86 | neg find find_laneWithPrevLane(l); | 93 | //pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) { |
87 | } | 94 | // neg find find_headVertLane(l); |
88 | 95 | // neg find find_laneWithPrevLane(l); | |
89 | @Constraint(severity="error", key={l}, message="6.1 Lane") | 96 | //} |
90 | pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) { | 97 | // |
91 | neg find find_headHoriLane(l); | 98 | //@Constraint(severity="error", key={l}, message="6.1 Lane") |
92 | neg find find_laneWithPrevLane(l); | 99 | //pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) { |
93 | } | 100 | // neg find find_headHoriLane(l); |
94 | 101 | // neg find find_laneWithPrevLane(l); | |
95 | private pattern find_headVertLane(l:Lane_Vertical) { | 102 | //} |
96 | CrossingScenario.vertical_head(_, l); | 103 | // |
97 | } | 104 | //private pattern find_headVertLane(l:Lane_Vertical) { |
98 | private pattern find_headHoriLane(l:Lane_Horizontal) { | 105 | // CrossingScenario.vertical_head(_, l); |
99 | CrossingScenario.horizontal_head(_, l); | 106 | //} |
100 | } | 107 | //private pattern find_headHoriLane(l:Lane_Horizontal) { |
101 | private pattern find_laneWithPrevLane(l:Lane) { | 108 | // CrossingScenario.horizontal_head(_, l); |
102 | Lane.prevLane(l, _); | 109 | //} |
103 | } | 110 | //private pattern find_laneWithPrevLane(l:Lane) { |
104 | 111 | // Lane.prevLane(l, _); | |
105 | /////////Lane cannot be its own recursive prevLane | 112 | //} |
106 | @Constraint(severity="error", key={l}, message="6.1 Lane") | 113 | // |
107 | pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) { | 114 | ///////////Lane cannot be its own recursive prevLane |
108 | Lane.prevLane(l, l); | 115 | //@Constraint(severity="error", key={l}, message="6.1 Lane") |
109 | } | 116 | //pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) { |
110 | 117 | // Lane.prevLane(l, l); | |
111 | @Constraint(severity="error", key={l}, message="6.2 Lane") | 118 | //} |
112 | pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) { | 119 | // |
113 | find find_prevLane+(l, l); | 120 | //@Constraint(severity="error", key={l}, message="6.2 Lane") |
114 | } | 121 | //pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) { |
115 | private pattern find_prevLane(l1:Lane, l2:Lane) { | 122 | // find find_prevLane+(l, l); |
116 | Lane.prevLane(l1, l2); | 123 | //} |
117 | } | 124 | //private pattern find_prevLane(l1:Lane, l2:Lane) { |
118 | 125 | // Lane.prevLane(l1, l2); | |
119 | //////Lane cannot be prevLane of >1 other lane | 126 | //} |
120 | @Constraint(severity="error", key={l1, l2}, message="7 Lane") | 127 | // |
121 | pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) { | 128 | ////////Lane cannot be prevLane of >1 other lane |
122 | Lane.prevLane(l1, l); | 129 | //@Constraint(severity="error", key={l1, l2}, message="7 Lane") |
123 | Lane.prevLane(l2, l); | 130 | //pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) { |
124 | l1 != l2; | 131 | // Lane.prevLane(l1, l); |
125 | } | 132 | // Lane.prevLane(l2, l); |
126 | 133 | // l1 != l2; | |
127 | //////consecutive lanes must have same orientation | 134 | //} |
128 | @Constraint(severity="error", key={l1, l2}, message="8 Lane") | 135 | // |
129 | pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) { | 136 | ////////consecutive lanes must have same orientation |
130 | Lane.prevLane(l1, l2); | 137 | //@Constraint(severity="error", key={l1, l2}, message="8 Lane") |
131 | } | 138 | //pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) { |
132 | 139 | // Lane.prevLane(l1, l2); | |
133 | @Constraint(severity="error", key={l1, l2}, message="8 Lane") | 140 | //} |
134 | pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) { | 141 | // |
135 | Lane.prevLane(l1, l2); | 142 | //@Constraint(severity="error", key={l1, l2}, message="8 Lane") |
136 | } | 143 | //pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) { |
137 | 144 | // Lane.prevLane(l1, l2); | |
138 | /////////////ReferenceCoord | 145 | //} |
139 | 146 | // | |
140 | /////refCoord of head lanes must be 0 | 147 | ///////////////ReferenceCoord |
141 | @Constraint(severity="error", key={l}, message="6.2 Lane") | 148 | // |
142 | pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) { | 149 | ///////refCoord of head lanes must be 0 |
143 | CrossingScenario.horizontal_head(cs, l); | 150 | //@Constraint(severity="error", key={l}, message="6.2 Lane") |
144 | Lane.referenceCoord(l, rc); | 151 | //pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) { |
145 | check(rc != 0.0); | 152 | // CrossingScenario.horizontal_head(cs, l); |
146 | } | 153 | // Lane.referenceCoord(l, rc); |
147 | 154 | // check(rc != 0.0); | |
148 | @Constraint(severity="error", key={l}, message="6.2 Lane") | 155 | //} |
149 | pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) { | 156 | // |
150 | CrossingScenario.vertical_head(cs, l); | 157 | //@Constraint(severity="error", key={l}, message="6.2 Lane") |
151 | Lane.referenceCoord(l, rc); | 158 | //pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) { |
152 | check(rc != 0.0); | 159 | // CrossingScenario.vertical_head(cs, l); |
153 | } | 160 | // Lane.referenceCoord(l, rc); |
154 | 161 | // check(rc != 0.0); | |
155 | //////refCoord of a lane is prevLane.rc + curLane.numWidth | 162 | //} |
156 | 163 | // | |
157 | @Constraint(severity="error", key={l}, message="6.2 Lane") | 164 | ////////refCoord of a lane is prevLane.rc + curLane.numWidth |
158 | pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) { | 165 | // |
159 | Lane.prevLane(l, prev); | 166 | //@Constraint(severity="error", key={l}, message="6.2 Lane") |
160 | Lane.referenceCoord(l, rcCur); | 167 | //pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) { |
161 | 168 | // Lane.prevLane(l, prev); | |
162 | Lane.numWidth(prev, wPrev); | 169 | // Lane.referenceCoord(l, rcCur); |
163 | Lane.referenceCoord(prev, rcPrev); | 170 | // |
164 | check(rcCur != rcPrev + wPrev); | 171 | // Lane.numWidth(prev, wPrev); |
165 | } | 172 | // Lane.referenceCoord(prev, rcPrev); |
173 | // check(rcCur != rcPrev + wPrev); | ||
174 | //} | ||
166 | 175 | ||
176 | //<<<<NEW>>>> | ||
177 | //Lanes are all predefind | ||
178 | */ | ||
167 | 179 | ||
168 | ////////////// | 180 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
169 | //Lane+Actor | 181 | //Lane+Actor |
170 | ////////////// | 182 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
171 | 183 | ||
172 | /////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] | 184 | /////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] |
173 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | 185 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") |
@@ -180,8 +192,12 @@ pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { | |||
180 | Actor.placedOn(a, vl); | 192 | Actor.placedOn(a, vl); |
181 | Actor.xPos(a, x); | 193 | Actor.xPos(a, x); |
182 | Lane.referenceCoord(vl, r); | 194 | Lane.referenceCoord(vl, r); |
183 | Lane.numWidth(vl, w); | 195 | // //<<<<OLD>>>> |
184 | check(x >= (r + w)); | 196 | // Lane.numWidth(vl, w); |
197 | // check(x >= (r + w)); | ||
198 | |||
199 | //<<<<NEW>>>>: lanes all have width=5 | ||
200 | check(x >= (r + 5.0)); | ||
185 | } | 201 | } |
186 | 202 | ||
187 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | 203 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") |
@@ -192,62 +208,88 @@ pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { | |||
192 | check(y <= r); | 208 | check(y <= r); |
193 | } or { | 209 | } or { |
194 | Actor.placedOn(a, hl); | 210 | Actor.placedOn(a, hl); |
195 | Actor.yPos(a, y); | 211 | Actor.yPos(a, y); |
196 | Lane.referenceCoord(hl, r); | 212 | Lane.referenceCoord(hl, r); |
197 | Lane.numWidth(hl, w); | 213 | // //<<OLD>> |
198 | check(y >= (r + w)); | 214 | // Lane.numWidth(hl, w); |
215 | // check(y >= (r + w)); | ||
216 | |||
217 | //<<NEW>> | ||
218 | check(y >= (r + 5.0)); | ||
219 | |||
199 | } | 220 | } |
200 | 221 | ||
201 | ////////////// | 222 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
202 | //Actor | 223 | //Actor |
203 | ////////////// | 224 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
204 | 225 | ||
205 | //Hard-coded stuff | 226 | //Xpos and Ypos Bounds |
206 | //TODO THIS IS HARD_CODED | ||
207 | @Constraint(severity="error", key={a}, message="x") | ||
208 | pattern define_actor_maxXp(a:Actor) { | ||
209 | Actor.xPos(a, xP); | ||
210 | check(xP >= 1000.0);} | ||
211 | 227 | ||
212 | @Constraint(severity="error", key={a}, message="x") | 228 | private pattern helper_getXAndBounds(cs:CrossingScenario, a:Actor, |
213 | pattern define_actor_minXp(a:Actor) { | 229 | xMax:java Double, xP:java Double) { |
230 | CrossingScenario.actors(cs, a); | ||
231 | CrossingScenario.xSize(cs, xMax); | ||
214 | Actor.xPos(a, xP); | 232 | Actor.xPos(a, xP); |
215 | check(xP <= 0-1000.0);} | 233 | } |
216 | 234 | ||
217 | //TODO THIS IS HARD_CODED | 235 | private pattern helper_getYAndBounds(cs:CrossingScenario, a:Actor, |
218 | @Constraint(severity="error", key={a}, message="x") | 236 | yMax:java Double, yP:java Double) { |
219 | pattern define_actor_maxYp(a:Actor) { | 237 | CrossingScenario.actors(cs, a); |
220 | Actor.yPos(a, yP); | 238 | CrossingScenario.ySize(cs, yMax); |
221 | check(yP >= 1000.0);} | ||
222 | |||
223 | @Constraint(severity="error", key={a}, message="x") | ||
224 | pattern define_actor_minYp(a:Actor) { | ||
225 | Actor.yPos(a, yP); | 239 | Actor.yPos(a, yP); |
226 | check(yP <= 0-1000.0);} | 240 | } |
241 | |||
242 | @Constraint(severity="error", key={cs}, message="x") | ||
243 | pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { | ||
244 | Actor.placedOn(a, hl); | ||
245 | Lane_Horizontal(hl); | ||
246 | find helper_getXAndBounds(cs, a, xMax, xP); | ||
247 | check(xP >= xMax);} | ||
248 | |||
249 | @Constraint(severity="error", key={cs}, message="x") | ||
250 | pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { | ||
251 | Actor.placedOn(a, hl); | ||
252 | Lane_Horizontal(hl); | ||
253 | find helper_getXAndBounds(cs, a, xMax, xP); | ||
254 | check(xP <= 0-xMax);} | ||
227 | 255 | ||
228 | //TODO THIS IS HARD_CODED | 256 | @Constraint(severity="error", key={cs}, message="x") |
229 | @Constraint(severity="error", key={a}, message="x") | 257 | pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { |
230 | pattern define_actor_maxXs(a:Actor) { | 258 | Actor.placedOn(a, vl); |
231 | Actor.xSpeed(a, xS); | 259 | Lane_Vertical(vl); |
232 | check(xS >= 100.0);} | 260 | find helper_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 | Actor.placedOn(a, vl); | ||
266 | Lane_Vertical(vl); | ||
267 | find helper_getYAndBounds(cs, a, yMax, yP); | ||
268 | check(yP <= 0-yMax);} | ||
233 | 269 | ||
234 | @Constraint(severity="error", key={a}, message="x") | 270 | //Xspeed and Yspeed bounds |
235 | pattern define_actor_minXs(a:Actor) { | ||
236 | Actor.xSpeed(a, xS); | ||
237 | check(xS <= 0-100.0);} | ||
238 | 271 | ||
239 | //TODO THIS IS HARD_CODED | 272 | //TODO THIS IS HARD_CODED |
240 | @Constraint(severity="error", key={a}, message="x") | 273 | //@Constraint(severity="error", key={a}, message="x") |
241 | pattern define_actor_maxYs(a:Actor) { | 274 | //pattern define_actor_maxXs(a:Actor) { |
242 | Actor.ySpeed(a, yS); | 275 | // Actor.xSpeed(a, xS); |
243 | check(yS >= 100.0);} | 276 | // check(xS >= 100.0);} |
244 | 277 | // | |
245 | @Constraint(severity="error", key={a}, message="x") | 278 | //@Constraint(severity="error", key={a}, message="x") |
246 | pattern define_actor_minYs(a:Actor) { | 279 | //pattern define_actor_minXs(a:Actor) { |
247 | Actor.ySpeed(a, yS); | 280 | // Actor.xSpeed(a, xS); |
248 | check(yS <= 0-100.0);} | 281 | // check(xS <= 0-100.0);} |
249 | 282 | // | |
250 | 283 | ////TODO THIS IS HARD_CODED | |
284 | //@Constraint(severity="error", key={a}, message="x") | ||
285 | //pattern define_actor_maxYs(a:Actor) { | ||
286 | // Actor.ySpeed(a, yS); | ||
287 | // check(yS >= 100.0);} | ||
288 | // | ||
289 | //@Constraint(severity="error", key={a}, message="x") | ||
290 | //pattern define_actor_minYs(a:Actor) { | ||
291 | // Actor.ySpeed(a, yS); | ||
292 | // check(yS <= 0-100.0);} | ||
251 | //END Hard-coded stuff | 293 | //END Hard-coded stuff |
252 | 294 | ||
253 | ////TODO May be required | 295 | ////TODO May be required |
@@ -323,237 +365,218 @@ pattern define_actor_actorOnHoriLaneHasySpeed0(a:Actor, hl:Lane_Horizontal) { | |||
323 | check(ySpeed != 0); | 365 | check(ySpeed != 0); |
324 | } | 366 | } |
325 | 367 | ||
326 | ////////////// | 368 | //<<NEW>> Derived Features |
327 | //Relation | 369 | private pattern helper_getCoords(a1:Actor, |
328 | ////////////// | 370 | a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { |
329 | @Constraint(severity="error", key={a1, a2}, message="1 Relation") | 371 | Actor.xPos(a1, x1); |
330 | pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { | 372 | Actor.yPos(a1, y1); |
331 | Actor.relations(a1, r); | 373 | Actor.xPos(a2, x2); |
332 | Relation.target(r, a2); | 374 | Actor.yPos(a2, y2); |
333 | a1 == a2; | ||
334 | } | 375 | } |
335 | 376 | ||
336 | //TODO do above but transitively? | 377 | @QueryBasedFeature |
337 | 378 | pattern dist_near(a1: Actor, a2: Actor) { | |
338 | ////////////// | 379 | find helper_actorsAreNear(a1, a2); |
339 | //CollisionExists | 380 | Actor.dist_near(a1, a2); |
340 | ////////////// | ||
341 | |||
342 | //TODO THIS IS HARD_CODED | ||
343 | @Constraint(severity="error", key={c}, message="x") | ||
344 | pattern collisionExists_timeWithinBound(c:CollisionExists) { | ||
345 | CollisionExists. collisionTime(c, cTime); | ||
346 | check(cTime >= 60.0);} | ||
347 | |||
348 | //TODO replace above with this (more general) | ||
349 | //@Constraint(severity="error", key={c}, message="x") | ||
350 | //pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { | ||
351 | // CrossingScenario.actors.relations(ss, c); | ||
352 | // CrossingScenario.maxTime(ss, maxTime); | ||
353 | // CollisionExists. collisionTime(c, cTime); | ||
354 | // check(cTime >= maxTime);} | ||
355 | |||
356 | @Constraint(severity="error", key={c}, message="x") | ||
357 | pattern collisionExists_timeNotNegative(c:CollisionExists) { | ||
358 | CollisionExists. collisionTime(c, cTime); | ||
359 | check(cTime <= 0.0);} | ||
360 | |||
361 | @Constraint(severity="error", key={a1, c}, message="x") | ||
362 | pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) { | ||
363 | Actor.relations(a1, c); | ||
364 | CollisionExists.target(c, a2); | ||
365 | |||
366 | Actor.length(a1, l1); | ||
367 | Actor.yPos(a1, yPos1); | ||
368 | Actor.ySpeed(a1, ySpeed1); | ||
369 | Actor.length(a2, l2); | ||
370 | Actor.yPos(a2, yPos2); | ||
371 | Actor.ySpeed(a2, ySpeed2); | ||
372 | CollisionExists. collisionTime(c, cTime); | ||
373 | //check(y_1_bottom > y_2_top | ||
374 | check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); | ||
375 | } | 381 | } |
376 | 382 | ||
377 | @Constraint(severity="error", key={a1, c}, message="x") | 383 | private pattern helper_actorsAreNear(a1: Actor, a2: Actor) { |
378 | pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor, c:CollisionExists) { | 384 | find helper_getCoords(a1, a2, x1, x2, y1, y2); |
379 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 385 | //check(dx^2 + dy^2 < 10^2) |
380 | Actor.relations(a1, c); | 386 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); |
381 | CollisionExists.target(c, a2); | ||
382 | |||
383 | Actor.length(a1, l1); | ||
384 | Actor.yPos(a1, yPos1); | ||
385 | Actor.ySpeed(a1, ySpeed1); | ||
386 | Actor.length(a2, l2); | ||
387 | Actor.yPos(a2, yPos2); | ||
388 | Actor.ySpeed(a2, ySpeed2); | ||
389 | CollisionExists. collisionTime(c, cTime); | ||
390 | //check(y_1_top < y_2_bottom) | ||
391 | check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); | ||
392 | } | 387 | } |
393 | 388 | ||
394 | @Constraint(severity="error", key={a1, c}, message="x") | 389 | @QueryBasedFeature |
395 | pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) { | 390 | pattern dist_med(a1: Actor, a2: Actor) { |
396 | Actor.relations(a1, c); | 391 | find helper_actorsAreMed(a1, a2); |
397 | CollisionExists.target(c, a2); | 392 | Actor.dist_med(a1, a2); |
398 | |||
399 | Actor.width(a1, w1); | ||
400 | Actor.xPos(a1, xPos1); | ||
401 | Actor.xSpeed(a1, xSpeed1); | ||
402 | Actor.width(a2, w2); | ||
403 | Actor.xPos(a2, xPos2); | ||
404 | Actor.xSpeed(a2, xSpeed2); | ||
405 | CollisionExists. collisionTime(c, cTime); | ||
406 | //check(x_1_left > x_2_right) | ||
407 | check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); | ||
408 | } | 393 | } |
409 | 394 | ||
410 | @Constraint(severity="error", key={a1, c}, message="x") | 395 | private pattern helper_actorsAreMed(a1: Actor, a2: Actor) { |
411 | pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists) { | 396 | find helper_getCoords(a1, a2, x1, x2, y1, y2); |
412 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 397 | //check(10^2 < dx^2 + dy^2 < 15^2) |
413 | Actor.relations(a1, c); | 398 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); |
414 | CollisionExists.target(c, a2); | 399 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); |
415 | |||
416 | Actor.width(a1, w1); | ||
417 | Actor.xPos(a1, xPos1); | ||
418 | Actor.xSpeed(a1, xSpeed1); | ||
419 | Actor.width(a2, w2); | ||
420 | Actor.xPos(a2, xPos2); | ||
421 | Actor.xSpeed(a2, xSpeed2); | ||
422 | CollisionExists. collisionTime(c, cTime); | ||
423 | //check(x_1_right < x_2_left) | ||
424 | check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | ||
425 | } | 400 | } |
426 | 401 | ||
427 | ////////////// | 402 | @QueryBasedFeature |
428 | //SeparationDistance | 403 | pattern dist_far(a1: Actor, a2: Actor) { |
429 | ////////////// | 404 | find helper_actorsAreFar(a1, a2); |
430 | @Constraint(severity="error", key={a1, sd}, message="x") | 405 | Actor.dist_far(a1, a2); |
431 | pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
432 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
433 | Actor.relations(a1, sd); | ||
434 | SeparationDistance.target(sd, a2); | ||
435 | SeparationDistance.distance(sd, Distance::D_Near); | ||
436 | |||
437 | Actor.xPos(a1, x1); | ||
438 | Actor.yPos(a1, y1); | ||
439 | Actor.xPos(a2, x2); | ||
440 | Actor.yPos(a2, y2); | ||
441 | //check(dx^2 + dy^2 < 5^2) | ||
442 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); | ||
443 | } | 406 | } |
444 | 407 | ||
445 | @Constraint(severity="error", key={a1, sd}, message="x") | 408 | private pattern helper_actorsAreFar(a1: Actor, a2: Actor) { |
446 | pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | 409 | find helper_getCoords(a1, a2, x1, x2, y1, y2); |
447 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 410 | //check(dx^2 + dy^2 > 20^2) |
448 | Actor.relations(a1, sd); | 411 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); |
449 | SeparationDistance.target(sd, a2); | ||
450 | SeparationDistance.distance(sd, Distance::D_Near); | ||
451 | |||
452 | Actor.xPos(a1, x1); | ||
453 | Actor.yPos(a1, y1); | ||
454 | Actor.xPos(a2, x2); | ||
455 | Actor.yPos(a2, y2); | ||
456 | //check(dx^2 + dy^2 > 10^2) | ||
457 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | ||
458 | } | 412 | } |
459 | 413 | ||
460 | @Constraint(severity="error", key={a1, sd}, message="x") | 414 | //<<END NEW>> |
461 | pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | 415 | |
462 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 416 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
463 | Actor.relations(a1, sd); | 417 | //Relation |
464 | SeparationDistance.target(sd, a2); | 418 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
465 | SeparationDistance.distance(sd, Distance::D_Med); | ||
466 | |||
467 | Actor.xPos(a1, x1); | ||
468 | Actor.yPos(a1, y1); | ||
469 | Actor.xPos(a2, x2); | ||
470 | Actor.yPos(a2, y2); | ||
471 | //check(dx^2 + dy^2 < 10^2) | ||
472 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | ||
473 | } | ||
474 | 419 | ||
475 | @Constraint(severity="error", key={a1, sd}, message="x") | 420 | @Constraint(severity="error", key={a1, a2}, message="1 Relation") |
476 | pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | 421 | pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { |
477 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 422 | Relation.source(r, a1); |
478 | Actor.relations(a1, sd); | 423 | Relation.target(r, a2); |
479 | SeparationDistance.target(sd, a2); | 424 | a1 == a2; |
480 | SeparationDistance.distance(sd, Distance::D_Med); | ||
481 | |||
482 | Actor.xPos(a1, x1); | ||
483 | Actor.yPos(a1, y1); | ||
484 | Actor.xPos(a2, x2); | ||
485 | Actor.yPos(a2, y2); | ||
486 | //check(dx^2 + dy^2 > 1^2) | ||
487 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); | ||
488 | } | 425 | } |
489 | 426 | ||
490 | @Constraint(severity="error", key={a1, sd}, message="x") | 427 | //TODO do above but transitively?/ |
491 | pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | 428 | //////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
492 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 429 | //CollisionExists |
493 | Actor.relations(a1, sd); | 430 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
494 | SeparationDistance.target(sd, a2); | ||
495 | SeparationDistance.distance(sd, Distance::D_Far); | ||
496 | 431 | ||
497 | Actor.xPos(a1, x1); | 432 | //@Constraint(severity="error", key={c}, message="x") |
498 | Actor.yPos(a1, y1); | 433 | //pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { |
499 | Actor.xPos(a2, x2); | 434 | // CrossingScenario.relations(ss, c); |
500 | Actor.yPos(a2, y2); | 435 | // CrossingScenario.maxTime(ss, maxTime); |
501 | //check(dx^2 + dy^2 < 15^2) | 436 | // CollisionExists.collisionTime(c, cTime); |
502 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | 437 | // check(cTime >= maxTime);} |
503 | } | 438 | // |
439 | //@Constraint(severity="error", key={c}, message="x") | ||
440 | //pattern collisionExists_timeNotNegative(c:CollisionExists) { | ||
441 | // CollisionExists. collisionTime(c, cTime); | ||
442 | // check(cTime <= 0.0);} | ||
443 | // | ||
444 | //private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) { | ||
445 | // CollisionExists.source(c, a1); | ||
446 | // CollisionExists.target(c, a2); | ||
447 | // CollisionExists. collisionTime(c, cTime); | ||
448 | //} | ||
449 | // | ||
450 | //private pattern helper_getYCoords(a:Actor, l:java Double, | ||
451 | // yPos:java Double, ySpeed:java Double) { | ||
452 | // | ||
453 | // Actor.length(a, l); | ||
454 | // Actor.yPos(a, yPos); | ||
455 | // Actor.ySpeed(a, ySpeed); | ||
456 | //} | ||
457 | // | ||
458 | //private pattern helper_getAllYCoords(a1:Actor, a2: Actor, | ||
459 | // l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double, | ||
460 | // ySpeed1:java Double, ySpeed2:java Double) { | ||
461 | // | ||
462 | // find helper_getYCoords(a1, l1, yPos1, ySpeed1); | ||
463 | // find helper_getYCoords(a2, l2, yPos2, ySpeed2); | ||
464 | //} | ||
465 | // | ||
466 | //private pattern helper_getXCoords(a:Actor, l:java Double, | ||
467 | // xPos:java Double, xSpeed:java Double) { | ||
468 | // | ||
469 | // Actor.length(a, l); | ||
470 | // Actor.xPos(a, xPos); | ||
471 | // Actor.xSpeed(a, xSpeed); | ||
472 | //} | ||
473 | // | ||
474 | //private pattern helper_getAllXCoords(a1:Actor, a2: Actor, | ||
475 | // w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double, | ||
476 | // xSpeed1:java Double, xSpeed2:java Double) { | ||
477 | // | ||
478 | // find helper_getYCoords(a1, w1, xPos1, xSpeed1); | ||
479 | // find helper_getYCoords(a2, w2, xPos2, xSpeed2); | ||
480 | //} | ||
481 | // | ||
482 | //@Constraint(severity="error", key={a1}, message="x") | ||
483 | //pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) { | ||
484 | // | ||
485 | // find helper_getCollExistsTime(a1, a2, cTime); | ||
486 | // find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | ||
487 | // | ||
488 | // //check(y_1_bottom > y_2_top | ||
489 | // check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); | ||
490 | //} | ||
491 | // | ||
492 | //@Constraint(severity="error", key={a1}, message="x") | ||
493 | //pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) { | ||
494 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
495 | // | ||
496 | // find helper_getCollExistsTime(a1, a2, cTime); | ||
497 | // find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | ||
498 | // | ||
499 | // //check(y_1_top < y_2_bottom) | ||
500 | // check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); | ||
501 | //} | ||
502 | // | ||
503 | //@Constraint(severity="error", key={a1}, message="x") | ||
504 | //pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) { | ||
505 | // | ||
506 | // find helper_getCollExistsTime(a1, a2, cTime); | ||
507 | // find helper_getAllYCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | ||
508 | // | ||
509 | // //check(x_1_left > x_2_right) | ||
510 | // check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); | ||
511 | //} | ||
512 | // | ||
513 | //@Constraint(severity="error", key={a1}, message="x") | ||
514 | //pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { | ||
515 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
516 | // | ||
517 | // find helper_getCollExistsTime(a1, a2, cTime); | ||
518 | // find helper_getAllYCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | ||
519 | // | ||
520 | // //check(x_1_right < x_2_left) | ||
521 | // check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | ||
522 | //} | ||
504 | 523 | ||
505 | //////////////// | ||
506 | ////CollisionDoesNotExist | ||
507 | //////////////// | ||
508 | //TODO | ||
509 | ////@Constraint(severity="error", key={a1, cdne}, message="x") | ||
510 | ////pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) { | ||
511 | //// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
512 | //// | ||
513 | //// CrossingScenario.actors(ss, a1); | ||
514 | //// CrossingScenario.actors(ss, a2); | ||
515 | //// Actor.relations(a1, cdne); | ||
516 | //// CollisionDoesNotExist.target(cdne, a2); | ||
517 | //// CrossingScenario.maxTime(ss, maxTime); | ||
518 | //// | ||
519 | //// Actor.width(a1, w1); | ||
520 | //// Actor.length(a1, l1); | ||
521 | //// Actor.xPos(a1, xPos1); | ||
522 | //// Actor.yPos(a1, yPos1); | ||
523 | //// Actor.xSpeed(a1, xSpeed1); | ||
524 | //// Actor.ySpeed(a1, ySpeed1); | ||
525 | //// | ||
526 | //// Actor.width(a2, w2); | ||
527 | //// Actor.length(a2, l2); | ||
528 | //// Actor.xPos(a2, xPos2); | ||
529 | //// Actor.yPos(a2, yPos2); | ||
530 | //// Actor.xSpeed(a2, xSpeed2); | ||
531 | //// Actor.ySpeed(a2, ySpeed2); | ||
532 | //// //check(dx^2 + dy^2 < 15^2) | ||
533 | //// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
534 | ////} | ||
535 | 524 | ||
536 | ////////////// | 525 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
537 | //VisionBlocked | 526 | //VisionBlocked |
538 | ////////////// | 527 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
528 | |||
529 | //<<QUALTATIF ABSTRACTION>> | ||
539 | 530 | ||
540 | @Constraint(severity="error", key={a1, a2}, message="x") | 531 | @Constraint(severity="error", key={a1, a2}, message="x") |
541 | pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) { | 532 | pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { |
542 | Actor.relations(a1, vb); | 533 | VisionBlocked.source(vb, a1); |
543 | VisionBlocked.target(vb, a2); | 534 | VisionBlocked.target(vb, a2); |
535 | Actor.placedOn(a1, l); | ||
536 | Actor.placedOn(a2, l); | ||
537 | } or { | ||
538 | VisionBlocked.source(vb, a1); | ||
539 | VisionBlocked.blockedBy(vb, a2); | ||
540 | Actor.placedOn(a1, l); | ||
541 | Actor.placedOn(a2, l); | ||
542 | } or { | ||
544 | VisionBlocked.blockedBy(vb, a1); | 543 | VisionBlocked.blockedBy(vb, a1); |
544 | VisionBlocked.target(vb, a2); | ||
545 | Actor.placedOn(a1, l); | ||
546 | Actor.placedOn(a2, l); | ||
547 | } | ||
548 | //<<END QUALITATIF ABSTRACTION>> | ||
549 | |||
550 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
551 | pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) { | ||
552 | VisionBlocked.source(vb, a1); | ||
553 | VisionBlocked.target(vb, a2); | ||
554 | VisionBlocked.blockedBy(vb, a2); | ||
545 | } or { | 555 | } or { |
546 | Actor.relations(a1, vb); | 556 | VisionBlocked.source(vb, a1); |
547 | VisionBlocked.target(vb, a2); | 557 | VisionBlocked.target(vb, a2); |
548 | VisionBlocked.blockedBy(vb, a1); | 558 | VisionBlocked.blockedBy(vb, a1); |
549 | } | 559 | } |
550 | 560 | ||
561 | @Constraint(severity="error", key={a1, vb}, message="x") | ||
562 | pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
563 | //REQUIRED to avoid division by 0 in next 2 queries | ||
564 | VisionBlocked.source(vb, a1); | ||
565 | VisionBlocked.target(vb, a2); | ||
566 | |||
567 | Actor.xPos(a1, x1); | ||
568 | Actor.xPos(a2, x2); | ||
569 | |||
570 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | ||
571 | check(x1 == x2); | ||
572 | } | ||
573 | |||
551 | //OPTIONS 1: everything is from a single check expression containing ITEs | 574 | //OPTIONS 1: everything is from a single check expression containing ITEs |
552 | //Currently unhandled bygenerator | 575 | //Currently unhandled bygenerator |
553 | @Constraint(severity="error", key={a1, vb}, message="x") | 576 | @Constraint(severity="error", key={a1, vb}, message="x") |
554 | pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { | 577 | pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { |
555 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 578 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
556 | Actor.relations(a1, vb); | 579 | VisionBlocked.source(vb, a1); |
557 | VisionBlocked.target(vb, a2); | 580 | VisionBlocked.target(vb, a2); |
558 | VisionBlocked.blockedBy(vb, aBlocker); | 581 | VisionBlocked.blockedBy(vb, aBlocker); |
559 | 582 | ||
@@ -576,7 +599,7 @@ pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { | |||
576 | @Constraint(severity="error", key={a1, vb}, message="x") | 599 | @Constraint(severity="error", key={a1, vb}, message="x") |
577 | pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { | 600 | pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { |
578 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 601 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
579 | Actor.relations(a1, vb); | 602 | VisionBlocked.source(vb, a1); |
580 | VisionBlocked.target(vb, a2); | 603 | VisionBlocked.target(vb, a2); |
581 | VisionBlocked.blockedBy(vb, aBlocker); | 604 | VisionBlocked.blockedBy(vb, aBlocker); |
582 | 605 | ||
@@ -596,15 +619,104 @@ pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { | |||
596 | > ((y1-y2)/(x1-x2))); | 619 | > ((y1-y2)/(x1-x2))); |
597 | } | 620 | } |
598 | 621 | ||
622 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
623 | //SeparationDistance | ||
624 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
625 | /* | ||
626 | private pattern helper_getSeperateActorsCoords(a1:Actor, | ||
627 | a2: Actor, sd:SeparationDistance, | ||
628 | x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | ||
629 | SeperationDistance.source(sd, a1); | ||
630 | SeparationDistance.target(sd, a2); | ||
631 | |||
632 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
633 | } | ||
634 | |||
635 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
636 | pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
637 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
638 | |||
639 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
640 | SeparationDistance.distance(sd, Distance::D_Near); | ||
641 | |||
642 | //check(dx^2 + dy^2 < 5^2) | ||
643 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); | ||
644 | } | ||
645 | |||
646 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
647 | pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
648 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
649 | |||
650 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
651 | SeparationDistance.distance(sd, Distance::D_Near); | ||
599 | 652 | ||
653 | //check(dx^2 + dy^2 > 10^2) | ||
654 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | ||
655 | } | ||
600 | 656 | ||
601 | ////OPTION 2: | 657 | @Constraint(severity="error", key={a1, sd}, message="x") |
602 | ////we handle ITE by seperating the constraints | 658 | pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { |
603 | // | 659 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
604 | ////This will involve 1 constarint for each decision path, but will require multiple check expressions within the same pattern | 660 | |
605 | // | 661 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); |
606 | ////OPTION 3: | 662 | SeparationDistance.distance(sd, Distance::D_Med); |
607 | ////If this is nott working still, we will have to add some strctural components to the MM | 663 | |
608 | ////to differentiate the different cases and reduce the requirements of if, then, else | 664 | //check(dx^2 + dy^2 < 10^2) |
609 | // | 665 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); |
610 | ////This will involve more patterns, and some that are pstructural as well. \ No newline at end of file | 666 | } |
667 | |||
668 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
669 | pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
670 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
671 | |||
672 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
673 | SeparationDistance.distance(sd, Distance::D_Med); | ||
674 | |||
675 | //check(dx^2 + dy^2 > 1^2) | ||
676 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); | ||
677 | } | ||
678 | |||
679 | @Constraint(severity="error", key={a1, sd}, message="x") | ||
680 | pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
681 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
682 | |||
683 | find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2); | ||
684 | SeparationDistance.distance(sd, Distance::D_Far); | ||
685 | |||
686 | //check(dx^2 + dy^2 < 15^2) | ||
687 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
688 | } | ||
689 | */ | ||
690 | |||
691 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
692 | //CollisionDoesNotExist | ||
693 | /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
694 | /* | ||
695 | //TODO | ||
696 | @Constraint(severity="error", key={a1, cdne}, message="x") | ||
697 | pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) { | ||
698 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
699 | |||
700 | CrossingScenario.actors(ss, a1); | ||
701 | CrossingScenario.actors(ss, a2); | ||
702 | Actor.relations(a1, cdne); | ||
703 | CollisionDoesNotExist.target(cdne, a2); | ||
704 | CrossingScenario.maxTime(ss, maxTime); | ||
705 | |||
706 | Actor.width(a1, w1); | ||
707 | Actor.length(a1, l1); | ||
708 | Actor.xPos(a1, xPos1); | ||
709 | Actor.yPos(a1, yPos1); | ||
710 | Actor.xSpeed(a1, xSpeed1); | ||
711 | Actor.ySpeed(a1, ySpeed1); | ||
712 | |||
713 | Actor.width(a2, w2); | ||
714 | Actor.length(a2, l2); | ||
715 | Actor.xPos(a2, xPos2); | ||
716 | Actor.yPos(a2, yPos2); | ||
717 | Actor.xSpeed(a2, xSpeed2); | ||
718 | Actor.ySpeed(a2, ySpeed2); | ||
719 | //check(dx^2 + dy^2 < 15^2) | ||
720 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
721 | } | ||
722 | */ \ No newline at end of file | ||