diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-02-16 09:01:25 +0100 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-02-16 09:01:25 +0100 |
commit | bc403272d867f82edd623179d82c080e57154c1a (patch) | |
tree | 3551ba142ed725595ee684981fc8973cade2ebf4 /Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql | |
parent | add dreal-timeout flag (diff) | |
download | VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.tar.gz VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.tar.zst VIATRA-Generator-bc403272d867f82edd623179d82c080e57154c1a.zip |
CrossingScenario case study is ready for serverdreal-integration
Diffstat (limited to 'Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql')
-rw-r--r-- | Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql | 220 |
1 files changed, 220 insertions, 0 deletions
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql new file mode 100644 index 00000000..d3afa775 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql | |||
@@ -0,0 +1,220 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http://www.example.com/crossingScenario" | ||
4 | import "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") | ||
12 | pattern 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") | ||
30 | pattern 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 | |||
56 | private 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 | |||
65 | private 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") | ||
75 | pattern 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") | ||
80 | pattern 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") | ||
85 | pattern 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") | ||
90 | pattern 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 | ||
95 | private 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") | ||
105 | pattern 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") | ||
118 | pattern 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 | |||
125 | private 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") | ||
135 | pattern 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") | ||
141 | pattern 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") | ||
148 | pattern 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 | |||
155 | private 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") | ||
165 | pattern 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") | ||
171 | pattern 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") | ||
182 | pattern 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") | ||
189 | pattern 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") | ||
196 | pattern 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") | ||
210 | pattern 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 | } | ||