aboutsummaryrefslogtreecommitdiffstats
path: root/Domains/crossingScenario/queries/crossingScenarioQueries.vql
diff options
context:
space:
mode:
Diffstat (limited to 'Domains/crossingScenario/queries/crossingScenarioQueries.vql')
-rw-r--r--Domains/crossingScenario/queries/crossingScenarioQueries.vql277
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) { 431pattern 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) { 446pattern 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) { 461pattern 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) { 476pattern 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) { 491pattern 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 541pattern 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); 554pattern 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); 577pattern 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//
generated by cgit v1.2.3-54-g00ecf (git 2.44.0) at 2024-05-02 02:54:54 +0000