diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-19 12:46:58 +0100 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-01-19 12:46:58 +0100 |
commit | 953227f62ece22f06bc54a47eeec8bf79b25dc27 (patch) | |
tree | 72bf39c26b2e58bd5ac4ba0506cf78608e80c309 /Domains/crossingScenario/queries/crossingScenarioQueries.vql | |
parent | add vsconfig flag to allow running dreal locally (diff) | |
download | VIATRA-Generator-953227f62ece22f06bc54a47eeec8bf79b25dc27.tar.gz VIATRA-Generator-953227f62ece22f06bc54a47eeec8bf79b25dc27.tar.zst VIATRA-Generator-953227f62ece22f06bc54a47eeec8bf79b25dc27.zip |
add Actor+CollisionExists constrs & adjust dreal parser & measurements
Diffstat (limited to 'Domains/crossingScenario/queries/crossingScenarioQueries.vql')
-rw-r--r-- | Domains/crossingScenario/queries/crossingScenarioQueries.vql | 299 |
1 files changed, 191 insertions, 108 deletions
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index f8bcc92c..03dafc97 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql | |||
@@ -16,7 +16,14 @@ import "http://www.eclipse.org/emf/2002/Ecore" | |||
16 | 16 | ||
17 | //TODO Hard-code xSize? | 17 | //TODO Hard-code xSize? |
18 | //TODO Hard-code ySize? | 18 | //TODO Hard-code ySize? |
19 | |||
19 | //TODO Hard-code maxTime? | 20 | //TODO Hard-code maxTime? |
21 | //@Constraint(severity="error", key={l}, message="3 CrossingScenari") | ||
22 | //pattern define_cs_maxTime(cs:CrossingScenario) { | ||
23 | // CrossingScenario.maxTime(cs, mt); | ||
24 | // check(mt != 60.0); | ||
25 | //} | ||
26 | |||
20 | 27 | ||
21 | ////////////// | 28 | ////////////// |
22 | //Lane | 29 | //Lane |
@@ -195,14 +202,62 @@ pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { | |||
195 | //Actor | 202 | //Actor |
196 | ////////////// | 203 | ////////////// |
197 | 204 | ||
198 | ////TODO | 205 | //Hard-coded stuff |
206 | //TODO THIS IS HARD_CODED | ||
207 | @Constraint(severity="error", key={a}, message="x") | ||
208 | pattern define_actor_maxXp(a:Actor) { | ||
209 | Actor.xPos(a, xP); | ||
210 | check(xP >= 1000.0);} | ||
211 | |||
212 | @Constraint(severity="error", key={a}, message="x") | ||
213 | pattern define_actor_minXp(a:Actor) { | ||
214 | Actor.xPos(a, xP); | ||
215 | check(xP <= 0-1000.0);} | ||
216 | |||
217 | //TODO THIS IS HARD_CODED | ||
218 | @Constraint(severity="error", key={a}, message="x") | ||
219 | pattern define_actor_maxYp(a:Actor) { | ||
220 | Actor.yPos(a, yP); | ||
221 | check(yP >= 1000.0);} | ||
222 | |||
223 | @Constraint(severity="error", key={a}, message="x") | ||
224 | pattern define_actor_minYp(a:Actor) { | ||
225 | Actor.yPos(a, yP); | ||
226 | check(yP <= 0-1000.0);} | ||
227 | |||
228 | //TODO THIS IS HARD_CODED | ||
229 | @Constraint(severity="error", key={a}, message="x") | ||
230 | pattern define_actor_maxXs(a:Actor) { | ||
231 | Actor.xSpeed(a, xS); | ||
232 | check(xS >= 100.0);} | ||
233 | |||
234 | @Constraint(severity="error", key={a}, message="x") | ||
235 | pattern define_actor_minXs(a:Actor) { | ||
236 | Actor.xSpeed(a, xS); | ||
237 | check(xS <= 0-100.0);} | ||
238 | |||
239 | //TODO THIS IS HARD_CODED | ||
240 | @Constraint(severity="error", key={a}, message="x") | ||
241 | pattern define_actor_maxYs(a:Actor) { | ||
242 | Actor.ySpeed(a, yS); | ||
243 | check(yS >= 100.0);} | ||
244 | |||
245 | @Constraint(severity="error", key={a}, message="x") | ||
246 | pattern define_actor_minYs(a:Actor) { | ||
247 | Actor.ySpeed(a, yS); | ||
248 | check(yS <= 0-100.0);} | ||
249 | |||
250 | |||
251 | //END Hard-coded stuff | ||
252 | |||
253 | ////TODO May be required | ||
199 | /////////xPos of every actor mmust be within bounds defined in CS | 254 | /////////xPos of every actor mmust be within bounds defined in CS |
200 | //@Constraint(severity="error", key={l}, message="1 Actor") | 255 | //@Constraint(severity="error", key={l}, message="1 Actor") |
201 | //pattern define_actor_xPosWithinCSbounds(cs:CrossingScenario, a:Actor) { | 256 | //pattern define_actor_xPosWithinCSbounds(cs:CrossingScenario, a:Actor) { |
202 | // | 257 | // |
203 | //} | 258 | //} |
204 | // | 259 | // |
205 | ////TODO | 260 | ////TODO May be required |
206 | /////////yPos of every actor mmust be within bounds defined in CS | 261 | /////////yPos of every actor mmust be within bounds defined in CS |
207 | //@Constraint(severity="error", key={l}, message="2 Actor") | 262 | //@Constraint(severity="error", key={l}, message="2 Actor") |
208 | //pattern define_actor_yPosWithinCSbounds(cs:CrossingScenario, a:Actor) { | 263 | //pattern define_actor_yPosWithinCSbounds(cs:CrossingScenario, a:Actor) { |
@@ -210,38 +265,47 @@ pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { | |||
210 | //} | 265 | //} |
211 | 266 | ||
212 | 267 | ||
213 | /////////pedestrian-width (3) | 268 | ///////pedestrian-width (3) //TODO Derived? |
214 | //pattern define_actor_pedestrianWidth(p:Pedestrian) { | 269 | @Constraint(severity="error", key={p}, message="3 Actor") |
215 | // Pedestrian.width(p, 1.0); | 270 | pattern define_actor_pedestrianWidth(p:Pedestrian) { |
216 | //} | 271 | Pedestrian.width(p, w); |
217 | // | 272 | check(w != 1.0); |
218 | ///////////pedestrian-width (4) | 273 | } |
219 | //pattern define_actor_pedestrianLength(p:Pedestrian) { | ||
220 | // Pedestrian.length(p, 1.0); | ||
221 | //} | ||
222 | 274 | ||
223 | ///////////actor-width (5) | 275 | /////////pedestrian-width (4) //TODO Derived? |
224 | //pattern define_actor_actorWidth(a:Actor) { | 276 | @Constraint(severity="error", key={p}, message="4 Actor") |
225 | // Actor.placedOn(a, l); | 277 | pattern define_actor_pedestrianLength(p:Pedestrian) { |
226 | // Lane_Vertical(l); | 278 | Pedestrian.length(p, l); |
227 | // Actor.width(p, 1.0); | 279 | check(l != 1.0); |
228 | //} or { | 280 | } |
229 | // Actor.placedOn(a, l); | ||
230 | // Lane_Horizontal(l); | ||
231 | // Actor.width(p, 3.0); | ||
232 | //} | ||
233 | // | ||
234 | ///////////actor-width (6) | ||
235 | //pattern define_actor_actorLength(a:Actor) { | ||
236 | // Actor.placedOn(a, l); | ||
237 | // Lane_Vertical(l); | ||
238 | // Actor.length(p, 3.0); | ||
239 | //} or { | ||
240 | // Actor.placedOn(a, l); | ||
241 | // Lane_Horizontal(l); | ||
242 | // Actor.length(p, 1.0); | ||
243 | //} | ||
244 | 281 | ||
282 | /////////actor-width (5) //TODO Derived? | ||
283 | @Constraint(severity="error", key={v}, message="5 Actor") | ||
284 | pattern define_actor_vehicleWidth(v:Vehicle) { | ||
285 | Vehicle.placedOn(v, lane); | ||
286 | Lane_Vertical(lane); | ||
287 | Vehicle.width(v, w); | ||
288 | check(w != 1.0); | ||
289 | } or { | ||
290 | Vehicle.placedOn(v, lane); | ||
291 | Lane_Horizontal(lane); | ||
292 | Vehicle.width(v, w); | ||
293 | check(w != 3.0); | ||
294 | } | ||
295 | |||
296 | /////////actor-width (6) //TODO Derived? | ||
297 | @Constraint(severity="error", key={v}, message="6 Actor") | ||
298 | pattern define_actor_vehicleLength(v:Vehicle) { | ||
299 | Vehicle.placedOn(v, lane); | ||
300 | Lane_Vertical(lane); | ||
301 | Vehicle.length(v, l); | ||
302 | check(l != 3.0); | ||
303 | } or { | ||
304 | Vehicle.placedOn(v, lane); | ||
305 | Lane_Horizontal(lane); | ||
306 | Vehicle.length(v, l); | ||
307 | check(l != 1.0); | ||
308 | } | ||
245 | 309 | ||
246 | /////////xSpeed of actor on verticalLane is 0 | 310 | /////////xSpeed of actor on verticalLane is 0 |
247 | @Constraint(severity="error", key={a}, message="7 Actor") | 311 | @Constraint(severity="error", key={a}, message="7 Actor") |
@@ -259,88 +323,107 @@ pattern define_actor_actorOnHoriLaneHasySpeed0(a:Actor, hl:Lane_Horizontal) { | |||
259 | check(ySpeed != 0); | 323 | check(ySpeed != 0); |
260 | } | 324 | } |
261 | 325 | ||
262 | //////////////// | 326 | ////////////// |
263 | ////CollisionExists | 327 | //Relation |
264 | //////////////// | 328 | ////////////// |
265 | // | 329 | @Constraint(severity="error", key={a1, a2}, message="1 Relation") |
330 | pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { | ||
331 | Actor.relations(a1, r); | ||
332 | Relation.target(r, a2); | ||
333 | a1 == a2; | ||
334 | } | ||
335 | |||
336 | //TODO do above but transitively? | ||
337 | |||
338 | ////////////// | ||
339 | //CollisionExists | ||
340 | ////////////// | ||
341 | |||
342 | //TODO THIS IS HARD_CODED | ||
343 | @Constraint(severity="error", key={c}, message="x") | ||
344 | pattern collisionExists_timeWithinBound(c:CollisionExists) { | ||
345 | CollisionExists. collisionTime(c, cTime); | ||
346 | check(cTime >= 60.0);} | ||
347 | |||
348 | //TODO replace above with this (more general) | ||
266 | //@Constraint(severity="error", key={c}, message="x") | 349 | //@Constraint(severity="error", key={c}, message="x") |
267 | //pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { | 350 | //pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { |
268 | // CrossingScenario.actors.relations(ss, c); | 351 | // CrossingScenario.actors.relations(ss, c); |
269 | // CrossingScenario.maxTime(ss, maxTime); | 352 | // CrossingScenario.maxTime(ss, maxTime); |
270 | // CollisionExists. collisionTime(c, cTime); | 353 | // CollisionExists. collisionTime(c, cTime); |
271 | // check(cTime >= maxTime);} | 354 | // check(cTime >= maxTime);} |
272 | // | 355 | |
273 | //@Constraint(severity="error", key={c}, message="x") | 356 | @Constraint(severity="error", key={c}, message="x") |
274 | //pattern collisionExists_timeNotNegative(c:CollisionExists) { | 357 | pattern collisionExists_timeNotNegative(c:CollisionExists) { |
275 | // CollisionExists. collisionTime(c, cTime); | 358 | CollisionExists. collisionTime(c, cTime); |
276 | // check(cTime <= 0);} | 359 | check(cTime <= 0.0);} |
277 | // | 360 | |
278 | //@Constraint(severity="error", key={a1, c}, message="x") | 361 | @Constraint(severity="error", key={a1, c}, message="x") |
279 | //pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) { | 362 | pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) { |
280 | // Actor.relations(a1, c); | 363 | Actor.relations(a1, c); |
281 | // CollisionExists.target(c, a2); | 364 | CollisionExists.target(c, a2); |
282 | // | 365 | |
283 | // Actor.length(a1, l1); | 366 | Actor.length(a1, l1); |
284 | // Actor.yPos(a1, yPos1); | 367 | Actor.yPos(a1, yPos1); |
285 | // Actor.ySpeed(a1, ySpeed1); | 368 | Actor.ySpeed(a1, ySpeed1); |
286 | // Actor.length(a2, l2); | 369 | Actor.length(a2, l2); |
287 | // Actor.yPos(a2, yPos2); | 370 | Actor.yPos(a2, yPos2); |
288 | // Actor.ySpeed(a2, ySpeed2); | 371 | Actor.ySpeed(a2, ySpeed2); |
289 | // CollisionExists. collisionTime(c, cTime); | 372 | CollisionExists. collisionTime(c, cTime); |
290 | // //check(y_1_bottom > y_2_top | 373 | //check(y_1_bottom > y_2_top |
291 | // check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); | 374 | check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); |
292 | //} | 375 | } |
293 | // | 376 | |
294 | //@Constraint(severity="error", key={a1, c}, message="x") | 377 | @Constraint(severity="error", key={a1, c}, message="x") |
295 | //pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor, c:CollisionExists) { | 378 | pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor, c:CollisionExists) { |
296 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 379 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
297 | // Actor.relations(a1, c); | 380 | Actor.relations(a1, c); |
298 | // CollisionExists.target(c, a2); | 381 | CollisionExists.target(c, a2); |
299 | // | 382 | |
300 | // Actor.length(a1, l1); | 383 | Actor.length(a1, l1); |
301 | // Actor.yPos(a1, yPos1); | 384 | Actor.yPos(a1, yPos1); |
302 | // Actor.ySpeed(a1, ySpeed1); | 385 | Actor.ySpeed(a1, ySpeed1); |
303 | // Actor.length(a2, l2); | 386 | Actor.length(a2, l2); |
304 | // Actor.yPos(a2, yPos2); | 387 | Actor.yPos(a2, yPos2); |
305 | // Actor.ySpeed(a2, ySpeed2); | 388 | Actor.ySpeed(a2, ySpeed2); |
306 | // CollisionExists. collisionTime(c, cTime); | 389 | CollisionExists. collisionTime(c, cTime); |
307 | // //check(y_1_top < y_2_bottom) | 390 | //check(y_1_top < y_2_bottom) |
308 | // check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); | 391 | check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); |
309 | //} | 392 | } |
310 | // | 393 | |
311 | //@Constraint(severity="error", key={a1, c}, message="x") | 394 | @Constraint(severity="error", key={a1, c}, message="x") |
312 | //pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) { | 395 | pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) { |
313 | // Actor.relations(a1, c); | 396 | Actor.relations(a1, c); |
314 | // CollisionExists.target(c, a2); | 397 | CollisionExists.target(c, a2); |
315 | // | 398 | |
316 | // Actor.width(a1, w1); | 399 | Actor.width(a1, w1); |
317 | // Actor.xPos(a1, xPos1); | 400 | Actor.xPos(a1, xPos1); |
318 | // Actor.xSpeed(a1, xSpeed1); | 401 | Actor.xSpeed(a1, xSpeed1); |
319 | // Actor.width(a2, w2); | 402 | Actor.width(a2, w2); |
320 | // Actor.xPos(a2, xPos2); | 403 | Actor.xPos(a2, xPos2); |
321 | // Actor.xSpeed(a2, xSpeed2); | 404 | Actor.xSpeed(a2, xSpeed2); |
322 | // CollisionExists. collisionTime(c, cTime); | 405 | CollisionExists. collisionTime(c, cTime); |
323 | // //check(x_1_left > x_2_right) | 406 | //check(x_1_left > x_2_right) |
324 | // check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); | 407 | check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); |
325 | //} | 408 | } |
326 | // | 409 | |
327 | //@Constraint(severity="error", key={a1, c}, message="x") | 410 | @Constraint(severity="error", key={a1, c}, message="x") |
328 | //pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists) { | 411 | pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists) { |
329 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 412 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
330 | // Actor.relations(a1, c); | 413 | Actor.relations(a1, c); |
331 | // CollisionExists.target(c, a2); | 414 | CollisionExists.target(c, a2); |
332 | // | 415 | |
333 | // Actor.width(a1, w1); | 416 | Actor.width(a1, w1); |
334 | // Actor.xPos(a1, xPos1); | 417 | Actor.xPos(a1, xPos1); |
335 | // Actor.xSpeed(a1, xSpeed1); | 418 | Actor.xSpeed(a1, xSpeed1); |
336 | // Actor.width(a2, w2); | 419 | Actor.width(a2, w2); |
337 | // Actor.xPos(a2, xPos2); | 420 | Actor.xPos(a2, xPos2); |
338 | // Actor.xSpeed(a2, xSpeed2); | 421 | Actor.xSpeed(a2, xSpeed2); |
339 | // CollisionExists. collisionTime(c, cTime); | 422 | CollisionExists. collisionTime(c, cTime); |
340 | // //check(x_1_right < x_2_left) | 423 | //check(x_1_right < x_2_left) |
341 | // check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | 424 | check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); |
342 | //} | 425 | } |
343 | // | 426 | |
344 | //////////////// | 427 | //////////////// |
345 | ////SeparationDistance | 428 | ////SeparationDistance |
346 | //////////////// | 429 | //////////////// |