aboutsummaryrefslogtreecommitdiffstats
path: root/Domains/crossingScenario/queries
diff options
context:
space:
mode:
Diffstat (limited to 'Domains/crossingScenario/queries')
-rw-r--r--Domains/crossingScenario/queries/crossingScenarioQueries.vql325
-rw-r--r--Domains/crossingScenario/queries/moreCompleteQueries2._v_q_l891
2 files changed, 932 insertions, 284 deletions
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql
index c009e031..a26782ae 100644
--- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql
+++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql
@@ -3,180 +3,6 @@ package queries
3import "http://www.example.com/crossingScenario" 3import "http://www.example.com/crossingScenario"
4import "http://www.eclipse.org/emf/2002/Ecore" 4import "http://www.eclipse.org/emf/2002/Ecore"
5 5
6//////Minimal Failing Example
7//@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation")
8//pattern patterThatOnlyWorksWithInt(l : Lane) {
9// Lane.referenceCoord(l, w);
10// check(w <= 0-10.0);
11//}
12
13//////////////
14//CrossingScenario
15/////////////
16
17/*
18//TODO Hard-code xSize?
19//TODO Hard-code ySize?
20
21//TODO Hard-code maxTime?
22@Constraint(severity="error", key={l}, message="3 CrossingScenari")
23pattern define_cs_maxTime(cs:CrossingScenario) {
24 CrossingScenario.maxTime(cs, mt);
25 check(mt != 60.0);
26}
27*/
28
29///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
30//Lane
31///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
32/*
33
34////<<<<OLD>>>>
35////Width: Different Lanes
36//@Constraint(severity="error", key={l}, message="1 Lane")
37//pattern define_numWidth_small(l : Lane) {
38// Lane.width(l, Size::S_Small);
39// Lane.numWidth(l, nw);
40// check(nw <= 5.0);
41//} or {
42// Lane.width(l, Size::S_Small);
43// Lane.numWidth(l, nw);
44// check(nw >= 10.0);
45//}
46//
47//@Constraint(severity="error", key={l}, message="2 Lane")
48//pattern define_numWidth_medium(l : Lane) {
49// Lane.width(l, ::S_Med);
50// Lane.numWidth(l, nw);
51// check(nw <= 10.0);
52//}
53//or {
54// Lane.width(l, Size::S_Med);
55// Lane.numWidth(l, nw);
56// check(nw >= 15.0);
57//}
58//
59//@Constraint(severity="error", key={l}, message="3 Lane")
60//pattern define_numWidth_large(l : Lane) {
61// Lane.width(l, Size::S_Large);
62// Lane.numWidth(l, nw);
63// check(nw <= 15.0);
64//}
65//or {
66// Lane.width(l, Size::S_Large);
67// Lane.numWidth(l, nw);
68// check(nw >= 20.0);
69//}
70
71//<<<<NEW>>>>
72//Width is FIXED: always 5
73
74/////////////Prevlane
75
76////<<<<OLD>>>>
77////Generating 2 linkedlists (1 for horizontal, 1 for vertical lanes)
78//////////head lanes do not have prevLane
79//@Constraint(severity="error", key={l}, message="6.1 Lane")
80//pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) {
81// CrossingScenario.vertical_head(cs, l);
82// Lane.prevLane(l, _);
83//}
84//
85//@Constraint(severity="error", key={l}, message="6.2 Lane")
86//pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) {
87// CrossingScenario.horizontal_head(cs, l);
88// Lane.prevLane(l, _);
89//}
90//
91//////////Non-head lanes must have prevLane
92//@Constraint(severity="error", key={l}, message="6.1 Lane")
93//pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) {
94// neg find find_headVertLane(l);
95// neg find find_laneWithPrevLane(l);
96//}
97//
98//@Constraint(severity="error", key={l}, message="6.1 Lane")
99//pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) {
100// neg find find_headHoriLane(l);
101// neg find find_laneWithPrevLane(l);
102//}
103//
104//private pattern find_headVertLane(l:Lane_Vertical) {
105// CrossingScenario.vertical_head(_, l);
106//}
107//private pattern find_headHoriLane(l:Lane_Horizontal) {
108// CrossingScenario.horizontal_head(_, l);
109//}
110//private pattern find_laneWithPrevLane(l:Lane) {
111// Lane.prevLane(l, _);
112//}
113//
114///////////Lane cannot be its own recursive prevLane
115//@Constraint(severity="error", key={l}, message="6.1 Lane")
116//pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) {
117// Lane.prevLane(l, l);
118//}
119//
120//@Constraint(severity="error", key={l}, message="6.2 Lane")
121//pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) {
122// find find_prevLane+(l, l);
123//}
124//private pattern find_prevLane(l1:Lane, l2:Lane) {
125// Lane.prevLane(l1, l2);
126//}
127//
128////////Lane cannot be prevLane of >1 other lane
129//@Constraint(severity="error", key={l1, l2}, message="7 Lane")
130//pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) {
131// Lane.prevLane(l1, l);
132// Lane.prevLane(l2, l);
133// l1 != l2;
134//}
135//
136////////consecutive lanes must have same orientation
137//@Constraint(severity="error", key={l1, l2}, message="8 Lane")
138//pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) {
139// Lane.prevLane(l1, l2);
140//}
141//
142//@Constraint(severity="error", key={l1, l2}, message="8 Lane")
143//pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) {
144// Lane.prevLane(l1, l2);
145//}
146//
147///////////////ReferenceCoord
148//
149///////refCoord of head lanes must be 0
150//@Constraint(severity="error", key={l}, message="6.2 Lane")
151//pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) {
152// CrossingScenario.horizontal_head(cs, l);
153// Lane.referenceCoord(l, rc);
154// check(rc != 0.0);
155//}
156//
157//@Constraint(severity="error", key={l}, message="6.2 Lane")
158//pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) {
159// CrossingScenario.vertical_head(cs, l);
160// Lane.referenceCoord(l, rc);
161// check(rc != 0.0);
162//}
163//
164////////refCoord of a lane is prevLane.rc + curLane.numWidth
165//
166//@Constraint(severity="error", key={l}, message="6.2 Lane")
167//pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) {
168// Lane.prevLane(l, prev);
169// Lane.referenceCoord(l, rcCur);
170//
171// Lane.numWidth(prev, wPrev);
172// Lane.referenceCoord(prev, rcPrev);
173// check(rcCur != rcPrev + wPrev);
174//}
175
176//<<<<NEW>>>>
177//Lanes are all predefind
178*/
179
180///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// 6///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
181//Lane+Actor 7//Lane+Actor
182///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// 8///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
@@ -430,12 +256,12 @@ private pattern helper_actorsAreFar(a1: Actor, a2: Actor) {
430//Relation 256//Relation
431///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// 257///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
432 258
433@Constraint(severity="error", key={a1, a2}, message="1 Relation") 259//@Constraint(severity="error", key={a1, a2}, message="1 Relation")
434pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { 260//pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) {
435 Relation.source(r, a1); 261// Relation.source(r, a1);
436 Relation.target(r, a2); 262// Relation.target(r, a2);
437 a1 == a2; 263// a1 == a2;
438} 264//}
439 265
440//TODO do above but transitively?/ 266//TODO do above but transitively?/
441//////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// 267//////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
@@ -462,7 +288,7 @@ pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) {
462 Lane_Horizontal(hl2); 288 Lane_Horizontal(hl2);
463} 289}
464 290
465//<<END QUALITATIF ABSTRACTION>> 291//<<END TEMP QUALITATIF ABSTRACTION>>
466 292
467//// 293////
468//VS VisionBlocked 294//VS VisionBlocked
@@ -470,6 +296,36 @@ pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) {
470//TODO Very prone to corner cases 296//TODO Very prone to corner cases
471/* 297/*
472@Constraint(severity="error", key={a1}, message="x") 298@Constraint(severity="error", key={a1}, message="x")
299pattern collisionExists_vsVisionBlockedX1(a1:Actor) {
300 VisionBlocked.blockedBy(_, a1);
301 CollisionExists.target(_, a1);
302}
303@Constraint(severity="error", key={a1}, message="x")
304pattern collisionExists_vsVisionBlockedX2(a1:Actor) {
305 VisionBlocked.blockedBy(_, a1);
306 CollisionExists.source(_, a1);
307}
308
309@Constraint(severity="error", key={a1}, message="x")
310pattern collisionExists_vsVisionBlocked1(a1:Actor) {
311 VisionBlocked.source(_, a1);
312 neg find helper_source(a1);
313}
314private pattern helper_source(a1:Actor) {
315 CollisionExists.source(_, a1);
316}
317
318@Constraint(severity="error", key={a1}, message="x")
319pattern collisionExists_vsVisionBlocked2(a1:Actor) {
320 VisionBlocked.target(_, a1);
321 neg find helper_target(a1);
322}
323private pattern helper_target(a1:Actor) {
324 CollisionExists.target(_, a1);
325}
326*/
327/*
328@Constraint(severity="error", key={a1}, message="x")
473pattern collisionExists_vsVisionBlocked(a1:Actor) { 329pattern collisionExists_vsVisionBlocked(a1:Actor) {
474 VisionBlocked.source(vb, a1); 330 VisionBlocked.source(vb, a1);
475 VisionBlocked.target(vb, a2); 331 VisionBlocked.target(vb, a2);
@@ -610,7 +466,7 @@ pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) {
610 466
611//<<QUALTATIF ABSTRACTION>> 467//<<QUALTATIF ABSTRACTION>>
612 468
613@Constraint(severity="error", key={a1, a2}, message="x") 469@Constraint(severity="error", key={a1, a2}, message="on 3 different lanes")
614pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { 470pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) {
615 VisionBlocked.source(vb, a1); 471 VisionBlocked.source(vb, a1);
616 VisionBlocked.target(vb, a2); 472 VisionBlocked.target(vb, a2);
@@ -628,7 +484,7 @@ pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) {
628 Actor.placedOn(a2, l); 484 Actor.placedOn(a2, l);
629} 485}
630 486
631@Constraint(severity="error", key={a1, a2}, message="x") 487@Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation")
632pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { 488pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) {
633 VisionBlocked.source(ce, a1); 489 VisionBlocked.source(ce, a1);
634 VisionBlocked.target(ce, a2); 490 VisionBlocked.target(ce, a2);
@@ -734,6 +590,7 @@ pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor, vb:VisionBloc
734 590
735 //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) 591 //check(slope of a1-to-BlockerBottom > slope of a1-to-a2)
736 //TODO implement ABSOLUTE VALUE or MULTI-CHECK 592 //TODO implement ABSOLUTE VALUE or MULTI-CHECK
593 //TODO do pythagoras
737 check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); 594 check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2));
738} 595}
739 596
@@ -752,110 +609,10 @@ pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor, vb:VisionBloc
752 609
753 //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) 610 //check(slope of a1-to-BlockerBottom > slope of a1-to-a2)
754 //TODO implement ABSOLUTE VALUE or MULTI-CHECK 611 //TODO implement ABSOLUTE VALUE or MULTI-CHECK
612 //TODO do pythagoras
755 check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); 613 check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2));
756} 614}
757 615
758//TODO same as above for Y??? 616//TODO same as above for Y???
759//TODO same as above for Y ???? 617//TODO same as above for Y ????
760 618
761/////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
762//SeparationDistance
763/////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
764/*
765private pattern helper_getSeperateActorsCoords(a1:Actor,
766 a2: Actor, sd:SeparationDistance,
767 x1:java Double, x2:java Double, y1:java Double, y2:java Double) {
768 SeperationDistance.source(sd, a1);
769 SeparationDistance.target(sd, a2);
770
771 find helper_getCoords(a1, a2, x1, x2, y1, y2);
772}
773
774@Constraint(severity="error", key={a1, sd}, message="x")
775pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
776 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
777
778 find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2);
779 SeparationDistance.distance(sd, Distance::D_Near);
780
781 //check(dx^2 + dy^2 < 5^2)
782 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5);
783}
784
785@Constraint(severity="error", key={a1, sd}, message="x")
786pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) {
787 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
788
789 find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2);
790 SeparationDistance.distance(sd, Distance::D_Near);
791
792 //check(dx^2 + dy^2 > 10^2)
793 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10);
794}
795
796@Constraint(severity="error", key={a1, sd}, message="x")
797pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
798 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
799
800 find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2);
801 SeparationDistance.distance(sd, Distance::D_Med);
802
803 //check(dx^2 + dy^2 < 10^2)
804 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10);
805}
806
807@Constraint(severity="error", key={a1, sd}, message="x")
808pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) {
809 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
810
811 find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2);
812 SeparationDistance.distance(sd, Distance::D_Med);
813
814 //check(dx^2 + dy^2 > 1^2)
815 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15);
816}
817
818@Constraint(severity="error", key={a1, sd}, message="x")
819pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
820 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
821
822 find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2);
823 SeparationDistance.distance(sd, Distance::D_Far);
824
825 //check(dx^2 + dy^2 < 15^2)
826 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);
827}
828*/
829
830/////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
831//CollisionDoesNotExist
832/////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
833/*
834//TODO
835@Constraint(severity="error", key={a1, cdne}, message="x")
836pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) {
837 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
838
839 CrossingScenario.actors(ss, a1);
840 CrossingScenario.actors(ss, a2);
841 Actor.relations(a1, cdne);
842 CollisionDoesNotExist.target(cdne, a2);
843 CrossingScenario.maxTime(ss, maxTime);
844
845 Actor.width(a1, w1);
846 Actor.length(a1, l1);
847 Actor.xPos(a1, xPos1);
848 Actor.yPos(a1, yPos1);
849 Actor.xSpeed(a1, xSpeed1);
850 Actor.ySpeed(a1, ySpeed1);
851
852 Actor.width(a2, w2);
853 Actor.length(a2, l2);
854 Actor.xPos(a2, xPos2);
855 Actor.yPos(a2, yPos2);
856 Actor.xSpeed(a2, xSpeed2);
857 Actor.ySpeed(a2, ySpeed2);
858 //check(dx^2 + dy^2 < 15^2)
859 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);
860}
861*/ \ No newline at end of file
diff --git a/Domains/crossingScenario/queries/moreCompleteQueries2._v_q_l b/Domains/crossingScenario/queries/moreCompleteQueries2._v_q_l
new file mode 100644
index 00000000..51e1bf00
--- /dev/null
+++ b/Domains/crossingScenario/queries/moreCompleteQueries2._v_q_l
@@ -0,0 +1,891 @@
1package queries
2
3import "http://www.example.com/crossingScenario"
4import "http://www.eclipse.org/emf/2002/Ecore"
5
6//////Minimal Failing Example
7//@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation")
8//pattern patterThatOnlyWorksWithInt(l : Lane) {
9// Lane.referenceCoord(l, w);
10// check(w <= 0-10.0);
11//}
12
13//////////////
14//CrossingScenario
15/////////////
16
17/*
18//TODO Hard-code xSize?
19//TODO Hard-code ySize?
20
21//TODO Hard-code maxTime?
22@Constraint(severity="error", key={l}, message="3 CrossingScenari")
23pattern define_cs_maxTime(cs:CrossingScenario) {
24 CrossingScenario.maxTime(cs, mt);
25 check(mt != 60.0);
26}
27*/
28
29///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
30//Lane
31///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
32/*
33
34////<<<<OLD>>>>
35////Width: Different Lanes
36//@Constraint(severity="error", key={l}, message="1 Lane")
37//pattern define_numWidth_small(l : Lane) {
38// Lane.width(l, Size::S_Small);
39// Lane.numWidth(l, nw);
40// check(nw <= 5.0);
41//} or {
42// Lane.width(l, Size::S_Small);
43// Lane.numWidth(l, nw);
44// check(nw >= 10.0);
45//}
46//
47//@Constraint(severity="error", key={l}, message="2 Lane")
48//pattern define_numWidth_medium(l : Lane) {
49// Lane.width(l, ::S_Med);
50// Lane.numWidth(l, nw);
51// check(nw <= 10.0);
52//}
53//or {
54// Lane.width(l, Size::S_Med);
55// Lane.numWidth(l, nw);
56// check(nw >= 15.0);
57//}
58//
59//@Constraint(severity="error", key={l}, message="3 Lane")
60//pattern define_numWidth_large(l : Lane) {
61// Lane.width(l, Size::S_Large);
62// Lane.numWidth(l, nw);
63// check(nw <= 15.0);
64//}
65//or {
66// Lane.width(l, Size::S_Large);
67// Lane.numWidth(l, nw);
68// check(nw >= 20.0);
69//}
70
71//<<<<NEW>>>>
72//Width is FIXED: always 5
73
74/////////////Prevlane
75
76////<<<<OLD>>>>
77////Generating 2 linkedlists (1 for horizontal, 1 for vertical lanes)
78//////////head lanes do not have prevLane
79//@Constraint(severity="error", key={l}, message="6.1 Lane")
80//pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) {
81// CrossingScenario.vertical_head(cs, l);
82// Lane.prevLane(l, _);
83//}
84//
85//@Constraint(severity="error", key={l}, message="6.2 Lane")
86//pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) {
87// CrossingScenario.horizontal_head(cs, l);
88// Lane.prevLane(l, _);
89//}
90//
91//////////Non-head lanes must have prevLane
92//@Constraint(severity="error", key={l}, message="6.1 Lane")
93//pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) {
94// neg find find_headVertLane(l);
95// neg find find_laneWithPrevLane(l);
96//}
97//
98//@Constraint(severity="error", key={l}, message="6.1 Lane")
99//pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) {
100// neg find find_headHoriLane(l);
101// neg find find_laneWithPrevLane(l);
102//}
103//
104//private pattern find_headVertLane(l:Lane_Vertical) {
105// CrossingScenario.vertical_head(_, l);
106//}
107//private pattern find_headHoriLane(l:Lane_Horizontal) {
108// CrossingScenario.horizontal_head(_, l);
109//}
110//private pattern find_laneWithPrevLane(l:Lane) {
111// Lane.prevLane(l, _);
112//}
113//
114///////////Lane cannot be its own recursive prevLane
115//@Constraint(severity="error", key={l}, message="6.1 Lane")
116//pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) {
117// Lane.prevLane(l, l);
118//}
119//
120//@Constraint(severity="error", key={l}, message="6.2 Lane")
121//pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) {
122// find find_prevLane+(l, l);
123//}
124//private pattern find_prevLane(l1:Lane, l2:Lane) {
125// Lane.prevLane(l1, l2);
126//}
127//
128////////Lane cannot be prevLane of >1 other lane
129//@Constraint(severity="error", key={l1, l2}, message="7 Lane")
130//pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) {
131// Lane.prevLane(l1, l);
132// Lane.prevLane(l2, l);
133// l1 != l2;
134//}
135//
136////////consecutive lanes must have same orientation
137//@Constraint(severity="error", key={l1, l2}, message="8 Lane")
138//pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) {
139// Lane.prevLane(l1, l2);
140//}
141//
142//@Constraint(severity="error", key={l1, l2}, message="8 Lane")
143//pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) {
144// Lane.prevLane(l1, l2);
145//}
146//
147///////////////ReferenceCoord
148//
149///////refCoord of head lanes must be 0
150//@Constraint(severity="error", key={l}, message="6.2 Lane")
151//pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) {
152// CrossingScenario.horizontal_head(cs, l);
153// Lane.referenceCoord(l, rc);
154// check(rc != 0.0);
155//}
156//
157//@Constraint(severity="error", key={l}, message="6.2 Lane")
158//pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) {
159// CrossingScenario.vertical_head(cs, l);
160// Lane.referenceCoord(l, rc);
161// check(rc != 0.0);
162//}
163//
164////////refCoord of a lane is prevLane.rc + curLane.numWidth
165//
166//@Constraint(severity="error", key={l}, message="6.2 Lane")
167//pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) {
168// Lane.prevLane(l, prev);
169// Lane.referenceCoord(l, rcCur);
170//
171// Lane.numWidth(prev, wPrev);
172// Lane.referenceCoord(prev, rcPrev);
173// check(rcCur != rcPrev + wPrev);
174//}
175
176//<<<<NEW>>>>
177//Lanes are all predefind
178*/
179
180///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
181//Lane+Actor
182///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
183
184/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw]
185@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
186pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) {
187 Actor.placedOn(a, vl);
188 Actor.xPos(a, x);
189 Lane.referenceCoord(vl, r);
190 check(x <= r);
191} or {
192 Actor.placedOn(a, vl);
193 Actor.xPos(a, x);
194 Lane.referenceCoord(vl, r);
195// //<<<<OLD>>>>
196// Lane.numWidth(vl, w);
197// check(x >= (r + w));
198
199 //<<<<NEW>>>>: lanes all have width=5
200 check(x >= (r + 5.0));
201}
202
203@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
204pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) {
205 Actor.placedOn(a, hl);
206 Actor.yPos(a, y);
207 Lane.referenceCoord(hl, r);
208 check(y <= r);
209} or {
210 Actor.placedOn(a, hl);
211 Actor.yPos(a, y);
212 Lane.referenceCoord(hl, r);
213// //<<OLD>>
214// Lane.numWidth(hl, w);
215// check(y >= (r + w));
216
217 //<<NEW>>
218 check(y >= (r + 5.0));
219
220}
221
222///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
223//Actor
224///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
225
226/////----------------
227//Xpos and Ypos Bounds
228/////----------------
229
230private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor,
231 xMax:java Double, xP:java Double) {
232 Actor.placedOn(a, hl);
233 Lane_Horizontal(hl);
234 CrossingScenario.actors(cs, a);
235 CrossingScenario.xSize(cs, xMax);
236 Actor.xPos(a, xP);
237}
238
239private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor,
240 yMax:java Double, yP:java Double) {
241 Actor.placedOn(a, vl);
242 Lane_Vertical(vl);
243 CrossingScenario.actors(cs, a);
244 CrossingScenario.ySize(cs, yMax);
245 Actor.yPos(a, yP);
246}
247
248@Constraint(severity="error", key={cs}, message="x")
249pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) {
250 find helper_horiz_getXAndBounds(cs, a, xMax, xP);
251 check(xP >= xMax);}
252
253@Constraint(severity="error", key={cs}, message="x")
254pattern define_actor_minXp(cs:CrossingScenario, a:Actor) {
255 find helper_horiz_getXAndBounds(cs, a, xMax, xP);
256 check(xP <= 0-xMax);}
257
258@Constraint(severity="error", key={cs}, message="x")
259pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) {
260 find helper_vert_getYAndBounds(cs, a, yMax, yP);
261 check(yP >= yMax);}
262
263@Constraint(severity="error", key={cs}, message="x")
264pattern define_actor_minYp(cs:CrossingScenario, a:Actor) {
265 find helper_vert_getYAndBounds(cs, a, yMax, yP);
266 check(yP <= 0-yMax);}
267
268/////----------------
269//Xspeed and Yspeed bounds
270/////----------------
271
272//TODO THIS IS HARD_CODED
273
274/////////VERTICAL LANE
275@Constraint(severity="error", key={a}, message="7 Actor")
276pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) {
277 Actor.placedOn(a, vl);
278 Lane_Vertical(vl);
279 Actor.xSpeed(a, xSpeed);
280 check(xSpeed != 0);
281}
282
283private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor,
284 ySpeedMax:java Double, ySpeed:java Double) {
285 Actor.placedOn(a, vl);
286 Lane_Vertical(vl);
287 CrossingScenario.actors(cs, a);
288 CrossingScenario.maxYSpeed(cs, ySpeedMax);
289 Actor.ySpeed(a, ySpeed);
290}
291
292@Constraint(severity="error", key={cs}, message="x")
293pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) {
294 find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS);
295 check(yS <= 0-ySMax);
296}
297
298@Constraint(severity="error", key={cs}, message="x")
299pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) {
300 find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS);
301 check(yS >= ySMax);
302}
303
304/////////HORIZONTAL LANE
305@Constraint(severity="error", key={a}, message="7 Actor")
306pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) {
307 Actor.placedOn(a, hl);
308 Lane_Horizontal(hl);
309 Actor.ySpeed(a, ySpeed);
310 check(ySpeed != 0);
311}
312
313private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor,
314 xSpeedMax:java Double, xSpeed:java Double) {
315 Actor.placedOn(a, hl);
316 Lane_Horizontal(hl);
317 CrossingScenario.actors(cs, a);
318 CrossingScenario.maxXSpeed(cs, xSpeedMax);
319 Actor.xSpeed(a, xSpeed);
320}
321
322@Constraint(severity="error", key={cs}, message="x")
323pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) {
324 find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS);
325 check(xS <= 0-xSMax);
326}
327
328@Constraint(severity="error", key={cs}, message="x")
329pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) {
330 find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS);
331 check(xS >= xSMax);
332}
333
334/////----------------
335/////WIDTH and LENGTH
336/////----------------
337
338///////pedestrian-width (3)
339@Constraint(severity="error", key={p}, message="3 Actor")
340pattern define_actor_pedestrianWidth(p:Pedestrian) {
341 Pedestrian.width(p, w);
342 check(w != 1.0);
343}
344
345/////////pedestrian-width (4)
346@Constraint(severity="error", key={p}, message="4 Actor")
347pattern define_actor_pedestrianLength(p:Pedestrian) {
348 Pedestrian.length(p, l);
349 check(l != 1.0);
350}
351
352/////////actor-width (5)
353@Constraint(severity="error", key={v}, message="5 Actor")
354pattern define_actor_vehicleWidth(v:Vehicle) {
355 Vehicle.placedOn(v, lane);
356 Lane_Vertical(lane);
357 Vehicle.width(v, w);
358 check(w != 1.0);
359} or {
360 Vehicle.placedOn(v, lane);
361 Lane_Horizontal(lane);
362 Vehicle.width(v, w);
363 check(w != 3.0);
364}
365
366/////////actor-width (6)
367@Constraint(severity="error", key={v}, message="6 Actor")
368pattern define_actor_vehicleLength(v:Vehicle) {
369 Vehicle.placedOn(v, lane);
370 Lane_Vertical(lane);
371 Vehicle.length(v, l);
372 check(l != 3.0);
373} or {
374 Vehicle.placedOn(v, lane);
375 Lane_Horizontal(lane);
376 Vehicle.length(v, l);
377 check(l != 1.0);
378}
379
380/////----------------
381/////DERIVED FEATURES
382/////----------------
383
384private pattern helper_getCoords(a1:Actor,
385 a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) {
386 Actor.xPos(a1, x1);
387 Actor.yPos(a1, y1);
388 Actor.xPos(a2, x2);
389 Actor.yPos(a2, y2);
390}
391
392@QueryBasedFeature
393pattern dist_near(a1: Actor, a2: Actor) {
394 find helper_actorsAreNear(a1, a2);
395 Actor.dist_near(a1, a2);
396}
397
398private pattern helper_actorsAreNear(a1: Actor, a2: Actor) {
399 find helper_getCoords(a1, a2, x1, x2, y1, y2);
400 //check(dx^2 + dy^2 < 10^2)
401 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10);
402}
403
404@QueryBasedFeature
405pattern dist_med(a1: Actor, a2: Actor) {
406 find helper_actorsAreMed(a1, a2);
407 Actor.dist_med(a1, a2);
408}
409
410private pattern helper_actorsAreMed(a1: Actor, a2: Actor) {
411 find helper_getCoords(a1, a2, x1, x2, y1, y2);
412 //check(10^2 < dx^2 + dy^2 < 15^2)
413 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10);
414 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);
415}
416
417@QueryBasedFeature
418pattern dist_far(a1: Actor, a2: Actor) {
419 find helper_actorsAreFar(a1, a2);
420 Actor.dist_far(a1, a2);
421}
422
423private pattern helper_actorsAreFar(a1: Actor, a2: Actor) {
424 find helper_getCoords(a1, a2, x1, x2, y1, y2);
425 //check(dx^2 + dy^2 > 20^2)
426 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20);
427}
428
429///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
430//Relation
431///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
432
433@Constraint(severity="error", key={a1, a2}, message="1 Relation")
434pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) {
435 Relation.source(r, a1);
436 Relation.target(r, a2);
437 a1 == a2;
438}
439
440//TODO do above but transitively?/
441//////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
442//CollisionExists
443///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
444
445
446//<<QUALTATIF ABSTRACTION>>
447
448@Constraint(severity="error", key={a1, a2}, message="x")
449pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) {
450 CollisionExists.source(ce, a1);
451 CollisionExists.target(ce, a2);
452 Actor.placedOn(a1, vl1);
453 Lane_Vertical(vl1);
454 Actor.placedOn(a2, vl2);
455 Lane_Vertical(vl2);
456} or {
457 CollisionExists.source(ce, a1);
458 CollisionExists.target(ce, a2);
459 Actor.placedOn(a1, hl1);
460 Lane_Horizontal(hl1);
461 Actor.placedOn(a2, hl2);
462 Lane_Horizontal(hl2);
463}
464
465//<<END TEMP QUALITATIF ABSTRACTION>>
466
467////
468//VS VisionBlocked
469////
470//TODO Very prone to corner cases
471/*
472@Constraint(severity="error", key={a1}, message="x")
473pattern collisionExists_vsVisionBlockedX1(a1:Actor) {
474 VisionBlocked.blockedBy(_, a1);
475 CollisionExists.target(_, a1);
476}
477@Constraint(severity="error", key={a1}, message="x")
478pattern collisionExists_vsVisionBlockedX2(a1:Actor) {
479 VisionBlocked.blockedBy(_, a1);
480 CollisionExists.source(_, a1);
481}
482
483@Constraint(severity="error", key={a1}, message="x")
484pattern collisionExists_vsVisionBlocked1(a1:Actor) {
485 VisionBlocked.source(_, a1);
486 neg find helper_source(a1);
487}
488private pattern helper_source(a1:Actor) {
489 CollisionExists.source(_, a1);
490}
491
492@Constraint(severity="error", key={a1}, message="x")
493pattern collisionExists_vsVisionBlocked2(a1:Actor) {
494 VisionBlocked.target(_, a1);
495 neg find helper_target(a1);
496}
497private pattern helper_target(a1:Actor) {
498 CollisionExists.target(_, a1);
499}
500*/
501/*
502@Constraint(severity="error", key={a1}, message="x")
503pattern collisionExists_vsVisionBlocked(a1:Actor) {
504 VisionBlocked.source(vb, a1);
505 VisionBlocked.target(vb, a2);
506 CollisionExists.source(ce, a1);
507 CollisionExists.target(ce, a3);
508 a2 != a3;
509} or {
510 VisionBlocked.source(vb, a1);
511 VisionBlocked.target(vb, a2);
512 CollisionExists.source(ce, a3);
513 CollisionExists.target(ce, a1);
514 a2 != a3;
515} or {
516 VisionBlocked.source(vb, a2);
517 VisionBlocked.target(vb, a1);
518 CollisionExists.source(ce, a3);
519 CollisionExists.target(ce, a1);
520 a2 != a3;
521} or {
522 VisionBlocked.source(vb, a2);
523 VisionBlocked.target(vb, a1);
524 CollisionExists.source(ce, a1);
525 CollisionExists.target(ce, a3);
526 a2 != a3;
527}
528*/
529//<<END QUALITATIF ABSTRACTION>>
530
531////
532//CollisionExists - Time
533////
534
535
536@Constraint(severity="error", key={c}, message="x")
537pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) {
538 CrossingScenario.relations(ss, c);
539 CrossingScenario.maxTime(ss, maxTime);
540 CollisionExists.collisionTime(c, cTime);
541 check(cTime >= maxTime);}
542
543@Constraint(severity="error", key={c}, message="x")
544pattern collisionExists_timeNotNegative(c:CollisionExists) {
545 CollisionExists. collisionTime(c, cTime);
546 check(cTime <= 0.0);}
547
548////
549//CollisionExists - Physical Positioniung
550////
551
552private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) {
553 CollisionExists.source(c, a1);
554 CollisionExists.target(c, a2);
555 CollisionExists. collisionTime(c, cTime);
556}
557
558private pattern helper_getYCoords(a:Actor, l:java Double,
559 yPos:java Double, ySpeed:java Double) {
560
561 Actor.length(a, l);
562 Actor.yPos(a, yPos);
563 Actor.ySpeed(a, ySpeed);
564}
565
566private pattern helper_getAllYCoords(a1:Actor, a2: Actor,
567 l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double,
568 ySpeed1:java Double, ySpeed2:java Double) {
569
570 CollisionExists.source(c, a1);
571 CollisionExists.target(c, a2);
572 find helper_getYCoords(a1, l1, yPos1, ySpeed1);
573 find helper_getYCoords(a2, l2, yPos2, ySpeed2);
574}
575
576private pattern helper_getXCoords(a:Actor, l:java Double,
577 xPos:java Double, xSpeed:java Double) {
578
579 Actor.length(a, l);
580 Actor.xPos(a, xPos);
581 Actor.xSpeed(a, xSpeed);
582}
583
584private pattern helper_getAllXCoords(a1:Actor, a2: Actor,
585 w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double,
586 xSpeed1:java Double, xSpeed2:java Double) {
587
588 CollisionExists.source(c, a1);
589 CollisionExists.target(c, a2);
590 find helper_getXCoords(a1, w1, xPos1, xSpeed1);
591 find helper_getXCoords(a2, w2, xPos2, xSpeed2);
592}
593
594@Constraint(severity="error", key={a1}, message="x")
595pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) {
596
597 find helper_getCollExistsTime(a1, a2, cTime);
598 find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2);
599
600 //check(y_1_bottom > y_2_top
601 check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2));
602}
603
604@Constraint(severity="error", key={a1}, message="x")
605pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) {
606 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
607
608 find helper_getCollExistsTime(a1, a2, cTime);
609 find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2);
610
611 //check(y_1_top < y_2_bottom)
612 check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2));
613}
614
615@Constraint(severity="error", key={a1}, message="x")
616pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) {
617
618 find helper_getCollExistsTime(a1, a2, cTime);
619 find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2);
620
621 //check(x_1_left > x_2_right)
622 check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2));
623}
624
625@Constraint(severity="error", key={a1}, message="x")
626pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) {
627 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
628
629 find helper_getCollExistsTime(a1, a2, cTime);
630 find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2);
631
632 //check(x_1_right < x_2_left)
633 check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2));
634}
635
636
637///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
638//VisionBlocked
639///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
640
641//<<QUALTATIF ABSTRACTION>>
642
643@Constraint(severity="error", key={a1, a2}, message="x")
644pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) {
645 VisionBlocked.source(vb, a1);
646 VisionBlocked.target(vb, a2);
647 Actor.placedOn(a1, l);
648 Actor.placedOn(a2, l);
649} or {
650 VisionBlocked.source(vb, a1);
651 VisionBlocked.blockedBy(vb, a2);
652 Actor.placedOn(a1, l);
653 Actor.placedOn(a2, l);
654} or {
655 VisionBlocked.blockedBy(vb, a1);
656 VisionBlocked.target(vb, a2);
657 Actor.placedOn(a1, l);
658 Actor.placedOn(a2, l);
659}
660
661@Constraint(severity="error", key={a1, a2}, message="x")
662pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) {
663 VisionBlocked.source(ce, a1);
664 VisionBlocked.target(ce, a2);
665 Actor.placedOn(a1, vl1);
666 Lane_Vertical(vl1);
667 Actor.placedOn(a2, vl2);
668 Lane_Vertical(vl2);
669} or {
670 VisionBlocked.source(ce, a1);
671 VisionBlocked.target(ce, a2);
672 Actor.placedOn(a1, hl1);
673 Lane_Horizontal(hl1);
674 Actor.placedOn(a2, hl2);
675 Lane_Horizontal(hl2);
676}
677
678//<<END QUALITATIF ABSTRACTION>>
679
680@Constraint(severity="error", key={a1, a2}, message="x")
681pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) {
682 VisionBlocked.source(vb, a1);
683 VisionBlocked.target(vb, a2);
684 VisionBlocked.blockedBy(vb, a2);
685} or {
686 VisionBlocked.source(vb, a1);
687 VisionBlocked.target(vb, a2);
688 VisionBlocked.blockedBy(vb, a1);
689}
690
691@Constraint(severity="error", key={a1, vb}, message="x")
692pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocked) {
693 //REQUIRED to avoid division by 0 in next 2 queries
694 VisionBlocked.source(vb, a1);
695 VisionBlocked.target(vb, a2);
696
697 Actor.xPos(a1, x1);
698 Actor.xPos(a2, x2);
699
700 //check(slope of a1-to-BlockerTop < slope of a1-to-a2)
701 check(x1 == x2);
702}
703
704//TODO refactor?
705@Constraint(severity="error", key={a1, vb}, message="x")
706pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) {
707 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
708 VisionBlocked.source(vb, a1);
709 VisionBlocked.target(vb, a2);
710 VisionBlocked.blockedBy(vb, aBlocker);
711
712 Actor.xPos(a1, x1);
713 Actor.yPos(a1, y1);
714 Actor.xPos(a2, x2);
715 Actor.yPos(a2, y2);
716 Actor.xPos(aBlocker, xBlocker);
717 Actor.yPos(aBlocker, yBlocker);
718 Actor.length(aBlocker, lenBlocker);
719 Actor.width(aBlocker, widBlocker);
720
721 //check(slope of a1-to-BlockerTop < slope of a1-to-a2)
722 check(
723 ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) /
724 ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2}))
725 < ((y1-y2)/(x1-x2)));
726}
727
728//TODO refactor?
729@Constraint(severity="error", key={a1, vb}, message="x")
730pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) {
731 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
732 VisionBlocked.source(vb, a1);
733 VisionBlocked.target(vb, a2);
734 VisionBlocked.blockedBy(vb, aBlocker);
735
736 Actor.xPos(a1, x1);
737 Actor.yPos(a1, y1);
738 Actor.xPos(a2, x2);
739 Actor.yPos(a2, y2);
740 Actor.xPos(aBlocker, xBlocker);
741 Actor.yPos(aBlocker, yBlocker);
742 Actor.length(aBlocker, lenBlocker);
743 Actor.width(aBlocker, widBlocker);
744
745 //check(slope of a1-to-BlockerBottom > slope of a1-to-a2)
746 check(
747 ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) /
748 ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2}))
749 > ((y1-y2)/(x1-x2)));
750}
751
752//TODO refactor?
753//TODO CORNER CASES
754@Constraint(severity="error", key={a1, vb}, message="x")
755pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor, vb:VisionBlocked) {
756 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
757 VisionBlocked.source(vb, a1);
758 VisionBlocked.target(vb, a2);
759 VisionBlocked.blockedBy(vb, aBlocker);
760
761 Actor.xPos(a1, x1);
762 Actor.xPos(a2, x2);
763 Actor.xPos(aBlocker, xBlocker);
764
765 //check(slope of a1-to-BlockerBottom > slope of a1-to-a2)
766 //TODO implement ABSOLUTE VALUE or MULTI-CHECK
767 check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2));
768}
769
770//TODO refactor?
771//TODO CORNER CASES
772@Constraint(severity="error", key={a1, vb}, message="x")
773pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor, vb:VisionBlocked) {
774 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
775 VisionBlocked.source(vb, a2);
776 VisionBlocked.target(vb, a1);
777 VisionBlocked.blockedBy(vb, aBlocker);
778
779 Actor.xPos(a1, x1);
780 Actor.xPos(a2, x2);
781 Actor.xPos(aBlocker, xBlocker);
782
783 //check(slope of a1-to-BlockerBottom > slope of a1-to-a2)
784 //TODO implement ABSOLUTE VALUE or MULTI-CHECK
785 check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2));
786}
787
788//TODO same as above for Y???
789//TODO same as above for Y ????
790
791/////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
792//SeparationDistance
793/////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
794/*
795private pattern helper_getSeperateActorsCoords(a1:Actor,
796 a2: Actor, sd:SeparationDistance,
797 x1:java Double, x2:java Double, y1:java Double, y2:java Double) {
798 SeperationDistance.source(sd, a1);
799 SeparationDistance.target(sd, a2);
800
801 find helper_getCoords(a1, a2, x1, x2, y1, y2);
802}
803
804@Constraint(severity="error", key={a1, sd}, message="x")
805pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
806 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
807
808 find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2);
809 SeparationDistance.distance(sd, Distance::D_Near);
810
811 //check(dx^2 + dy^2 < 5^2)
812 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5);
813}
814
815@Constraint(severity="error", key={a1, sd}, message="x")
816pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) {
817 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
818
819 find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2);
820 SeparationDistance.distance(sd, Distance::D_Near);
821
822 //check(dx^2 + dy^2 > 10^2)
823 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10);
824}
825
826@Constraint(severity="error", key={a1, sd}, message="x")
827pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
828 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
829
830 find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2);
831 SeparationDistance.distance(sd, Distance::D_Med);
832
833 //check(dx^2 + dy^2 < 10^2)
834 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10);
835}
836
837@Constraint(severity="error", key={a1, sd}, message="x")
838pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) {
839 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
840
841 find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2);
842 SeparationDistance.distance(sd, Distance::D_Med);
843
844 //check(dx^2 + dy^2 > 1^2)
845 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15);
846}
847
848@Constraint(severity="error", key={a1, sd}, message="x")
849pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
850 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
851
852 find helper_getSeparateActorsCoords(a1, a2, sd, x1, x2, y1, y2);
853 SeparationDistance.distance(sd, Distance::D_Far);
854
855 //check(dx^2 + dy^2 < 15^2)
856 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);
857}
858*/
859
860/////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
861//CollisionDoesNotExist
862/////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*//////
863/*
864//TODO
865@Constraint(severity="error", key={a1, cdne}, message="x")
866pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) {
867 //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
868
869 CrossingScenario.actors(ss, a1);
870 CrossingScenario.actors(ss, a2);
871 Actor.relations(a1, cdne);
872 CollisionDoesNotExist.target(cdne, a2);
873 CrossingScenario.maxTime(ss, maxTime);
874
875 Actor.width(a1, w1);
876 Actor.length(a1, l1);
877 Actor.xPos(a1, xPos1);
878 Actor.yPos(a1, yPos1);
879 Actor.xSpeed(a1, xSpeed1);
880 Actor.ySpeed(a1, ySpeed1);
881
882 Actor.width(a2, w2);
883 Actor.length(a2, l2);
884 Actor.xPos(a2, xPos2);
885 Actor.yPos(a2, yPos2);
886 Actor.xSpeed(a2, xSpeed2);
887 Actor.ySpeed(a2, ySpeed2);
888 //check(dx^2 + dy^2 < 15^2)
889 check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);
890}
891*/ \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-30 13:27:06 +0000