From dc0249ec0e322387ec98350c3c633dffade21f63 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Fri, 12 Feb 2021 19:04:16 +0100 Subject: add cs scalability case study artifacts --- .../crossingScenario/inputs/csGenScale.vsconfig | 33 ++++ Domains/crossingScenario/inputs/csInitScale.xmi | 31 +++ .../crossingScenario/queries/csQueriesScale.vql | 220 +++++++++++++++++++++ 3 files changed, 284 insertions(+) create mode 100644 Domains/crossingScenario/inputs/csGenScale.vsconfig create mode 100644 Domains/crossingScenario/inputs/csInitScale.xmi create mode 100644 Domains/crossingScenario/queries/csQueriesScale.vql diff --git a/Domains/crossingScenario/inputs/csGenScale.vsconfig b/Domains/crossingScenario/inputs/csGenScale.vsconfig new file mode 100644 index 00000000..d770986b --- /dev/null +++ b/Domains/crossingScenario/inputs/csGenScale.vsconfig @@ -0,0 +1,33 @@ +import epackage "model/crossingScenario.ecore" +import viatra "queries/csQueriesScale.vql" + +generate { + metamodel = { package crossingScenario } + constraints = { package queries} + partial-model = { "inputs/csInitScale.xmi"} + solver = ViatraSolver + scope = { + #node += 15..* + ,# += 0 + ,# += 0 + //,# = 1 + //,# = 0 + //,# += 0 + //,# += 0 + } + + config = { + runtime = 10000, + log-level = none, + "numeric-solver" = "z3", + "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal", + //"strategy" = "crossingScenario", + "scopePropagator" = "polyhedral"} + + runs = 1 + number = 3 + debug = "outputs/debug" + log = "outputs/debug/log.txt" + output = "outputs/models" + statistics = "outputs/statistics.csv" +} diff --git a/Domains/crossingScenario/inputs/csInitScale.xmi b/Domains/crossingScenario/inputs/csInitScale.xmi new file mode 100644 index 00000000..5eee1734 --- /dev/null +++ b/Domains/crossingScenario/inputs/csInitScale.xmi @@ -0,0 +1,31 @@ + + + + + + + + + + + + + diff --git a/Domains/crossingScenario/queries/csQueriesScale.vql b/Domains/crossingScenario/queries/csQueriesScale.vql new file mode 100644 index 00000000..d3afa775 --- /dev/null +++ b/Domains/crossingScenario/queries/csQueriesScale.vql @@ -0,0 +1,220 @@ +package queries + +import "http://www.example.com/crossingScenario" +import "http://www.eclipse.org/emf/2002/Ecore" + +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//Lane+Actor +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] +@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") +pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { + Actor.placedOn(a, vl); + Actor.xPos(a, x); + Lane.referenceCoord(vl, r); + check(x <= r); +} or { + Actor.placedOn(a, vl); + Actor.xPos(a, x); + Lane.referenceCoord(vl, r); +// //<<<>>> +// Lane.numWidth(vl, w); +// check(x >= (r + w)); + + //<<<>>>: lanes all have width=3 + check(x >= (r + 3.0)); +} + +@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") +pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { + Actor.placedOn(a, hl); + Actor.yPos(a, y); + Lane.referenceCoord(hl, r); + check(y <= r); +} or { + Actor.placedOn(a, hl); + Actor.yPos(a, y); + Lane.referenceCoord(hl, r); +// //<> +// Lane.numWidth(hl, w); +// check(y >= (r + w)); + + //<>: lanes all have width=3 + check(y >= (r + 3.0)); + +} + +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//Actor +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +/////---------------- +//Xpos and Ypos Bounds +/////---------------- + +private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor, + xMax:java Double, xP:java Double) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + CrossingScenario.actors(cs, a); + CrossingScenario.xSize(cs, xMax); + Actor.xPos(a, xP); +} + +private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor, + yMax:java Double, yP:java Double) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + CrossingScenario.actors(cs, a); + CrossingScenario.ySize(cs, yMax); + Actor.yPos(a, yP); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXAndBounds(cs, a, xMax, xP); + check(xP >= xMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXAndBounds(cs, a, xMax, xP); + check(xP <= 0-xMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { + find helper_vert_getYAndBounds(cs, a, yMax, yP); + check(yP >= yMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { + find helper_vert_getYAndBounds(cs, a, yMax, yP); + check(yP <= 0-yMax);} + +//Minimum Distances +private pattern helper_getCoords(a1:Actor, + a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { + Actor.xPos(a1, x1); + Actor.yPos(a1, y1); + Actor.xPos(a2, x2); + Actor.yPos(a2, y2); +} + +//INFO may remove? +@Constraint(severity="error", key={a1, a2}, message="x") +pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + a1 != a2; + //check(dx^2 + dy^2 < 4^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 4*4); +} + +/////---------------- +//Xspeed and Yspeed bounds +/////---------------- +/* +/////////VERTICAL LANE +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + Actor.xSpeed(a, xSpeed); + check(xSpeed != 0.0); +} + +private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, + ySpeedMax:java Double, ySpeed:java Double) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + CrossingScenario.actors(cs, a); + CrossingScenario.maxYSpeed(cs, ySpeedMax); + Actor.ySpeed(a, ySpeed); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { + find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); + check(yS <= 0.0-ySMax); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) { + find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); + check(yS >= ySMax); +} + +/////////HORIZONTAL LANE +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + Actor.ySpeed(a, ySpeed); + check(ySpeed != 0.0); +} + +private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, + xSpeedMax:java Double, xSpeed:java Double) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + CrossingScenario.actors(cs, a); + CrossingScenario.maxXSpeed(cs, xSpeedMax); + Actor.xSpeed(a, xSpeed); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); + check(xS <= 0.0-xSMax); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); + check(xS >= xSMax); +} +*/ +/////---------------- +/////WIDTH and LENGTH +/////---------------- + +///////pedestrian-width (3) +@Constraint(severity="error", key={p}, message="3 Actor") +pattern define_actor_pedestrianWidth(p:Pedestrian) { + Pedestrian.width(p, w); + check(w != 1.0); +} + +/////////pedestrian-width (4) +@Constraint(severity="error", key={p}, message="4 Actor") +pattern define_actor_pedestrianLength(p:Pedestrian) { + Pedestrian.length(p, l); + check(l != 1.0); +} + +/////////actor-width (5) +@Constraint(severity="error", key={v}, message="5 Actor") +pattern define_actor_vehicleWidth(v:Vehicle) { + Vehicle.placedOn(v, lane); + Lane_Vertical(lane); + Vehicle.width(v, w); + check(w != 2.0); +} or { + Vehicle.placedOn(v, lane); + Lane_Horizontal(lane); + Vehicle.width(v, w); + check(w != 3.0); +} + +/////////actor-width (6) +@Constraint(severity="error", key={v}, message="6 Actor") +pattern define_actor_vehicleLength(v:Vehicle) { + Vehicle.placedOn(v, lane); + Lane_Vertical(lane); + Vehicle.length(v, l); + check(l != 3.0); +} or { + Vehicle.placedOn(v, lane); + Lane_Horizontal(lane); + Vehicle.length(v, l); + check(l != 2.0); +} -- cgit v1.2.3-54-g00ecf