diff options
author | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-02-14 10:34:21 +0100 |
---|---|---|
committer | Aren Babikian <aren.babikian@mail.mcgill.ca> | 2021-02-14 10:34:21 +0100 |
commit | 803429243a248aef91bc8696c0da5924278e1cb6 (patch) | |
tree | 203e8eda42f6b96a45aca2ab5d623b2793b7b2e8 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner | |
parent | Add strategy flag + implement alost working crossingScenarioStrategy (diff) | |
download | VIATRA-Generator-803429243a248aef91bc8696c0da5924278e1cb6.tar.gz VIATRA-Generator-803429243a248aef91bc8696c0da5924278e1cb6.tar.zst VIATRA-Generator-803429243a248aef91bc8696c0da5924278e1cb6.zip |
finished first impl that works sometimes (issue w/ SAT in Dreal rerun)
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner')
2 files changed, 42 insertions, 13 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index ed04ae4a..5ad78506 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | |||
@@ -156,6 +156,7 @@ class ViatraReasoner extends LogicReasoner { | |||
156 | val transformationTime = transformationFinished - transformationStartTime | 156 | val transformationTime = transformationFinished - transformationStartTime |
157 | val solverStartTime = System.nanoTime | 157 | val solverStartTime = System.nanoTime |
158 | 158 | ||
159 | println(">>begin exploration") | ||
159 | var boolean stoppedByTimeout | 160 | var boolean stoppedByTimeout |
160 | try { | 161 | try { |
161 | stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000); | 162 | stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000); |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index b8fcb6a0..bb2c7dbf 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | |||
@@ -148,8 +148,14 @@ class NumericSolver { | |||
148 | val propagatedConstraints = new HashMap | 148 | val propagatedConstraints = new HashMap |
149 | //Filter constraints if there are phase-related restricutions | 149 | //Filter constraints if there are phase-related restricutions |
150 | //null whitelist means accept everything | 150 | //null whitelist means accept everything |
151 | val whitelist = getConstraintWhitelist(phase) | 151 | |
152 | println("<<<<START-STEP>>>> (" + phase + ")") | 152 | println("<<<<START-STEP>>>> (" + phase + ")") |
153 | if (phase == -2) { | ||
154 | println("Skipping numeric check") | ||
155 | //TODO Big assumption | ||
156 | return true | ||
157 | } | ||
158 | val whitelist = getConstraintWhitelist(phase) | ||
153 | for(entry : matches.entrySet) { | 159 | for(entry : matches.entrySet) { |
154 | if (entry.value !== null){ | 160 | if (entry.value !== null){ |
155 | val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName | 161 | val name = (entry.key as ExpressionEvaluation).body.pattern.simpleName |
@@ -182,8 +188,11 @@ class NumericSolver { | |||
182 | //TODO ASSUME Always True | 188 | //TODO ASSUME Always True |
183 | //GET LIST OF VARS TO FILL | 189 | //GET LIST OF VARS TO FILL |
184 | val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) | 190 | val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) |
185 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | 191 | if (fillMap === null) res = false |
186 | res = true | 192 | else { |
193 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | ||
194 | res = true | ||
195 | } | ||
187 | } else { | 196 | } else { |
188 | res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) | 197 | res = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) |
189 | } | 198 | } |
@@ -201,8 +210,11 @@ class NumericSolver { | |||
201 | //TODO ASSUME Always True | 210 | //TODO ASSUME Always True |
202 | //GET LIST OF VARS TO FILL | 211 | //GET LIST OF VARS TO FILL |
203 | val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) | 212 | val fillMap = t.delegateGetSolution(dataObjects, propagatedConstraints, selectSolver(phase)) |
204 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | 213 | if (fillMap === null) finalResult = false |
205 | finalResult = true | 214 | else { |
215 | fillWithPartialSolutionsDirectly(dataObjects, fillMap) | ||
216 | finalResult = true | ||
217 | } | ||
206 | } else { | 218 | } else { |
207 | finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) | 219 | finalResult = t.delegateIsSatisfiable(propagatedConstraints, selectSolver(phase)) |
208 | } | 220 | } |
@@ -211,6 +223,7 @@ class NumericSolver { | |||
211 | } | 223 | } |
212 | } | 224 | } |
213 | this.runtime+=System.nanoTime-start | 225 | this.runtime+=System.nanoTime-start |
226 | if (phase == 2) finalResult = isSatisfiable(matches, 3) | ||
214 | return finalResult | 227 | return finalResult |
215 | } | 228 | } |
216 | 229 | ||
@@ -230,27 +243,43 @@ class NumericSolver { | |||
230 | //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors | 243 | //assumikng standard input, w/ visinBlocked and CollisionExists between pre-included actors |
231 | val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; | 244 | val PartialInterpretation head = threadContext.getModel() as PartialInterpretation; |
232 | val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation(); | 245 | val List<PartialRelationInterpretation> relations = head.getPartialrelationinterpretation(); |
233 | var boolean foundActorWithDefinedPos = false; | 246 | var boolean foundBlockedBy = false; |
247 | |||
248 | var int numActors; | ||
249 | var int numPlacedOn; | ||
250 | var int numPlacements = 0; | ||
251 | |||
234 | for (PartialRelationInterpretation rel : relations) { | 252 | for (PartialRelationInterpretation rel : relations) { |
253 | if(rel.getInterpretationOf().getName().equals("actors reference CrossingScenario")) { | ||
254 | numActors = rel.relationlinks.size | ||
255 | } | ||
256 | |||
257 | if(rel.getInterpretationOf().getName().equals("placedOn reference Actor")) { | ||
258 | numPlacedOn = rel.relationlinks.size | ||
259 | } | ||
260 | |||
235 | if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) { | 261 | if(rel.getInterpretationOf().getName().equals("xPos attribute Actor")) { |
236 | for (RelationLink link : rel.getRelationlinks()) { | 262 | for (RelationLink link : rel.getRelationlinks()) { |
237 | val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement; | 263 | val PrimitiveElement param2 = (link as BinaryElementRelationLink).getParam2() as PrimitiveElement; |
238 | if (param2.isValueSet()) { | 264 | if (param2.isValueSet()) { |
239 | foundActorWithDefinedPos = true; | 265 | numPlacements++ |
240 | } | 266 | } |
241 | } | 267 | } |
242 | } | 268 | } |
243 | 269 | ||
244 | if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { | 270 | if(rel.getInterpretationOf().getName().equals("blockedBy reference VisionBlocked")) { |
245 | if (!rel.getRelationlinks().isEmpty()) { | 271 | if (!rel.getRelationlinks().isEmpty()) { |
246 | return 3; | 272 | foundBlockedBy = true |
247 | } | 273 | } |
248 | } | 274 | } |
249 | } | 275 | } |
276 | val boolean unplacedActorExists = numPlacements < numActors | ||
250 | //it means that there is no blockedBy | 277 | //it means that there is no blockedBy |
251 | //so we are at most at phase 2 | 278 | //so we are at most at phase 2 |
252 | if (foundActorWithDefinedPos) return 2; | 279 | if (numPlacedOn == 1 && numPlacements == 0) return 1 |
253 | return 1; | 280 | if (foundBlockedBy && unplacedActorExists) return 2 |
281 | if (numPlacements == numActors) return 3; | ||
282 | return -2; | ||
254 | } | 283 | } |
255 | return -1; | 284 | return -1; |
256 | } | 285 | } |
@@ -418,6 +447,8 @@ class NumericSolver { | |||
418 | } | 447 | } |
419 | 448 | ||
420 | def fillSolutionCopy(Map<EObject, EObject> trace) { | 449 | def fillSolutionCopy(Map<EObject, EObject> trace) { |
450 | //No need to do a final check to fill if we are using a strategy | ||
451 | if (strategy === ExplorationStrategy.CrossingScenario) return | ||
421 | val model = threadContext.getModel as PartialInterpretation | 452 | val model = threadContext.getModel as PartialInterpretation |
422 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | 453 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList |
423 | if(constraint2CurrentUnitPropagationPrecondition.empty) { | 454 | if(constraint2CurrentUnitPropagationPrecondition.empty) { |
@@ -481,9 +512,6 @@ class NumericSolver { | |||
481 | val value = solution.get(element) | 512 | val value = solution.get(element) |
482 | if (value !== null){ | 513 | if (value !== null){ |
483 | element.fillWithValue(value) | 514 | element.fillWithValue(value) |
484 | println("<" + element + "> is filled") | ||
485 | } else { | ||
486 | println("<" + element + "> is unfilled") | ||
487 | } | 515 | } |
488 | } | 516 | } |
489 | } | 517 | } |