diff options
Diffstat (limited to 'Domains/crossingScenario/queries/crossingScenarioQueries.vql')
-rw-r--r-- | Domains/crossingScenario/queries/crossingScenarioQueries.vql | 1026 |
1 files changed, 513 insertions, 513 deletions
diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index 352c77c0..f8bcc92c 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql | |||
@@ -1,514 +1,514 @@ | |||
1 | package queries | 1 | package queries |
2 | 2 | ||
3 | import "http://www.example.com/crossingScenario" | 3 | import "http://www.example.com/crossingScenario" |
4 | import "http://www.eclipse.org/emf/2002/Ecore" | 4 | import "http://www.eclipse.org/emf/2002/Ecore" |
5 | 5 | ||
6 | //////Minimal Failing Example | 6 | //////Minimal Failing Example |
7 | //@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation") | 7 | //@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation") |
8 | //pattern patterThatOnlyWorksWithInt(l : Lane) { | 8 | //pattern patterThatOnlyWorksWithInt(l : Lane) { |
9 | // Lane.referenceCoord(l, w); | 9 | // Lane.referenceCoord(l, w); |
10 | // check(w <= 0-10.0); | 10 | // check(w <= 0-10.0); |
11 | //} | 11 | //} |
12 | 12 | ||
13 | ////////////// | 13 | ////////////// |
14 | //CrossingScenario | 14 | //CrossingScenario |
15 | ///////////// | 15 | ///////////// |
16 | 16 | ||
17 | //TODO Hard-code xSize? | 17 | //TODO Hard-code xSize? |
18 | //TODO Hard-code ySize? | 18 | //TODO Hard-code ySize? |
19 | //TODO Hard-code maxTime? | 19 | //TODO Hard-code maxTime? |
20 | 20 | ||
21 | ////////////// | 21 | ////////////// |
22 | //Lane | 22 | //Lane |
23 | ////////////// | 23 | ////////////// |
24 | 24 | ||
25 | @Constraint(severity="error", key={l}, message="1 Lane") | 25 | @Constraint(severity="error", key={l}, message="1 Lane") |
26 | pattern define_numWidth_small(l : Lane) { | 26 | pattern define_numWidth_small(l : Lane) { |
27 | Lane.width(l, Size::S_Small); | 27 | Lane.width(l, Size::S_Small); |
28 | Lane.numWidth(l, nw); | 28 | Lane.numWidth(l, nw); |
29 | check(nw <= 5.0); | 29 | check(nw <= 5.0); |
30 | } or { | 30 | } or { |
31 | Lane.width(l, Size::S_Small); | 31 | Lane.width(l, Size::S_Small); |
32 | Lane.numWidth(l, nw); | 32 | Lane.numWidth(l, nw); |
33 | check(nw >= 10.0); | 33 | check(nw >= 10.0); |
34 | } | 34 | } |
35 | 35 | ||
36 | @Constraint(severity="error", key={l}, message="2 Lane") | 36 | @Constraint(severity="error", key={l}, message="2 Lane") |
37 | pattern define_numWidth_medium(l : Lane) { | 37 | pattern define_numWidth_medium(l : Lane) { |
38 | Lane.width(l, ::S_Med); | 38 | Lane.width(l, ::S_Med); |
39 | Lane.numWidth(l, nw); | 39 | Lane.numWidth(l, nw); |
40 | check(nw <= 10.0); | 40 | check(nw <= 10.0); |
41 | } | 41 | } |
42 | or { | 42 | or { |
43 | Lane.width(l, Size::S_Med); | 43 | Lane.width(l, Size::S_Med); |
44 | Lane.numWidth(l, nw); | 44 | Lane.numWidth(l, nw); |
45 | check(nw >= 15.0); | 45 | check(nw >= 15.0); |
46 | } | 46 | } |
47 | 47 | ||
48 | @Constraint(severity="error", key={l}, message="3 Lane") | 48 | @Constraint(severity="error", key={l}, message="3 Lane") |
49 | pattern define_numWidth_large(l : Lane) { | 49 | pattern define_numWidth_large(l : Lane) { |
50 | Lane.width(l, Size::S_Large); | 50 | Lane.width(l, Size::S_Large); |
51 | Lane.numWidth(l, nw); | 51 | Lane.numWidth(l, nw); |
52 | check(nw <= 15.0); | 52 | check(nw <= 15.0); |
53 | } | 53 | } |
54 | or { | 54 | or { |
55 | Lane.width(l, Size::S_Large); | 55 | Lane.width(l, Size::S_Large); |
56 | Lane.numWidth(l, nw); | 56 | Lane.numWidth(l, nw); |
57 | check(nw >= 20.0); | 57 | check(nw >= 20.0); |
58 | } | 58 | } |
59 | 59 | ||
60 | /////////////Prevlane | 60 | /////////////Prevlane |
61 | 61 | ||
62 | ////////head lanes do not have prevLane | 62 | ////////head lanes do not have prevLane |
63 | @Constraint(severity="error", key={l}, message="6.1 Lane") | 63 | @Constraint(severity="error", key={l}, message="6.1 Lane") |
64 | pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) { | 64 | pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) { |
65 | CrossingScenario.vertical_head(cs, l); | 65 | CrossingScenario.vertical_head(cs, l); |
66 | Lane.prevLane(l, _); | 66 | Lane.prevLane(l, _); |
67 | } | 67 | } |
68 | 68 | ||
69 | @Constraint(severity="error", key={l}, message="6.2 Lane") | 69 | @Constraint(severity="error", key={l}, message="6.2 Lane") |
70 | pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) { | 70 | pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) { |
71 | CrossingScenario.horizontal_head(cs, l); | 71 | CrossingScenario.horizontal_head(cs, l); |
72 | Lane.prevLane(l, _); | 72 | Lane.prevLane(l, _); |
73 | } | 73 | } |
74 | 74 | ||
75 | ////////Non-head lanes must have prevLane | 75 | ////////Non-head lanes must have prevLane |
76 | @Constraint(severity="error", key={l}, message="6.1 Lane") | 76 | @Constraint(severity="error", key={l}, message="6.1 Lane") |
77 | pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) { | 77 | pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) { |
78 | neg find find_headVertLane(l); | 78 | neg find find_headVertLane(l); |
79 | neg find find_laneWithPrevLane(l); | 79 | neg find find_laneWithPrevLane(l); |
80 | } | 80 | } |
81 | 81 | ||
82 | @Constraint(severity="error", key={l}, message="6.1 Lane") | 82 | @Constraint(severity="error", key={l}, message="6.1 Lane") |
83 | pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) { | 83 | pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) { |
84 | neg find find_headHoriLane(l); | 84 | neg find find_headHoriLane(l); |
85 | neg find find_laneWithPrevLane(l); | 85 | neg find find_laneWithPrevLane(l); |
86 | } | 86 | } |
87 | 87 | ||
88 | private pattern find_headVertLane(l:Lane_Vertical) { | 88 | private pattern find_headVertLane(l:Lane_Vertical) { |
89 | CrossingScenario.vertical_head(_, l); | 89 | CrossingScenario.vertical_head(_, l); |
90 | } | 90 | } |
91 | private pattern find_headHoriLane(l:Lane_Horizontal) { | 91 | private pattern find_headHoriLane(l:Lane_Horizontal) { |
92 | CrossingScenario.horizontal_head(_, l); | 92 | CrossingScenario.horizontal_head(_, l); |
93 | } | 93 | } |
94 | private pattern find_laneWithPrevLane(l:Lane) { | 94 | private pattern find_laneWithPrevLane(l:Lane) { |
95 | Lane.prevLane(l, _); | 95 | Lane.prevLane(l, _); |
96 | } | 96 | } |
97 | 97 | ||
98 | /////////Lane cannot be its own recursive prevLane | 98 | /////////Lane cannot be its own recursive prevLane |
99 | @Constraint(severity="error", key={l}, message="6.1 Lane") | 99 | @Constraint(severity="error", key={l}, message="6.1 Lane") |
100 | pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) { | 100 | pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) { |
101 | Lane.prevLane(l, l); | 101 | Lane.prevLane(l, l); |
102 | } | 102 | } |
103 | 103 | ||
104 | @Constraint(severity="error", key={l}, message="6.2 Lane") | 104 | @Constraint(severity="error", key={l}, message="6.2 Lane") |
105 | pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) { | 105 | pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) { |
106 | find find_prevLane+(l, l); | 106 | find find_prevLane+(l, l); |
107 | } | 107 | } |
108 | private pattern find_prevLane(l1:Lane, l2:Lane) { | 108 | private pattern find_prevLane(l1:Lane, l2:Lane) { |
109 | Lane.prevLane(l1, l2); | 109 | Lane.prevLane(l1, l2); |
110 | } | 110 | } |
111 | 111 | ||
112 | //////Lane cannot be prevLane of >1 other lane | 112 | //////Lane cannot be prevLane of >1 other lane |
113 | @Constraint(severity="error", key={l1, l2}, message="7 Lane") | 113 | @Constraint(severity="error", key={l1, l2}, message="7 Lane") |
114 | pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) { | 114 | pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) { |
115 | Lane.prevLane(l1, l); | 115 | Lane.prevLane(l1, l); |
116 | Lane.prevLane(l2, l); | 116 | Lane.prevLane(l2, l); |
117 | l1 != l2; | 117 | l1 != l2; |
118 | } | 118 | } |
119 | 119 | ||
120 | //////consecutive lanes must have same orientation | 120 | //////consecutive lanes must have same orientation |
121 | @Constraint(severity="error", key={l1, l2}, message="8 Lane") | 121 | @Constraint(severity="error", key={l1, l2}, message="8 Lane") |
122 | pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) { | 122 | pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) { |
123 | Lane.prevLane(l1, l2); | 123 | Lane.prevLane(l1, l2); |
124 | } | 124 | } |
125 | 125 | ||
126 | @Constraint(severity="error", key={l1, l2}, message="8 Lane") | 126 | @Constraint(severity="error", key={l1, l2}, message="8 Lane") |
127 | pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) { | 127 | pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) { |
128 | Lane.prevLane(l1, l2); | 128 | Lane.prevLane(l1, l2); |
129 | } | 129 | } |
130 | 130 | ||
131 | /////////////ReferenceCoord | 131 | /////////////ReferenceCoord |
132 | 132 | ||
133 | /////refCoord of head lanes must be 0 | 133 | /////refCoord of head lanes must be 0 |
134 | @Constraint(severity="error", key={l}, message="6.2 Lane") | 134 | @Constraint(severity="error", key={l}, message="6.2 Lane") |
135 | pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) { | 135 | pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) { |
136 | CrossingScenario.horizontal_head(cs, l); | 136 | CrossingScenario.horizontal_head(cs, l); |
137 | Lane.referenceCoord(l, rc); | 137 | Lane.referenceCoord(l, rc); |
138 | check(rc != 0.0); | 138 | check(rc != 0.0); |
139 | } | 139 | } |
140 | 140 | ||
141 | @Constraint(severity="error", key={l}, message="6.2 Lane") | 141 | @Constraint(severity="error", key={l}, message="6.2 Lane") |
142 | pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) { | 142 | pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) { |
143 | CrossingScenario.vertical_head(cs, l); | 143 | CrossingScenario.vertical_head(cs, l); |
144 | Lane.referenceCoord(l, rc); | 144 | Lane.referenceCoord(l, rc); |
145 | check(rc != 0.0); | 145 | check(rc != 0.0); |
146 | } | 146 | } |
147 | 147 | ||
148 | //////refCoord of a lane is prevLane.rc + curLane.numWidth | 148 | //////refCoord of a lane is prevLane.rc + curLane.numWidth |
149 | 149 | ||
150 | @Constraint(severity="error", key={l}, message="6.2 Lane") | 150 | @Constraint(severity="error", key={l}, message="6.2 Lane") |
151 | pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) { | 151 | pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) { |
152 | Lane.prevLane(l, prev); | 152 | Lane.prevLane(l, prev); |
153 | Lane.referenceCoord(l, rcCur); | 153 | Lane.referenceCoord(l, rcCur); |
154 | 154 | ||
155 | Lane.numWidth(prev, wPrev); | 155 | Lane.numWidth(prev, wPrev); |
156 | Lane.referenceCoord(prev, rcPrev); | 156 | Lane.referenceCoord(prev, rcPrev); |
157 | check(rcCur != rcPrev + wPrev); | 157 | check(rcCur != rcPrev + wPrev); |
158 | } | 158 | } |
159 | 159 | ||
160 | 160 | ||
161 | ////////////// | 161 | ////////////// |
162 | //Lane+Actor | 162 | //Lane+Actor |
163 | ////////////// | 163 | ////////////// |
164 | 164 | ||
165 | /////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] | 165 | /////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] |
166 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | 166 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") |
167 | pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { | 167 | pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { |
168 | Actor.placedOn(a, vl); | 168 | Actor.placedOn(a, vl); |
169 | Actor.xPos(a, x); | 169 | Actor.xPos(a, x); |
170 | Lane.referenceCoord(vl, r); | 170 | Lane.referenceCoord(vl, r); |
171 | check(x <= r); | 171 | check(x <= r); |
172 | } or { | 172 | } or { |
173 | Actor.placedOn(a, vl); | 173 | Actor.placedOn(a, vl); |
174 | Actor.xPos(a, x); | 174 | Actor.xPos(a, x); |
175 | Lane.referenceCoord(vl, r); | 175 | Lane.referenceCoord(vl, r); |
176 | Lane.numWidth(vl, w); | 176 | Lane.numWidth(vl, w); |
177 | check(x >= (r + w)); | 177 | check(x >= (r + w)); |
178 | } | 178 | } |
179 | 179 | ||
180 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | 180 | @Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") |
181 | pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { | 181 | pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { |
182 | Actor.placedOn(a, hl); | 182 | Actor.placedOn(a, hl); |
183 | Actor.yPos(a, y); | 183 | Actor.yPos(a, y); |
184 | Lane.referenceCoord(hl, r); | 184 | Lane.referenceCoord(hl, r); |
185 | check(y <= r); | 185 | check(y <= r); |
186 | } or { | 186 | } or { |
187 | Actor.placedOn(a, hl); | 187 | Actor.placedOn(a, hl); |
188 | Actor.yPos(a, y); | 188 | Actor.yPos(a, y); |
189 | Lane.referenceCoord(hl, r); | 189 | Lane.referenceCoord(hl, r); |
190 | Lane.numWidth(hl, w); | 190 | Lane.numWidth(hl, w); |
191 | check(y >= (r + w)); | 191 | check(y >= (r + w)); |
192 | } | 192 | } |
193 | 193 | ||
194 | ////////////// | 194 | ////////////// |
195 | //Actor | 195 | //Actor |
196 | ////////////// | 196 | ////////////// |
197 | 197 | ||
198 | ////TODO | 198 | ////TODO |
199 | /////////xPos of every actor mmust be within bounds defined in CS | 199 | /////////xPos of every actor mmust be within bounds defined in CS |
200 | //@Constraint(severity="error", key={l}, message="1 Actor") | 200 | //@Constraint(severity="error", key={l}, message="1 Actor") |
201 | //pattern define_actor_xPosWithinCSbounds(cs:CrossingScenario, a:Actor) { | 201 | //pattern define_actor_xPosWithinCSbounds(cs:CrossingScenario, a:Actor) { |
202 | // | 202 | // |
203 | //} | 203 | //} |
204 | // | 204 | // |
205 | ////TODO | 205 | ////TODO |
206 | /////////yPos of every actor mmust be within bounds defined in CS | 206 | /////////yPos of every actor mmust be within bounds defined in CS |
207 | //@Constraint(severity="error", key={l}, message="2 Actor") | 207 | //@Constraint(severity="error", key={l}, message="2 Actor") |
208 | //pattern define_actor_yPosWithinCSbounds(cs:CrossingScenario, a:Actor) { | 208 | //pattern define_actor_yPosWithinCSbounds(cs:CrossingScenario, a:Actor) { |
209 | // | 209 | // |
210 | //} | 210 | //} |
211 | 211 | ||
212 | 212 | ||
213 | /////////pedestrian-width (3) | 213 | /////////pedestrian-width (3) |
214 | pattern define_actor_pedestrianWidth(p:Pedestrian) { | 214 | //pattern define_actor_pedestrianWidth(p:Pedestrian) { |
215 | Pedestrian.width(p, 1.0); | 215 | // Pedestrian.width(p, 1.0); |
216 | } | 216 | //} |
217 | 217 | // | |
218 | /////////pedestrian-width (4) | 218 | ///////////pedestrian-width (4) |
219 | pattern define_actor_pedestrianLength(p:Pedestrian) { | 219 | //pattern define_actor_pedestrianLength(p:Pedestrian) { |
220 | Pedestrian.length(p, 1.0); | 220 | // Pedestrian.length(p, 1.0); |
221 | } | 221 | //} |
222 | 222 | ||
223 | /////////actor-width (5) | 223 | ///////////actor-width (5) |
224 | pattern define_actor_actorWidth(a:Actor) { | 224 | //pattern define_actor_actorWidth(a:Actor) { |
225 | Actor.placedOn(a, l); | 225 | // Actor.placedOn(a, l); |
226 | Lane_Vertical(l); | 226 | // Lane_Vertical(l); |
227 | Actor.width(p, 1.0); | 227 | // Actor.width(p, 1.0); |
228 | } or { | 228 | //} or { |
229 | Actor.placedOn(a, l); | 229 | // Actor.placedOn(a, l); |
230 | Lane_Horizontal(l); | 230 | // Lane_Horizontal(l); |
231 | Actor.width(p, 3.0); | 231 | // Actor.width(p, 3.0); |
232 | } | 232 | //} |
233 | 233 | // | |
234 | /////////actor-width (6) | 234 | ///////////actor-width (6) |
235 | pattern define_actor_actorLength(a:Actor) { | 235 | //pattern define_actor_actorLength(a:Actor) { |
236 | Actor.placedOn(a, l); | 236 | // Actor.placedOn(a, l); |
237 | Lane_Vertical(l); | 237 | // Lane_Vertical(l); |
238 | Actor.length(p, 3.0); | 238 | // Actor.length(p, 3.0); |
239 | } or { | 239 | //} or { |
240 | Actor.placedOn(a, l); | 240 | // Actor.placedOn(a, l); |
241 | Lane_Horizontal(l); | 241 | // Lane_Horizontal(l); |
242 | Actor.length(p, 1.0); | 242 | // Actor.length(p, 1.0); |
243 | } | 243 | //} |
244 | 244 | ||
245 | 245 | ||
246 | /////////xSpeed of actor on verticalLane is 0 | 246 | /////////xSpeed of actor on verticalLane is 0 |
247 | @Constraint(severity="error", key={a}, message="7 Actor") | 247 | @Constraint(severity="error", key={a}, message="7 Actor") |
248 | pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor, vl:Lane_Vertical) { | 248 | pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor, vl:Lane_Vertical) { |
249 | Actor.placedOn(a, vl); | 249 | Actor.placedOn(a, vl); |
250 | Actor.xSpeed(a, xSpeed); | 250 | Actor.xSpeed(a, xSpeed); |
251 | check(xSpeed != 0); | 251 | check(xSpeed != 0); |
252 | } | 252 | } |
253 | 253 | ||
254 | /////////ySpeed of actor on horizontalLane is 0 | 254 | /////////ySpeed of actor on horizontalLane is 0 |
255 | @Constraint(severity="error", key={a}, message="8 Actor") | 255 | @Constraint(severity="error", key={a}, message="8 Actor") |
256 | pattern define_actor_actorOnHoriLaneHasySpeed0(a:Actor, hl:Lane_Horizontal) { | 256 | pattern define_actor_actorOnHoriLaneHasySpeed0(a:Actor, hl:Lane_Horizontal) { |
257 | Actor.placedOn(a, hl); | 257 | Actor.placedOn(a, hl); |
258 | Actor.ySpeed(a, ySpeed); | 258 | Actor.ySpeed(a, ySpeed); |
259 | check(ySpeed != 0); | 259 | check(ySpeed != 0); |
260 | } | 260 | } |
261 | 261 | ||
262 | //////////////// | 262 | //////////////// |
263 | ////CollisionExists | 263 | ////CollisionExists |
264 | //////////////// | 264 | //////////////// |
265 | // | 265 | // |
266 | //@Constraint(severity="error", key={c}, message="x") | 266 | //@Constraint(severity="error", key={c}, message="x") |
267 | //pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { | 267 | //pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { |
268 | // CrossingScenario.actors.relations(ss, c); | 268 | // CrossingScenario.actors.relations(ss, c); |
269 | // CrossingScenario.maxTime(ss, maxTime); | 269 | // CrossingScenario.maxTime(ss, maxTime); |
270 | // CollisionExists. collisionTime(c, cTime); | 270 | // CollisionExists. collisionTime(c, cTime); |
271 | // check(cTime >= maxTime);} | 271 | // check(cTime >= maxTime);} |
272 | // | 272 | // |
273 | //@Constraint(severity="error", key={c}, message="x") | 273 | //@Constraint(severity="error", key={c}, message="x") |
274 | //pattern collisionExists_timeNotNegative(c:CollisionExists) { | 274 | //pattern collisionExists_timeNotNegative(c:CollisionExists) { |
275 | // CollisionExists. collisionTime(c, cTime); | 275 | // CollisionExists. collisionTime(c, cTime); |
276 | // check(cTime <= 0);} | 276 | // check(cTime <= 0);} |
277 | // | 277 | // |
278 | //@Constraint(severity="error", key={a1, c}, message="x") | 278 | //@Constraint(severity="error", key={a1, c}, message="x") |
279 | //pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) { | 279 | //pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) { |
280 | // Actor.relations(a1, c); | 280 | // Actor.relations(a1, c); |
281 | // CollisionExists.target(c, a2); | 281 | // CollisionExists.target(c, a2); |
282 | // | 282 | // |
283 | // Actor.length(a1, l1); | 283 | // Actor.length(a1, l1); |
284 | // Actor.yPos(a1, yPos1); | 284 | // Actor.yPos(a1, yPos1); |
285 | // Actor.ySpeed(a1, ySpeed1); | 285 | // Actor.ySpeed(a1, ySpeed1); |
286 | // Actor.length(a2, l2); | 286 | // Actor.length(a2, l2); |
287 | // Actor.yPos(a2, yPos2); | 287 | // Actor.yPos(a2, yPos2); |
288 | // Actor.ySpeed(a2, ySpeed2); | 288 | // Actor.ySpeed(a2, ySpeed2); |
289 | // CollisionExists. collisionTime(c, cTime); | 289 | // CollisionExists. collisionTime(c, cTime); |
290 | // //check(y_1_bottom > y_2_top | 290 | // //check(y_1_bottom > y_2_top |
291 | // check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); | 291 | // check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); |
292 | //} | 292 | //} |
293 | // | 293 | // |
294 | //@Constraint(severity="error", key={a1, c}, message="x") | 294 | //@Constraint(severity="error", key={a1, c}, message="x") |
295 | //pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor, c:CollisionExists) { | 295 | //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 | 296 | // //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); | 297 | // Actor.relations(a1, c); |
298 | // CollisionExists.target(c, a2); | 298 | // CollisionExists.target(c, a2); |
299 | // | 299 | // |
300 | // Actor.length(a1, l1); | 300 | // Actor.length(a1, l1); |
301 | // Actor.yPos(a1, yPos1); | 301 | // Actor.yPos(a1, yPos1); |
302 | // Actor.ySpeed(a1, ySpeed1); | 302 | // Actor.ySpeed(a1, ySpeed1); |
303 | // Actor.length(a2, l2); | 303 | // Actor.length(a2, l2); |
304 | // Actor.yPos(a2, yPos2); | 304 | // Actor.yPos(a2, yPos2); |
305 | // Actor.ySpeed(a2, ySpeed2); | 305 | // Actor.ySpeed(a2, ySpeed2); |
306 | // CollisionExists. collisionTime(c, cTime); | 306 | // CollisionExists. collisionTime(c, cTime); |
307 | // //check(y_1_top < y_2_bottom) | 307 | // //check(y_1_top < y_2_bottom) |
308 | // check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); | 308 | // check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); |
309 | //} | 309 | //} |
310 | // | 310 | // |
311 | //@Constraint(severity="error", key={a1, c}, message="x") | 311 | //@Constraint(severity="error", key={a1, c}, message="x") |
312 | //pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) { | 312 | //pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) { |
313 | // Actor.relations(a1, c); | 313 | // Actor.relations(a1, c); |
314 | // CollisionExists.target(c, a2); | 314 | // CollisionExists.target(c, a2); |
315 | // | 315 | // |
316 | // Actor.width(a1, w1); | 316 | // Actor.width(a1, w1); |
317 | // Actor.xPos(a1, xPos1); | 317 | // Actor.xPos(a1, xPos1); |
318 | // Actor.xSpeed(a1, xSpeed1); | 318 | // Actor.xSpeed(a1, xSpeed1); |
319 | // Actor.width(a2, w2); | 319 | // Actor.width(a2, w2); |
320 | // Actor.xPos(a2, xPos2); | 320 | // Actor.xPos(a2, xPos2); |
321 | // Actor.xSpeed(a2, xSpeed2); | 321 | // Actor.xSpeed(a2, xSpeed2); |
322 | // CollisionExists. collisionTime(c, cTime); | 322 | // CollisionExists. collisionTime(c, cTime); |
323 | // //check(x_1_left > x_2_right) | 323 | // //check(x_1_left > x_2_right) |
324 | // check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); | 324 | // check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); |
325 | //} | 325 | //} |
326 | // | 326 | // |
327 | //@Constraint(severity="error", key={a1, c}, message="x") | 327 | //@Constraint(severity="error", key={a1, c}, message="x") |
328 | //pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists) { | 328 | //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 | 329 | // //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); | 330 | // Actor.relations(a1, c); |
331 | // CollisionExists.target(c, a2); | 331 | // CollisionExists.target(c, a2); |
332 | // | 332 | // |
333 | // Actor.width(a1, w1); | 333 | // Actor.width(a1, w1); |
334 | // Actor.xPos(a1, xPos1); | 334 | // Actor.xPos(a1, xPos1); |
335 | // Actor.xSpeed(a1, xSpeed1); | 335 | // Actor.xSpeed(a1, xSpeed1); |
336 | // Actor.width(a2, w2); | 336 | // Actor.width(a2, w2); |
337 | // Actor.xPos(a2, xPos2); | 337 | // Actor.xPos(a2, xPos2); |
338 | // Actor.xSpeed(a2, xSpeed2); | 338 | // Actor.xSpeed(a2, xSpeed2); |
339 | // CollisionExists. collisionTime(c, cTime); | 339 | // CollisionExists. collisionTime(c, cTime); |
340 | // //check(x_1_right < x_2_left) | 340 | // //check(x_1_right < x_2_left) |
341 | // check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | 341 | // check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); |
342 | //} | 342 | //} |
343 | // | 343 | // |
344 | //////////////// | 344 | //////////////// |
345 | ////SeparationDistance | 345 | ////SeparationDistance |
346 | //////////////// | 346 | //////////////// |
347 | //@Constraint(severity="error", key={a1, sd}, message="x") | 347 | //@Constraint(severity="error", key={a1, sd}, message="x") |
348 | //pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | 348 | //pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { |
349 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 349 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
350 | // Actor.relations(a1, sd); | 350 | // Actor.relations(a1, sd); |
351 | // SeparationDistance.target(sd, a2); | 351 | // SeparationDistance.target(sd, a2); |
352 | // SeparationDistance.distance(sd, Distance::Near); | 352 | // SeparationDistance.distance(sd, Distance::Near); |
353 | // | 353 | // |
354 | // Actor.xPos(a1, x1); | 354 | // Actor.xPos(a1, x1); |
355 | // Actor.yPos(a1, y1); | 355 | // Actor.yPos(a1, y1); |
356 | // Actor.xPos(a2, x2); | 356 | // Actor.xPos(a2, x2); |
357 | // Actor.yPos(a2, y2); | 357 | // Actor.yPos(a2, y2); |
358 | // //check(dx^2 + dy^2 < 5^2) | 358 | // //check(dx^2 + dy^2 < 5^2) |
359 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); | 359 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); |
360 | //} | 360 | //} |
361 | // | 361 | // |
362 | //@Constraint(severity="error", key={a1, sd}, message="x") | 362 | //@Constraint(severity="error", key={a1, sd}, message="x") |
363 | //pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | 363 | //pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { |
364 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 364 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
365 | // Actor.relations(a1, sd); | 365 | // Actor.relations(a1, sd); |
366 | // SeparationDistance.target(sd, a2); | 366 | // SeparationDistance.target(sd, a2); |
367 | // SeparationDistance.distance(sd, Distance::Near); | 367 | // SeparationDistance.distance(sd, Distance::Near); |
368 | // | 368 | // |
369 | // Actor.xPos(a1, x1); | 369 | // Actor.xPos(a1, x1); |
370 | // Actor.yPos(a1, y1); | 370 | // Actor.yPos(a1, y1); |
371 | // Actor.xPos(a2, x2); | 371 | // Actor.xPos(a2, x2); |
372 | // Actor.yPos(a2, y2); | 372 | // Actor.yPos(a2, y2); |
373 | // //check(dx^2 + dy^2 > 10^2) | 373 | // //check(dx^2 + dy^2 > 10^2) |
374 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | 374 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); |
375 | //} | 375 | //} |
376 | // | 376 | // |
377 | //@Constraint(severity="error", key={a1, sd}, message="x") | 377 | //@Constraint(severity="error", key={a1, sd}, message="x") |
378 | //pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | 378 | //pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { |
379 | // //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 |
380 | // Actor.relations(a1, sd); | 380 | // Actor.relations(a1, sd); |
381 | // SeparationDistance.target(sd, a2); | 381 | // SeparationDistance.target(sd, a2); |
382 | // SeparationDistance.distance(sd, Distance::Medium); | 382 | // SeparationDistance.distance(sd, Distance::Medium); |
383 | // | 383 | // |
384 | // Actor.xPos(a1, x1); | 384 | // Actor.xPos(a1, x1); |
385 | // Actor.yPos(a1, y1); | 385 | // Actor.yPos(a1, y1); |
386 | // Actor.xPos(a2, x2); | 386 | // Actor.xPos(a2, x2); |
387 | // Actor.yPos(a2, y2); | 387 | // Actor.yPos(a2, y2); |
388 | // //check(dx^2 + dy^2 < 10^2) | 388 | // //check(dx^2 + dy^2 < 10^2) |
389 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | 389 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); |
390 | //} | 390 | //} |
391 | // | 391 | // |
392 | //@Constraint(severity="error", key={a1, sd}, message="x") | 392 | //@Constraint(severity="error", key={a1, sd}, message="x") |
393 | //pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | 393 | //pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { |
394 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 394 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
395 | // Actor.relations(a1, sd); | 395 | // Actor.relations(a1, sd); |
396 | // SeparationDistance.target(sd, a2); | 396 | // SeparationDistance.target(sd, a2); |
397 | // SeparationDistance.distance(sd, Distance::Medium); | 397 | // SeparationDistance.distance(sd, Distance::Medium); |
398 | // | 398 | // |
399 | // Actor.xPos(a1, x1); | 399 | // Actor.xPos(a1, x1); |
400 | // Actor.yPos(a1, y1); | 400 | // Actor.yPos(a1, y1); |
401 | // Actor.xPos(a2, x2); | 401 | // Actor.xPos(a2, x2); |
402 | // Actor.yPos(a2, y2); | 402 | // Actor.yPos(a2, y2); |
403 | // //check(dx^2 + dy^2 > 1^2) | 403 | // //check(dx^2 + dy^2 > 1^2) |
404 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); | 404 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); |
405 | //} | 405 | //} |
406 | // | 406 | // |
407 | //@Constraint(severity="error", key={a1, sd}, message="x") | 407 | //@Constraint(severity="error", key={a1, sd}, message="x") |
408 | //pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | 408 | //pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { |
409 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 409 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
410 | // Actor.relations(a1, sd); | 410 | // Actor.relations(a1, sd); |
411 | // SeparationDistance.target(sd, a2); | 411 | // SeparationDistance.target(sd, a2); |
412 | // SeparationDistance.distance(sd, Distance::Far); | 412 | // SeparationDistance.distance(sd, Distance::Far); |
413 | // | 413 | // |
414 | // Actor.xPos(a1, x1); | 414 | // Actor.xPos(a1, x1); |
415 | // Actor.yPos(a1, y1); | 415 | // Actor.yPos(a1, y1); |
416 | // Actor.xPos(a2, x2); | 416 | // Actor.xPos(a2, x2); |
417 | // Actor.yPos(a2, y2); | 417 | // Actor.yPos(a2, y2); |
418 | // //check(dx^2 + dy^2 < 15^2) | 418 | // //check(dx^2 + dy^2 < 15^2) |
419 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | 419 | // check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); |
420 | //} | 420 | //} |
421 | // | 421 | // |
422 | //////////////// | 422 | //////////////// |
423 | ////CollisionDoesNotExist | 423 | ////CollisionDoesNotExist |
424 | //////////////// | 424 | //////////////// |
425 | // | 425 | // |
426 | ////@Constraint(severity="error", key={a1, cdne}, message="x") | 426 | ////@Constraint(severity="error", key={a1, cdne}, message="x") |
427 | ////pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) { | 427 | ////pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) { |
428 | //// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 428 | //// //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
429 | //// | 429 | //// |
430 | //// CrossingScenario.actors(ss, a1); | 430 | //// CrossingScenario.actors(ss, a1); |
431 | //// CrossingScenario.actors(ss, a2); | 431 | //// CrossingScenario.actors(ss, a2); |
432 | //// Actor.relations(a1, cdne); | 432 | //// Actor.relations(a1, cdne); |
433 | //// CollisionDoesNotExist.target(cdne, a2); | 433 | //// CollisionDoesNotExist.target(cdne, a2); |
434 | //// CrossingScenario.maxTime(ss, maxTime); | 434 | //// CrossingScenario.maxTime(ss, maxTime); |
435 | //// | 435 | //// |
436 | //// Actor.width(a1, w1); | 436 | //// Actor.width(a1, w1); |
437 | //// Actor.length(a1, l1); | 437 | //// Actor.length(a1, l1); |
438 | //// Actor.xPos(a1, xPos1); | 438 | //// Actor.xPos(a1, xPos1); |
439 | //// Actor.yPos(a1, yPos1); | 439 | //// Actor.yPos(a1, yPos1); |
440 | //// Actor.xSpeed(a1, xSpeed1); | 440 | //// Actor.xSpeed(a1, xSpeed1); |
441 | //// Actor.ySpeed(a1, ySpeed1); | 441 | //// Actor.ySpeed(a1, ySpeed1); |
442 | //// | 442 | //// |
443 | //// Actor.width(a2, w2); | 443 | //// Actor.width(a2, w2); |
444 | //// Actor.length(a2, l2); | 444 | //// Actor.length(a2, l2); |
445 | //// Actor.xPos(a2, xPos2); | 445 | //// Actor.xPos(a2, xPos2); |
446 | //// Actor.yPos(a2, yPos2); | 446 | //// Actor.yPos(a2, yPos2); |
447 | //// Actor.xSpeed(a2, xSpeed2); | 447 | //// Actor.xSpeed(a2, xSpeed2); |
448 | //// Actor.ySpeed(a2, ySpeed2); | 448 | //// Actor.ySpeed(a2, ySpeed2); |
449 | //// //check(dx^2 + dy^2 < 15^2) | 449 | //// //check(dx^2 + dy^2 < 15^2) |
450 | //// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | 450 | //// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); |
451 | ////} | 451 | ////} |
452 | // | 452 | // |
453 | //////////////// | 453 | //////////////// |
454 | ////VisionBlocked | 454 | ////VisionBlocked |
455 | //////////////// | 455 | //////////////// |
456 | // | 456 | // |
457 | ////OPTIONS 1: everything is from a single check expression containing ITEs | 457 | ////OPTIONS 1: everything is from a single check expression containing ITEs |
458 | ////Currently unhandled bygenerator | 458 | ////Currently unhandled bygenerator |
459 | //@Constraint(severity="error", key={a1, vb}, message="x") | 459 | //@Constraint(severity="error", key={a1, vb}, message="x") |
460 | //pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { | 460 | //pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { |
461 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 461 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
462 | // Actor.relations(a1, vb); | 462 | // Actor.relations(a1, vb); |
463 | // VisionBlocked.target(vb, a2); | 463 | // VisionBlocked.target(vb, a2); |
464 | // VisionBlocked.blockedBy(vb, aBlocker); | 464 | // VisionBlocked.blockedBy(vb, aBlocker); |
465 | // | 465 | // |
466 | // Actor.xPos(a1, x1); | 466 | // Actor.xPos(a1, x1); |
467 | // Actor.yPos(a1, y1); | 467 | // Actor.yPos(a1, y1); |
468 | // Actor.xPos(a2, x2); | 468 | // Actor.xPos(a2, x2); |
469 | // Actor.yPos(a2, y2); | 469 | // Actor.yPos(a2, y2); |
470 | // Actor.xPos(aBlocker, xBlocker); | 470 | // Actor.xPos(aBlocker, xBlocker); |
471 | // Actor.yPos(aBlocker, yBlocker); | 471 | // Actor.yPos(aBlocker, yBlocker); |
472 | // Actor.length(aBlocker, lenBlocker); | 472 | // Actor.length(aBlocker, lenBlocker); |
473 | // Actor.width(aBlocker, widBlocker); | 473 | // Actor.width(aBlocker, widBlocker); |
474 | // | 474 | // |
475 | // //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | 475 | // //check(slope of a1-to-BlockerTop < slope of a1-to-a2) |
476 | // check( | 476 | // check( |
477 | // ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / | 477 | // ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / |
478 | // ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) | 478 | // ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) |
479 | // < ((y1-y2)/(x1-x2))); | 479 | // < ((y1-y2)/(x1-x2))); |
480 | //} | 480 | //} |
481 | // | 481 | // |
482 | //@Constraint(severity="error", key={a1, vb}, message="x") | 482 | //@Constraint(severity="error", key={a1, vb}, message="x") |
483 | //pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { | 483 | //pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { |
484 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | 484 | // //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 |
485 | // Actor.relations(a1, vb); | 485 | // Actor.relations(a1, vb); |
486 | // VisionBlocked.target(vb, a2); | 486 | // VisionBlocked.target(vb, a2); |
487 | // VisionBlocked.blockedBy(vb, aBlocker); | 487 | // VisionBlocked.blockedBy(vb, aBlocker); |
488 | // | 488 | // |
489 | // Actor.xPos(a1, x1); | 489 | // Actor.xPos(a1, x1); |
490 | // Actor.yPos(a1, y1); | 490 | // Actor.yPos(a1, y1); |
491 | // Actor.xPos(a2, x2); | 491 | // Actor.xPos(a2, x2); |
492 | // Actor.yPos(a2, y2); | 492 | // Actor.yPos(a2, y2); |
493 | // Actor.xPos(aBlocker, xBlocker); | 493 | // Actor.xPos(aBlocker, xBlocker); |
494 | // Actor.yPos(aBlocker, yBlocker); | 494 | // Actor.yPos(aBlocker, yBlocker); |
495 | // Actor.length(aBlocker, lenBlocker); | 495 | // Actor.length(aBlocker, lenBlocker); |
496 | // Actor.width(aBlocker, widBlocker); | 496 | // Actor.width(aBlocker, widBlocker); |
497 | // | 497 | // |
498 | // //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | 498 | // //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) |
499 | // check( | 499 | // check( |
500 | // ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / | 500 | // ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / |
501 | // ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) | 501 | // ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) |
502 | // > ((y1-y2)/(x1-x2))); | 502 | // > ((y1-y2)/(x1-x2))); |
503 | //} | 503 | //} |
504 | // | 504 | // |
505 | ////OPTION 2: | 505 | ////OPTION 2: |
506 | ////we handle ITE by seperating the constraints | 506 | ////we handle ITE by seperating the constraints |
507 | // | 507 | // |
508 | ////This will involve 1 constarint for each decision path, but will require multiple check expressions within the same pattern | 508 | ////This will involve 1 constarint for each decision path, but will require multiple check expressions within the same pattern |
509 | // | 509 | // |
510 | ////OPTION 3: | 510 | ////OPTION 3: |
511 | ////If this is nott working still, we will have to add some strctural components to the MM | 511 | ////If this is nott working still, we will have to add some strctural components to the MM |
512 | ////to differentiate the different cases and reduce the requirements of if, then, else | 512 | ////to differentiate the different cases and reduce the requirements of if, then, else |
513 | // | 513 | // |
514 | ////This will involve more patterns, and some that are pstructural as well. \ No newline at end of file | 514 | ////This will involve more patterns, and some that are pstructural as well. \ No newline at end of file |