diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-02-03 02:35:39 +0100 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-02-03 02:35:39 +0100 |
commit | 14afb998045e508b07633ea63c72b582084f8c4c (patch) | |
tree | 9c03bcfce180a950adb26ed0ec0bcc5c45fdfaec /Domains/crossingScenario/queries | |
parent | fix derived feature handling + impove dreal calling (diff) | |
download | VIATRA-Generator-14afb998045e508b07633ea63c72b582084f8c4c.tar.gz VIATRA-Generator-14afb998045e508b07633ea63c72b582084f8c4c.tar.zst VIATRA-Generator-14afb998045e508b07633ea63c72b582084f8c4c.zip |
major changes to CS case study, working example, few issues, major assumptions
Diffstat (limited to 'Domains/crossingScenario/queries')
-rw-r--r-- | Domains/crossingScenario/queries/crossingScenarioQueries.vql | 242 |
1 files changed, 130 insertions, 112 deletions
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index 32348399..0a28d774 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql | |||
@@ -91,6 +91,23 @@ pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { | |||
91 | find helper_vert_getYAndBounds(cs, a, yMax, yP); | 91 | find helper_vert_getYAndBounds(cs, a, yMax, yP); |
92 | check(yP <= 0-yMax);} | 92 | check(yP <= 0-yMax);} |
93 | 93 | ||
94 | ////////////ADDED | ||
95 | //to reduce overlap | ||
96 | //NEEDED | ||
97 | @Constraint(severity="error", key={a}, message="5 Actor") | ||
98 | pattern define_actor_wrtLane(a:Actor) { | ||
99 | Actor.placedOn(a, lane); | ||
100 | Lane_Vertical(lane); | ||
101 | Actor.yPos(a, yP); | ||
102 | check(yP > 0.0-1.0); | ||
103 | } or { | ||
104 | Actor.placedOn(a, lane); | ||
105 | Lane_Horizontal(lane); | ||
106 | Actor.xPos(a, xP); | ||
107 | check(xP > 0.0-1.0); | ||
108 | } | ||
109 | ////////////ADDED | ||
110 | |||
94 | //Minimum Distances | 111 | //Minimum Distances |
95 | private pattern helper_getCoords(a1:Actor, | 112 | private pattern helper_getCoords(a1:Actor, |
96 | a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { | 113 | a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { |
@@ -105,8 +122,8 @@ private pattern helper_getCoords(a1:Actor, | |||
105 | pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { | 122 | pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { |
106 | find helper_getCoords(a1, a2, x1, x2, y1, y2); | 123 | find helper_getCoords(a1, a2, x1, x2, y1, y2); |
107 | a1 != a2; | 124 | a1 != a2; |
108 | //check(dx^2 + dy^2 < 5^2) | 125 | //check(dx^2 + dy^2 < 3^2) |
109 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); | 126 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 3*3); |
110 | } | 127 | } |
111 | 128 | ||
112 | /////---------------- | 129 | /////---------------- |
@@ -219,47 +236,38 @@ pattern define_actor_vehicleLength(v:Vehicle) { | |||
219 | check(l != 2.0); | 236 | check(l != 2.0); |
220 | } | 237 | } |
221 | 238 | ||
222 | ///////---------------- | 239 | /////---------------- |
223 | ///////DERIVED FEATURES | 240 | /////DERIVED FEATURES |
224 | ///////---------------- | 241 | /////---------------- |
225 | // | 242 | /* |
226 | //@QueryBasedFeature | 243 | @QueryBasedFeature |
227 | //pattern dist_near(a1: Actor, a2: Actor) { | 244 | pattern dist_near(a1: Actor, a2: Actor) { |
228 | // find helper_actorsAreNear(a1, a2); | 245 | find helper_getCoords(a1, a2, x1, x2, y1, y2); |
229 | // Actor.dist_near(a1, a2); | 246 | |
230 | //} | 247 | //check(dx^2 + dy^2 < 10^2) |
231 | // | 248 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); |
232 | //private pattern helper_actorsAreNear(a1: Actor, a2: Actor) { | 249 | Actor.dist_near(a1, a2); |
233 | // find helper_getCoords(a1, a2, x1, x2, y1, y2); | 250 | } |
234 | // //check(dx^2 + dy^2 < 10^2) | 251 | |
235 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | 252 | @QueryBasedFeature |
236 | //} | 253 | pattern dist_med(a1: Actor, a2: Actor) { |
237 | // | 254 | find helper_getCoords(a1, a2, x1, x2, y1, y2); |
238 | //@QueryBasedFeature | 255 | |
239 | //pattern dist_med(a1: Actor, a2: Actor) { | 256 | //check(10^2 < dx^2 + dy^2 < 15^2) |
240 | // find helper_actorsAreMed(a1, a2); | 257 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); |
241 | // Actor.dist_med(a1, a2); | 258 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); |
242 | //} | 259 | Actor.dist_med(a1, a2); |
243 | // | 260 | } |
244 | //private pattern helper_actorsAreMed(a1: Actor, a2: Actor) { | 261 | |
245 | // find helper_getCoords(a1, a2, x1, x2, y1, y2); | 262 | @QueryBasedFeature |
246 | // //check(10^2 < dx^2 + dy^2 < 15^2) | 263 | pattern dist_far(a1: Actor, a2: Actor) { |
247 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | 264 | find helper_getCoords(a1, a2, x1, x2, y1, y2); |
248 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | 265 | |
249 | //} | 266 | //check(dx^2 + dy^2 > 20^2) |
250 | // | 267 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); |
251 | //@QueryBasedFeature | 268 | Actor.dist_far(a1, a2); |
252 | //pattern dist_far(a1: Actor, a2: Actor) { | 269 | } |
253 | // find helper_actorsAreFar(a1, a2); | 270 | */ |
254 | // Actor.dist_far(a1, a2); | ||
255 | //} | ||
256 | // | ||
257 | //private pattern helper_actorsAreFar(a1: Actor, a2: Actor) { | ||
258 | // find helper_getCoords(a1, a2, x1, x2, y1, y2); | ||
259 | // //check(dx^2 + dy^2 > 20^2) | ||
260 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); | ||
261 | //} | ||
262 | |||
263 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | 271 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
264 | //Relation | 272 | //Relation |
265 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | 273 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
@@ -278,7 +286,7 @@ pattern define_actor_vehicleLength(v:Vehicle) { | |||
278 | 286 | ||
279 | 287 | ||
280 | //<<QUALTATIF ABSTRACTION>> | 288 | //<<QUALTATIF ABSTRACTION>> |
281 | 289 | /* | |
282 | @Constraint(severity="error", key={a1, a2}, message="x") | 290 | @Constraint(severity="error", key={a1, a2}, message="x") |
283 | pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { | 291 | pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { |
284 | CollisionExists.source(ce, a1); | 292 | CollisionExists.source(ce, a1); |
@@ -295,72 +303,9 @@ pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { | |||
295 | Actor.placedOn(a2, hl2); | 303 | Actor.placedOn(a2, hl2); |
296 | Lane_Horizontal(hl2); | 304 | Lane_Horizontal(hl2); |
297 | } | 305 | } |
298 | 306 | */ | |
299 | //<<END TEMP QUALITATIF ABSTRACTION>> | 307 | //<<END TEMP QUALITATIF ABSTRACTION>> |
300 | 308 | ||
301 | //// | ||
302 | //VS VisionBlocked | ||
303 | //// | ||
304 | //TODO Very prone to corner cases | ||
305 | /* | ||
306 | @Constraint(severity="error", key={a1}, message="x") | ||
307 | pattern collisionExists_vsVisionBlockedX1(a1:Actor) { | ||
308 | VisionBlocked.blockedBy(_, a1); | ||
309 | CollisionExists.target(_, a1); | ||
310 | } | ||
311 | @Constraint(severity="error", key={a1}, message="x") | ||
312 | pattern collisionExists_vsVisionBlockedX2(a1:Actor) { | ||
313 | VisionBlocked.blockedBy(_, a1); | ||
314 | CollisionExists.source(_, a1); | ||
315 | } | ||
316 | |||
317 | @Constraint(severity="error", key={a1}, message="x") | ||
318 | pattern collisionExists_vsVisionBlocked1(a1:Actor) { | ||
319 | VisionBlocked.source(_, a1); | ||
320 | neg find helper_source(a1); | ||
321 | } | ||
322 | private pattern helper_source(a1:Actor) { | ||
323 | CollisionExists.source(_, a1); | ||
324 | } | ||
325 | |||
326 | @Constraint(severity="error", key={a1}, message="x") | ||
327 | pattern collisionExists_vsVisionBlocked2(a1:Actor) { | ||
328 | VisionBlocked.target(_, a1); | ||
329 | neg find helper_target(a1); | ||
330 | } | ||
331 | private pattern helper_target(a1:Actor) { | ||
332 | CollisionExists.target(_, a1); | ||
333 | } | ||
334 | */ | ||
335 | /* | ||
336 | @Constraint(severity="error", key={a1}, message="x") | ||
337 | pattern collisionExists_vsVisionBlocked(a1:Actor) { | ||
338 | VisionBlocked.source(vb, a1); | ||
339 | VisionBlocked.target(vb, a2); | ||
340 | CollisionExists.source(ce, a1); | ||
341 | CollisionExists.target(ce, a3); | ||
342 | a2 != a3; | ||
343 | } or { | ||
344 | VisionBlocked.source(vb, a1); | ||
345 | VisionBlocked.target(vb, a2); | ||
346 | CollisionExists.source(ce, a3); | ||
347 | CollisionExists.target(ce, a1); | ||
348 | a2 != a3; | ||
349 | } or { | ||
350 | VisionBlocked.source(vb, a2); | ||
351 | VisionBlocked.target(vb, a1); | ||
352 | CollisionExists.source(ce, a3); | ||
353 | CollisionExists.target(ce, a1); | ||
354 | a2 != a3; | ||
355 | } or { | ||
356 | VisionBlocked.source(vb, a2); | ||
357 | VisionBlocked.target(vb, a1); | ||
358 | CollisionExists.source(ce, a1); | ||
359 | CollisionExists.target(ce, a3); | ||
360 | a2 != a3; | ||
361 | } | ||
362 | */ | ||
363 | //<<END QUALITATIF ABSTRACTION>> | ||
364 | 309 | ||
365 | //// | 310 | //// |
366 | //CollisionExists - Time | 311 | //CollisionExists - Time |
@@ -407,10 +352,10 @@ private pattern helper_getAllYCoords(a1:Actor, a2: Actor, | |||
407 | find helper_getYCoords(a2, l2, yPos2, ySpeed2); | 352 | find helper_getYCoords(a2, l2, yPos2, ySpeed2); |
408 | } | 353 | } |
409 | 354 | ||
410 | private pattern helper_getXCoords(a:Actor, l:java Double, | 355 | private pattern helper_getXCoords(a:Actor, w:java Double, |
411 | xPos:java Double, xSpeed:java Double) { | 356 | xPos:java Double, xSpeed:java Double) { |
412 | 357 | ||
413 | Actor.length(a, l); | 358 | Actor.width(a, w); |
414 | Actor.xPos(a, xPos); | 359 | Actor.xPos(a, xPos); |
415 | Actor.xSpeed(a, xSpeed); | 360 | Actor.xSpeed(a, xSpeed); |
416 | } | 361 | } |
@@ -473,7 +418,7 @@ pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { | |||
473 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | 418 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
474 | 419 | ||
475 | //<<QUALTATIF ABSTRACTION>> | 420 | //<<QUALTATIF ABSTRACTION>> |
476 | 421 | /* | |
477 | @Constraint(severity="error", key={a1, a2}, message="on 3 different lanes") | 422 | @Constraint(severity="error", key={a1, a2}, message="on 3 different lanes") |
478 | pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { | 423 | pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { |
479 | VisionBlocked.source(vb, a1); | 424 | VisionBlocked.source(vb, a1); |
@@ -491,7 +436,7 @@ pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { | |||
491 | Actor.placedOn(a1, l); | 436 | Actor.placedOn(a1, l); |
492 | Actor.placedOn(a2, l); | 437 | Actor.placedOn(a2, l); |
493 | } | 438 | } |
494 | 439 | */ | |
495 | @Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation") | 440 | @Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation") |
496 | pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { | 441 | pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { |
497 | VisionBlocked.source(ce, a1); | 442 | VisionBlocked.source(ce, a1); |
@@ -509,6 +454,30 @@ pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { | |||
509 | Lane_Horizontal(hl2); | 454 | Lane_Horizontal(hl2); |
510 | } | 455 | } |
511 | 456 | ||
457 | ////////////ADDED | ||
458 | //to make decision for ITE | ||
459 | //NOT NEEDED | ||
460 | /* | ||
461 | @Constraint(severity="error", key={a}, message="5 Actor") | ||
462 | pattern define_vb_blvssrc(a:Actor) { | ||
463 | VisionBlocked.source(vb, a); | ||
464 | VisionBlocked.blockedBy(vb, b); | ||
465 | Actor.placedOn(a, lane); | ||
466 | Lane_Vertical(lane); | ||
467 | Actor.yPos(a, yPa); | ||
468 | Actor.yPos(b, yPb); | ||
469 | check(yPb <= yPa); | ||
470 | } or { | ||
471 | VisionBlocked.source(vb, a); | ||
472 | VisionBlocked.blockedBy(vb, b); | ||
473 | Actor.placedOn(a, lane); | ||
474 | Lane_Horizontal(lane); | ||
475 | Actor.xPos(a, xPa); | ||
476 | Actor.xPos(a, xPb); | ||
477 | check(xPb <= xPa); | ||
478 | } | ||
479 | */ | ||
480 | ////////////ADDED | ||
512 | //<<END QUALITATIF ABSTRACTION>> | 481 | //<<END QUALITATIF ABSTRACTION>> |
513 | 482 | ||
514 | @Constraint(severity="error", key={a1, a2}, message="x") | 483 | @Constraint(severity="error", key={a1, a2}, message="x") |
@@ -582,6 +551,9 @@ pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor) { | |||
582 | > ((y1-y2)/(x1-x2))); | 551 | > ((y1-y2)/(x1-x2))); |
583 | } | 552 | } |
584 | 553 | ||
554 | /////// | ||
555 | //BLOCKER IN BETWEEN | ||
556 | /////// | ||
585 | 557 | ||
586 | private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, | 558 | private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, |
587 | x1:java Double, y1:java Double, | 559 | x1:java Double, y1:java Double, |
@@ -600,6 +572,7 @@ private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, | |||
600 | Actor.yPos(aBlocker, yBlocker); | 572 | Actor.yPos(aBlocker, yBlocker); |
601 | } | 573 | } |
602 | 574 | ||
575 | /* | ||
603 | //INFO may use approximation instead | 576 | //INFO may use approximation instead |
604 | @Constraint(severity="error", key={a1}, message="x") | 577 | @Constraint(severity="error", key={a1}, message="x") |
605 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { | 578 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { |
@@ -621,4 +594,49 @@ pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { | |||
621 | //check(dist(A2, ABlocker) > dist(A2, A1)) | 594 | //check(dist(A2, ABlocker) > dist(A2, A1)) |
622 | check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1)); | 595 | check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1)); |
623 | } | 596 | } |
597 | */ | ||
598 | |||
599 | //INFO may use approximation instead | ||
600 | @Constraint(severity="error", key={a1}, message="x") | ||
601 | pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { | ||
602 | |||
603 | find helper_VB_getJustCoords(a1, a2, | ||
604 | x1, _, x2, _, xBlocker, _); | ||
605 | |||
606 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
607 | check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); | ||
608 | } | ||
609 | |||
610 | //INFO may use approximation instead | ||
611 | @Constraint(severity="error", key={a1}, message="x") | ||
612 | pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { | ||
613 | |||
614 | find helper_VB_getJustCoords(a1, a2, | ||
615 | x1, _, x2, _, xBlocker, _); | ||
616 | |||
617 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
618 | check((x2-xBlocker)*(x2-xBlocker) > (x2-x1)*(x2-x1)); | ||
619 | } | ||
620 | |||
621 | //INFO may use approximation instead | ||
622 | @Constraint(severity="error", key={a1}, message="x") | ||
623 | pattern visionBlocked_ydistBSlargerThanydistTS(a1:Actor, a2:Actor) { | ||
624 | |||
625 | find helper_VB_getJustCoords(a1, a2, | ||
626 | _, y1, _, y2, _, yBlocker); | ||
627 | |||
628 | //check(dist(A1, ABlocker) > dist(A1, A2)) | ||
629 | check((y1-yBlocker)*(y1-yBlocker) > (y1-y2)*(y1-y2)); | ||
630 | } | ||
631 | |||
632 | //INFO may use approximation instead | ||
633 | @Constraint(severity="error", key={a1}, message="x") | ||
634 | pattern visionBlocked_ydistBTlargerThanydistST(a1:Actor, a2:Actor) { | ||
635 | |||
636 | find helper_VB_getJustCoords(a1, a2, | ||
637 | _, y1, _, y2, _, yBlocker); | ||
638 | |||
639 | //check(dist(A2, ABlocker) > dist(A2, A1)) | ||
640 | check((y2-yBlocker)*(y2-yBlocker) > (y2-y1)*(y2-y1)); | ||
641 | } | ||
624 | 642 | ||