diff options
author | 2021-01-22 00:50:08 +0100 | |
---|---|---|
committer | 2021-01-22 00:50:08 +0100 | |
commit | 8ac747b1b84513c70f8445a7c84c6a3644a1f6fa (patch) | |
tree | 7dcb0ae4b0c62c5528be51e9396185fc9b7274a7 /Domains/crossingScenario | |
parent | Major MM update + Refactor VQL + post-meeting approach change (diff) | |
download | VIATRA-Generator-8ac747b1b84513c70f8445a7c84c6a3644a1f6fa.tar.gz VIATRA-Generator-8ac747b1b84513c70f8445a7c84c6a3644a1f6fa.tar.zst VIATRA-Generator-8ac747b1b84513c70f8445a7c84c6a3644a1f6fa.zip |
implement ignored attribute values as a config option
Diffstat (limited to 'Domains/crossingScenario')
-rw-r--r-- | Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig | 1 | ||||
-rw-r--r-- | Domains/crossingScenario/queries/crossingScenarioQueries.vql | 182 |
2 files changed, 92 insertions, 91 deletions
diff --git a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig index 1db557a9..bee56db6 100644 --- a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig +++ b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig | |||
@@ -23,6 +23,7 @@ generate { | |||
23 | log-level = none, | 23 | log-level = none, |
24 | "numeric-solver" = "dreal-local", | 24 | "numeric-solver" = "dreal-local", |
25 | "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal", | 25 | "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal", |
26 | "ignored-attributes" = "CrossingScenario.maxTime=60", | ||
26 | "scopePropagator" = "polyhedral"} | 27 | "scopePropagator" = "polyhedral"} |
27 | 28 | ||
28 | runs = 1 | 29 | runs = 1 |
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index 179da874..2b67e14c 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql | |||
@@ -429,97 +429,97 @@ pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { | |||
429 | //CollisionExists | 429 | //CollisionExists |
430 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | 430 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |
431 | 431 | ||
432 | //@Constraint(severity="error", key={c}, message="x") | 432 | @Constraint(severity="error", key={c}, message="x") |
433 | //pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { | 433 | pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { |
434 | // CrossingScenario.relations(ss, c); | 434 | CrossingScenario.relations(ss, c); |
435 | // CrossingScenario.maxTime(ss, maxTime); | 435 | CrossingScenario.maxTime(ss, maxTime); |
436 | // CollisionExists.collisionTime(c, cTime); | 436 | CollisionExists.collisionTime(c, cTime); |
437 | // check(cTime >= maxTime);} | 437 | check(cTime >= maxTime);} |
438 | // | 438 | |
439 | //@Constraint(severity="error", key={c}, message="x") | 439 | @Constraint(severity="error", key={c}, message="x") |
440 | //pattern collisionExists_timeNotNegative(c:CollisionExists) { | 440 | pattern collisionExists_timeNotNegative(c:CollisionExists) { |
441 | // CollisionExists. collisionTime(c, cTime); | 441 | CollisionExists. collisionTime(c, cTime); |
442 | // check(cTime <= 0.0);} | 442 | check(cTime <= 0.0);} |
443 | // | 443 | |
444 | //private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) { | 444 | private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) { |
445 | // CollisionExists.source(c, a1); | 445 | CollisionExists.source(c, a1); |
446 | // CollisionExists.target(c, a2); | 446 | CollisionExists.target(c, a2); |
447 | // CollisionExists. collisionTime(c, cTime); | 447 | CollisionExists. collisionTime(c, cTime); |
448 | //} | 448 | } |
449 | // | 449 | |
450 | //private pattern helper_getYCoords(a:Actor, l:java Double, | 450 | private pattern helper_getYCoords(a:Actor, l:java Double, |
451 | // yPos:java Double, ySpeed:java Double) { | 451 | yPos:java Double, ySpeed:java Double) { |
452 | // | 452 | |
453 | // Actor.length(a, l); | 453 | Actor.length(a, l); |
454 | // Actor.yPos(a, yPos); | 454 | Actor.yPos(a, yPos); |
455 | // Actor.ySpeed(a, ySpeed); | 455 | Actor.ySpeed(a, ySpeed); |
456 | //} | 456 | } |
457 | // | 457 | |
458 | //private pattern helper_getAllYCoords(a1:Actor, a2: Actor, | 458 | private pattern helper_getAllYCoords(a1:Actor, a2: Actor, |
459 | // l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double, | 459 | l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double, |
460 | // ySpeed1:java Double, ySpeed2:java Double) { | 460 | ySpeed1:java Double, ySpeed2:java Double) { |
461 | // | 461 | |
462 | // find helper_getYCoords(a1, l1, yPos1, ySpeed1); | 462 | find helper_getYCoords(a1, l1, yPos1, ySpeed1); |
463 | // find helper_getYCoords(a2, l2, yPos2, ySpeed2); | 463 | find helper_getYCoords(a2, l2, yPos2, ySpeed2); |
464 | //} | 464 | } |
465 | // | 465 | |
466 | //private pattern helper_getXCoords(a:Actor, l:java Double, | 466 | private pattern helper_getXCoords(a:Actor, l:java Double, |
467 | // xPos:java Double, xSpeed:java Double) { | 467 | xPos:java Double, xSpeed:java Double) { |
468 | // | 468 | |
469 | // Actor.length(a, l); | 469 | Actor.length(a, l); |
470 | // Actor.xPos(a, xPos); | 470 | Actor.xPos(a, xPos); |
471 | // Actor.xSpeed(a, xSpeed); | 471 | Actor.xSpeed(a, xSpeed); |
472 | //} | 472 | } |
473 | // | 473 | |
474 | //private pattern helper_getAllXCoords(a1:Actor, a2: Actor, | 474 | private pattern helper_getAllXCoords(a1:Actor, a2: Actor, |
475 | // w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double, | 475 | w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double, |
476 | // xSpeed1:java Double, xSpeed2:java Double) { | 476 | xSpeed1:java Double, xSpeed2:java Double) { |
477 | // | 477 | |
478 | // find helper_getYCoords(a1, w1, xPos1, xSpeed1); | 478 | find helper_getYCoords(a1, w1, xPos1, xSpeed1); |
479 | // find helper_getYCoords(a2, w2, xPos2, xSpeed2); | 479 | find helper_getYCoords(a2, w2, xPos2, xSpeed2); |
480 | //} | 480 | } |
481 | // | 481 | |
482 | //@Constraint(severity="error", key={a1}, message="x") | 482 | @Constraint(severity="error", key={a1}, message="x") |
483 | //pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) { | 483 | pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) { |
484 | // | 484 | |
485 | // find helper_getCollExistsTime(a1, a2, cTime); | 485 | find helper_getCollExistsTime(a1, a2, cTime); |
486 | // find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | 486 | find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); |
487 | // | 487 | |
488 | // //check(y_1_bottom > y_2_top | 488 | //check(y_1_bottom > y_2_top |
489 | // check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); | 489 | check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); |
490 | //} | 490 | } |
491 | // | 491 | |
492 | //@Constraint(severity="error", key={a1}, message="x") | 492 | @Constraint(severity="error", key={a1}, message="x") |
493 | //pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) { | 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 | 494 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
495 | // | 495 | |
496 | // find helper_getCollExistsTime(a1, a2, cTime); | 496 | find helper_getCollExistsTime(a1, a2, cTime); |
497 | // find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); | 497 | find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); |
498 | // | 498 | |
499 | // //check(y_1_top < y_2_bottom) | 499 | //check(y_1_top < y_2_bottom) |
500 | // check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); | 500 | check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); |
501 | //} | 501 | } |
502 | // | 502 | |
503 | //@Constraint(severity="error", key={a1}, message="x") | 503 | @Constraint(severity="error", key={a1}, message="x") |
504 | //pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) { | 504 | pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) { |
505 | // | 505 | |
506 | // find helper_getCollExistsTime(a1, a2, cTime); | 506 | find helper_getCollExistsTime(a1, a2, cTime); |
507 | // find helper_getAllYCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | 507 | find helper_getAllYCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); |
508 | // | 508 | |
509 | // //check(x_1_left > x_2_right) | 509 | //check(x_1_left > x_2_right) |
510 | // check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); | 510 | check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); |
511 | //} | 511 | } |
512 | // | 512 | |
513 | //@Constraint(severity="error", key={a1}, message="x") | 513 | @Constraint(severity="error", key={a1}, message="x") |
514 | //pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { | 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 | 515 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
516 | // | 516 | |
517 | // find helper_getCollExistsTime(a1, a2, cTime); | 517 | find helper_getCollExistsTime(a1, a2, cTime); |
518 | // find helper_getAllYCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); | 518 | find helper_getAllYCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); |
519 | // | 519 | |
520 | // //check(x_1_right < x_2_left) | 520 | //check(x_1_right < x_2_left) |
521 | // check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | 521 | check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); |
522 | //} | 522 | } |
523 | 523 | ||
524 | 524 | ||
525 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// | 525 | ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// |