diff options
author | 2020-05-09 20:33:19 +0200 | |
---|---|---|
committer | 2020-05-09 20:33:19 +0200 | |
commit | 3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0 (patch) | |
tree | 204cbd6fd1e7f439bc44e6210e684dbed8917e54 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner | |
parent | Merge branch 'master' of https://github.com/viatra/VIATRA-Generator (diff) | |
download | VIATRA-Generator-3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0.tar.gz VIATRA-Generator-3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0.tar.zst VIATRA-Generator-3776a7c6bc1d6fc3ebbdc9e8afb5ea99207798e0.zip |
Numeric Solver integration to exploration
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner')
4 files changed, 140 insertions, 11 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 1e623823..cb73f4e8 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 | |||
@@ -77,7 +77,7 @@ class ViatraReasoner extends LogicReasoner{ | |||
77 | scopePropagator, | 77 | scopePropagator, |
78 | viatraConfig.documentationLevel | 78 | viatraConfig.documentationLevel |
79 | ) | 79 | ) |
80 | println("parsed") | 80 | //println("parsed") |
81 | 81 | ||
82 | dse.addObjective(new ModelGenerationCompositeObjective( | 82 | dse.addObjective(new ModelGenerationCompositeObjective( |
83 | new ScopeObjective, | 83 | new ScopeObjective, |
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 60f46033..1cd61e9a 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 | |||
@@ -17,10 +17,12 @@ import java.util.Comparator; | |||
17 | import java.util.Iterator; | 17 | import java.util.Iterator; |
18 | import java.util.LinkedList; | 18 | import java.util.LinkedList; |
19 | import java.util.List; | 19 | import java.util.List; |
20 | import java.util.Map; | ||
20 | import java.util.PriorityQueue; | 21 | import java.util.PriorityQueue; |
21 | import java.util.Random; | 22 | import java.util.Random; |
22 | 23 | ||
23 | import org.apache.log4j.Logger; | 24 | import org.apache.log4j.Logger; |
25 | import org.eclipse.emf.ecore.EObject; | ||
24 | import org.eclipse.emf.ecore.util.EcoreUtil; | 26 | import org.eclipse.emf.ecore.util.EcoreUtil; |
25 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; | 27 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; |
26 | import org.eclipse.viatra.dse.base.ThreadContext; | 28 | import org.eclipse.viatra.dse.base.ThreadContext; |
@@ -38,6 +40,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | |||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; | 40 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; |
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 41 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 42 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
43 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver; | ||
41 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; | 44 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; |
42 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; | 45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; |
43 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; | 46 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; |
@@ -80,12 +83,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
80 | private volatile boolean isInterrupted = false; | 83 | private volatile boolean isInterrupted = false; |
81 | private ModelResult modelResultByInternalSolver = null; | 84 | private ModelResult modelResultByInternalSolver = null; |
82 | private Random random = new Random(); | 85 | private Random random = new Random(); |
83 | private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; | 86 | //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; |
84 | 87 | ||
85 | // Statistics | 88 | // Statistics |
86 | private int numberOfStatecoderFail = 0; | 89 | private int numberOfStatecoderFail = 0; |
87 | private int numberOfPrintedModel = 0; | 90 | private int numberOfPrintedModel = 0; |
88 | private int numberOfSolverCalls = 0; | 91 | private int numberOfSolverCalls = 0; |
92 | |||
93 | private NumericSolver numericSolver = null; | ||
89 | 94 | ||
90 | public BestFirstStrategyForModelGeneration( | 95 | public BestFirstStrategyForModelGeneration( |
91 | ReasonerWorkspace workspace, | 96 | ReasonerWorkspace workspace, |
@@ -112,14 +117,14 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
112 | this.context = context; | 117 | this.context = context; |
113 | this.solutionStore = context.getGlobalContext().getSolutionStore(); | 118 | this.solutionStore = context.getGlobalContext().getSolutionStore(); |
114 | 119 | ||
115 | ViatraQueryEngine engine = context.getQueryEngine(); | 120 | // ViatraQueryEngine engine = context.getQueryEngine(); |
116 | // // TODO: visualisation | 121 | // // TODO: visualisation |
117 | matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); | 122 | // matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); |
118 | for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) { | 123 | // for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) { |
119 | //System.out.println(p.getSimpleName()); | 124 | // //System.out.println(p.getSimpleName()); |
120 | ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine); | 125 | // ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine); |
121 | matchers.add(matcher); | 126 | // matchers.add(matcher); |
122 | } | 127 | // } |
123 | 128 | ||
124 | this.solutionStoreWithCopy = new SolutionStoreWithCopy(); | 129 | this.solutionStoreWithCopy = new SolutionStoreWithCopy(); |
125 | this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement); | 130 | this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement); |
@@ -131,6 +136,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
131 | return objectiveComparatorHelper.compare(o2.fitness, o1.fitness); | 136 | return objectiveComparatorHelper.compare(o2.fitness, o1.fitness); |
132 | } | 137 | } |
133 | }; | 138 | }; |
139 | |||
140 | this.numericSolver = new NumericSolver(context, method); | ||
134 | 141 | ||
135 | trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); | 142 | trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); |
136 | } | 143 | } |
@@ -140,6 +147,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
140 | if (!context.checkGlobalConstraints()) { | 147 | if (!context.checkGlobalConstraints()) { |
141 | 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."); |
142 | return; | 149 | return; |
150 | } else if(!numericSolver.isSatisfiable()) { | ||
151 | logger.info("Numeric contraints are not satisifed in the first state. Terminate."); | ||
152 | return; | ||
143 | } | 153 | } |
144 | if (configuration.searchSpaceConstraints.maxDepth == 0) { | 154 | if (configuration.searchSpaceConstraints.maxDepth == 0) { |
145 | logger.info("Maximal depth is reached in the initial solution. Terminate."); | 155 | logger.info("Maximal depth is reached in the initial solution. Terminate."); |
@@ -218,6 +228,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
218 | } else if (!context.checkGlobalConstraints()) { | 228 | } else if (!context.checkGlobalConstraints()) { |
219 | logger.debug("Global contraint is not satisifed."); | 229 | logger.debug("Global contraint is not satisifed."); |
220 | context.backtrack(); | 230 | context.backtrack(); |
231 | } else if (!numericSolver.isSatisfiable()) { | ||
232 | logger.debug("Numeric constraints are not satisifed."); | ||
233 | context.backtrack(); | ||
221 | } else { | 234 | } else { |
222 | final Fitness nextFitness = context.calculateFitness(); | 235 | final Fitness nextFitness = context.calculateFitness(); |
223 | checkForSolution(nextFitness); | 236 | checkForSolution(nextFitness); |
@@ -272,7 +285,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
272 | private void checkForSolution(final Fitness fittness) { | 285 | private void checkForSolution(final Fitness fittness) { |
273 | if (fittness.isSatisifiesHardObjectives()) { | 286 | if (fittness.isSatisifiesHardObjectives()) { |
274 | if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { | 287 | if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { |
275 | solutionStoreWithCopy.newSolution(context); | 288 | Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context); |
289 | numericSolver.fillSolutionCopy(trace); | ||
276 | solutionStoreWithDiversityDescriptor.newSolution(context); | 290 | solutionStoreWithDiversityDescriptor.newSolution(context); |
277 | solutionStore.newSolution(context); | 291 | solutionStore.newSolution(context); |
278 | configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); | 292 | configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); |
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 new file mode 100644 index 00000000..b72bdb44 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | |||
@@ -0,0 +1,114 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
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 | ||
11 | import org.eclipse.viatra.dse.base.ThreadContext | ||
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 | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | ||
20 | import java.util.List | ||
21 | import java.math.BigDecimal | ||
22 | |||
23 | class NumericSolver { | ||
24 | val ThreadContext threadContext; | ||
25 | val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | ||
26 | NumericTranslator t = new NumericTranslator | ||
27 | |||
28 | new(ThreadContext threadContext, ModelGenerationMethod method) { | ||
29 | this.threadContext = threadContext | ||
30 | val engine = threadContext.queryEngine | ||
31 | for(entry : method.unitPropagationPreconditions.entrySet) { | ||
32 | val constraint = entry.key | ||
33 | val querySpec = entry.value | ||
34 | val matcher = querySpec.getMatcher(engine); | ||
35 | constraint2UnitPropagationPrecondition.put(constraint,matcher) | ||
36 | } | ||
37 | } | ||
38 | |||
39 | def boolean isSatisfiable() { | ||
40 | if(constraint2UnitPropagationPrecondition.empty) return true | ||
41 | else { | ||
42 | val propagatedConstraints = new HashMap | ||
43 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { | ||
44 | val constraint = entry.key | ||
45 | //println(constraint) | ||
46 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
47 | //println(allMatches.toList) | ||
48 | propagatedConstraints.put(constraint,allMatches) | ||
49 | } | ||
50 | |||
51 | if(propagatedConstraints.values.forall[empty]) { | ||
52 | return true | ||
53 | } else { | ||
54 | val res = t.delegateIsSatisfiable(propagatedConstraints) | ||
55 | //println(res) | ||
56 | return res | ||
57 | } | ||
58 | } | ||
59 | } | ||
60 | |||
61 | def fillSolutionCopy(Map<EObject, EObject> trace) { | ||
62 | val model = threadContext.getModel as PartialInterpretation | ||
63 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | ||
64 | if(constraint2UnitPropagationPrecondition.empty) { | ||
65 | fillWithDefaultValues(dataObjects,trace) | ||
66 | } else { | ||
67 | val propagatedConstraints = new HashMap | ||
68 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { | ||
69 | val constraint = entry.key | ||
70 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
71 | propagatedConstraints.put(constraint,allMatches) | ||
72 | } | ||
73 | |||
74 | if(propagatedConstraints.values.forall[empty]) { | ||
75 | fillWithDefaultValues(dataObjects,trace) | ||
76 | } else { | ||
77 | val solution = t.delegateGetSolution(dataObjects,propagatedConstraints) | ||
78 | fillWithSolutions(dataObjects,solution,trace) | ||
79 | } | ||
80 | } | ||
81 | } | ||
82 | |||
83 | def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) { | ||
84 | for(element : elements) { | ||
85 | if(element.valueSet==false) { | ||
86 | val value = getDefaultValue(element) | ||
87 | val target = trace.get(element) as PrimitiveElement | ||
88 | target.fillWithValue(value) | ||
89 | } | ||
90 | } | ||
91 | } | ||
92 | |||
93 | def protected dispatch getDefaultValue(BooleanElement e) {false} | ||
94 | def protected dispatch getDefaultValue(IntegerElement e) {0} | ||
95 | def protected dispatch getDefaultValue(RealElement e) {0.0} | ||
96 | def protected dispatch getDefaultValue(StringElement e) {""} | ||
97 | |||
98 | def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Integer> solution, Map<EObject, EObject> trace) { | ||
99 | for(element : elements) { | ||
100 | if(element.valueSet==false) { | ||
101 | if(solution.containsKey(element)) { | ||
102 | val value = solution.get(element) | ||
103 | val target = trace.get(element) as PrimitiveElement | ||
104 | target.fillWithValue(value) | ||
105 | } | ||
106 | } | ||
107 | } | ||
108 | } | ||
109 | |||
110 | def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean} | ||
111 | def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} | ||
112 | def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=BigDecimal.valueOf(value as Double) } | ||
113 | def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} | ||
114 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend index a8b7301e..21867a4e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend | |||
@@ -25,7 +25,7 @@ class SolutionStoreWithCopy { | |||
25 | newSolution(context) | 25 | newSolution(context) |
26 | }*/ | 26 | }*/ |
27 | 27 | ||
28 | def newSolution(ThreadContext context) { | 28 | def Map<EObject,EObject> newSolution(ThreadContext context) { |
29 | //print(System.nanoTime-initTime + ";") | 29 | //print(System.nanoTime-initTime + ";") |
30 | val copyStart = System.nanoTime | 30 | val copyStart = System.nanoTime |
31 | val solution = context.model as PartialInterpretation | 31 | val solution = context.model as PartialInterpretation |
@@ -36,6 +36,7 @@ class SolutionStoreWithCopy { | |||
36 | copyTraces.add(copier) | 36 | copyTraces.add(copier) |
37 | runtime += System.nanoTime - copyStart | 37 | runtime += System.nanoTime - copyStart |
38 | solutionTimes.add(System.nanoTime-sartTime) | 38 | solutionTimes.add(System.nanoTime-sartTime) |
39 | return copier | ||
39 | } | 40 | } |
40 | def getSumRuntime() { | 41 | def getSumRuntime() { |
41 | return runtime | 42 | return runtime |