diff options
author | 2021-02-16 09:01:25 +0100 | |
---|---|---|
committer | 2021-02-16 09:01:25 +0100 | |
commit | bc403272d867f82edd623179d82c080e57154c1a (patch) | |
tree | 3551ba142ed725595ee684981fc8973cade2ebf4 /Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql | |
parent | add dreal-timeout flag (diff) | |
download | VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.tar.gz VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.tar.zst VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.zip |
CrossingScenario case study is ready for serverdreal-integration
Diffstat (limited to 'Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql')
-rw-r--r-- | Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql | 646 |
1 files changed, 646 insertions, 0 deletions
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql new file mode 100644 index 00000000..5f35cd2b --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql | |||
@@ -0,0 +1,646 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http://www.example.com/crossingScenario" | ||
4 | import "http://www.eclipse.org/emf/2002/Ecore" | ||
5 | |||
6 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
7 | //Lane+Actor | ||
8 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
9 | |||
10 | /////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] | ||
11 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
12 | pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { | ||
13 | Actor.placedOn(a, vl); | ||
14 | Actor.xPos(a, x); | ||
15 | Lane.referenceCoord(vl, r); | ||
16 | check(x <= r); | ||
17 | } or { | ||
18 | Actor.placedOn(a, vl); | ||
19 | Actor.xPos(a, x); | ||
20 | Lane.referenceCoord(vl, r); | ||
21 | // //<<<<OLD>>>> | ||
22 | // Lane.numWidth(vl, w); | ||
23 | // check(x >= (r + w)); | ||
24 | |||
25 | //<<<<NEW>>>>: lanes all have width=3 | ||
26 | check(x >= (r + 3.0)); | ||
27 | } | ||
28 | |||
29 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
30 | pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { | ||
31 | Actor.placedOn(a, hl); | ||
32 | Actor.yPos(a, y); | ||
33 | Lane.referenceCoord(hl, r); | ||
34 | check(y <= r); | ||
35 | } or { | ||
36 | Actor.placedOn(a, hl); | ||
37 | Actor.yPos(a, y); | ||
38 | Lane.referenceCoord(hl, r); | ||
39 | // //<<OLD>> | ||
40 | // Lane.numWidth(hl, w); | ||
41 | // check(y >= (r + w)); | ||
42 | |||
43 | //<<NEW>>: lanes all have width=3 | ||
44 | check(y >= (r + 3.0)); | ||
45 | |||
46 | } | ||
47 | |||
48 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
49 | //Actor | ||
50 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
51 | |||
52 | /////---------------- | ||
53 | //Xpos and Ypos Bounds | ||
54 | /////---------------- | ||
55 | |||
56 | private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor, | ||
57 | xMax:java Double, xP:java Double) { | ||
58 | Actor.placedOn(a, hl); | ||
59 | Lane_Horizontal(hl); | ||
60 | CrossingScenario.actors(cs, a); | ||
61 | CrossingScenario.xSize(cs, xMax); | ||
62 | Actor.xPos(a, xP); | ||
63 | } | ||
64 | |||
65 | private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor, | ||
66 | yMax:java Double, yP:java Double) { | ||
67 | Actor.placedOn(a, vl); | ||
68 | Lane_Vertical(vl); | ||
69 | CrossingScenario.actors(cs, a); | ||
70 | CrossingScenario.ySize(cs, yMax); | ||
71 | Actor.yPos(a, yP); | ||
72 | } | ||
73 | |||
74 | @Constraint(severity="error", key={cs}, message="x") | ||
75 | pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { | ||
76 | find helper_horiz_getXAndBounds(cs, a, xMax, xP); | ||
77 | check(xP >= xMax);} | ||
78 | |||
79 | @Constraint(severity="error", key={cs}, message="x") | ||
80 | pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { | ||
81 | find helper_horiz_getXAndBounds(cs, a, xMax, xP); | ||
82 | check(xP <= 0-xMax);} | ||
83 | |||
84 | @Constraint(severity="error", key={cs}, message="x") | ||
85 | pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { | ||
86 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | ||
87 | check(yP >= yMax);} | ||
88 | |||
89 | @Constraint(severity="error", key={cs}, message="x") | ||
90 | pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { | ||
91 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | ||
92 | check(yP <= 0-yMax);} | ||
93 | |||
94 | ////////////ADDED | ||
95 | //to reduce overlap | ||
96 | //NEEDED | ||
97 | /* | ||
98 | @Constraint(severity="error", key={a}, message="5 Actor") | ||
99 | pattern define_actor_wrtLane(a:Actor) { | ||
100 | Actor.placedOn(a, lane); | ||
101 | Lane_Vertical(lane); | ||
102 | Actor.yPos(a, yP); | ||
103 | check(yP > 0.0-1.0); | ||
104 | } or { | ||
105 | Actor.placedOn(a, lane); | ||
106 | Lane_Horizontal(lane); | ||
107 | Actor.xPos(a, xP); | ||
108 | check(xP > 0.0-1.0); | ||
109 | } | ||
110 | */ | ||
111 | ////////////ADDED | ||
112 | |||
113 | //Minimum Distances | ||
114 | private pattern helper_getCoords(a1:Actor, | ||
115 | a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | ||
116 | Actor.xPos(a1, x1); | ||
117 | Actor.yPos(a1, y1); | ||
118 | Actor.xPos(a2, x2); | ||
119 | Actor.yPos(a2, y2); | ||
120 | } | ||
121 | |||
122 | //INFO may remove? | ||
123 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
124 | pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { | ||
125 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
126 | a1 != a2; | ||
127 | //check(dx^2 + dy^2 < 3^2) | ||
128 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 3*3); | ||
129 | } | ||
130 | |||
131 | /////---------------- | ||
132 | //Xspeed and Yspeed bounds | ||
133 | /////---------------- | ||
134 | |||
135 | /////////VERTICAL LANE | ||
136 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
137 | pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { | ||
138 | Actor.placedOn(a, vl); | ||
139 | Lane_Vertical(vl); | ||
140 | Actor.xSpeed(a, xSpeed); | ||
141 | check(xSpeed != 0.0); | ||
142 | } | ||
143 | |||
144 | private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, | ||
145 | ySpeedMax:java Double, ySpeed:java Double) { | ||
146 | Actor.placedOn(a, vl); | ||
147 | Lane_Vertical(vl); | ||
148 | CrossingScenario.actors(cs, a); | ||
149 | CrossingScenario.maxYSpeed(cs, ySpeedMax); | ||
150 | Actor.ySpeed(a, ySpeed); | ||
151 | } | ||
152 | |||
153 | @Constraint(severity="error", key={cs}, message="x") | ||
154 | pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { | ||
155 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | ||
156 | check(yS <= 0.0-ySMax); | ||
157 | } | ||
158 | |||
159 | @Constraint(severity="error", key={cs}, message="x") | ||
160 | pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) { | ||
161 | find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); | ||
162 | check(yS >= ySMax); | ||
163 | } | ||
164 | |||
165 | /////////HORIZONTAL LANE | ||
166 | @Constraint(severity="error", key={a}, message="7 Actor") | ||
167 | pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { | ||
168 | Actor.placedOn(a, hl); | ||
169 | Lane_Horizontal(hl); | ||
170 | Actor.ySpeed(a, ySpeed); | ||
171 | check(ySpeed != 0.0); | ||
172 | } | ||
173 | |||
174 | private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, | ||
175 | xSpeedMax:java Double, xSpeed:java Double) { | ||
176 | Actor.placedOn(a, hl); | ||
177 | Lane_Horizontal(hl); | ||
178 | CrossingScenario.actors(cs, a); | ||
179 | CrossingScenario.maxXSpeed(cs, xSpeedMax); | ||
180 | Actor.xSpeed(a, xSpeed); | ||
181 | } | ||
182 | |||
183 | @Constraint(severity="error", key={cs}, message="x") | ||
184 | pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { | ||
185 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | ||
186 | check(xS <= 0.0-xSMax); | ||
187 | } | ||
188 | |||
189 | @Constraint(severity="error", key={cs}, message="x") | ||
190 | pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) { | ||
191 | find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); | ||
192 | check(xS >= xSMax); | ||
193 | } | ||
194 | |||
195 | /////---------------- | ||
196 | /////WIDTH and LENGTH | ||
197 | /////---------------- | ||
198 | |||
199 | ///////pedestrian-width (3) | ||
200 | @Constraint(severity="error", key={p}, message="3 Actor") | ||
201 | pattern define_actor_pedestrianWidth(p:Pedestrian) { | ||
202 | Pedestrian.width(p, w); | ||
203 | check(w != 1.0); | ||
204 | } | ||
205 | |||
206 | /////////pedestrian-width (4) | ||
207 | @Constraint(severity="error", key={p}, message="4 Actor") | ||
208 | pattern define_actor_pedestrianLength(p:Pedestrian) { | ||
209 | Pedestrian.length(p, l); | ||
210 | check(l != 1.0); | ||
211 | } | ||
212 | |||
213 | /////////actor-width (5) | ||
214 | @Constraint(severity="error", key={v}, message="5 Actor") | ||
215 | pattern define_actor_vehicleWidth(v:Vehicle) { | ||
216 | Vehicle.placedOn(v, lane); | ||
217 | Lane_Vertical(lane); | ||
218 | Vehicle.width(v, w); | ||
219 | check(w != 2.0); | ||
220 | } or { | ||
221 | Vehicle.placedOn(v, lane); | ||
222 | Lane_Horizontal(lane); | ||
223 | Vehicle.width(v, w); | ||
224 | check(w != 3.0); | ||
225 | } | ||
226 | |||
227 | /////////actor-width (6) | ||
228 | @Constraint(severity="error", key={v}, message="6 Actor") | ||
229 | pattern define_actor_vehicleLength(v:Vehicle) { | ||
230 | Vehicle.placedOn(v, lane); | ||
231 | Lane_Vertical(lane); | ||
232 | Vehicle.length(v, l); | ||
233 | check(l != 3.0); | ||
234 | } or { | ||
235 | Vehicle.placedOn(v, lane); | ||
236 | Lane_Horizontal(lane); | ||
237 | Vehicle.length(v, l); | ||
238 | check(l != 2.0); | ||
239 | } | ||
240 | |||
241 | /////---------------- | ||
242 | /////DERIVED FEATURES | ||
243 | /////---------------- | ||
244 | /* | ||
245 | @QueryBasedFeature | ||
246 | pattern dist_near(a1: Actor, a2: Actor) { | ||
247 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
248 | |||
249 | //check(dx^2 + dy^2 < 10^2) | ||
250 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | ||
251 | Actor.dist_near(a1, a2); | ||
252 | } | ||
253 | |||
254 | @QueryBasedFeature | ||
255 | pattern dist_med(a1: Actor, a2: Actor) { | ||
256 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
257 | |||
258 | //check(10^2 < dx^2 + dy^2 < 15^2) | ||
259 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | ||
260 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
261 | Actor.dist_med(a1, a2); | ||
262 | } | ||
263 | |||
264 | @QueryBasedFeature | ||
265 | pattern dist_far(a1: Actor, a2: Actor) { | ||
266 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
267 | |||
268 | //check(dx^2 + dy^2 > 20^2) | ||
269 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); | ||
270 | Actor.dist_far(a1, a2); | ||
271 | } | ||
272 | */ | ||
273 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
274 | //Relation | ||
275 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
276 | |||
277 | //@Constraint(severity="error", key={a1, a2}, message="1 Relation") | ||
278 | //pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { | ||
279 | // Relation.source(r, a1); | ||
280 | // Relation.target(r, a2); | ||
281 | // a1 == a2; | ||
282 | //} | ||
283 | |||
284 | //TODO do above but transitively?/ | ||
285 | //////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
286 | //CollisionExists | ||
287 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
288 | |||
289 | |||
290 | //<<QUALTATIF ABSTRACTION>> | ||
291 | /* | ||
292 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
293 | pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { | ||
294 | CollisionExists.source(ce, a1); | ||
295 | CollisionExists.target(ce, a2); | ||
296 | Actor.placedOn(a1, vl1); | ||
297 | Lane_Vertical(vl1); | ||
298 | Actor.placedOn(a2, vl2); | ||
299 | Lane_Vertical(vl2); | ||
300 | } or { | ||
301 | CollisionExists.source(ce, a1); | ||
302 | CollisionExists.target(ce, a2); | ||
303 | Actor.placedOn(a1, hl1); | ||
304 | Lane_Horizontal(hl1); | ||
305 | Actor.placedOn(a2, hl2); | ||
306 | Lane_Horizontal(hl2); | ||
307 | } | ||
308 | */ | ||
309 | //<<END TEMP QUALITATIF ABSTRACTION>> | ||
310 | |||
311 | |||
312 | //// | ||
313 | //CollisionExists - Time | ||
314 | //// | ||
315 | |||
316 | |||
317 | @Constraint(severity="error", key={c}, message="x") | ||
318 | pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { | ||
319 | CrossingScenario.relations(ss, c); | ||
320 | CrossingScenario.maxTime(ss, maxTime); | ||
321 | CollisionExists.collisionTime(c, cTime); | ||
322 | check(cTime >= maxTime);} | ||
323 | |||
324 | @Constraint(severity="error", key={c}, message="x") | ||
325 | pattern collisionExists_timeNotNegative(c:CollisionExists) { | ||
326 | CollisionExists. collisionTime(c, cTime); | ||
327 | check(cTime <= 0.0);} | ||
328 | |||
329 | //// | ||
330 | //CollisionExists - Physical Positioniung | ||
331 | //// | ||
332 | |||
333 | private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) { | ||
334 | CollisionExists.source(c, a1); | ||
335 | CollisionExists.target(c, a2); | ||
336 | CollisionExists. collisionTime(c, cTime); | ||
337 | } | ||
338 | |||
339 | private pattern helper_getYCoords(a:Actor, l:java Double, | ||
340 | yPos:java Double, ySpeed:java Double) { | ||
341 | |||
342 | Actor.length(a, l); | ||
343 | Actor.yPos(a, yPos); | ||
344 | Actor.ySpeed(a, ySpeed); | ||
345 | } | ||
346 | |||
347 | private pattern helper_getAllYCoords(a1:Actor, a2: Actor, | ||
348 | l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double, | ||
349 | ySpeed1:java Double, ySpeed2:java Double) { | ||
350 | |||
351 | CollisionExists.source(c, a1); | ||
352 | CollisionExists.target(c, a2); | ||
353 | find helper_getYCoords(a1, l1, yPos1, ySpeed1); | ||
354 | find helper_getYCoords(a2, l2, yPos2, ySpeed2); | ||
355 | } | ||
356 | |||
357 | private pattern helper_getXCoords(a:Actor, w:java Double, | ||
358 | xPos:java Double, xSpeed:java Double) { | ||
359 | |||
360 | Actor.width(a, w); | ||
361 | Actor.xPos(a, xPos); | ||
362 | Actor.xSpeed(a, xSpeed); | ||
363 | } | ||
364 | |||
365 | private pattern helper_getAllXCoords(a1:Actor, a2: Actor, | ||
366 | w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double, | ||
367 | xSpeed1:java Double, xSpeed2:java Double) { | ||
368 | |||
369 | CollisionExists.source(c, a1); | ||
370 | CollisionExists.target(c, a2); | ||
371 | find helper_getXCoords(a1, w1, xPos1, xSpeed1); | ||
372 | find helper_getXCoords(a2, w2, xPos2, xSpeed2); | ||
373 | } | ||
374 | |||
375 | @Constraint(severity="error", key={a1}, message="x") | ||
376 | pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) { | ||
377 | |||
378 | find helper_getCollExistsTime(a1, a2, cTime); | ||
379 | find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | ||
380 | |||
381 | //check(y_1_bottom > y_2_top | ||
382 | check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); | ||
383 | } | ||
384 | |||
385 | @Constraint(severity="error", key={a1}, message="x") | ||
386 | pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) { | ||
387 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
388 | |||
389 | find helper_getCollExistsTime(a1, a2, cTime); | ||
390 | find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | ||
391 | |||
392 | //check(y_1_top < y_2_bottom) | ||
393 | check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); | ||
394 | } | ||
395 | |||
396 | @Constraint(severity="error", key={a1}, message="x") | ||
397 | pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) { | ||
398 | |||
399 | find helper_getCollExistsTime(a1, a2, cTime); | ||
400 | find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | ||
401 | |||
402 | //check(x_1_left > x_2_right) | ||
403 | check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); | ||
404 | } | ||
405 | |||
406 | @Constraint(severity="error", key={a1}, message="x") | ||
407 | pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { | ||
408 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
409 | |||
410 | find helper_getCollExistsTime(a1, a2, cTime); | ||
411 | find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | ||
412 | |||
413 | //check(x_1_right < x_2_left) | ||
414 | check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | ||
415 | } | ||
416 | |||
417 | |||
418 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
419 | //VisionBlocked | ||
420 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | ||
421 | |||
422 | //<<QUALTATIF ABSTRACTION>> | ||
423 | /* | ||
424 | @Constraint(severity="error", key={a1, a2}, message="on 3 different lanes") | ||
425 | pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { | ||
426 | VisionBlocked.source(vb, a1); | ||
427 | VisionBlocked.target(vb, a2); | ||
428 | Actor.placedOn(a1, l); | ||
429 | Actor.placedOn(a2, l); | ||
430 | } or { | ||
431 | VisionBlocked.source(vb, a1); | ||
432 | VisionBlocked.blockedBy(vb, a2); | ||
433 | Actor.placedOn(a1, l); | ||
434 | Actor.placedOn(a2, l); | ||
435 | } or { | ||
436 | VisionBlocked.blockedBy(vb, a1); | ||
437 | VisionBlocked.target(vb, a2); | ||
438 | Actor.placedOn(a1, l); | ||
439 | Actor.placedOn(a2, l); | ||
440 | } | ||
441 | */ | ||
442 | /* | ||
443 | @Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation") | ||
444 | pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { | ||
445 | VisionBlocked.source(ce, a1); | ||
446 | VisionBlocked.target(ce, a2); | ||
447 | Actor.placedOn(a1, vl1); | ||
448 | Lane_Vertical(vl1); | ||
449 | Actor.placedOn(a2, vl2); | ||
450 | Lane_Vertical(vl2); | ||
451 | } or { | ||
452 | VisionBlocked.source(ce, a1); | ||
453 | VisionBlocked.target(ce, a2); | ||
454 | Actor.placedOn(a1, hl1); | ||
455 | Lane_Horizontal(hl1); | ||
456 | Actor.placedOn(a2, hl2); | ||
457 | Lane_Horizontal(hl2); | ||
458 | } | ||
459 | */ | ||
460 | |||
461 | ////////////ADDED | ||
462 | //to make decision for ITE | ||
463 | //NOT NEEDED | ||
464 | /* | ||
465 | @Constraint(severity="error", key={a}, message="5 Actor") | ||
466 | pattern define_vb_blvssrc(a:Actor) { | ||
467 | VisionBlocked.source(vb, a); | ||
468 | VisionBlocked.blockedBy(vb, b); | ||
469 | Actor.placedOn(a, lane); | ||
470 | Lane_Vertical(lane); | ||
471 | Actor.yPos(a, yPa); | ||
472 | Actor.yPos(b, yPb); | ||
473 | check(yPb <= yPa); | ||
474 | } or { | ||
475 | VisionBlocked.source(vb, a); | ||
476 | VisionBlocked.blockedBy(vb, b); | ||
477 | Actor.placedOn(a, lane); | ||
478 | Lane_Horizontal(lane); | ||
479 | Actor.xPos(a, xPa); | ||
480 | Actor.xPos(a, xPb); | ||
481 | check(xPb <= xPa); | ||
482 | } | ||
483 | */ | ||
484 | ////////////ADDED | ||
485 | //<<END QUALITATIF ABSTRACTION>> | ||
486 | |||
487 | @Constraint(severity="error", key={a1, a2}, message="x") | ||
488 | pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) { | ||
489 | VisionBlocked.source(vb, a1); | ||
490 | VisionBlocked.target(vb, a2); | ||
491 | VisionBlocked.blockedBy(vb, a2); | ||
492 | } or { | ||
493 | VisionBlocked.source(vb, a1); | ||
494 | VisionBlocked.target(vb, a2); | ||
495 | VisionBlocked.blockedBy(vb, a1); | ||
496 | } | ||
497 | |||
498 | @Constraint(severity="error", key={a1, vb}, message="x") | ||
499 | pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
500 | //REQUIRED to avoid division by 0 in next 2 queries | ||
501 | VisionBlocked.source(vb, a1); | ||
502 | VisionBlocked.target(vb, a2); | ||
503 | |||
504 | Actor.xPos(a1, x1); | ||
505 | Actor.xPos(a2, x2); | ||
506 | |||
507 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | ||
508 | check(x1 == x2); | ||
509 | } | ||
510 | |||
511 | private pattern helper_VB_getAllCoords(a1:Actor, a2: Actor, | ||
512 | x1:java Double, y1:java Double, | ||
513 | x2:java Double, y2:java Double, | ||
514 | xBlocker:java Double, yBlocker:java Double, | ||
515 | lenBlocker:java Double, widBlocker:java Double) { | ||
516 | |||
517 | VisionBlocked.source(vb, a1); | ||
518 | VisionBlocked.target(vb, a2); | ||
519 | VisionBlocked.blockedBy(vb, aBlocker); | ||
520 | |||
521 | Actor.xPos(a1, x1); | ||
522 | Actor.yPos(a1, y1); | ||
523 | Actor.xPos(a2, x2); | ||
524 | Actor.yPos(a2, y2); | ||
525 | Actor.xPos(aBlocker, xBlocker); | ||
526 | Actor.yPos(aBlocker, yBlocker); | ||
527 | Actor.length(aBlocker, lenBlocker); | ||
528 | Actor.width(aBlocker, widBlocker); | ||
529 | } | ||
530 | |||
531 | @Constraint(severity="error", key={a1}, message="x") | ||
532 | pattern visionBlocked_ites_top(a1:Actor, a2:Actor) { | ||
533 | |||
534 | find helper_VB_getAllCoords(a1, a2, | ||
535 | x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); | ||
536 | |||
537 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | ||
538 | check( | ||
539 | ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / | ||
540 | ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) | ||
541 | < ((y1-y2)/(x1-x2))); | ||
542 | } | ||
543 | |||
544 | |||
545 | @Constraint(severity="error", key={a1}, message="x") | ||
546 | pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor) { | ||
547 | |||
548 | find helper_VB_getAllCoords(a1, a2, | ||
549 | x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); | ||
550 | |||
551 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | ||
552 | check( | ||
553 | ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / | ||
554 | ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) | ||
555 | > ((y1-y2)/(x1-x2))); | ||
556 | } | ||
557 | |||
558 | /////// | ||
559 | //BLOCKER IN BETWEEN | ||
560 | /////// | ||
561 | |||
562 | private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, | ||
563 | x1:java Double, y1:java Double, | ||
564 | x2:java Double, y2:java Double, | ||
565 | xBlocker:java Double, yBlocker:java Double) { | ||
566 | |||
567 | VisionBlocked.source(vb, a1); | ||
568 | VisionBlocked.target(vb, a2); | ||
569 | VisionBlocked.blockedBy(vb, aBlocker); | ||
570 | |||
571 | Actor.xPos(a1, x1); | ||
572 | Actor.yPos(a1, y1); | ||
573 | Actor.xPos(a2, x2); | ||
574 | Actor.yPos(a2, y2); | ||
575 | Actor.xPos(aBlocker, xBlocker); | ||
576 | Actor.yPos(aBlocker, yBlocker); | ||
577 | } | ||
578 | |||
579 | /* | ||
580 | //INFO may use approximation instead | ||
581 | @Constraint(severity="error", key={a1}, message="x") | ||
582 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { | ||
583 | |||
584 | find helper_VB_getJustCoords(a1, a2, | ||
585 | x1, y1, x2, y2, xBlocker, yBlocker); | ||
586 | |||
587 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
588 | check((x1-xBlocker)*(x1-xBlocker) + (y1-yBlocker)*(y1-yBlocker) > (x1-x2)*(x1-x2) + (y1-y2)*(y1-y2)); | ||
589 | } | ||
590 | |||
591 | //INFO may use approximation instead | ||
592 | @Constraint(severity="error", key={a1}, message="x") | ||
593 | pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { | ||
594 | |||
595 | find helper_VB_getJustCoords(a1, a2, | ||
596 | x1, y1, x2, y2, xBlocker, yBlocker); | ||
597 | |||
598 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
599 | check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1)); | ||
600 | } | ||
601 | */ | ||
602 | |||
603 | //INFO may use approximation instead | ||
604 | @Constraint(severity="error", key={a1}, message="x") | ||
605 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { | ||
606 | |||
607 | find helper_VB_getJustCoords(a1, a2, | ||
608 | x1, _, x2, _, xBlocker, _); | ||
609 | |||
610 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
611 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); | ||
612 | } | ||
613 | |||
614 | //INFO may use approximation instead | ||
615 | @Constraint(severity="error", key={a1}, message="x") | ||
616 | pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { | ||
617 | |||
618 | find helper_VB_getJustCoords(a1, a2, | ||
619 | x1, _, x2, _, xBlocker, _); | ||
620 | |||
621 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
622 | check((x2-xBlocker)*(x2-xBlocker) > (x2-x1)*(x2-x1)); | ||
623 | } | ||
624 | |||
625 | //INFO may use approximation instead | ||
626 | @Constraint(severity="error", key={a1}, message="x") | ||
627 | pattern visionBlocked_ydistBSlargerThanydistTS(a1:Actor, a2:Actor) { | ||
628 | |||
629 | find helper_VB_getJustCoords(a1, a2, | ||
630 | _, y1, _, y2, _, yBlocker); | ||
631 | |||
632 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
633 | check((y1-yBlocker)*(y1-yBlocker) > (y1-y2)*(y1-y2)); | ||
634 | } | ||
635 | |||
636 | //INFO may use approximation instead | ||
637 | @Constraint(severity="error", key={a1}, message="x") | ||
638 | pattern visionBlocked_ydistBTlargerThanydistST(a1:Actor, a2:Actor) { | ||
639 | |||
640 | find helper_VB_getJustCoords(a1, a2, | ||
641 | _, y1, _, y2, _, yBlocker); | ||
642 | |||
643 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
644 | check((y2-yBlocker)*(y2-yBlocker) > (y2-y1)*(y2-y1)); | ||
645 | } | ||
646 | |||