diff options
author | 2021-01-14 10:34:59 -0500 | |
---|---|---|
committer | 2021-01-14 10:34:59 -0500 | |
commit | dc931c24870432efcd3c3fca4fb6fbd401c70420 (patch) | |
tree | 60e417e047ac712be38058a5b358d5ea2f24c3fe /Domains/simpleScenario/queries | |
parent | deactivate the constraints used for debugging (diff) | |
download | VIATRA-Generator-dc931c24870432efcd3c3fca4fb6fbd401c70420.tar.gz VIATRA-Generator-dc931c24870432efcd3c3fca4fb6fbd401c70420.tar.zst VIATRA-Generator-dc931c24870432efcd3c3fca4fb6fbd401c70420.zip |
refactor simpleScenario->crossingScenario
Diffstat (limited to 'Domains/simpleScenario/queries')
-rw-r--r-- | Domains/simpleScenario/queries/logProb._vql | 41 | ||||
-rw-r--r-- | Domains/simpleScenario/queries/simpleScenarioQueries.vql | 400 |
2 files changed, 0 insertions, 441 deletions
diff --git a/Domains/simpleScenario/queries/logProb._vql b/Domains/simpleScenario/queries/logProb._vql deleted file mode 100644 index e6045909..00000000 --- a/Domains/simpleScenario/queries/logProb._vql +++ /dev/null | |||
@@ -1,41 +0,0 @@ | |||
1 | package queries | ||
2 | |||
3 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" | ||
4 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" | ||
5 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" | ||
6 | |||
7 | pattern UPMUSTPropagateConstraint0_pattern_queries_refSpec( | ||
8 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
9 | var_l) | ||
10 | { | ||
11 | // Original Constraints | ||
12 | // var_l exported | ||
13 | find mustInRelationreferenceCoord_attribute_Lane(problem,interpretation,var_l,var_w); | ||
14 | // Propagation for constraint | ||
15 | PrimitiveElement.valueSet(var_w,setted_var_w); | ||
16 | IntegerElement.value(var_w,value_var_w); | ||
17 | // Matching variables | ||
18 | //var_w==up_1; | ||
19 | } | ||
20 | |||
21 | /** | ||
22 | * Matcher for detecting tuples t where []referenceCoord attribute Lane(source,target) | ||
23 | */ | ||
24 | pattern mustInRelationreferenceCoord_attribute_Lane( | ||
25 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
26 | source: DefinedElement, target:DefinedElement) | ||
27 | { | ||
28 | find interpretation(problem,interpretation); | ||
29 | PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); | ||
30 | PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"referenceCoord attribute Lane"); | ||
31 | PartialRelationInterpretation.relationlinks(relationIterpretation,link); | ||
32 | BinaryElementRelationLink.param1(link,source); | ||
33 | BinaryElementRelationLink.param2(link,target); | ||
34 | } | ||
35 | |||
36 | ////////// | ||
37 | // 0. Util | ||
38 | ////////// | ||
39 | pattern interpretation(problem:LogicProblem, interpretation:PartialInterpretation) { | ||
40 | PartialInterpretation.problem(interpretation,problem); | ||
41 | } \ No newline at end of file | ||
diff --git a/Domains/simpleScenario/queries/simpleScenarioQueries.vql b/Domains/simpleScenario/queries/simpleScenarioQueries.vql deleted file mode 100644 index 735abdc5..00000000 --- a/Domains/simpleScenario/queries/simpleScenarioQueries.vql +++ /dev/null | |||
@@ -1,400 +0,0 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http://www.example.com/simpleScenario" | ||
4 | import "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 <= 2.0); | ||
11 | } | ||
12 | |||
13 | ////////////// | ||
14 | //Lane | ||
15 | ////////////// | ||
16 | |||
17 | /////////width, numWidth | ||
18 | @Constraint(severity="error", key={l}, message="x") | ||
19 | pattern define_numWidth_small(l : Lane) { | ||
20 | Lane.width(l, Size::Small); | ||
21 | Lane.numWidth(l, nw); | ||
22 | check(nw <= 5); | ||
23 | } or { | ||
24 | Lane.width(l, Size::Small); | ||
25 | Lane.numWidth(l, nw); | ||
26 | check(nw >= 10); | ||
27 | } | ||
28 | |||
29 | @Constraint(severity="error", key={l}, message="x") | ||
30 | pattern define_numWidth_medium(l : Lane) { | ||
31 | Lane.width(l, Size::Medium); | ||
32 | Lane.numWidth(l, nw); | ||
33 | check(nw <= 10); | ||
34 | } or { | ||
35 | Lane.width(l, Size::Medium); | ||
36 | Lane.numWidth(l, nw); | ||
37 | check(nw >= 15); | ||
38 | } | ||
39 | |||
40 | @Constraint(severity="error", key={l}, message="x") | ||
41 | pattern define_numWidth_large(l : Lane) { | ||
42 | Lane.width(l, Size::Large); | ||
43 | Lane.numWidth(l, nw); | ||
44 | check(nw <= 15); | ||
45 | } or { | ||
46 | Lane.width(l, Size::Large); | ||
47 | Lane.numWidth(l, nw); | ||
48 | check(nw >= 20); | ||
49 | } | ||
50 | |||
51 | /////////referenceCoord | ||
52 | @Constraint(severity="error", key={l}, message="x") | ||
53 | pattern define_referenceCoord_horizontalAtOrigin(l:Lane) { | ||
54 | 1 == count find find_horizontalLaneAtOrigin(l); | ||
55 | } | ||
56 | |||
57 | private pattern find_horizontalLaneAtOrigin(l:Lane){ | ||
58 | Lane.orientation(l, Orientation::Horizontal); | ||
59 | Lane.referenceCoord(l, rc); | ||
60 | Lane.prevLane(l, prev); | ||
61 | rc != 0.0; | ||
62 | } | ||
63 | |||
64 | @Constraint(severity="error", key={l}, message="x") | ||
65 | pattern define_referenceCoord_verticalAtOrigin(l:Lane) { | ||
66 | 1 == count find find_verticalLaneAtOrigin(l); | ||
67 | } | ||
68 | |||
69 | private pattern find_verticalLaneAtOrigin(l:Lane){ | ||
70 | Lane.orientation(l, Orientation::Vertical); | ||
71 | Lane.referenceCoord(l, rc); | ||
72 | rc == 0.0; | ||
73 | } | ||
74 | |||
75 | pattern define_referenceCoord_VerticalifMultipleLanes(l1:Lane, l2:Lane) { | ||
76 | //calculated risk??? | ||
77 | Lane.orientation(l1, Orientation::Vertical); | ||
78 | Lane.orientation(l2, Orientation::Vertical); | ||
79 | Lane.referenceCoord(l1, rc1); | ||
80 | Lane.numWidth(l1, nw1); | ||
81 | Lane.referenceCoord(l2, rc2); | ||
82 | check(rc2 == rc1 + nw1); | ||
83 | } | ||
84 | |||
85 | |||
86 | //@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") | ||
87 | //pattern actorOnVerticalLane(a : Actor) { | ||
88 | // Actor.placedOn(a, l); | ||
89 | // Lane.orientation(l, Orientation::Vertical); | ||
90 | // Actor.xPos(a, x); | ||
91 | // Lane.referenceCoord(l, r); | ||
92 | // check(x <= r); | ||
93 | //} or { | ||
94 | // Actor.placedOn(a, l); | ||
95 | // Lane.orientation(l, Orientation::Vertical); | ||
96 | // Actor.xPos(a, x); | ||
97 | // Lane.referenceCoord(l, r); | ||
98 | // Lane.numWidth(l, w); | ||
99 | // check(x >= (r + w)); | ||
100 | //} | ||
101 | // | ||
102 | //@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for horizontal lanes") | ||
103 | //pattern actorOnHorizontalLane(a : Actor) { | ||
104 | // Actor.placedOn(a, l); | ||
105 | // Lane.orientation(l, Orientation::Horizontal); | ||
106 | // Actor.yPos(a, y); | ||
107 | // Lane.referenceCoord(l, r); | ||
108 | // check(y <= r); | ||
109 | //} or { | ||
110 | // Actor.placedOn(a, l); | ||
111 | // Lane.orientation(l, Orientation::Horizontal); | ||
112 | // Actor.yPos(a, y); | ||
113 | // Lane.referenceCoord(l, r); | ||
114 | // Lane.numWidth(l, w); | ||
115 | // check(y >= (r + w)); | ||
116 | //} | ||
117 | |||
118 | //@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation") | ||
119 | //pattern actorOnLane(a : Actor) { | ||
120 | // find actorOnVerticalLane(a); | ||
121 | //// neg find actorOnHorizontalLane(a); | ||
122 | //} | ||
123 | // | ||
124 | //private pattern actorOnVerticalLane(a : Actor) { | ||
125 | // Actor.placedOn(a, l); | ||
126 | // Lane.orientation(l, Orientation::Vertical); | ||
127 | // Actor.xPos(a, x); | ||
128 | // Lane.referenceCoord(l, r); | ||
129 | // Lane.numWidth(l, w); | ||
130 | // check(x >= r); | ||
131 | // check(x <= (r + w)); | ||
132 | //} | ||
133 | |||
134 | //@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation") | ||
135 | //pattern widthSpec(l : Lane) { | ||
136 | // Lane.numWidth(l, w); | ||
137 | // check(w != 5); | ||
138 | //} | ||
139 | |||
140 | //private pattern actorOnHorizontalLane(a : Actor) { | ||
141 | // Actor.placedOn(a, l); | ||
142 | // Lane.orientation(l, Orientation::Vertical); | ||
143 | // Actor.yPos(a, y); | ||
144 | // Lane.referenceCoord(l, r); | ||
145 | // Lane.widthNum(l, w); | ||
146 | // check(y >= r); | ||
147 | // check(y <= (r + w)); | ||
148 | //} | ||
149 | |||
150 | ////////////// | ||
151 | //CollisionExists | ||
152 | ////////////// | ||
153 | |||
154 | @Constraint(severity="error", key={c}, message="x") | ||
155 | pattern collisionExists_timeWithinBound(ss:SimpleScenario, c:CollisionExists) { | ||
156 | SimpleScenario.actors.relations(ss, c); | ||
157 | SimpleScenario.maxTime(ss, maxTime); | ||
158 | CollisionExists. collisionTime(c, cTime); | ||
159 | check(cTime >= maxTime);} | ||
160 | |||
161 | @Constraint(severity="error", key={c}, message="x") | ||
162 | pattern collisionExists_timeNotNegative(c:CollisionExists) { | ||
163 | CollisionExists. collisionTime(c, cTime); | ||
164 | check(cTime <= 0);} | ||
165 | |||
166 | @Constraint(severity="error", key={a1, c}, message="x") | ||
167 | pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) { | ||
168 | Actor.relations(a1, c); | ||
169 | CollisionExists.target(c, a2); | ||
170 | |||
171 | Actor.length(a1, l1); | ||
172 | Actor.yPos(a1, yPos1); | ||
173 | Actor.ySpeed(a1, ySpeed1); | ||
174 | Actor.length(a2, l2); | ||
175 | Actor.yPos(a2, yPos2); | ||
176 | Actor.ySpeed(a2, ySpeed2); | ||
177 | CollisionExists. collisionTime(c, cTime); | ||
178 | //check(y_1_bottom > y_2_top | ||
179 | check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); | ||
180 | } | ||
181 | |||
182 | @Constraint(severity="error", key={a1, c}, message="x") | ||
183 | pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor, c:CollisionExists) { | ||
184 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
185 | Actor.relations(a1, c); | ||
186 | CollisionExists.target(c, a2); | ||
187 | |||
188 | Actor.length(a1, l1); | ||
189 | Actor.yPos(a1, yPos1); | ||
190 | Actor.ySpeed(a1, ySpeed1); | ||
191 | Actor.length(a2, l2); | ||
192 | Actor.yPos(a2, yPos2); | ||
193 | Actor.ySpeed(a2, ySpeed2); | ||
194 | CollisionExists. collisionTime(c, cTime); | ||
195 | //check(y_1_top < y_2_bottom) | ||
196 | check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); | ||
197 | } | ||
198 | |||
199 | @Constraint(severity="error", key={a1, c}, message="x") | ||
200 | pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) { | ||
201 | Actor.relations(a1, c); | ||
202 | CollisionExists.target(c, a2); | ||
203 | |||
204 | Actor.width(a1, w1); | ||
205 | Actor.xPos(a1, xPos1); | ||
206 | Actor.xSpeed(a1, xSpeed1); | ||
207 | Actor.width(a2, w2); | ||
208 | Actor.xPos(a2, xPos2); | ||
209 | Actor.xSpeed(a2, xSpeed2); | ||
210 | CollisionExists. collisionTime(c, cTime); | ||
211 | //check(x_1_left > x_2_right) | ||
212 | check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); | ||
213 | } | ||
214 | |||
215 | @Constraint(severity="error", key={a1, c}, message="x") | ||
216 | pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists) { | ||
217 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
218 | Actor.relations(a1, c); | ||
219 | CollisionExists.target(c, a2); | ||
220 | |||
221 | Actor.width(a1, w1); | ||
222 | Actor.xPos(a1, xPos1); | ||
223 | Actor.xSpeed(a1, xSpeed1); | ||
224 | Actor.width(a2, w2); | ||
225 | Actor.xPos(a2, xPos2); | ||
226 | Actor.xSpeed(a2, xSpeed2); | ||
227 | CollisionExists. collisionTime(c, cTime); | ||
228 | //check(x_1_right < x_2_left) | ||
229 | check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); | ||
230 | } | ||
231 | |||
232 | ////////////// | ||
233 | //SeparationDistance | ||
234 | ////////////// | ||
235 | @Constraint(severity="error", key={a1, c}, message="x") | ||
236 | pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
237 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
238 | Actor.relations(a1, sd); | ||
239 | SeparationDistance.target(sd, a2); | ||
240 | SeparationDistance.distance(sd, Distance::Near); | ||
241 | |||
242 | Actor.xPos(a1, x1); | ||
243 | Actor.yPos(a1, y1); | ||
244 | Actor.xPos(a2, x2); | ||
245 | Actor.yPos(a2, y2); | ||
246 | //check(dx^2 + dy^2 < 5^2) | ||
247 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); | ||
248 | } | ||
249 | |||
250 | @Constraint(severity="error", key={a1, c}, message="x") | ||
251 | pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
252 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
253 | Actor.relations(a1, sd); | ||
254 | SeparationDistance.target(sd, a2); | ||
255 | SeparationDistance.distance(sd, Distance::Near); | ||
256 | |||
257 | Actor.xPos(a1, x1); | ||
258 | Actor.yPos(a1, y1); | ||
259 | Actor.xPos(a2, x2); | ||
260 | Actor.yPos(a2, y2); | ||
261 | //check(dx^2 + dy^2 > 10^2) | ||
262 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); | ||
263 | } | ||
264 | |||
265 | @Constraint(severity="error", key={a1, c}, message="x") | ||
266 | pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
267 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
268 | Actor.relations(a1, sd); | ||
269 | SeparationDistance.target(sd, a2); | ||
270 | SeparationDistance.distance(sd, Distance::Medium); | ||
271 | |||
272 | Actor.xPos(a1, x1); | ||
273 | Actor.yPos(a1, y1); | ||
274 | Actor.xPos(a2, x2); | ||
275 | Actor.yPos(a2, y2); | ||
276 | //check(dx^2 + dy^2 < 10^2) | ||
277 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); | ||
278 | } | ||
279 | |||
280 | @Constraint(severity="error", key={a1, c}, message="x") | ||
281 | pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
282 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
283 | Actor.relations(a1, sd); | ||
284 | SeparationDistance.target(sd, a2); | ||
285 | SeparationDistance.distance(sd, Distance::Medium); | ||
286 | |||
287 | Actor.xPos(a1, x1); | ||
288 | Actor.yPos(a1, y1); | ||
289 | Actor.xPos(a2, x2); | ||
290 | Actor.yPos(a2, y2); | ||
291 | //check(dx^2 + dy^2 > 1^2) | ||
292 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15); | ||
293 | } | ||
294 | |||
295 | @Constraint(severity="error", key={a1, c}, message="x") | ||
296 | pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) { | ||
297 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
298 | Actor.relations(a1, sd); | ||
299 | SeparationDistance.target(sd, a2); | ||
300 | SeparationDistance.distance(sd, Distance::Far); | ||
301 | |||
302 | Actor.xPos(a1, x1); | ||
303 | Actor.yPos(a1, y1); | ||
304 | Actor.xPos(a2, x2); | ||
305 | Actor.yPos(a2, y2); | ||
306 | //check(dx^2 + dy^2 < 15^2) | ||
307 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
308 | } | ||
309 | |||
310 | ////////////// | ||
311 | //CollisionDoesNotExist | ||
312 | ////////////// | ||
313 | |||
314 | @Constraint(severity="error", key={a1, c}, message="x") | ||
315 | pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:SimpleScenario, cdne:CollisionDoesNotExist) { | ||
316 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
317 | |||
318 | SimpleScenario.actors(ss, a1); | ||
319 | SimpleScenario.actors(ss, a2); | ||
320 | Actor.relations(a1, cdne); | ||
321 | CollisionDoesNotExist.target(cdne, a2); | ||
322 | SimpleScenario.maxTime(ss, maxTime); | ||
323 | |||
324 | Actor.width(a1, w1); | ||
325 | Actor.length(a1, l1); | ||
326 | Actor.xPos(a1, xPos1); | ||
327 | Actor.yPos(a1, yPos1); | ||
328 | Actor.xSpeed(a1, xSpeed1); | ||
329 | Actor.ySpeed(a1, ySpeed1); | ||
330 | |||
331 | Actor.width(a2, w2); | ||
332 | Actor.length(a2, l2); | ||
333 | Actor.xPos(a2, xPos2); | ||
334 | Actor.yPos(a2, yPos2); | ||
335 | Actor.xSpeed(a2, xSpeed2); | ||
336 | Actor.ySpeed(a2, ySpeed2); | ||
337 | //check(dx^2 + dy^2 < 15^2) | ||
338 | check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); | ||
339 | } | ||
340 | |||
341 | ////////////// | ||
342 | //VisionBlocked | ||
343 | ////////////// | ||
344 | |||
345 | //OPTIONS 1: everything is from a single check expression containing ITEs | ||
346 | //Currently unhandled bygenerator | ||
347 | pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
348 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
349 | Actor.relations(a1, vb); | ||
350 | VisionBlocked.target(vb, a2); | ||
351 | VisionBlocked.blockedBy(vb, aBlocker); | ||
352 | |||
353 | Actor.xPos(a1, x1); | ||
354 | Actor.yPos(a1, y1); | ||
355 | Actor.xPos(a2, x2); | ||
356 | Actor.yPos(a2, y2); | ||
357 | Actor.xPos(aBlocker, xBlocker); | ||
358 | Actor.yPos(aBlocker, yBlocker); | ||
359 | Actor.length(aBlocker, lenBlocker); | ||
360 | Actor.width(aBlocker, widBlocker); | ||
361 | |||
362 | //check(slope of a1-to-BlockerTop < slope of a1-to-a2) | ||
363 | check( | ||
364 | ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / | ||
365 | ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) | ||
366 | < ((y1-y2)/(x1-x2))); | ||
367 | } | ||
368 | |||
369 | pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { | ||
370 | //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 | ||
371 | Actor.relations(a1, vb); | ||
372 | VisionBlocked.target(vb, a2); | ||
373 | VisionBlocked.blockedBy(vb, aBlocker); | ||
374 | |||
375 | Actor.xPos(a1, x1); | ||
376 | Actor.yPos(a1, y1); | ||
377 | Actor.xPos(a2, x2); | ||
378 | Actor.yPos(a2, y2); | ||
379 | Actor.xPos(aBlocker, xBlocker); | ||
380 | Actor.yPos(aBlocker, yBlocker); | ||
381 | Actor.length(aBlocker, lenBlocker); | ||
382 | Actor.width(aBlocker, widBlocker); | ||
383 | |||
384 | //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) | ||
385 | check( | ||
386 | ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / | ||
387 | ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) | ||
388 | > ((y1-y2)/(x1-x2))); | ||
389 | } | ||
390 | |||
391 | //OPTION 2: | ||
392 | //we handle ITE by seperating the constraints | ||
393 | |||
394 | //This will involve 1 constarint for each decision path, but will require multiple check expressions within the same pattern | ||
395 | |||
396 | //OPTION 3: | ||
397 | //If this is nott working still, we will have to add some strctural components to the MM | ||
398 | //to differentiate the different cases and reduce the requirements of if, then, else | ||
399 | |||
400 | //This will involve more patterns, and some that are pstructural as well. \ No newline at end of file | ||