diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-20 08:44:27 +0100 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-20 08:44:27 +0100 |
commit | 41a48543aea119acae321aae61b85d711610b652 (patch) | |
tree | da29d1d172eaaa4c9744d77851966b727720ce06 /Domains/crossingScenario/queries/crossingScenarioQueries.vql | |
parent | add Actor+CollisionExists constrs & adjust dreal parser & measurements (diff) | |
download | VIATRA-Generator-41a48543aea119acae321aae61b85d711610b652.tar.gz VIATRA-Generator-41a48543aea119acae321aae61b85d711610b652.tar.zst VIATRA-Generator-41a48543aea119acae321aae61b85d711610b652.zip |
almost finish crossscen VQL + implement ITE handling + prelim results
Diffstat (limited to 'Domains/crossingScenario/queries/crossingScenarioQueries.vql')
-rw-r--r-- | Domains/crossingScenario/queries/crossingScenarioQueries.vql | 277 |
1 files changed, 145 insertions, 132 deletions
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index 03dafc97..34eff55c 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql | |||
@@ -424,88 +424,88 @@ pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists | |||
424 | check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | 424 | check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); |
425 | } | 425 | } |
426 | 426 | ||
427 | //////////////// | 427 | ////////////// |
428 | ////SeparationDistance | 428 | //SeparationDistance |
429 | //////////////// | 429 | ////////////// |
430 | //@Constraint(severity="error", key={a1, sd}, message="x") | 430 | @Constraint(severity="error", key={a1, sd}, message="x") |
431 | //pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | 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 | 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); | 433 | Actor.relations(a1, sd); |
434 | // SeparationDistance.target(sd, a2); | 434 | SeparationDistance.target(sd, a2); |
435 | // SeparationDistance.distance(sd, Distance::Near); | 435 | SeparationDistance.distance(sd, Distance::D_Near); |
436 | // | 436 | |
437 | // Actor.xPos(a1, x1); | 437 | Actor.xPos(a1, x1); |
438 | // Actor.yPos(a1, y1); | 438 | Actor.yPos(a1, y1); |
439 | // Actor.xPos(a2, x2); | 439 | Actor.xPos(a2, x2); |
440 | // Actor.yPos(a2, y2); | 440 | Actor.yPos(a2, y2); |
441 | // //check(dx^2 + dy^2 < 5^2) | 441 | //check(dx^2 + dy^2 < 5^2) |
442 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); | 442 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); |
443 | //} | 443 | } |
444 | // | 444 | |
445 | //@Constraint(severity="error", key={a1, sd}, message="x") | 445 | @Constraint(severity="error", key={a1, sd}, message="x") |
446 | //pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | 446 | pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { |
447 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 447 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
448 | // Actor.relations(a1, sd); | 448 | Actor.relations(a1, sd); |
449 | // SeparationDistance.target(sd, a2); | 449 | SeparationDistance.target(sd, a2); |
450 | // SeparationDistance.distance(sd, Distance::Near); | 450 | SeparationDistance.distance(sd, Distance::D_Near); |
451 | // | 451 | |
452 | // Actor.xPos(a1, x1); | 452 | Actor.xPos(a1, x1); |
453 | // Actor.yPos(a1, y1); | 453 | Actor.yPos(a1, y1); |
454 | // Actor.xPos(a2, x2); | 454 | Actor.xPos(a2, x2); |
455 | // Actor.yPos(a2, y2); | 455 | Actor.yPos(a2, y2); |
456 | // //check(dx^2 + dy^2 > 10^2) | 456 | //check(dx^2 + dy^2 > 10^2) |
457 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | 457 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); |
458 | //} | 458 | } |
459 | // | 459 | |
460 | //@Constraint(severity="error", key={a1, sd}, message="x") | 460 | @Constraint(severity="error", key={a1, sd}, message="x") |
461 | //pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | 461 | pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { |
462 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 462 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
463 | // Actor.relations(a1, sd); | 463 | Actor.relations(a1, sd); |
464 | // SeparationDistance.target(sd, a2); | 464 | SeparationDistance.target(sd, a2); |
465 | // SeparationDistance.distance(sd, Distance::Medium); | 465 | SeparationDistance.distance(sd, Distance::D_Med); |
466 | // | 466 | |
467 | // Actor.xPos(a1, x1); | 467 | Actor.xPos(a1, x1); |
468 | // Actor.yPos(a1, y1); | 468 | Actor.yPos(a1, y1); |
469 | // Actor.xPos(a2, x2); | 469 | Actor.xPos(a2, x2); |
470 | // Actor.yPos(a2, y2); | 470 | Actor.yPos(a2, y2); |
471 | // //check(dx^2 + dy^2 < 10^2) | 471 | //check(dx^2 + dy^2 < 10^2) |
472 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | 472 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); |
473 | //} | 473 | } |
474 | // | 474 | |
475 | //@Constraint(severity="error", key={a1, sd}, message="x") | 475 | @Constraint(severity="error", key={a1, sd}, message="x") |
476 | //pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | 476 | pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { |
477 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 477 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
478 | // Actor.relations(a1, sd); | 478 | Actor.relations(a1, sd); |
479 | // SeparationDistance.target(sd, a2); | 479 | SeparationDistance.target(sd, a2); |
480 | // SeparationDistance.distance(sd, Distance::Medium); | 480 | SeparationDistance.distance(sd, Distance::D_Med); |
481 | // | 481 | |
482 | // Actor.xPos(a1, x1); | 482 | Actor.xPos(a1, x1); |
483 | // Actor.yPos(a1, y1); | 483 | Actor.yPos(a1, y1); |
484 | // Actor.xPos(a2, x2); | 484 | Actor.xPos(a2, x2); |
485 | // Actor.yPos(a2, y2); | 485 | Actor.yPos(a2, y2); |
486 | // //check(dx^2 + dy^2 > 1^2) | 486 | //check(dx^2 + dy^2 > 1^2) |
487 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); | 487 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); |
488 | //} | 488 | } |
489 | // | 489 | |
490 | //@Constraint(severity="error", key={a1, sd}, message="x") | 490 | @Constraint(severity="error", key={a1, sd}, message="x") |
491 | //pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | 491 | pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { |
492 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 492 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
493 | // Actor.relations(a1, sd); | 493 | Actor.relations(a1, sd); |
494 | // SeparationDistance.target(sd, a2); | 494 | SeparationDistance.target(sd, a2); |
495 | // SeparationDistance.distance(sd, Distance::Far); | 495 | SeparationDistance.distance(sd, Distance::D_Far); |
496 | // | 496 | |
497 | // Actor.xPos(a1, x1); | 497 | Actor.xPos(a1, x1); |
498 | // Actor.yPos(a1, y1); | 498 | Actor.yPos(a1, y1); |
499 | // Actor.xPos(a2, x2); | 499 | Actor.xPos(a2, x2); |
500 | // Actor.yPos(a2, y2); | 500 | Actor.yPos(a2, y2); |
501 | // //check(dx^2 + dy^2 < 15^2) | 501 | //check(dx^2 + dy^2 < 15^2) |
502 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | 502 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); |
503 | //} | 503 | } |
504 | // | 504 | |
505 | //////////////// | 505 | //////////////// |
506 | ////CollisionDoesNotExist | 506 | ////CollisionDoesNotExist |
507 | //////////////// | 507 | //////////////// |
508 | // | 508 | //TODO |
509 | ////@Constraint(severity="error", key={a1, cdne}, message="x") | 509 | ////@Constraint(severity="error", key={a1, cdne}, message="x") |
510 | ////pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) { | 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 | 511 | //// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
@@ -532,59 +532,72 @@ pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists | |||
532 | //// //check(dx^2 + dy^2 < 15^2) | 532 | //// //check(dx^2 + dy^2 < 15^2) |
533 | //// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | 533 | //// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); |
534 | ////} | 534 | ////} |
535 | // | 535 | |
536 | //////////////// | 536 | ////////////// |
537 | ////VisionBlocked | 537 | //VisionBlocked |
538 | //////////////// | 538 | ////////////// |
539 | // | 539 | |
540 | ////OPTIONS 1: everything is from a single check expression containing ITEs | 540 | @Constraint(severity="error", key={a1, a2}, message="x") |
541 | ////Currently unhandled bygenerator | 541 | pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) { |
542 | //@Constraint(severity="error", key={a1, vb}, message="x") | 542 | Actor.relations(a1, vb); |
543 | //pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { | 543 | VisionBlocked.target(vb, a2); |
544 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 544 | VisionBlocked.blockedBy(vb, a1); |
545 | // Actor.relations(a1, vb); | 545 | } or { |
546 | // VisionBlocked.target(vb, a2); | 546 | Actor.relations(a1, vb); |
547 | // VisionBlocked.blockedBy(vb, aBlocker); | 547 | VisionBlocked.target(vb, a2); |
548 | // | 548 | VisionBlocked.blockedBy(vb, a1); |
549 | // Actor.xPos(a1, x1); | 549 | } |
550 | // Actor.yPos(a1, y1); | 550 | |
551 | // Actor.xPos(a2, x2); | 551 | //OPTIONS 1: everything is from a single check expression containing ITEs |
552 | // Actor.yPos(a2, y2); | 552 | //Currently unhandled bygenerator |
553 | // Actor.xPos(aBlocker, xBlocker); | 553 | @Constraint(severity="error", key={a1, vb}, message="x") |
554 | // Actor.yPos(aBlocker, yBlocker); | 554 | pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { |
555 | // Actor.length(aBlocker, lenBlocker); | 555 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
556 | // Actor.width(aBlocker, widBlocker); | 556 | Actor.relations(a1, vb); |
557 | // | 557 | VisionBlocked.target(vb, a2); |
558 | // //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | 558 | VisionBlocked.blockedBy(vb, aBlocker); |
559 | // check( | 559 | |
560 | // ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / | 560 | Actor.xPos(a1, x1); |
561 | // ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) | 561 | Actor.yPos(a1, y1); |
562 | // < ((y1-y2)/(x1-x2))); | 562 | Actor.xPos(a2, x2); |
563 | //} | 563 | Actor.yPos(a2, y2); |
564 | // | 564 | Actor.xPos(aBlocker, xBlocker); |
565 | //@Constraint(severity="error", key={a1, vb}, message="x") | 565 | Actor.yPos(aBlocker, yBlocker); |
566 | //pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { | 566 | Actor.length(aBlocker, lenBlocker); |
567 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 567 | Actor.width(aBlocker, widBlocker); |
568 | // Actor.relations(a1, vb); | 568 | |
569 | // VisionBlocked.target(vb, a2); | 569 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) |
570 | // VisionBlocked.blockedBy(vb, aBlocker); | 570 | check( |
571 | // | 571 | ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / |
572 | // Actor.xPos(a1, x1); | 572 | ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) |
573 | // Actor.yPos(a1, y1); | 573 | < ((y1-y2)/(x1-x2))); |
574 | // Actor.xPos(a2, x2); | 574 | } |
575 | // Actor.yPos(a2, y2); | 575 | |
576 | // Actor.xPos(aBlocker, xBlocker); | 576 | @Constraint(severity="error", key={a1, vb}, message="x") |
577 | // Actor.yPos(aBlocker, yBlocker); | 577 | pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { |
578 | // Actor.length(aBlocker, lenBlocker); | 578 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
579 | // Actor.width(aBlocker, widBlocker); | 579 | Actor.relations(a1, vb); |
580 | // | 580 | VisionBlocked.target(vb, a2); |
581 | // //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | 581 | VisionBlocked.blockedBy(vb, aBlocker); |
582 | // check( | 582 | |
583 | // ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / | 583 | Actor.xPos(a1, x1); |
584 | // ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) | 584 | Actor.yPos(a1, y1); |
585 | // > ((y1-y2)/(x1-x2))); | 585 | Actor.xPos(a2, x2); |
586 | //} | 586 | Actor.yPos(a2, y2); |
587 | // | 587 | Actor.xPos(aBlocker, xBlocker); |
588 | Actor.yPos(aBlocker, yBlocker); | ||
589 | Actor.length(aBlocker, lenBlocker); | ||
590 | Actor.width(aBlocker, widBlocker); | ||
591 | |||
592 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | ||
593 | check( | ||
594 | ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / | ||
595 | ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) | ||
596 | > ((y1-y2)/(x1-x2))); | ||
597 | } | ||
598 | |||
599 | |||
600 | |||
588 | ////OPTION 2: | 601 | ////OPTION 2: |
589 | ////we handle ITE by seperating the constraints | 602 | ////we handle ITE by seperating the constraints |
590 | // | 603 | // |