aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend103
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java131
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend184
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend66
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend25
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend24
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend90
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend17
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend6
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend86
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend6
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend120
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend27
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend15
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend54
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend150
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend43
18 files changed, 850 insertions, 299 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend
new file mode 100644
index 00000000..67f447ed
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend
@@ -0,0 +1,103 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import com.google.common.collect.ImmutableList
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
6import java.util.Comparator
7import java.util.List
8import org.eclipse.viatra.dse.base.ThreadContext
9import org.eclipse.viatra.dse.objectives.Comparators
10import org.eclipse.viatra.dse.objectives.IGlobalConstraint
11import org.eclipse.viatra.dse.objectives.IObjective
12import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
13
14class BasicScopeGlobalConstraint implements IGlobalConstraint, IObjective {
15 val PartialInterpretation p
16 val List<ScopeAssertion> assertions
17
18 new(PartialInterpretation p) {
19 this.p = p
20 assertions = ImmutableList.copyOf(p.scopes.map [
21 val currentSize = targetTypeInterpretation.elements.size
22 val minElements = minNewElements + currentSize
23 val maxElements = if (maxNewElements < 0) {
24 -1
25 } else {
26 maxNewElements + currentSize
27 }
28 new ScopeAssertion(minElements, maxElements, targetTypeInterpretation)
29 ])
30 }
31
32 override init(ThreadContext context) {
33 if (context.model != p) {
34 throw new IllegalArgumentException(
35 "Partial model must be passed to the constructor of BasicScopeGlobalConstraint")
36 }
37 }
38
39 override checkGlobalConstraint(ThreadContext context) {
40 assertions.forall[upperBoundSatisfied]
41 }
42
43 override getFitness(ThreadContext context) {
44 var double fitness = p.minNewElements
45 for (assertion : assertions) {
46 if (!assertion.lowerBoundSatisfied) {
47 fitness += 1
48 }
49 }
50 fitness
51 }
52
53 override satisifiesHardObjective(Double fitness) {
54 fitness <= 0.01
55 }
56
57 override BasicScopeGlobalConstraint createNew() {
58 this
59 }
60
61 override getName() {
62 class.name
63 }
64
65 override getComparator() {
66 Comparators.LOWER_IS_BETTER
67 }
68
69 override getLevel() {
70 2
71 }
72
73 override isHardObjective() {
74 true
75 }
76
77 override setComparator(Comparator<Double> comparator) {
78 throw new UnsupportedOperationException
79 }
80
81 override setLevel(int level) {
82 throw new UnsupportedOperationException
83 }
84
85 @FinalFieldsConstructor
86 private static class ScopeAssertion {
87 val int lowerBound
88 val int upperBound
89 val PartialTypeInterpratation typeDefinitions
90
91 private def getCount() {
92 typeDefinitions.elements.size
93 }
94
95 private def isLowerBoundSatisfied() {
96 count >= lowerBound
97 }
98
99 private def isUpperBoundSatisfied() {
100 upperBound < 0 || count <= upperBound
101 }
102 }
103}
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 e3603af3..e529892c 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
@@ -9,34 +9,25 @@
9 *******************************************************************************/ 9 *******************************************************************************/
10package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse; 10package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse;
11 11
12import java.io.BufferedReader;
13import java.io.IOException;
14import java.io.InputStreamReader;
15import java.util.ArrayList;
16import java.util.Arrays; 12import java.util.Arrays;
17import java.util.Collection;
18import java.util.Collections; 13import java.util.Collections;
19import java.util.Comparator; 14import java.util.Comparator;
20import java.util.Iterator; 15import java.util.Iterator;
21import java.util.LinkedList; 16import java.util.LinkedList;
22import java.util.List; 17import java.util.List;
23import java.util.Map;
24import java.util.PriorityQueue; 18import java.util.PriorityQueue;
25import java.util.Random; 19import java.util.Random;
26 20
27import org.apache.log4j.Logger; 21import org.apache.log4j.Logger;
28import org.eclipse.emf.ecore.EObject; 22import org.eclipse.emf.ecore.EObject;
29import org.eclipse.emf.ecore.util.EcoreUtil; 23import org.eclipse.emf.ecore.util.EcoreUtil;
24import org.eclipse.viatra.dse.api.SolutionTrajectory;
30import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; 25import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;
31import org.eclipse.viatra.dse.base.ThreadContext; 26import org.eclipse.viatra.dse.base.ThreadContext;
32import org.eclipse.viatra.dse.objectives.Fitness; 27import org.eclipse.viatra.dse.objectives.Fitness;
33import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; 28import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper;
29import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler;
34import org.eclipse.viatra.dse.solutionstore.SolutionStore; 30import org.eclipse.viatra.dse.solutionstore.SolutionStore;
35import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine;
36import org.eclipse.viatra.query.runtime.api.IPatternMatch;
37import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
38import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;
39import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher;
40 31
41import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; 32import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
42import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; 33import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
@@ -44,7 +35,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
44import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; 35import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult;
45import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; 36import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
46import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; 37import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
47import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver;
48import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; 38import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod;
49import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; 39import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
50import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; 40import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
@@ -83,14 +73,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
83 // Running 73 // Running
84 private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore; 74 private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore;
85 private SolutionStore solutionStore; 75 private SolutionStore solutionStore;
86 private SolutionStoreWithCopy solutionStoreWithCopy;
87 private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor;
88 private volatile boolean isInterrupted = false; 76 private volatile boolean isInterrupted = false;
89 private ModelResult modelResultByInternalSolver = null; 77 private ModelResult modelResultByInternalSolver = null;
90 private Random random = new Random(); 78 private Random random = new Random();
91 //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; 79 //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers;
92 public ActivationSelector activationSelector = new EvenActivationSelector(random); 80 public ActivationSelector activationSelector = new EvenActivationSelector(random);
93 public NumericSolver numericSolver = null; 81 public ViatraReasonerSolutionSaver solutionSaver;
82 public NumericSolver numericSolver;
94 // Statistics 83 // Statistics
95 private int numberOfStatecoderFail = 0; 84 private int numberOfStatecoderFail = 0;
96 private int numberOfPrintedModel = 0; 85 private int numberOfPrintedModel = 0;
@@ -103,19 +92,17 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
103 public BestFirstStrategyForModelGeneration( 92 public BestFirstStrategyForModelGeneration(
104 ReasonerWorkspace workspace, 93 ReasonerWorkspace workspace,
105 ViatraReasonerConfiguration configuration, 94 ViatraReasonerConfiguration configuration,
106 ModelGenerationMethod method) 95 ModelGenerationMethod method,
107 { 96 ViatraReasonerSolutionSaver solutionSaver,
97 NumericSolver numericSolver) {
108 this.workspace = workspace; 98 this.workspace = workspace;
109 this.configuration = configuration; 99 this.configuration = configuration;
110 this.method = method; 100 this.method = method;
101 this.solutionSaver = solutionSaver;
102 this.numericSolver = numericSolver;
103 //logger.setLevel(Level.DEBUG);
111 } 104 }
112 105
113 public SolutionStoreWithCopy getSolutionStoreWithCopy() {
114 return solutionStoreWithCopy;
115 }
116 public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
117 return solutionStoreWithDiversityDescriptor;
118 }
119 public int getNumberOfStatecoderFail() { 106 public int getNumberOfStatecoderFail() {
120 return numberOfStatecoderFail; 107 return numberOfStatecoderFail;
121 } 108 }
@@ -125,22 +112,35 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
125 public long getBacktrackingTime() { 112 public long getBacktrackingTime() {
126 return context.getDesignSpaceManager().getBacktrackingTime(); 113 return context.getDesignSpaceManager().getBacktrackingTime();
127 } 114 }
128 //LinkedList<ViatraQueryMatcher<? extends IPatternMatch>> matchers; 115
129 @Override 116 @Override
130 public void initStrategy(ThreadContext context) { 117 public void initStrategy(ThreadContext context) {
131 this.context = context; 118 this.context = context;
132 this.solutionStore = context.getGlobalContext().getSolutionStore(); 119 this.solutionStore = context.getGlobalContext().getSolutionStore();
120 solutionStore.registerSolutionFoundHandler(new ISolutionFoundHandler() {
121
122 @Override
123 public void solutionTriedToSave(ThreadContext context, SolutionTrajectory trajectory) {
124 // Ignore.
125 }
126
127 @Override
128 public void solutionFound(ThreadContext context, SolutionTrajectory trajectory) {
129 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions);
130 saveTimes();
131 logger.debug("Found a solution.");
132 }
133 });
134 numericSolver.init(context);
133 135
134// ViatraQueryEngine engine = context.getQueryEngine(); 136// ViatraQueryEngine engine = context.getQueryEngine();
135// // TODO: visualisation
136// matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); 137// matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>();
137// for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) { 138// for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) {
138// //System.out.println(p.getSimpleName()); 139// //System.out.println(p.getSimpleName());
139// ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine); 140// ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine);
140// matchers.add(matcher); 141// matchers.add(matcher);
141// } 142// }
142 this.solutionStoreWithCopy = new SolutionStoreWithCopy(); 143
143 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
144 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); 144 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
145 this.comparator = new Comparator<TrajectoryWithFitness>() { 145 this.comparator = new Comparator<TrajectoryWithFitness>() {
146 @Override 146 @Override
@@ -148,8 +148,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
148 return objectiveComparatorHelper.compare(o2.fitness, o1.fitness); 148 return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);
149 } 149 }
150 }; 150 };
151
152 this.numericSolver = new NumericSolver(context, method, this.configuration.runIntermediateNumericalConsistencyChecks, false);
153 151
154 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); 152 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);
155 } 153 }
@@ -176,14 +174,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
176 return; 174 return;
177 } 175 }
178 176
179 final Fitness firstFittness = calculateFitness(); 177 final Fitness firstFitness = calculateFitness();
180 checkForSolution(firstFittness); 178 checkForSolution(firstFitness);
181 179
182 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); 180 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
183 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); 181 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
184 TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness); 182 TrajectoryWithFitness currentTrajectoryWithFitness = new TrajectoryWithFitness(firstTrajectory, firstFitness);
185 trajectoiresToExplore.add(currentTrajectoryWithFittness); 183 trajectoiresToExplore.add(currentTrajectoryWithFitness);
186
187 //if(configuration) 184 //if(configuration)
188 visualiseCurrentState(); 185 visualiseCurrentState();
189// for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { 186// for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
@@ -197,22 +194,22 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
197 194
198 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) { 195 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) {
199 196
200 if (currentTrajectoryWithFittness == null) { 197 if (currentTrajectoryWithFitness == null) {
201 if (trajectoiresToExplore.isEmpty()) { 198 if (trajectoiresToExplore.isEmpty()) {
202 logger.debug("State space is fully traversed."); 199 logger.debug("State space is fully traversed.");
203 return; 200 return;
204 } else { 201 } else {
205 currentTrajectoryWithFittness = selectState(); 202 currentTrajectoryWithFitness = selectState();
206 if (logger.isDebugEnabled()) { 203 if (logger.isDebugEnabled()) {
207 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); 204 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
208 logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness); 205 logger.debug("New trajectory is chosen: " + currentTrajectoryWithFitness);
209 } 206 }
210 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory); 207 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFitness.trajectory);
211 } 208 }
212 } 209 }
213 210
214// visualiseCurrentState(); 211// visualiseCurrentState();
215// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); 212// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
216// if(consistencyCheckResult == true) { 213// if(consistencyCheckResult == true) {
217// continue mainLoop; 214// continue mainLoop;
218// } 215// }
@@ -224,10 +221,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
224 final Object nextActivation = iterator.next(); 221 final Object nextActivation = iterator.next();
225// if (!iterator.hasNext()) { 222// if (!iterator.hasNext()) {
226// logger.debug("Last untraversed activation of the state."); 223// logger.debug("Last untraversed activation of the state.");
227// trajectoiresToExplore.remove(currentTrajectoryWithFittness); 224// trajectoiresToExplore.remove(currentTrajectoryWithfitness);
228// } 225// }
229 logger.debug("Executing new activation: " + nextActivation); 226 logger.debug("Executing new activation: " + nextActivation);
230 context.executeAcitvationId(nextActivation); 227 context.executeAcitvationId(nextActivation);
228 method.getStatistics().incrementDecisionCount();
231 229
232 visualiseCurrentState(); 230 visualiseCurrentState();
233// for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { 231// for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) {
@@ -238,7 +236,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
238// 236//
239// } 237// }
240 238
241 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); 239 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness);
242 if(consistencyCheckResult == true) { continue mainLoop; } 240 if(consistencyCheckResult == true) { continue mainLoop; }
243 241
244 if (context.isCurrentStateAlreadyTraversed()) { 242 if (context.isCurrentStateAlreadyTraversed()) {
@@ -251,7 +249,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
251 logger.debug("Numeric constraints are not satisifed."); 249 logger.debug("Numeric constraints are not satisifed.");
252 context.backtrack(); 250 context.backtrack();
253 } else { 251 } else {
254 final Fitness nextFitness = calculateFitness(); 252 final Fitness nextFitness = context.calculateFitness();
255 checkForSolution(nextFitness); 253 checkForSolution(nextFitness);
256 if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) { 254 if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) {
257 logger.debug("Reached max depth."); 255 logger.debug("Reached max depth.");
@@ -259,31 +257,31 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
259 continue; 257 continue;
260 } 258 }
261 259
262 TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness( 260 TrajectoryWithFitness nextTrajectoryWithfitness = new TrajectoryWithFitness(
263 context.getTrajectory().toArray(), nextFitness); 261 context.getTrajectory().toArray(), nextFitness);
264 trajectoiresToExplore.add(nextTrajectoryWithFittness); 262 trajectoiresToExplore.add(nextTrajectoryWithfitness);
265 263
266 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness, 264 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFitness.fitness,
267 nextTrajectoryWithFittness.fitness); 265 nextTrajectoryWithfitness.fitness);
268 if (compare < 0) { 266 if (compare < 0) {
269 logger.debug("Better fitness, moving on: " + nextFitness); 267 logger.debug("Better fitness, moving on: " + nextFitness);
270 currentTrajectoryWithFittness = nextTrajectoryWithFittness; 268 currentTrajectoryWithFitness = nextTrajectoryWithfitness;
271 continue mainLoop; 269 continue mainLoop;
272 } else if (compare == 0) { 270 } else if (compare == 0) {
273 logger.debug("Equally good fitness, moving on: " + nextFitness); 271 logger.debug("Equally good fitness, moving on: " + nextFitness);
274 currentTrajectoryWithFittness = nextTrajectoryWithFittness; 272 currentTrajectoryWithFitness = nextTrajectoryWithfitness;
275 continue mainLoop; 273 continue mainLoop;
276 } else { 274 } else {
277 logger.debug("Worse fitness."); 275 logger.debug("Worse fitness.");
278 currentTrajectoryWithFittness = null; 276 currentTrajectoryWithFitness = null;
279 continue mainLoop; 277 continue mainLoop;
280 } 278 }
281 } 279 }
282 } 280 }
283 281
284 logger.debug("State is fully traversed."); 282 logger.debug("State is fully traversed.");
285 trajectoiresToExplore.remove(currentTrajectoryWithFittness); 283 trajectoiresToExplore.remove(currentTrajectoryWithFitness);
286 currentTrajectoryWithFittness = null; 284 currentTrajectoryWithFitness = null;
287 285
288 } 286 }
289 logger.info("Interrupted."); 287 logger.info("Interrupted.");
@@ -308,6 +306,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
308 try { 306 try {
309 activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds()); 307 activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds());
310 } catch (NullPointerException e) { 308 } catch (NullPointerException e) {
309// logger.warn("Unexpected state code: " + context.getDesignSpaceManager().getCurrentState());
311 numberOfStatecoderFail++; 310 numberOfStatecoderFail++;
312 activationIds = Collections.emptyList(); 311 activationIds = Collections.emptyList();
313 } 312 }
@@ -315,27 +314,16 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
315 } 314 }
316 315
317 private void checkForSolution(final Fitness fittness) { 316 private void checkForSolution(final Fitness fittness) {
318 if (fittness.isSatisifiesHardObjectives()) { 317 solutionStore.newSolution(context);
319 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
320 if(numericSolver.currentSatisfiable()) {
321 Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context);
322 numericSolver.fillSolutionCopy(trace);
323 solutionStoreWithDiversityDescriptor.newSolution(context);
324 solutionStore.newSolution(context);
325 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
326 saveTimes();
327 logger.debug("Found a solution.");
328 }
329 }
330 }
331 } 318 }
319
332 public List<String> times = new LinkedList<String>(); 320 public List<String> times = new LinkedList<String>();
333 private void saveTimes() { 321 private void saveTimes() {
334 long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder)this.context.getStateCoder()).getStatecoderRuntime()/1000000; 322 long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder<?, ?>)this.context.getStateCoder()).getStatecoderRuntime()/1000000;
335 long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000; 323 long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000;
336 long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000; 324 long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000;
337 long solutionCopy = solutionStoreWithCopy.getSumRuntime()/1000000;
338 long activationSelection = this.activationSelector.getRuntime()/1000000; 325 long activationSelection = this.activationSelector.getRuntime()/1000000;
326 long solutionCopierTime = this.solutionSaver.getTotalCopierRuntime()/1000000;
339 long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000; 327 long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000;
340 long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000; 328 long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000;
341 long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000; 329 long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000;
@@ -347,8 +335,8 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
347 "|Backtrackingtime:"+backtrackingTime+ 335 "|Backtrackingtime:"+backtrackingTime+
348 "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+ 336 "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+
349 "|FitnessCalculationTime:"+(fitnessCalculationTime/1000000)+ 337 "|FitnessCalculationTime:"+(fitnessCalculationTime/1000000)+
350 "|SolutionCopyTime:"+solutionCopy+
351 "|ActivationSelectionTime:"+activationSelection+ 338 "|ActivationSelectionTime:"+activationSelection+
339 "|SolutionCopyTime:"+solutionCopierTime+
352 "|NumericalSolverSumTime:"+numericalSolverSumTime+ 340 "|NumericalSolverSumTime:"+numericalSolverSumTime+
353 "|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+ 341 "|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+
354 "|NumericalSolverSolvingTime:"+numericalSolverSolving+ 342 "|NumericalSolverSolvingTime:"+numericalSolverSolving+
@@ -385,13 +373,16 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
385 } 373 }
386 374
387 public void visualiseCurrentState() { 375 public void visualiseCurrentState() {
388 PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser; 376 PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser;
389 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) { 377 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) {
390 PartialInterpretation p = (PartialInterpretation) (context.getModel()); 378 PartialInterpretation p = (PartialInterpretation) (context.getModel());
391 int id = ++numberOfPrintedModel; 379 int id = ++numberOfPrintedModel;
392 if (id % configuration.debugCongiguration.partalInterpretationVisualisationFrequency == 0) { 380 if (id % configuration.debugConfiguration.partalInterpretationVisualisationFrequency == 0) {
393 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p); 381 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p);
394 visualisation.writeToFile(workspace, String.format("state%09d.png", id)); 382 logger.debug("Visualizing state: " + id + " (" + context.getDesignSpaceManager().getCurrentState() + ")");
383 String name = String.format("state%09d", id);
384 visualisation.writeToFile(workspace, name + ".png");
385 workspace.writeModel((EObject) context.getModel(), name + ".xmi");
395 } 386 }
396 } 387 }
397 } 388 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend
new file mode 100644
index 00000000..fb1b2066
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend
@@ -0,0 +1,184 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import com.google.common.collect.HashMultiset
4import com.google.common.collect.ImmutableSet
5import com.google.common.collect.Multiset
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.NeighbourhoodWithTraces
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
10import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
11import java.util.Collection
12import java.util.HashSet
13import java.util.Map
14import java.util.Set
15import org.eclipse.viatra.dse.base.ThreadContext
16import org.eclipse.xtend.lib.annotations.Accessors
17
18interface DiversityChecker {
19 public static val NO_DIVERSITY_CHECKER = new DiversityChecker {
20 override isActive() {
21 false
22 }
23
24 override getTotalRuntime() {
25 0
26 }
27
28 override getSuccessRate() {
29 1.0
30 }
31
32 override newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) {
33 true
34 }
35 }
36
37 def boolean isActive()
38
39 def long getTotalRuntime()
40
41 def double getSuccessRate()
42
43 def boolean newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds)
44
45 static def of(DiversityDescriptor descriptor) {
46 if (descriptor.ensureDiversity) {
47 new NodewiseDiversityChecker(descriptor)
48 } else {
49 NO_DIVERSITY_CHECKER
50 }
51 }
52}
53
54abstract class AbstractDiversityChecker implements DiversityChecker {
55 val DiversityDescriptor descriptor
56 val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice
57
58 @Accessors(PUBLIC_GETTER) var long totalRuntime = 0
59 var int allCheckCount = 0
60 var int successfulCheckCount = 0
61
62 protected new(DiversityDescriptor descriptor) {
63 if (!descriptor.ensureDiversity) {
64 throw new IllegalArgumentException(
65 "Diversity description should enforce diversity or NO_DIVERSITY_CHECKER should be used instead.")
66 }
67 this.descriptor = descriptor
68 }
69
70 override isActive() {
71 true
72 }
73
74 override getTotalRuntime() {
75 throw new UnsupportedOperationException("TODO: auto-generated method stub")
76 }
77
78 override getSuccessRate() {
79 (allCheckCount as double) / (successfulCheckCount as double)
80 }
81
82 override newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) {
83 val start = System.nanoTime
84 val model = threadContext.model as PartialInterpretation
85 val representation = solutionCoder.createRepresentation(model, descriptor.range, descriptor.parallels,
86 descriptor.maxNumber, descriptor.relevantTypes, descriptor.relevantRelations)
87 val isDifferent = internalNewSolution(representation, solutionId, dominatedSolutionIds)
88 totalRuntime += System.nanoTime - start
89 allCheckCount++
90 if (isDifferent) {
91 successfulCheckCount++
92 }
93 isDifferent
94 }
95
96 protected abstract def boolean internalNewSolution(
97 NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation,
98 Object solutionId, Collection<Object> dominatedSolutionIds)
99}
100
101class NodewiseDiversityChecker extends AbstractDiversityChecker {
102 var Multiset<Integer> nodeCodes = HashMultiset.create
103 val Map<Object, Set<Integer>> tracedNodeCodes = newHashMap
104
105 new(DiversityDescriptor descriptor) {
106 super(descriptor)
107 }
108
109 override protected internalNewSolution(
110 NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation,
111 Object solutionId, Collection<Object> dominatedSolutionIds) {
112 val nodeCodesInSolution = ImmutableSet.copyOf(representation.modelRepresentation.keySet.map[hashCode])
113 val remainingNodeCodes = if (dominatedSolutionIds.empty) {
114 nodeCodes
115 } else {
116 getRemainingNodeCodes(dominatedSolutionIds)
117 }
118 val hasNewCode = nodeCodesInSolution.exists[!remainingNodeCodes.contains(it)]
119 if (hasNewCode) {
120 nodeCodes = remainingNodeCodes
121 nodeCodes.addAll(nodeCodesInSolution)
122 for (dominatedSolutionId : dominatedSolutionIds) {
123 tracedNodeCodes.remove(dominatedSolutionId)
124 }
125 tracedNodeCodes.put(solutionId, nodeCodesInSolution)
126 }
127 hasNewCode
128 }
129
130 private def getRemainingNodeCodes(Collection<Object> dominatedSolutionIds) {
131 // TODO Optimize multiset operations.
132 val copyOfNodeCodes = HashMultiset.create(nodeCodes)
133 for (dominatedSolutionId : dominatedSolutionIds) {
134 val dominatedModelCode = tracedNodeCodes.get(dominatedSolutionId)
135 if (dominatedModelCode === null) {
136 throw new IllegalArgumentException("Unknown dominated solution: " + dominatedSolutionId)
137 }
138 copyOfNodeCodes.removeAll(dominatedModelCode)
139 }
140 copyOfNodeCodes
141 }
142}
143
144class GraphwiseDiversityChecker extends AbstractDiversityChecker {
145 var Set<Integer> modelCodes = newHashSet
146 val Map<Object, Integer> tracedModelCodes = newHashMap
147
148 new(DiversityDescriptor descriptor) {
149 super(descriptor)
150 }
151
152 override protected internalNewSolution(
153 NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation,
154 Object solutionId, Collection<Object> dominatedSolutionIds) {
155 val modelCodeOfSolution = representation.modelRepresentation.hashCode
156 val remainingModelCodes = if (dominatedSolutionIds.empty) {
157 modelCodes
158 } else {
159 getRemainingModelCodes(dominatedSolutionIds)
160 }
161 val isNewCode = !remainingModelCodes.contains(modelCodeOfSolution)
162 if (isNewCode) {
163 modelCodes = remainingModelCodes
164 modelCodes += modelCodeOfSolution
165 for (dominatedSolutionId : dominatedSolutionIds) {
166 tracedModelCodes.remove(dominatedSolutionId)
167 }
168 tracedModelCodes.put(solutionId, modelCodeOfSolution)
169 }
170 isNewCode
171 }
172
173 private def getRemainingModelCodes(Collection<Object> dominatedSolutionIds) {
174 val copyOfModelCodes = new HashSet(modelCodes)
175 for (dominatedSolutionId : dominatedSolutionIds) {
176 val dominatedModelCode = tracedModelCodes.get(dominatedSolutionId)
177 if (dominatedModelCode === null) {
178 throw new IllegalArgumentException("Unknown dominated solution: " + dominatedSolutionId)
179 }
180 copyOfModelCodes -= dominatedModelCode
181 }
182 copyOfModelCodes
183 }
184}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend
new file mode 100644
index 00000000..3c2e3319
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend
@@ -0,0 +1,66 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective
4import org.eclipse.viatra.dse.base.ThreadContext
5import org.eclipse.viatra.dse.objectives.Comparators
6import org.eclipse.viatra.dse.objectives.Fitness
7import org.eclipse.viatra.dse.objectives.IObjective
8
9final class DseUtils {
10 private new() {
11 throw new IllegalStateException("This is a static utility class and should not be instantiated directly.")
12 }
13
14 static def calculateFitness(ThreadContext it, (IObjective)=>Double getFitness) {
15 val result = new Fitness
16 var boolean satisifiesHardObjectives = true
17 for (objective : objectives) {
18 val fitness = getFitness.apply(objective)
19 result.put(objective.name, fitness)
20 if (objective.isHardObjective() && !objective.satisifiesHardObjective(fitness)) {
21 satisifiesHardObjectives = false
22 }
23 }
24 result.satisifiesHardObjectives = satisifiesHardObjectives
25 result
26 }
27
28 static def caclulateBestPossibleFitness(ThreadContext threadContext) {
29 threadContext.calculateFitness [ objective |
30 if (objective instanceof IThreeValuedObjective) {
31 objective.getBestPossibleFitness(threadContext)
32 } else {
33 switch (objective.comparator) {
34 case Comparators.LOWER_IS_BETTER:
35 Double.NEGATIVE_INFINITY
36 case Comparators.HIGHER_IS_BETTER:
37 Double.POSITIVE_INFINITY
38 case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER:
39 0.0
40 default:
41 throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " +
42 objective.name)
43 }
44 }
45 ]
46 }
47
48 static def caclulateWorstPossibleFitness(ThreadContext threadContext) {
49 threadContext.calculateFitness [ objective |
50 if (objective instanceof IThreeValuedObjective) {
51 objective.getWorstPossibleFitness(threadContext)
52 } else {
53 switch (objective.comparator) {
54 case Comparators.LOWER_IS_BETTER,
55 case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER:
56 Double.POSITIVE_INFINITY
57 case Comparators.HIGHER_IS_BETTER:
58 Double.NEGATIVE_INFINITY
59 default:
60 throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " +
61 objective.name)
62 }
63 }
64 ]
65 }
66}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend
new file mode 100644
index 00000000..2e039ca2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend
@@ -0,0 +1,25 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import org.eclipse.viatra.dse.objectives.IGlobalConstraint
4import org.eclipse.viatra.dse.base.ThreadContext
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
6
7class InconsistentScopeGlobalConstraint implements IGlobalConstraint {
8
9 override init(ThreadContext context) {
10 // Nothing to initialize.
11 }
12
13 override createNew() {
14 this
15 }
16
17 override getName() {
18 class.name
19 }
20
21 override checkGlobalConstraint(ThreadContext context) {
22 val partialModel = context.model as PartialInterpretation
23 partialModel.minNewElements <= partialModel.maxNewElements || partialModel.maxNewElements < 0
24 }
25}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend
new file mode 100644
index 00000000..39ef5f9a
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend
@@ -0,0 +1,24 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
4import org.apache.log4j.Logger
5import org.eclipse.viatra.dse.api.SolutionTrajectory
6import org.eclipse.viatra.dse.base.ThreadContext
7import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler
8import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
9
10@FinalFieldsConstructor
11class LoggerSolutionFoundHandler implements ISolutionFoundHandler {
12 val ViatraReasonerConfiguration configuration
13
14 val logger = Logger.getLogger(SolutionCopier)
15
16 override solutionFound(ThreadContext context, SolutionTrajectory trajectory) {
17 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions)
18 logger.debug("Found a solution.")
19 }
20
21 override solutionTriedToSave(ThreadContext context, SolutionTrajectory trajectory) {
22 // We are not interested in invalid solutions, ignore.
23 }
24}
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 a10530c7..d2faaa65 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
@@ -1,34 +1,20 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import com.google.common.collect.ImmutableList
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
6import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective
3import java.util.Comparator 7import java.util.Comparator
4import java.util.List 8import java.util.List
5import org.eclipse.viatra.dse.base.ThreadContext 9import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.dse.objectives.Comparators 10import org.eclipse.viatra.dse.objectives.Comparators
7import org.eclipse.viatra.dse.objectives.IObjective 11import org.eclipse.viatra.dse.objectives.IObjective
8import org.eclipse.viatra.dse.objectives.impl.BaseObjective
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
10import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
11 12
12//class ViatraReasonerNumbers { 13class ModelGenerationCompositeObjective implements IThreeValuedObjective {
13// public static val scopePriority = 2 14 val IObjective scopeObjective
14// public static val unfinishedMultiplicityPriority = 2
15// public static val unifinshedWFPriority = 2
16// //public static val complexityPriority = 4
17//
18// public static val scopeWeigth = 1.0
19// public static val unfinishedMultiplicityWeigth = 1.5
20// public static val unfinishedWFWeigth = 1.5
21// //public static val complexityWeigth = 0.1
22//
23// public static val useCompositeObjective = true
24// public static val compositePriority = 2
25//}
26
27class ModelGenerationCompositeObjective implements IObjective{
28 val ScopeObjective scopeObjective
29 val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives 15 val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives
30 val UnfinishedWFObjective unfinishedWFObjective 16 val UnfinishedWFObjective unfinishedWFObjective
31 var PartialInterpretation model=null; 17 var PartialInterpretation model = null
32 val boolean punishSize 18 val boolean punishSize
33 val int scopeWeight 19 val int scopeWeight
34 val int conaintmentWeight 20 val int conaintmentWeight
@@ -36,23 +22,20 @@ class ModelGenerationCompositeObjective implements IObjective{
36 val int unfinishedWFWeight 22 val int unfinishedWFWeight
37 23
38 new( 24 new(
39 ScopeObjective scopeObjective, 25 IObjective scopeObjective,
40 List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives, 26 List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
41 UnfinishedWFObjective unfinishedWFObjective, 27 UnfinishedWFObjective unfinishedWFObjective,
42 ViatraReasonerConfiguration configuration) 28 ViatraReasonerConfiguration configuration)
43 { 29 {
44 this.scopeObjective = scopeObjective 30 this(
45 this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives 31 scopeObjective, unfinishedMultiplicityObjectives, unfinishedWFObjective, configuration.punishSize,
46 this.unfinishedWFObjective = unfinishedWFObjective 32 configuration.scopeWeight, configuration.conaintmentWeight, configuration.nonContainmentWeight,
47 33 configuration.unfinishedWFWeight
48 this.punishSize = configuration.punishSize 34 )
49 this.scopeWeight = configuration.scopeWeight
50 this.conaintmentWeight = configuration.conaintmentWeight
51 this.nonContainmentWeight = configuration.nonContainmentWeight
52 this.unfinishedWFWeight = configuration.unfinishedWFWeight
53 } 35 }
36
54 new( 37 new(
55 ScopeObjective scopeObjective, 38 IObjective scopeObjective,
56 List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives, 39 List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
57 UnfinishedWFObjective unfinishedWFObjective, 40 UnfinishedWFObjective unfinishedWFObjective,
58 boolean punishSize, int scopeWeight, int conaintmentWeight, int nonContainmentWeight, int unfinishedWFWeight) 41 boolean punishSize, int scopeWeight, int conaintmentWeight, int nonContainmentWeight, int unfinishedWFWeight)
@@ -74,18 +57,21 @@ class ModelGenerationCompositeObjective implements IObjective{
74 this.unfinishedMultiplicityObjectives.forEach[it.init(context)] 57 this.unfinishedMultiplicityObjectives.forEach[it.init(context)]
75 this.unfinishedWFObjective.init(context) 58 this.unfinishedWFObjective.init(context)
76 } 59 }
77 60
78 override createNew() { 61 override createNew() {
79 return new ModelGenerationCompositeObjective( 62 return new ModelGenerationCompositeObjective(
80 this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective, 63 scopeObjective.createNew,
81 this.punishSize, this.scopeWeight, this.conaintmentWeight, this.nonContainmentWeight, this.unfinishedWFWeight) 64 ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew as UnfinishedMultiplicityObjective]),
65 unfinishedWFObjective.createNew as UnfinishedWFObjective,
66 punishSize, scopeWeight, conaintmentWeight, nonContainmentWeight, unfinishedWFWeight
67 )
82 } 68 }
83 69
84 override getComparator() { Comparators.LOWER_IS_BETTER } 70 override getComparator() { Comparators.LOWER_IS_BETTER }
71
85 override getFitness(ThreadContext context) { 72 override getFitness(ThreadContext context) {
86 73
87 val scopeFitnes = scopeObjective.getFitness(context) 74 val scopeFitnes = scopeObjective.getFitness(context)
88 //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]
89 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) 75 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)
90 76
91 var containmentMultiplicity = 0.0 77 var containmentMultiplicity = 0.0
@@ -109,24 +95,30 @@ class ModelGenerationCompositeObjective implements IObjective{
109 sum += nonContainmentMultiplicity*nonContainmentWeight 95 sum += nonContainmentMultiplicity*nonContainmentWeight
110 sum += unfinishedWFsFitness*unfinishedWFWeight 96 sum += unfinishedWFsFitness*unfinishedWFWeight
111 sum+=size 97 sum+=size
112
113 //println('''Sum=«sum»|Scope=«scopeFitnes»|ContainmentMultiplicity=«containmentMultiplicity»|NonContainmentMultiplicity=«nonContainmentMultiplicity»|WFs=«unfinishedWFsFitness»''')
114
115 return sum 98 return sum
116 } 99 }
117 100
118 override getLevel() { 2 } 101 override getWorstPossibleFitness(ThreadContext threadContext) {
119 override getName() { "CompositeUnfinishednessObjective"} 102 Double.POSITIVE_INFINITY
103 }
120 104
105 override getBestPossibleFitness(ThreadContext threadContext) {
106 0.0
107 }
108
109 override getLevel() { 2 }
110
111 override getName() { "CompositeUnfinishednessObjective" }
112
121 override isHardObjective() { true } 113 override isHardObjective() { true }
122 override satisifiesHardObjective(Double fitness) { fitness < 0.95 } 114
123 115 override satisifiesHardObjective(Double fitness) { fitness <= 0.001 }
124 116
125 override setComparator(Comparator<Double> comparator) { 117 override setComparator(Comparator<Double> comparator) {
126 throw new UnsupportedOperationException("TODO: auto-generated method stub") 118 throw new UnsupportedOperationException("Model generation objective comparator cannot be set.")
127 } 119 }
120
128 override setLevel(int level) { 121 override setLevel(int level) {
129 throw new UnsupportedOperationException("TODO: auto-generated method stub") 122 throw new UnsupportedOperationException("Model generation objective level cannot be set.")
130 } 123 }
131 124}
132} \ 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/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 0b0feb1a..066040a0 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
@@ -21,7 +21,8 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
21import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint 21import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
22 22
23class NumericSolver { 23class NumericSolver {
24 val ThreadContext threadContext; 24 val ModelGenerationMethod method
25 var ThreadContext threadContext
25 val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> 26 val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
26 val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> 27 val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>>
27 NumericTranslator t = new NumericTranslator 28 NumericTranslator t = new NumericTranslator
@@ -35,8 +36,16 @@ class NumericSolver {
35 var int numberOfSolverCalls = 0 36 var int numberOfSolverCalls = 0
36 var int numberOfCachedSolverCalls = 0 37 var int numberOfCachedSolverCalls = 0
37 38
38 new(ThreadContext threadContext, ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) { 39 new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) {
39 this.threadContext = threadContext 40 this.method = method
41 this.intermediateConsistencyCheck = intermediateConsistencyCheck
42 this.caching = caching
43 }
44
45 def init(ThreadContext context) {
46 // This makes the NumericSolver single-threaded,
47 // but that's not a problem, because we only use the solver on a single thread anyways.
48 this.threadContext = context
40 val engine = threadContext.queryEngine 49 val engine = threadContext.queryEngine
41 for(entry : method.mustUnitPropagationPreconditions.entrySet) { 50 for(entry : method.mustUnitPropagationPreconditions.entrySet) {
42 val constraint = entry.key 51 val constraint = entry.key
@@ -50,8 +59,6 @@ class NumericSolver {
50 val matcher = querySpec.getMatcher(engine); 59 val matcher = querySpec.getMatcher(engine);
51 constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) 60 constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher)
52 } 61 }
53 this.intermediateConsistencyCheck = intermediateConsistencyCheck
54 this.caching = caching
55 } 62 }
56 63
57 def getRuntime(){runtime} 64 def getRuntime(){runtime}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
index efc2ef36..cfd11816 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
@@ -219,4 +219,4 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{
219 } 219 }
220 builder 220 builder
221 } 221 }
222} \ No newline at end of file 222}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
index 69efe0d7..69a734f8 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
@@ -23,9 +23,9 @@ class ScopeObjective implements IObjective{
23 23
24 override getFitness(ThreadContext context) { 24 override getFitness(ThreadContext context) {
25 val interpretation = context.model as PartialInterpretation 25 val interpretation = context.model as PartialInterpretation
26 var res = interpretation.minNewElements.doubleValue 26 var res = interpretation.minNewElementsHeuristic.doubleValue
27 for(scope : interpretation.scopes) { 27 for(scope : interpretation.scopes) {
28 res += scope.minNewElements*2 28 res += scope.minNewElementsHeuristic*2
29 } 29 }
30 return res 30 return res
31 } 31 }
@@ -41,4 +41,4 @@ class ScopeObjective implements IObjective{
41 throw new UnsupportedOperationException("TODO: auto-generated method stub") 41 throw new UnsupportedOperationException("TODO: auto-generated method stub")
42 } 42 }
43 override getLevel() { 2 } 43 override getLevel() { 2 }
44} \ No newline at end of file 44}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
new file mode 100644
index 00000000..38c8f5a1
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend
@@ -0,0 +1,86 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import com.google.common.collect.ImmutableList
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import java.util.LinkedHashMap
6import java.util.List
7import java.util.Map
8import org.eclipse.emf.ecore.EObject
9import org.eclipse.emf.ecore.util.EcoreUtil
10import org.eclipse.viatra.dse.base.ThreadContext
11import org.eclipse.xtend.lib.annotations.Accessors
12import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
13
14@FinalFieldsConstructor
15class CopiedSolution {
16 @Accessors val PartialInterpretation partialInterpretations
17 @Accessors val Map<EObject, EObject> trace
18 @Accessors val long copierRuntime
19 @Accessors var boolean current = true
20}
21
22/**
23 * Based on {@link SolutionStore.BestSolutionSaver}.
24 *
25 * Will also automatically fill any missing numerical values in the saved solutions
26 * using the supplied {@link NumericSolver}.
27 */
28class SolutionCopier {
29 val NumericSolver numericSolver
30 val copiedSolutions = new LinkedHashMap<Object, CopiedSolution>
31
32 long startTime = System.nanoTime
33 @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0
34
35 new(NumericSolver numericSolver) {
36 this.numericSolver = numericSolver
37 }
38
39 def void copySolution(ThreadContext context, Object solutionId) {
40 val existingCopy = copiedSolutions.get(solutionId)
41 if (existingCopy === null) {
42 val copyStart = System.nanoTime
43 val solution = context.model as PartialInterpretation
44 val copier = new EcoreUtil.Copier
45 val copiedPartialInterpretation = copier.copy(solution) as PartialInterpretation
46 copier.copyReferences
47 totalCopierRuntime += System.nanoTime - copyStart
48 val copierRuntime = System.nanoTime - startTime
49 val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime)
50 numericSolver.fillSolutionCopy(copiedSolution.trace)
51 copiedSolutions.put(solutionId, copiedSolution)
52 } else {
53 existingCopy.current = true
54 }
55 }
56
57 def void markAsObsolete(Object solutionId) {
58 val copiedSolution = copiedSolutions.get(solutionId)
59 if (copiedSolution === null) {
60 throw new IllegalStateException("No solution to mark as obsolete for state code: " + solutionId)
61 }
62 copiedSolution.current = false
63 }
64
65 def List<PartialInterpretation> getPartialInterpretations(boolean currentOnly) {
66 getListOfCopiedSolutions(currentOnly).map[partialInterpretations]
67 }
68
69 def List<Map<EObject, EObject>> getTraces(boolean currentOnly) {
70 getListOfCopiedSolutions(currentOnly).map[trace]
71 }
72
73 def List<Long> getAllCopierRuntimes(boolean currentOnly) {
74 getListOfCopiedSolutions(currentOnly).map[copierRuntime]
75 }
76
77 def List<CopiedSolution> getListOfCopiedSolutions(boolean currentOnly) {
78 val values = copiedSolutions.values
79 val filteredSolutions = if (currentOnly) {
80 values.filter[current]
81 } else {
82 values
83 }
84 ImmutableList.copyOf(filteredSolutions)
85 }
86}
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 21867a4e..4bd2c349 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
@@ -1,14 +1,12 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import java.util.List
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 3import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import java.util.LinkedList 4import java.util.LinkedList
6import org.eclipse.emf.ecore.EObject 5import java.util.List
7import java.util.Map 6import java.util.Map
7import org.eclipse.emf.ecore.EObject
8import org.eclipse.emf.ecore.util.EcoreUtil 8import org.eclipse.emf.ecore.util.EcoreUtil
9import org.eclipse.viatra.dse.base.ThreadContext 9import org.eclipse.viatra.dse.base.ThreadContext
10import java.util.TreeMap
11import java.util.SortedMap
12 10
13class SolutionStoreWithCopy { 11class SolutionStoreWithCopy {
14 12
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend
deleted file mode 100644
index 1e7f18a8..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend
+++ /dev/null
@@ -1,120 +0,0 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
6import java.util.LinkedList
7import java.util.List
8import org.eclipse.viatra.dse.base.ThreadContext
9import java.util.HashSet
10import java.util.Set
11
12enum DiversityGranularity {
13 Nodewise, Graphwise
14}
15
16class SolutionStoreWithDiversityDescriptor {
17 val DiversityDescriptor descriptor
18 DiversityGranularity granularity
19 val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice
20 val Set<Integer> solutionCodeList = new HashSet
21
22 var long runtime
23 var int allCheck
24 var int successfulCheck
25
26 new(DiversityDescriptor descriptor) {
27 if(descriptor.ensureDiversity) {
28 this.descriptor = descriptor
29 this.granularity = DiversityGranularity::Nodewise
30 } else {
31 this.descriptor = null
32 this.granularity = DiversityGranularity::Nodewise
33 }
34 }
35
36 def public isActive() {
37 descriptor!==null
38 }
39
40 def getSumRuntime() {
41 return runtime
42 }
43 def getSuccessRate() {
44 return successfulCheck as double / allCheck
45 }
46
47 def isDifferent(ThreadContext context) {
48 if(active) {
49 val start = System.nanoTime
50 val model = context.model as PartialInterpretation
51 var boolean isDifferent
52 if(this.granularity == DiversityGranularity::Graphwise) {
53 val code = solutionCoder.createRepresentation(model,
54 descriptor.range,
55 descriptor.parallels,
56 descriptor.maxNumber,
57 descriptor.relevantTypes,
58 descriptor.relevantRelations).modelRepresentation.hashCode
59
60 isDifferent = !solutionCodeList.contains(code)
61 } else if(this.granularity == DiversityGranularity::Nodewise){
62 val codes = solutionCoder.createRepresentation(model,
63 descriptor.range,
64 descriptor.parallels,
65 descriptor.maxNumber,
66 descriptor.relevantTypes,
67 descriptor.relevantRelations).modelRepresentation.keySet.map[hashCode].toList
68 val differentCodes = codes.filter[!solutionCodeList.contains(it)]
69 //println(differentCodes.size)
70
71 isDifferent = differentCodes.size>=1
72 } else {
73 throw new UnsupportedOperationException('''Unsupported diversity type: «this.granularity»''')
74 }
75
76 runtime += System.nanoTime - start
77 allCheck++
78 if(isDifferent) { successfulCheck++ }
79 return isDifferent
80 } else {
81 allCheck++
82 successfulCheck++
83 return true
84 }
85 }
86
87 def canBeDifferent(ThreadContext context) {
88 return true
89 }
90
91 def newSolution(ThreadContext context) {
92 if(active) {
93 val start = System.nanoTime
94 val model = context.model as PartialInterpretation
95 if(this.granularity == DiversityGranularity::Graphwise) {
96 val code = solutionCoder.createRepresentation(model,
97 descriptor.range,
98 descriptor.parallels,
99 descriptor.maxNumber,
100 descriptor.relevantTypes,
101 descriptor.relevantRelations).modelRepresentation.hashCode
102
103 solutionCodeList += code.hashCode
104 } else if(this.granularity == DiversityGranularity::Nodewise){
105 val codes = solutionCoder.createRepresentation(model,
106 descriptor.range,
107 descriptor.parallels,
108 descriptor.maxNumber,
109 descriptor.relevantTypes,
110 descriptor.relevantRelations).modelRepresentation.keySet.map[hashCode].toList
111
112 solutionCodeList += codes.map[it.hashCode]
113 } else {
114 throw new UnsupportedOperationException('''Unsupported diversity type: «this.granularity»''')
115 }
116
117 runtime += System.nanoTime - start
118 }
119 }
120} \ 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/SurelyViolatedObjectiveGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend
new file mode 100644
index 00000000..8ed3e912
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend
@@ -0,0 +1,27 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import org.eclipse.viatra.dse.base.ThreadContext
4import org.eclipse.viatra.dse.objectives.IGlobalConstraint
5import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
6
7@FinalFieldsConstructor
8class SurelyViolatedObjectiveGlobalConstraint implements IGlobalConstraint {
9 val ViatraReasonerSolutionSaver solutionSaver
10
11 override init(ThreadContext context) {
12 // Nothing to initialize.
13 }
14
15 override createNew() {
16 this
17 }
18
19 override getName() {
20 class.name
21 }
22
23 override checkGlobalConstraint(ThreadContext context) {
24 val bestFitness = DseUtils.caclulateBestPossibleFitness(context)
25 bestFitness.satisifiesHardObjectives && solutionSaver.fitnessMayBeSaved(bestFitness)
26 }
27}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
index 2b0807d6..e1582d3b 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
@@ -1,15 +1,15 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator 3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator
4import java.util.Comparator 4import java.util.Comparator
5import org.eclipse.viatra.dse.base.ThreadContext 5import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.dse.objectives.IObjective
7import org.eclipse.viatra.dse.objectives.Comparators 6import org.eclipse.viatra.dse.objectives.Comparators
7import org.eclipse.viatra.dse.objectives.IObjective
8 8
9class UnfinishedMultiplicityObjective implements IObjective { 9class UnfinishedMultiplicityObjective implements IObjective {
10 val MultiplicityGoalConstraintCalculator unfinishedMultiplicity; 10 val MultiplicityGoalConstraintCalculator unfinishedMultiplicity
11 11
12 public new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) { 12 new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {
13 this.unfinishedMultiplicity = unfinishedMultiplicity 13 this.unfinishedMultiplicity = unfinishedMultiplicity
14 } 14 }
15 15
@@ -29,12 +29,13 @@ class UnfinishedMultiplicityObjective implements IObjective {
29 override satisifiesHardObjective(Double fitness) { return fitness <=0.01 } 29 override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }
30 30
31 override setComparator(Comparator<Double> comparator) { 31 override setComparator(Comparator<Double> comparator) {
32 throw new UnsupportedOperationException("TODO: auto-generated method stub") 32 throw new UnsupportedOperationException
33 } 33 }
34 override setLevel(int level) { 34 override setLevel(int level) {
35 throw new UnsupportedOperationException("TODO: auto-generated method stub") 35 throw new UnsupportedOperationException
36 } 36 }
37
37 def isContainment() { 38 def isContainment() {
38 return this.unfinishedMultiplicity.containment 39 return this.unfinishedMultiplicity.containment
39 } 40 }
40} \ No newline at end of file 41}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
index e0111cf6..1b61ffa5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
@@ -1,56 +1,64 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import org.eclipse.viatra.dse.objectives.IObjective 3import java.util.ArrayList
4import org.eclipse.viatra.query.runtime.api.IPatternMatch
5import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
6import org.eclipse.viatra.query.runtime.api.IQuerySpecification
7import java.util.Collection 4import java.util.Collection
8import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine 5import java.util.Comparator
9import org.eclipse.viatra.query.runtime.emf.EMFScope
10import org.eclipse.viatra.dse.base.ThreadContext
11import java.util.List 6import java.util.List
7import org.eclipse.viatra.dse.base.ThreadContext
12import org.eclipse.viatra.dse.objectives.Comparators 8import org.eclipse.viatra.dse.objectives.Comparators
13import java.util.ArrayList 9import org.eclipse.viatra.dse.objectives.IObjective
14import java.util.Comparator 10import org.eclipse.viatra.query.runtime.api.IPatternMatch
11import org.eclipse.viatra.query.runtime.api.IQuerySpecification
12import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
15 13
16class UnfinishedWFObjective implements IObjective { 14class UnfinishedWFObjective implements IObjective {
17 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs 15 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs
18 val List<ViatraQueryMatcher<?>> matchers 16 val List<ViatraQueryMatcher<?>> matchers
19 17
20 public new(Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) { 18 new(
19 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) {
21 this.unfinishedWFs = unfinishedWFs 20 this.unfinishedWFs = unfinishedWFs
22 matchers = new ArrayList(unfinishedWFs.size) 21 matchers = new ArrayList(unfinishedWFs.size)
23 } 22 }
23
24 override getName() '''unfinishedWFs''' 24 override getName() '''unfinishedWFs'''
25
25 override createNew() { 26 override createNew() {
26 return new UnfinishedWFObjective(unfinishedWFs) 27 return new UnfinishedWFObjective(unfinishedWFs)
27 } 28 }
29
28 override init(ThreadContext context) { 30 override init(ThreadContext context) {
29 val engine = context.queryEngine//ViatraQueryEngine.on(new EMFScope(context.model)) 31 val engine = context.queryEngine // ViatraQueryEngine.on(new EMFScope(context.model))
30 for(unfinishedWF : unfinishedWFs) { 32 for (unfinishedWF : unfinishedWFs) {
31 matchers += unfinishedWF.getMatcher(engine) 33 matchers += unfinishedWF.getMatcher(engine)
32 } 34 }
33 } 35 }
34 36
35 override getComparator() { Comparators.LOWER_IS_BETTER } 37 override getComparator() { Comparators.LOWER_IS_BETTER }
38
36 override getFitness(ThreadContext context) { 39 override getFitness(ThreadContext context) {
37 var sumOfMatches = 0 40 var sumOfMatches = 0
38 for(matcher : matchers) { 41 for (matcher : matchers) {
39 val number = matcher.countMatches 42 val number = matcher.countMatches
40 //println('''«matcher.patternName» = «number»''') 43// if (number > 0) {
41 sumOfMatches+=number 44// println('''«matcher.patternName» = «number»''')
45// }
46 sumOfMatches += number
42 } 47 }
43 return sumOfMatches.doubleValue 48 return sumOfMatches.doubleValue
44 } 49 }
45 50
46 override getLevel() { 2 } 51 override getLevel() { 2 }
52
47 override isHardObjective() { true } 53 override isHardObjective() { true }
48 override satisifiesHardObjective(Double fitness) { return fitness <=0.01 } 54
49 55 override satisifiesHardObjective(Double fitness) { return fitness <= 0.01 }
56
50 override setComparator(Comparator<Double> comparator) { 57 override setComparator(Comparator<Double> comparator) {
51 throw new UnsupportedOperationException("TODO: auto-generated method stub") 58 throw new UnsupportedOperationException()
52 } 59 }
60
53 override setLevel(int level) { 61 override setLevel(int level) {
54 throw new UnsupportedOperationException("TODO: auto-generated method stub") 62 throw new UnsupportedOperationException()
55 } 63 }
56} \ No newline at end of file 64}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
new file mode 100644
index 00000000..d879d4cc
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
@@ -0,0 +1,150 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.HashMap
4import java.util.Map
5import org.eclipse.viatra.dse.api.DSEException
6import org.eclipse.viatra.dse.api.Solution
7import org.eclipse.viatra.dse.api.SolutionTrajectory
8import org.eclipse.viatra.dse.base.ThreadContext
9import org.eclipse.viatra.dse.objectives.Fitness
10import org.eclipse.viatra.dse.objectives.IObjective
11import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper
12import org.eclipse.viatra.dse.solutionstore.SolutionStore.ISolutionSaver
13import org.eclipse.xtend.lib.annotations.Accessors
14
15/**
16 * Based on {@link SolutionStore.BestSolutionSaver}.
17 *
18 * Will also automatically fill any missing numerical values in the saved solutions
19 * using the supplied {@link NumericSolver}.
20 */
21class ViatraReasonerSolutionSaver implements ISolutionSaver {
22 @Accessors val SolutionCopier solutionCopier
23 @Accessors val DiversityChecker diversityChecker
24 val boolean hasExtremalObjectives
25 val int numberOfRequiredSolutions
26 val ObjectiveComparatorHelper comparatorHelper
27 val Map<SolutionTrajectory, Fitness> trajectories = new HashMap
28
29 @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection
30
31 new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker, NumericSolver numericSolver) {
32 this.diversityChecker = diversityChecker
33 comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives)
34 hasExtremalObjectives = leveledExtremalObjectives.exists[!empty]
35 this.numberOfRequiredSolutions = numberOfRequiredSolutions
36 this.solutionCopier = new SolutionCopier(numericSolver)
37 }
38
39 override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
40 if (hasExtremalObjectives) {
41 saveBestSolutionOnly(context, id, solutionTrajectory)
42 } else {
43 saveAnyDiverseSolution(context, id, solutionTrajectory)
44 }
45 }
46
47 private def saveBestSolutionOnly(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
48 val fitness = context.lastFitness
49 if (!shouldSaveSolution(fitness, context)) {
50 return false
51 }
52 val dominatedTrajectories = newArrayList
53 for (entry : trajectories.entrySet) {
54 val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value)
55 if (isLastFitnessBetter < 0) {
56 // Found a trajectory that dominates the current one, no need to save
57 return false
58 }
59 if (isLastFitnessBetter > 0) {
60 dominatedTrajectories += entry.key
61 }
62 }
63 if (dominatedTrajectories.size == 0 && !needsMoreSolutionsWithSameFitness) {
64 return false
65 }
66 if (!diversityChecker.newSolution(context, id, dominatedTrajectories.map[solution.stateCode])) {
67 return false
68 }
69 // We must save the new trajectory before removing dominated trajectories
70 // to avoid removing the current solution when it is reachable only via dominated trajectories.
71 val solutionSaved = basicSaveSolution(context, id, solutionTrajectory, fitness)
72 for (dominatedTrajectory : dominatedTrajectories) {
73 trajectories -= dominatedTrajectory
74 val dominatedSolution = dominatedTrajectory.solution
75 if (!dominatedSolution.trajectories.remove(dominatedTrajectory)) {
76 throw new DSEException(
77 "Dominated solution is not reachable from dominated trajectory. This should never happen!")
78 }
79 if (dominatedSolution.trajectories.empty) {
80 val dominatedSolutionId = dominatedSolution.stateCode
81 solutionCopier.markAsObsolete(dominatedSolutionId)
82 solutionsCollection -= dominatedSolutionId
83 }
84 }
85 solutionSaved
86 }
87
88 private def saveAnyDiverseSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
89 val fitness = context.lastFitness
90 if (!shouldSaveSolution(fitness, context)) {
91 return false
92 }
93 if (!diversityChecker.newSolution(context, id, emptyList)) {
94 return false
95 }
96 basicSaveSolution(context, id, solutionTrajectory, fitness)
97 }
98
99 private def shouldSaveSolution(Fitness fitness, ThreadContext context) {
100 return fitness.satisifiesHardObjectives
101 }
102
103 private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory,
104 Fitness fitness) {
105 var boolean solutionSaved = false
106 var dseSolution = solutionsCollection.get(id)
107 if (dseSolution === null) {
108 solutionCopier.copySolution(context, id)
109 dseSolution = new Solution(id, solutionTrajectory)
110 solutionsCollection.put(id, dseSolution)
111 solutionSaved = true
112 } else {
113 solutionSaved = dseSolution.trajectories.add(solutionTrajectory)
114 }
115 if (solutionSaved) {
116 solutionTrajectory.solution = dseSolution
117 trajectories.put(solutionTrajectory, fitness)
118 }
119 solutionSaved
120 }
121
122 def fitnessMayBeSaved(Fitness fitness) {
123 if (!hasExtremalObjectives) {
124 return true
125 }
126 var boolean mayDominate
127 for (existingFitness : trajectories.values) {
128 val isNewFitnessBetter = comparatorHelper.compare(fitness, existingFitness)
129 if (isNewFitnessBetter < 0) {
130 return false
131 }
132 if (isNewFitnessBetter > 0) {
133 mayDominate = true
134 }
135 }
136 mayDominate || needsMoreSolutionsWithSameFitness
137 }
138
139 private def boolean needsMoreSolutionsWithSameFitness() {
140 if (solutionsCollection === null) {
141 // The solutions collection will only be initialized upon saving the first solution.
142 return true
143 }
144 solutionsCollection.size < numberOfRequiredSolutions
145 }
146
147 def getTotalCopierRuntime() {
148 solutionCopier.totalCopierRuntime
149 }
150}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
index 5a528a9e..6d772f32 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
@@ -1,5 +1,6 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import com.google.common.collect.ImmutableList
3import java.util.ArrayList 4import java.util.ArrayList
4import java.util.Collection 5import java.util.Collection
5import org.eclipse.viatra.dse.objectives.Comparators 6import org.eclipse.viatra.dse.objectives.Comparators
@@ -12,25 +13,33 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification
12import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 13import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
13 14
14class WF2ObjectiveConverter { 15class WF2ObjectiveConverter {
15 16 static val INVALIDATED_WFS_NAME = "invalidatedWFs"
17
16 def createCompletenessObjective( 18 def createCompletenessObjective(
17 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) 19 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) {
18 { 20 new UnfinishedWFObjective(unfinishedWF)
19 val res = new ConstraintsObjective('''unfinishedWFs''', 21 }
20 unfinishedWF.map[ 22
21 new QueryConstraint(it.fullyQualifiedName,it,2.0) 23 def createInvalidationObjective(
22 ].toList 24 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {
25 createConstraintObjective(INVALIDATED_WFS_NAME, invalidatedByWF)
26 }
27
28 def IGlobalConstraint createInvalidationGlobalConstraint(
29 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {
30 new ModelQueriesGlobalConstraint(INVALIDATED_WFS_NAME, new ArrayList(invalidatedByWF))
31 }
32
33 private def createConstraintObjective(String name,
34 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries) {
35 val res = new ConstraintsObjective(
36 name,
37 ImmutableList.copyOf(queries.map [
38 new QueryConstraint(it.fullyQualifiedName, it, 1.0)
39 ])
23 ) 40 )
24 res.withComparator(Comparators.LOWER_IS_BETTER) 41 res.withComparator(Comparators.LOWER_IS_BETTER)
25 res.level = 2 42 res.level = 2
26 return res 43 res
27 }
28
29 def IGlobalConstraint createInvalidationObjective(
30 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF)
31 {
32 return new ModelQueriesGlobalConstraint('''invalidatedWFs''',
33 new ArrayList(invalidatedByWF)
34 )
35 } 44 }
36} \ No newline at end of file 45}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-07 21:46:29 +0000