aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-12 19:04:16 +0100
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-12 19:04:16 +0100
commitdc0249ec0e322387ec98350c3c633dffade21f63 (patch)
tree4bf8c53ff71b5551dd246e1164de95d1bbc22781
parentmeasurement setup is ready for server (diff)
downloadVIATRA-Generator-dc0249ec0e322387ec98350c3c633dffade21f63.tar.gz
VIATRA-Generator-dc0249ec0e322387ec98350c3c633dffade21f63.tar.zst
VIATRA-Generator-dc0249ec0e322387ec98350c3c633dffade21f63.zip
add cs scalability case study artifacts
Diffstat
-rw-r--r--Domains/crossingScenario/inputs/csGenScale.vsconfig33
-rw-r--r--Domains/crossingScenario/inputs/csInitScale.xmi31
-rw-r--r--Domains/crossingScenario/queries/csQueriesScale.vql220
3 files changed, 284 insertions, 0 deletions
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 @@
1import epackage "model/crossingScenario.ecore"
2import viatra "queries/csQueriesScale.vql"
3
4generate {
5 metamodel = { package crossingScenario }
6 constraints = { package queries}
7 partial-model = { "inputs/csInitScale.xmi"}
8 solver = ViatraSolver
9 scope = {
10 #node += 15..*
11 ,#<Lane> += 0
12 ,#<Relation> += 0
13 //,#<CollisionExists> = 1
14 //,#<SeparationDistance> = 0
15 //,#<VisionBlocked> += 0
16 //,#<CollisionDoesNotExist> += 0
17 }
18
19 config = {
20 runtime = 10000,
21 log-level = none,
22 "numeric-solver" = "z3",
23 "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal",
24 //"strategy" = "crossingScenario",
25 "scopePropagator" = "polyhedral"}
26
27 runs = 1
28 number = 3
29 debug = "outputs/debug"
30 log = "outputs/debug/log.txt"
31 output = "outputs/models"
32 statistics = "outputs/statistics.csv"
33}
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 @@
1<?xml version="1.0" encoding="UTF-8"?>
2<crossingScenario:CrossingScenario
3 xmi:version="2.0"
4 xmlns:xmi="http://www.omg.org/XMI"
5 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
6 xmlns:crossingScenario="http://www.example.com/crossingScenario"
7 xsi:schemaLocation="http://www.example.com/crossingScenario ../model/crossingScenario.ecore"
8 xSize="30.0"
9 ySize="30.0"
10 maxTime="60.0"
11 maxXSpeed="10.0"
12 maxYSpeed="10.0">
13 <lanes xsi:type="crossingScenario:Lane_Horizontal"/>
14 <lanes xsi:type="crossingScenario:Lane_Horizontal"
15 referenceCoord="3.0"/>
16 <lanes xsi:type="crossingScenario:Lane_Horizontal"
17 referenceCoord="6.0"/>
18 <lanes xsi:type="crossingScenario:Lane_Horizontal"
19 referenceCoord="9.0"/>
20 <lanes xsi:type="crossingScenario:Lane_Horizontal"
21 referenceCoord="12.0"/>
22 <lanes xsi:type="crossingScenario:Lane_Vertical"/>
23 <lanes xsi:type="crossingScenario:Lane_Vertical"
24 referenceCoord="3.0"/>
25 <lanes xsi:type="crossingScenario:Lane_Vertical"
26 referenceCoord="6.0"/>
27 <lanes xsi:type="crossingScenario:Lane_Vertical"
28 referenceCoord="9.0"/>
29 <lanes xsi:type="crossingScenario:Lane_Vertical"
30 referenceCoord="12.0"/>
31</crossingScenario:CrossingScenario>
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 @@
1package queries
2
3import "http://www.example.com/crossingScenario"
4import "http://www.eclipse.org/emf/2002/Ecore"
5
6///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
7//Lane+Actor
8///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
9
10/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw]
11@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
12pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) {
13 Actor.placedOn(a, vl);
14 Actor.xPos(a, x);
15 Lane.referenceCoord(vl, r);
16 check(x <= r);
17} or {
18 Actor.placedOn(a, vl);
19 Actor.xPos(a, x);
20 Lane.referenceCoord(vl, r);
21// //<<<<OLD>>>>
22// Lane.numWidth(vl, w);
23// check(x >= (r + w));
24
25 //<<<<NEW>>>>: lanes all have width=3
26 check(x >= (r + 3.0));
27}
28
29@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
30pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) {
31 Actor.placedOn(a, hl);
32 Actor.yPos(a, y);
33 Lane.referenceCoord(hl, r);
34 check(y <= r);
35} or {
36 Actor.placedOn(a, hl);
37 Actor.yPos(a, y);
38 Lane.referenceCoord(hl, r);
39// //<<OLD>>
40// Lane.numWidth(hl, w);
41// check(y >= (r + w));
42
43 //<<NEW>>: lanes all have width=3
44 check(y >= (r + 3.0));
45
46}
47
48///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
49//Actor
50///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
51
52/////----------------
53//Xpos and Ypos Bounds
54/////----------------
55
56private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor,
57 xMax:java Double, xP:java Double) {
58 Actor.placedOn(a, hl);
59 Lane_Horizontal(hl);
60 CrossingScenario.actors(cs, a);
61 CrossingScenario.xSize(cs, xMax);
62 Actor.xPos(a, xP);
63}
64
65private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor,
66 yMax:java Double, yP:java Double) {
67 Actor.placedOn(a, vl);
68 Lane_Vertical(vl);
69 CrossingScenario.actors(cs, a);
70 CrossingScenario.ySize(cs, yMax);
71 Actor.yPos(a, yP);
72}
73
74@Constraint(severity="error", key={cs}, message="x")
75pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) {
76 find helper_horiz_getXAndBounds(cs, a, xMax, xP);
77 check(xP >= xMax);}
78
79@Constraint(severity="error", key={cs}, message="x")
80pattern define_actor_minXp(cs:CrossingScenario, a:Actor) {
81 find helper_horiz_getXAndBounds(cs, a, xMax, xP);
82 check(xP <= 0-xMax);}
83
84@Constraint(severity="error", key={cs}, message="x")
85pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) {
86 find helper_vert_getYAndBounds(cs, a, yMax, yP);
87 check(yP >= yMax);}
88
89@Constraint(severity="error", key={cs}, message="x")
90pattern define_actor_minYp(cs:CrossingScenario, a:Actor) {
91 find helper_vert_getYAndBounds(cs, a, yMax, yP);
92 check(yP <= 0-yMax);}
93
94//Minimum Distances
95private pattern helper_getCoords(a1:Actor,
96 a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) {
97 Actor.xPos(a1, x1);
98 Actor.yPos(a1, y1);
99 Actor.xPos(a2, x2);
100 Actor.yPos(a2, y2);
101}
102
103//INFO may remove?
104@Constraint(severity="error", key={a1, a2}, message="x")
105pattern define_actor_minimumDistance(a1: Actor, a2: Actor) {
106 find helper_getCoords(a1, a2, x1, x2, y1, y2);
107 a1 != a2;
108 //check(dx^2 + dy^2 < 4^2)
109 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 4*4);
110}
111
112/////----------------
113//Xspeed and Yspeed bounds
114/////----------------
115/*
116/////////VERTICAL LANE
117@Constraint(severity="error", key={a}, message="7 Actor")
118pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) {
119 Actor.placedOn(a, vl);
120 Lane_Vertical(vl);
121 Actor.xSpeed(a, xSpeed);
122 check(xSpeed != 0.0);
123}
124
125private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor,
126 ySpeedMax:java Double, ySpeed:java Double) {
127 Actor.placedOn(a, vl);
128 Lane_Vertical(vl);
129 CrossingScenario.actors(cs, a);
130 CrossingScenario.maxYSpeed(cs, ySpeedMax);
131 Actor.ySpeed(a, ySpeed);
132}
133
134@Constraint(severity="error", key={cs}, message="x")
135pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) {
136 find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS);
137 check(yS <= 0.0-ySMax);
138}
139
140@Constraint(severity="error", key={cs}, message="x")
141pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) {
142 find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS);
143 check(yS >= ySMax);
144}
145
146/////////HORIZONTAL LANE
147@Constraint(severity="error", key={a}, message="7 Actor")
148pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) {
149 Actor.placedOn(a, hl);
150 Lane_Horizontal(hl);
151 Actor.ySpeed(a, ySpeed);
152 check(ySpeed != 0.0);
153}
154
155private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor,
156 xSpeedMax:java Double, xSpeed:java Double) {
157 Actor.placedOn(a, hl);
158 Lane_Horizontal(hl);
159 CrossingScenario.actors(cs, a);
160 CrossingScenario.maxXSpeed(cs, xSpeedMax);
161 Actor.xSpeed(a, xSpeed);
162}
163
164@Constraint(severity="error", key={cs}, message="x")
165pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) {
166 find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS);
167 check(xS <= 0.0-xSMax);
168}
169
170@Constraint(severity="error", key={cs}, message="x")
171pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) {
172 find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS);
173 check(xS >= xSMax);
174}
175*/
176/////----------------
177/////WIDTH and LENGTH
178/////----------------
179
180///////pedestrian-width (3)
181@Constraint(severity="error", key={p}, message="3 Actor")
182pattern define_actor_pedestrianWidth(p:Pedestrian) {
183 Pedestrian.width(p, w);
184 check(w != 1.0);
185}
186
187/////////pedestrian-width (4)
188@Constraint(severity="error", key={p}, message="4 Actor")
189pattern define_actor_pedestrianLength(p:Pedestrian) {
190 Pedestrian.length(p, l);
191 check(l != 1.0);
192}
193
194/////////actor-width (5)
195@Constraint(severity="error", key={v}, message="5 Actor")
196pattern define_actor_vehicleWidth(v:Vehicle) {
197 Vehicle.placedOn(v, lane);
198 Lane_Vertical(lane);
199 Vehicle.width(v, w);
200 check(w != 2.0);
201} or {
202 Vehicle.placedOn(v, lane);
203 Lane_Horizontal(lane);
204 Vehicle.width(v, w);
205 check(w != 3.0);
206}
207
208/////////actor-width (6)
209@Constraint(severity="error", key={v}, message="6 Actor")
210pattern define_actor_vehicleLength(v:Vehicle) {
211 Vehicle.placedOn(v, lane);
212 Lane_Vertical(lane);
213 Vehicle.length(v, l);
214 check(l != 3.0);
215} or {
216 Vehicle.placedOn(v, lane);
217 Lane_Horizontal(lane);
218 Vehicle.length(v, l);
219 check(l != 2.0);
220}
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-19 15:32:53 +0000