diff options
author | OszkarSemerath <semerath@mit.bme.hu> | 2021-07-30 10:04:27 +0200 |
---|---|---|
committer | OszkarSemerath <semerath@mit.bme.hu> | 2021-07-30 10:04:27 +0200 |
commit | aaa67b0ef8840d97b062a4f1383bf93410984af3 (patch) | |
tree | 2c07208bb6b5ab27b47bd477dfbcc6e77b50d623 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend | |
parent | Config updated and createSharedVersionedMapStores service (diff) | |
download | VIATRA-Generator-V4transformation.tar.gz VIATRA-Generator-V4transformation.tar.zst VIATRA-Generator-V4transformation.zip |
Numeric solver dreal hardcoding -> configV4transformation
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend | 531 |
1 files changed, 531 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend new file mode 100644 index 00000000..b3e2d78d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericRefinementUnit.xtend | |||
@@ -0,0 +1,531 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericDrealProblemSolver | ||
4 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | ||
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericZ3ProblemSolver | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BinaryElementRelationLink | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRelationInterpretation | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RelationLink | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ExplorationStrategy | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.NumericSolverSelection | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
19 | import java.util.HashMap | ||
20 | import java.util.LinkedHashMap | ||
21 | import java.util.LinkedHashSet | ||
22 | import java.util.List | ||
23 | import java.util.Map | ||
24 | import org.eclipse.emf.ecore.EObject | ||
25 | import org.eclipse.viatra.dse.base.ThreadContext | ||
26 | import org.eclipse.viatra.dse.objectives.Fitness | ||
27 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
28 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
29 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
30 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
31 | import org.eclipse.viatra.dse.objectives.IObjective | ||
32 | |||
33 | class NumericRefinementUnit { | ||
34 | val ModelGenerationMethod method | ||
35 | var ThreadContext threadContext | ||
36 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | ||
37 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | ||
38 | var NumericTranslator translator = null; | ||
39 | |||
40 | |||
41 | val boolean intermediateConsistencyCheck | ||
42 | val boolean caching; | ||
43 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | ||
44 | val ExplorationStrategy strategy; | ||
45 | |||
46 | var long runtime = 0 | ||
47 | var long cachingTime = 0 | ||
48 | var int numberOfSolverCalls = 0 | ||
49 | var int numberOfCachedSolverCalls = 0 | ||
50 | |||
51 | new(ModelGenerationMethod method, ViatraReasonerConfiguration config, boolean caching) { | ||
52 | this.method = method | ||
53 | this.intermediateConsistencyCheck = config.runIntermediateNumericalConsistencyChecks | ||
54 | this.caching = caching | ||
55 | this.strategy = config.strategy | ||
56 | this.translator = new NumericTranslator(createNumericTranslator(config),config.numericSolverTimeout) | ||
57 | } | ||
58 | |||
59 | def createNumericTranslator(ViatraReasonerConfiguration config) { | ||
60 | val solverSelection = config.numericSolverSelection | ||
61 | val strategy = config.strategy | ||
62 | // if (strategy == ExplorationStrategy.None) { | ||
63 | // initialise the specified | ||
64 | if (solverSelection == NumericSolverSelection.DREAL_DOCKER) | ||
65 | return new NumericDrealProblemSolver(true, null, config.numericSolverTimeout) | ||
66 | if (solverSelection == NumericSolverSelection.DREAL_LOCAL) | ||
67 | return new NumericDrealProblemSolver(false, config.drealLocalPath, config.numericSolverTimeout) | ||
68 | if (solverSelection == NumericSolverSelection.Z3) { | ||
69 | // TODO THIS IS HARD-CODED for now | ||
70 | // val root = "/data/viatra/VIATRA-Generator"; | ||
71 | // val root = "/home/models/VIATRA-Generator"; | ||
72 | // END HARD-CODED | ||
73 | // String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | ||
74 | // System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | ||
75 | // System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | ||
76 | // System.load("libz3.so"); | ||
77 | // System.load("libz3java.so"); | ||
78 | return new NumericZ3ProblemSolver(config.numericSolverTimeout) | ||
79 | // } | ||
80 | } | ||
81 | // else { | ||
82 | // //initialise both dreal-local and z3 | ||
83 | // | ||
84 | // //TODO THIS IS HARD-CODED for now | ||
85 | //// val root = "/data/viatra/VIATRA-Generator"; | ||
86 | // val root = "/home/models/VIATRA-Generator"; | ||
87 | // //END HARD-CODED | ||
88 | //// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); | ||
89 | // System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); | ||
90 | // System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); | ||
91 | // return new NumericDynamicProblemSolver(drealLocalPath, config.drealTimeout) | ||
92 | // } | ||
93 | } | ||
94 | |||
95 | def init(ThreadContext context) { | ||
96 | // This makes the NumericSolver single-threaded, | ||
97 | // but that's not a problem, because we only use the solver on a single thread anyways. | ||
98 | this.threadContext = context | ||
99 | val engine = threadContext.queryEngine | ||
100 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { | ||
101 | val constraint = entry.key | ||
102 | val querySpec = entry.value | ||
103 | val matcher = querySpec.getMatcher(engine); | ||
104 | constraint2MustUnitPropagationPrecondition.put(constraint,matcher) | ||
105 | } | ||
106 | for(entry : method.currentUnitPropagationPreconditions.entrySet) { | ||
107 | val constraint = entry.key | ||
108 | val querySpec = entry.value | ||
109 | val matcher = querySpec.getMatcher(engine); | ||
110 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) | ||
111 | } | ||
112 | } | ||
113 | |||
114 | def getRuntime(){runtime} | ||
115 | def getCachingTime(){cachingTime} | ||
116 | def getNumberOfSolverCalls(){numberOfSolverCalls} | ||
117 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} | ||
118 | def getSolverFormingProblem(){this.translator.formingProblemTime} | ||
119 | def getSolverSolvingProblem(){this.translator.solvingProblemTime} | ||
120 | def getSolverSolution(){this.translator.formingSolutionTime} | ||
121 | def getNumericSolverSelection(){this.translator.numericSolver} | ||
122 | |||
123 | def boolean maySatisfiable() { | ||
124 | val int phase = determinePhase() | ||
125 | |||
126 | if(intermediateConsistencyCheck) { | ||
127 | return isSatisfiable(this.constraint2MustUnitPropagationPrecondition, phase) | ||
128 | } else { | ||
129 | return true | ||
130 | } | ||
131 | } | ||
132 | def boolean currentSatisfiable() { | ||
133 | val int phase = determinePhase() | ||
134 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition, phase) | ||
135 | } | ||
136 | |||
137 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches, int phase) { | ||
138 | val start = System.nanoTime | ||
139 | var boolean finalResult | ||
140 | val boolean needsFilling = needsFilling | ||
141 | val model = threadContext.getModel as PartialInterpretation | ||
142 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | ||
143 | |||
144 | if(matches.empty){ | ||
145 | finalResult=true | ||
146 | } else { | ||
147 | val propagatedConstraints = new HashMap | ||
148 | //Filter constraints if there are phase-related restricutions | ||
149 | //null whitelist means accept everything | ||
150 | |||
151 | // println("<<<<START-STEP>>>> (" + phase + ")") | ||
152 | if (phase == -2) { | ||
153 | // println("Skipping numeric check") | ||
154 | //TODO Big assumption | ||
155 | return true | ||
156 | } | ||
157 | val whitelist = getConstraintWhitelist(phase) | ||
158 | for(entry : matches.entrySet) { | ||
159 | if (entry.value !== null){ | ||
160 | val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName | ||
161 | if (whitelist === null || whitelist.contains(name)) { | ||
162 | // println(name) | ||
163 | val constraint = entry.key | ||
164 | // println("--match?-- " + constraint) | ||
165 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
166 | // println("---------- " + entry.value.allMatches) | ||
167 | propagatedConstraints.put(constraint,allMatches) | ||
168 | } | ||
169 | } | ||
170 | } | ||
171 | //check numeric problem | ||
172 | if(propagatedConstraints.values.forall[empty]) { | ||
173 | finalResult=true | ||
174 | } else { | ||
175 | if(caching) { | ||
176 | val code = getCode(propagatedConstraints) | ||
177 | val cachedResult = satisfiabilityCache.get(code) | ||
178 | if(cachedResult === null) { | ||
179 | // println('''new problem, call solver''') | ||
180 | // for(entry : code.entrySet) { | ||
181 | // println('''«entry.key» -> «entry.value»''') | ||
182 | // } | ||
183 | //println(code.hashCode) | ||
184 | this.numberOfSolverCalls++ | ||
185 | var boolean res = false | ||
186 | if (needsFilling){ | ||
187 | //TODO ASSUME Always True | ||
188 | //GET LIST OF VARS TO FILL | ||
189 | val fillMap = translator.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) | ||
190 | if (fillMap === null) res = false | ||
191 | else { | ||
192 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | ||
193 | res = true | ||
194 | } | ||
195 | } else { | ||
196 | res = translator.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) | ||
197 | } | ||
198 | //TODO FIX CACHING | ||
199 | satisfiabilityCache.put(code,res) | ||
200 | finalResult=res | ||
201 | } else { | ||
202 | //println('''similar problem, answer from cache''') | ||
203 | println('''potential issue, answer from cache''') | ||
204 | finalResult=cachedResult | ||
205 | this.numberOfCachedSolverCalls++ | ||
206 | } | ||
207 | } else { | ||
208 | if (needsFilling){ | ||
209 | //GET LIST OF VARS TO FILL | ||
210 | val fillMap = translator.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) | ||
211 | if (fillMap === null) finalResult = false | ||
212 | else { | ||
213 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | ||
214 | finalResult = true | ||
215 | } | ||
216 | } else { | ||
217 | finalResult = translator.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) | ||
218 | } | ||
219 | this.numberOfSolverCalls++ | ||
220 | } | ||
221 | } | ||
222 | } | ||
223 | this.runtime+=System.nanoTime-start | ||
224 | //STRATEGY | ||
225 | if (phase == 2) { | ||
226 | if (!finalResult) return finalResult | ||
227 | else { | ||
228 | finalResult = isSatisfiable(matches, 3) | ||
229 | } | ||
230 | } | ||
231 | return finalResult | ||
232 | } | ||
233 | |||
234 | def selectSolver(int phase) { | ||
235 | if (strategy === ExplorationStrategy.CrossingScenario){ | ||
236 | if (phase == 1) return "z3" | ||
237 | else return "dreal" | ||
238 | } | ||
239 | return "irrelevant" | ||
240 | } | ||
241 | |||
242 | def int determinePhase() { | ||
243 | // >= 0 : an actual phase | ||
244 | // -1 : take all numeric constraints | ||
245 | // -2 : SKIP (take no numeric constraints) | ||
246 | if (strategy == ExplorationStrategy.CrossingScenario) { | ||
247 | // //if has structural (non-WF) fitness issues, skip numeric handling | ||
248 | // val IObjective ob = threadContext.objectives.filter[it instanceof ModelGenerationCompositeObjective].get(0) | ||
249 | // val compo = ob as ModelGenerationCompositeObjective | ||
250 | // if (compo.getNonWFFitness(threadContext) > 0) { | ||
251 | // println("bootleg numeric-skip") | ||
252 | // return -2; | ||
253 | // } | ||
254 | |||
255 | //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors | ||
256 | val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; | ||
257 | val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation(); | ||
258 | var boolean foundBlockedBy = false; | ||
259 | |||
260 | var int numActors; | ||
261 | var int numPlacedOn; | ||
262 | var int numPlacements = 0; | ||
263 | |||
264 | for (PartialRelationInterpretation rel : relations) { | ||
265 | if(rel.getInterpretationOf().getName().equals("actors reference CrossingScenario")) { | ||
266 | numActors = rel.relationlinks.size | ||
267 | } | ||
268 | |||
269 | if(rel.getInterpretationOf().getName().equals("placedOn reference Actor")) { | ||
270 | numPlacedOn = rel.relationlinks.size | ||
271 | } | ||
272 | |||
273 | if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) { | ||
274 | for (RelationLink link : rel.getRelationlinks()) { | ||
275 | val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement; | ||
276 | if (param2.isValueSet()) { | ||
277 | numPlacements++ | ||
278 | } | ||
279 | } | ||
280 | } | ||
281 | |||
282 | if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { | ||
283 | if (!rel.getRelationlinks().isEmpty()) { | ||
284 | foundBlockedBy = true | ||
285 | } | ||
286 | } | ||
287 | } | ||
288 | val boolean unplacedActorExists = numPlacements < numActors | ||
289 | //it means that there is no blockedBy | ||
290 | //so we are at most at phase 2 | ||
291 | if (numPlacedOn == 1 && numPlacements == 0) return 1 | ||
292 | if (foundBlockedBy && unplacedActorExists) return 2 | ||
293 | if (numPlacements == numActors) return 3; | ||
294 | return -2; | ||
295 | } | ||
296 | return -1; | ||
297 | } | ||
298 | |||
299 | def getConstraintWhitelist(int phase) { | ||
300 | val List<String> wl = newArrayList | ||
301 | //null return means accept everything | ||
302 | if (strategy === ExplorationStrategy.None){ | ||
303 | return null | ||
304 | } else if (strategy === ExplorationStrategy.CrossingScenario){ | ||
305 | /* | ||
306 | "define_placedOn_actorOnVerticalLane", | ||
307 | "define_placedOn_actorOnHorizLane", | ||
308 | |||
309 | "define_actor_maxXp", | ||
310 | "define_actor_minXp", | ||
311 | "define_actor_maxYp", | ||
312 | "define_actor_minYp", | ||
313 | |||
314 | "define_actor_wrtLane", | ||
315 | |||
316 | "define_actor_minimumDistance", | ||
317 | |||
318 | "define_actor_actorOnVertLaneHasxSpeed0", | ||
319 | "define_actor_actorOnVertLaneMinYs", | ||
320 | "define_actor_actorOnVertLaneMaxYs", | ||
321 | "define_actor_actorOnHorizLaneHasySpeed0", | ||
322 | "define_actor_actorOnHorizLaneMinXs", | ||
323 | "define_actor_actorOnHorizLaneMaxXs", | ||
324 | |||
325 | "define_actor_pedestrianWidth", | ||
326 | "define_actor_pedestrianLength", | ||
327 | "define_actor_vehicleWidth", | ||
328 | "define_actor_vehicleWidth", | ||
329 | "define_actor_vehicleLength", | ||
330 | "define_actor_vehicleLength", | ||
331 | |||
332 | "collisionExists_timeWithinBound", | ||
333 | "collisionExists_timeNotNegative", | ||
334 | "collisionExists_defineCollision_y1", | ||
335 | "collisionExists_defineCollision_y2", | ||
336 | "collisionExists_defineCollision_x1", | ||
337 | "collisionExists_defineCollision_x2", | ||
338 | |||
339 | "visionBlocked_ites_notOnSameVertLine", | ||
340 | "visionBlocked_ites_top", | ||
341 | "visionBlocked_ites_bottom", | ||
342 | "visionBlocked_xdistBSlargerThanxdistTS", | ||
343 | "visionBlocked_xdistBTlargerThanxdistST", | ||
344 | "visionBlocked_ydistBSlargerThanydistTS", | ||
345 | "visionBlocked_ydistBTlargerThanydistST" | ||
346 | */ | ||
347 | |||
348 | //HINTS: | ||
349 | //define_actor_wrtLane | ||
350 | //28.5 is structural hint | ||
351 | switch (phase) { | ||
352 | case 1: { | ||
353 | wl.addAll(#[ | ||
354 | "define_placedOn_actorOnVerticalLane", | ||
355 | "define_placedOn_actorOnHorizLane", | ||
356 | |||
357 | "define_actor_maxXp", | ||
358 | "define_actor_minXp", | ||
359 | "define_actor_maxYp", | ||
360 | "define_actor_minYp", | ||
361 | |||
362 | "define_actor_pedestrianWidth", | ||
363 | "define_actor_pedestrianLength", | ||
364 | "define_actor_vehicleWidth", | ||
365 | "define_actor_vehicleWidth", | ||
366 | "define_actor_vehicleLength", | ||
367 | "define_actor_vehicleLength" | ||
368 | |||
369 | ]) | ||
370 | } | ||
371 | case 2: { | ||
372 | wl.addAll(#[ | ||
373 | |||
374 | "define_placedOn_actorOnVerticalLane", | ||
375 | "define_placedOn_actorOnHorizLane", | ||
376 | |||
377 | "define_actor_maxXp", | ||
378 | "define_actor_minXp", | ||
379 | "define_actor_maxYp", | ||
380 | "define_actor_minYp", | ||
381 | |||
382 | "define_actor_minimumDistance", | ||
383 | |||
384 | "define_actor_pedestrianWidth", | ||
385 | "define_actor_pedestrianLength", | ||
386 | "define_actor_vehicleWidth", | ||
387 | "define_actor_vehicleWidth", | ||
388 | "define_actor_vehicleLength", | ||
389 | "define_actor_vehicleLength", | ||
390 | |||
391 | "visionBlocked_ites_notOnSameVertLine", | ||
392 | "visionBlocked_ites_top", | ||
393 | "visionBlocked_ites_bottom", | ||
394 | "visionBlocked_xdistBSlargerThanxdistTS", | ||
395 | "visionBlocked_xdistBTlargerThanxdistST", | ||
396 | "visionBlocked_ydistBSlargerThanydistTS", | ||
397 | "visionBlocked_ydistBTlargerThanydistST" | ||
398 | ]) | ||
399 | } | ||
400 | case 3: { | ||
401 | wl.addAll(#[ | ||
402 | |||
403 | "define_placedOn_actorOnVerticalLane", | ||
404 | "define_placedOn_actorOnHorizLane", | ||
405 | |||
406 | "define_actor_maxXp", | ||
407 | "define_actor_minXp", | ||
408 | "define_actor_maxYp", | ||
409 | "define_actor_minYp", | ||
410 | |||
411 | "define_actor_minimumDistance", | ||
412 | |||
413 | "define_actor_actorOnVertLaneHasxSpeed0", | ||
414 | "define_actor_actorOnVertLaneMinYs", | ||
415 | "define_actor_actorOnVertLaneMaxYs", | ||
416 | "define_actor_actorOnHorizLaneHasySpeed0", | ||
417 | "define_actor_actorOnHorizLaneMinXs", | ||
418 | "define_actor_actorOnHorizLaneMaxXs", | ||
419 | |||
420 | "define_actor_pedestrianWidth", | ||
421 | "define_actor_pedestrianLength", | ||
422 | "define_actor_vehicleWidth", | ||
423 | "define_actor_vehicleWidth", | ||
424 | "define_actor_vehicleLength", | ||
425 | "define_actor_vehicleLength", | ||
426 | |||
427 | "collisionExists_timeWithinBound", | ||
428 | "collisionExists_timeNotNegative", | ||
429 | "collisionExists_defineCollision_y1", | ||
430 | "collisionExists_defineCollision_y2", | ||
431 | "collisionExists_defineCollision_x1", | ||
432 | "collisionExists_defineCollision_x2" | ||
433 | ]) | ||
434 | } | ||
435 | default: { | ||
436 | //this is for 3 if we implement 4 | ||
437 | // bl.addAll(#[0, 1, 2, 3, 4, 5, 6, 7]) | ||
438 | |||
439 | //this is for 4 if we do it | ||
440 | wl.addAll(#[]) | ||
441 | return null | ||
442 | } | ||
443 | } | ||
444 | } | ||
445 | return wl | ||
446 | } | ||
447 | |||
448 | def getNeedsFilling(){ | ||
449 | if (strategy == ExplorationStrategy.CrossingScenario) return true | ||
450 | return false | ||
451 | } | ||
452 | |||
453 | def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) { | ||
454 | val start = System.nanoTime | ||
455 | val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList | ||
456 | val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) | ||
457 | this.cachingTime += System.nanoTime-start | ||
458 | return res | ||
459 | } | ||
460 | |||
461 | def fillSolutionCopy(Map<EObject, EObject> trace) { | ||
462 | //No need to do a final check to fill if we are using a strategy | ||
463 | if (strategy === ExplorationStrategy.CrossingScenario) return | ||
464 | val model = threadContext.getModel as PartialInterpretation | ||
465 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | ||
466 | if(constraint2CurrentUnitPropagationPrecondition.empty) { | ||
467 | fillWithDefaultValues(dataObjects,trace) | ||
468 | } else { | ||
469 | val propagatedConstraints = new HashMap | ||
470 | for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { | ||
471 | val constraint = entry.key | ||
472 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
473 | propagatedConstraints.put(constraint,allMatches) | ||
474 | } | ||
475 | |||
476 | if(propagatedConstraints.values.forall[empty]) { | ||
477 | fillWithDefaultValues(dataObjects,trace) | ||
478 | } else { | ||
479 | val solution = translator.delegateGetSolution(dataObjects,propagatedConstraints, "dreal") | ||
480 | fillWithSolutions(dataObjects,solution,trace) | ||
481 | } | ||
482 | } | ||
483 | } | ||
484 | |||
485 | def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) { | ||
486 | for(element : elements) { | ||
487 | if(element.valueSet==false) { | ||
488 | val value = getDefaultValue(element) | ||
489 | val target = trace.get(element) as PrimitiveElement | ||
490 | target.fillWithValue(value) | ||
491 | } | ||
492 | } | ||
493 | } | ||
494 | |||
495 | def protected dispatch getDefaultValue(BooleanElement e) {false} | ||
496 | def protected dispatch getDefaultValue(IntegerElement e) {0} | ||
497 | def protected dispatch getDefaultValue(RealElement e) {0.0} | ||
498 | def protected dispatch getDefaultValue(StringElement e) {""} | ||
499 | |||
500 | def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) { | ||
501 | for(element : elements) { | ||
502 | if(element.valueSet==false) { | ||
503 | if(solution.containsKey(element)) { | ||
504 | val value = solution.get(element) | ||
505 | val target = trace.get(element) as PrimitiveElement | ||
506 | target.fillWithValue(value) | ||
507 | } else { | ||
508 | val target = trace.get(element) as PrimitiveElement | ||
509 | target.fillWithValue(target.defaultValue) | ||
510 | } | ||
511 | } | ||
512 | } | ||
513 | } | ||
514 | |||
515 | def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean} | ||
516 | def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} | ||
517 | def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=value as Double } | ||
518 | def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} | ||
519 | |||
520 | def protected fillWithPartialSolutionsDirectly(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution) { | ||
521 | for(element : elements) { | ||
522 | //we allow overwriting of already set variables | ||
523 | if(solution.containsKey(element)) { | ||
524 | val value = solution.get(element) | ||
525 | if (value !== null){ | ||
526 | element.fillWithValue(value) | ||
527 | } | ||
528 | } | ||
529 | } | ||
530 | } | ||
531 | } \ No newline at end of file | ||