diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse')
3 files changed, 46 insertions, 32 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index 18fe94e4..45dffe7c 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java | |||
@@ -147,7 +147,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
147 | if (!context.checkGlobalConstraints()) { | 147 | if (!context.checkGlobalConstraints()) { |
148 | logger.info("Global contraint is not satisifed in the first state. Terminate."); | 148 | logger.info("Global contraint is not satisifed in the first state. Terminate."); |
149 | return; | 149 | return; |
150 | } else if(!numericSolver.isSatisfiable()) { | 150 | } else if(!numericSolver.maySatisfiable()) { |
151 | logger.info("Numeric contraints are not satisifed in the first state. Terminate."); | 151 | logger.info("Numeric contraints are not satisifed in the first state. Terminate."); |
152 | return; | 152 | return; |
153 | } | 153 | } |
@@ -228,7 +228,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
228 | } else if (!context.checkGlobalConstraints()) { | 228 | } else if (!context.checkGlobalConstraints()) { |
229 | logger.debug("Global contraint is not satisifed."); | 229 | logger.debug("Global contraint is not satisifed."); |
230 | context.backtrack(); | 230 | context.backtrack(); |
231 | } else if (!numericSolver.isSatisfiable()) { | 231 | } else if (!numericSolver.maySatisfiable()) { |
232 | logger.debug("Numeric constraints are not satisifed."); | 232 | logger.debug("Numeric constraints are not satisifed."); |
233 | context.backtrack(); | 233 | context.backtrack(); |
234 | } else { | 234 | } else { |
@@ -284,13 +284,15 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
284 | private void checkForSolution(final Fitness fittness) { | 284 | private void checkForSolution(final Fitness fittness) { |
285 | if (fittness.isSatisifiesHardObjectives()) { | 285 | if (fittness.isSatisifiesHardObjectives()) { |
286 | if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { | 286 | if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { |
287 | Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context); | 287 | if(numericSolver.currentSatisfiable()) { |
288 | numericSolver.fillSolutionCopy(trace); | 288 | Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context); |
289 | solutionStoreWithDiversityDescriptor.newSolution(context); | 289 | numericSolver.fillSolutionCopy(trace); |
290 | solutionStore.newSolution(context); | 290 | solutionStoreWithDiversityDescriptor.newSolution(context); |
291 | configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); | 291 | solutionStore.newSolution(context); |
292 | configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); | ||
292 | 293 | ||
293 | logger.debug("Found a solution."); | 294 | logger.debug("Found a solution."); |
295 | } | ||
294 | } | 296 | } |
295 | } | 297 | } |
296 | } | 298 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend index a75ddf76..9e4792e0 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend | |||
@@ -62,7 +62,7 @@ class ModelGenerationCompositeObjective implements IObjective{ | |||
62 | } | 62 | } |
63 | var sum = 0.0 | 63 | var sum = 0.0 |
64 | sum += scopeFitnes | 64 | sum += scopeFitnes |
65 | sum +=Math.sqrt(multiplicity *0.1) | 65 | sum +=multiplicity |
66 | sum += unfinishedWFsFitness//*0.5 | 66 | sum += unfinishedWFsFitness//*0.5 |
67 | 67 | ||
68 | println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') | 68 | println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') |
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 71793aa6..fe378bd3 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 | |||
@@ -1,30 +1,29 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
5 | import java.util.HashMap | ||
6 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
7 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
9 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
10 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | 3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator |
11 | import org.eclipse.viatra.dse.base.ThreadContext | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod |
12 | import org.eclipse.emf.ecore.EObject | ||
13 | import java.util.Map | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement |
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
20 | import java.util.List | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement |
21 | import java.math.BigDecimal | 11 | import java.math.BigDecimal |
22 | import java.util.LinkedHashSet | 12 | import java.util.HashMap |
23 | import java.util.LinkedHashMap | 13 | import java.util.LinkedHashMap |
14 | import java.util.LinkedHashSet | ||
15 | import java.util.List | ||
16 | import java.util.Map | ||
17 | import org.eclipse.emf.ecore.EObject | ||
18 | import org.eclipse.viatra.dse.base.ThreadContext | ||
19 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
20 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
24 | 22 | ||
25 | class NumericSolver { | 23 | class NumericSolver { |
26 | val ThreadContext threadContext; | 24 | val ThreadContext threadContext; |
27 | val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 25 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
26 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | ||
28 | NumericTranslator t = new NumericTranslator | 27 | NumericTranslator t = new NumericTranslator |
29 | 28 | ||
30 | val boolean caching; | 29 | val boolean caching; |
@@ -38,11 +37,17 @@ class NumericSolver { | |||
38 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { | 37 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { |
39 | this.threadContext = threadContext | 38 | this.threadContext = threadContext |
40 | val engine = threadContext.queryEngine | 39 | val engine = threadContext.queryEngine |
41 | for(entry : method.unitPropagationPreconditions.entrySet) { | 40 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { |
41 | val constraint = entry.key | ||
42 | val querySpec = entry.value | ||
43 | val matcher = querySpec.getMatcher(engine); | ||
44 | constraint2MustUnitPropagationPrecondition.put(constraint,matcher) | ||
45 | } | ||
46 | for(entry : method.currentUnitPropagationPreconditions.entrySet) { | ||
42 | val constraint = entry.key | 47 | val constraint = entry.key |
43 | val querySpec = entry.value | 48 | val querySpec = entry.value |
44 | val matcher = querySpec.getMatcher(engine); | 49 | val matcher = querySpec.getMatcher(engine); |
45 | constraint2UnitPropagationPrecondition.put(constraint,matcher) | 50 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) |
46 | } | 51 | } |
47 | this.caching = caching | 52 | this.caching = caching |
48 | } | 53 | } |
@@ -52,14 +57,21 @@ class NumericSolver { | |||
52 | def getNumberOfSolverCalls(){numberOfSolverCalls} | 57 | def getNumberOfSolverCalls(){numberOfSolverCalls} |
53 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} | 58 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} |
54 | 59 | ||
55 | def boolean isSatisfiable() { | 60 | def boolean maySatisfiable() { |
61 | isSatisfiable(this.constraint2MustUnitPropagationPrecondition) | ||
62 | } | ||
63 | def boolean currentSatisfiable() { | ||
64 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition) | ||
65 | } | ||
66 | |||
67 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { | ||
56 | val start = System.nanoTime | 68 | val start = System.nanoTime |
57 | var boolean finalResult | 69 | var boolean finalResult |
58 | if(constraint2UnitPropagationPrecondition.empty){ | 70 | if(matches.empty){ |
59 | finalResult=true | 71 | finalResult=true |
60 | } else { | 72 | } else { |
61 | val propagatedConstraints = new HashMap | 73 | val propagatedConstraints = new HashMap |
62 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { | 74 | for(entry : matches.entrySet) { |
63 | val constraint = entry.key | 75 | val constraint = entry.key |
64 | //println(constraint) | 76 | //println(constraint) |
65 | val allMatches = entry.value.allMatches.map[it.toArray] | 77 | val allMatches = entry.value.allMatches.map[it.toArray] |
@@ -108,11 +120,11 @@ class NumericSolver { | |||
108 | def fillSolutionCopy(Map<EObject, EObject> trace) { | 120 | def fillSolutionCopy(Map<EObject, EObject> trace) { |
109 | val model = threadContext.getModel as PartialInterpretation | 121 | val model = threadContext.getModel as PartialInterpretation |
110 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | 122 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList |
111 | if(constraint2UnitPropagationPrecondition.empty) { | 123 | if(constraint2CurrentUnitPropagationPrecondition.empty) { |
112 | fillWithDefaultValues(dataObjects,trace) | 124 | fillWithDefaultValues(dataObjects,trace) |
113 | } else { | 125 | } else { |
114 | val propagatedConstraints = new HashMap | 126 | val propagatedConstraints = new HashMap |
115 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { | 127 | for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { |
116 | val constraint = entry.key | 128 | val constraint = entry.key |
117 | val allMatches = entry.value.allMatches.map[it.toArray] | 129 | val allMatches = entry.value.allMatches.map[it.toArray] |
118 | propagatedConstraints.put(constraint,allMatches) | 130 | propagatedConstraints.put(constraint,allMatches) |