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/BestFirstStrategyForModelGeneration.java70
-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/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.xtend78
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend74
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend52
-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.xtend29
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend137
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend45
12 files changed, 607 insertions, 274 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
index 60f46033..6ff867d7 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
@@ -75,8 +75,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
75 // Running 75 // Running
76 private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore; 76 private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore;
77 private SolutionStore solutionStore; 77 private SolutionStore solutionStore;
78 private SolutionStoreWithCopy solutionStoreWithCopy;
79 private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor;
80 private volatile boolean isInterrupted = false; 78 private volatile boolean isInterrupted = false;
81 private ModelResult modelResultByInternalSolver = null; 79 private ModelResult modelResultByInternalSolver = null;
82 private Random random = new Random(); 80 private Random random = new Random();
@@ -97,12 +95,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
97 this.method = method; 95 this.method = method;
98 } 96 }
99 97
100 public SolutionStoreWithCopy getSolutionStoreWithCopy() {
101 return solutionStoreWithCopy;
102 }
103 public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
104 return solutionStoreWithDiversityDescriptor;
105 }
106 public int getNumberOfStatecoderFail() { 98 public int getNumberOfStatecoderFail() {
107 return numberOfStatecoderFail; 99 return numberOfStatecoderFail;
108 } 100 }
@@ -121,9 +113,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
121 matchers.add(matcher); 113 matchers.add(matcher);
122 } 114 }
123 115
124 this.solutionStoreWithCopy = new SolutionStoreWithCopy();
125 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
126
127 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); 116 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
128 this.comparator = new Comparator<TrajectoryWithFitness>() { 117 this.comparator = new Comparator<TrajectoryWithFitness>() {
129 @Override 118 @Override
@@ -146,13 +135,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
146 return; 135 return;
147 } 136 }
148 137
149 final Fitness firstFittness = context.calculateFitness(); 138 final Fitness firstfitness = context.calculateFitness();
150 checkForSolution(firstFittness); 139 solutionStore.newSolution(context);
151 140
152 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); 141 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
153 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); 142 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
154 TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness); 143 TrajectoryWithFitness currentTrajectoryWithfitness = new TrajectoryWithFitness(firstTrajectory, firstfitness);
155 trajectoiresToExplore.add(currentTrajectoryWithFittness); 144 trajectoiresToExplore.add(currentTrajectoryWithfitness);
156 145
157 //if(configuration) 146 //if(configuration)
158 visualiseCurrentState(); 147 visualiseCurrentState();
@@ -167,22 +156,22 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
167 156
168 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) { 157 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) {
169 158
170 if (currentTrajectoryWithFittness == null) { 159 if (currentTrajectoryWithfitness == null) {
171 if (trajectoiresToExplore.isEmpty()) { 160 if (trajectoiresToExplore.isEmpty()) {
172 logger.debug("State space is fully traversed."); 161 logger.debug("State space is fully traversed.");
173 return; 162 return;
174 } else { 163 } else {
175 currentTrajectoryWithFittness = selectState(); 164 currentTrajectoryWithfitness = selectState();
176 if (logger.isDebugEnabled()) { 165 if (logger.isDebugEnabled()) {
177 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); 166 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
178 logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness); 167 logger.debug("New trajectory is chosen: " + currentTrajectoryWithfitness);
179 } 168 }
180 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory); 169 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithfitness.trajectory);
181 } 170 }
182 } 171 }
183 172
184// visualiseCurrentState(); 173// visualiseCurrentState();
185// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); 174// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
186// if(consistencyCheckResult == true) { 175// if(consistencyCheckResult == true) {
187// continue mainLoop; 176// continue mainLoop;
188// } 177// }
@@ -194,7 +183,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
194 final Object nextActivation = iterator.next(); 183 final Object nextActivation = iterator.next();
195// if (!iterator.hasNext()) { 184// if (!iterator.hasNext()) {
196// logger.debug("Last untraversed activation of the state."); 185// logger.debug("Last untraversed activation of the state.");
197// trajectoiresToExplore.remove(currentTrajectoryWithFittness); 186// trajectoiresToExplore.remove(currentTrajectoryWithfitness);
198// } 187// }
199 logger.debug("Executing new activation: " + nextActivation); 188 logger.debug("Executing new activation: " + nextActivation);
200 context.executeAcitvationId(nextActivation); 189 context.executeAcitvationId(nextActivation);
@@ -209,7 +198,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
209// System.out.println("---------"); 198// System.out.println("---------");
210// } 199// }
211 200
212 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); 201 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
213 if(consistencyCheckResult == true) { continue mainLoop; } 202 if(consistencyCheckResult == true) { continue mainLoop; }
214 203
215 if (context.isCurrentStateAlreadyTraversed()) { 204 if (context.isCurrentStateAlreadyTraversed()) {
@@ -220,38 +209,38 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
220 context.backtrack(); 209 context.backtrack();
221 } else { 210 } else {
222 final Fitness nextFitness = context.calculateFitness(); 211 final Fitness nextFitness = context.calculateFitness();
223 checkForSolution(nextFitness); 212 solutionStore.newSolution(context);
224 if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) { 213 if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) {
225 logger.debug("Reached max depth."); 214 logger.debug("Reached max depth.");
226 context.backtrack(); 215 context.backtrack();
227 continue; 216 continue;
228 } 217 }
229 218
230 TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness( 219 TrajectoryWithFitness nextTrajectoryWithfitness = new TrajectoryWithFitness(
231 context.getTrajectory().toArray(), nextFitness); 220 context.getTrajectory().toArray(), nextFitness);
232 trajectoiresToExplore.add(nextTrajectoryWithFittness); 221 trajectoiresToExplore.add(nextTrajectoryWithfitness);
233 222
234 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness, 223 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithfitness.fitness,
235 nextTrajectoryWithFittness.fitness); 224 nextTrajectoryWithfitness.fitness);
236 if (compare < 0) { 225 if (compare < 0) {
237 logger.debug("Better fitness, moving on: " + nextFitness); 226 logger.debug("Better fitness, moving on: " + nextFitness);
238 currentTrajectoryWithFittness = nextTrajectoryWithFittness; 227 currentTrajectoryWithfitness = nextTrajectoryWithfitness;
239 continue mainLoop; 228 continue mainLoop;
240 } else if (compare == 0) { 229 } else if (compare == 0) {
241 logger.debug("Equally good fitness, moving on: " + nextFitness); 230 logger.debug("Equally good fitness, moving on: " + nextFitness);
242 currentTrajectoryWithFittness = nextTrajectoryWithFittness; 231 currentTrajectoryWithfitness = nextTrajectoryWithfitness;
243 continue mainLoop; 232 continue mainLoop;
244 } else { 233 } else {
245 logger.debug("Worse fitness."); 234 logger.debug("Worse fitness.");
246 currentTrajectoryWithFittness = null; 235 currentTrajectoryWithfitness = null;
247 continue mainLoop; 236 continue mainLoop;
248 } 237 }
249 } 238 }
250 } 239 }
251 240
252 logger.debug("State is fully traversed."); 241 logger.debug("State is fully traversed.");
253 trajectoiresToExplore.remove(currentTrajectoryWithFittness); 242 trajectoiresToExplore.remove(currentTrajectoryWithfitness);
254 currentTrajectoryWithFittness = null; 243 currentTrajectoryWithfitness = null;
255 244
256 } 245 }
257 logger.info("Interrupted."); 246 logger.info("Interrupted.");
@@ -269,19 +258,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
269 return activationIds; 258 return activationIds;
270 } 259 }
271 260
272 private void checkForSolution(final Fitness fittness) {
273 if (fittness.isSatisifiesHardObjectives()) {
274 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
275 solutionStoreWithCopy.newSolution(context);
276 solutionStoreWithDiversityDescriptor.newSolution(context);
277 solutionStore.newSolution(context);
278 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
279
280 logger.debug("Found a solution.");
281 }
282 }
283 }
284
285 @Override 261 @Override
286 public void interruptStrategy() { 262 public void interruptStrategy() {
287 isInterrupted = true; 263 isInterrupted = true;
@@ -311,11 +287,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
311 } 287 }
312 288
313 public void visualiseCurrentState() { 289 public void visualiseCurrentState() {
314 PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser; 290 PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser;
315 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) { 291 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) {
316 PartialInterpretation p = (PartialInterpretation) (context.getModel()); 292 PartialInterpretation p = (PartialInterpretation) (context.getModel());
317 int id = ++numberOfPrintedModel; 293 int id = ++numberOfPrintedModel;
318 if (id % configuration.debugCongiguration.partalInterpretationVisualisationFrequency == 0) { 294 if (id % configuration.debugConfiguration.partalInterpretationVisualisationFrequency == 0) {
319 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p); 295 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p);
320 visualisation.writeToFile(workspace, String.format("state%09d.png", id)); 296 visualisation.writeToFile(workspace, String.format("state%09d.png", id));
321 } 297 }
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/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 2489c751..9a33753c 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,11 +1,13 @@
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.reasoner.optimization.IThreeValuedObjective
3import java.util.Comparator 5import java.util.Comparator
4import java.util.List 6import java.util.List
5import org.eclipse.viatra.dse.base.ThreadContext 7import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.dse.objectives.Comparators 8import org.eclipse.viatra.dse.objectives.Comparators
7import org.eclipse.viatra.dse.objectives.IObjective 9import org.eclipse.viatra.dse.objectives.IObjective
8import org.eclipse.viatra.dse.objectives.impl.BaseObjective 10import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
9 11
10//class ViatraReasonerNumbers { 12//class ViatraReasonerNumbers {
11// public static val scopePriority = 2 13// public static val scopePriority = 2
@@ -22,64 +24,66 @@ import org.eclipse.viatra.dse.objectives.impl.BaseObjective
22// public static val compositePriority = 2 24// public static val compositePriority = 2
23//} 25//}
24 26
25class ModelGenerationCompositeObjective implements IObjective{ 27@FinalFieldsConstructor
26 val ScopeObjective scopeObjective 28class ModelGenerationCompositeObjective implements IThreeValuedObjective {
27 val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives 29 val IObjective scopeObjective
28 val UnfinishedWFObjective unfinishedWFObjective 30 val List<IObjective> unfinishedMultiplicityObjectives
29 31 val IObjective unfinishedWFObjective
30 public new( 32
31 ScopeObjective scopeObjective,
32 List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives,
33 UnfinishedWFObjective unfinishedWFObjective)
34 {
35 this.scopeObjective = scopeObjective
36 this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives
37 this.unfinishedWFObjective = unfinishedWFObjective
38 }
39
40 override init(ThreadContext context) { 33 override init(ThreadContext context) {
41 this.scopeObjective.init(context) 34 this.scopeObjective.init(context)
42 this.unfinishedMultiplicityObjectives.forEach[it.init(context)] 35 this.unfinishedMultiplicityObjectives.forEach[it.init(context)]
43 this.unfinishedWFObjective.init(context) 36 this.unfinishedWFObjective.init(context)
44 } 37 }
45 38
46 override createNew() { 39 override createNew() {
47 return new ModelGenerationCompositeObjective( 40 return new ModelGenerationCompositeObjective(
48 this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective) 41 scopeObjective.createNew,
42 ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew]),
43 unfinishedWFObjective.createNew
44 )
49 } 45 }
50 46
51 override getComparator() { Comparators.LOWER_IS_BETTER } 47 override getComparator() { Comparators.LOWER_IS_BETTER }
48
52 override getFitness(ThreadContext context) { 49 override getFitness(ThreadContext context) {
53 var sum = 0.0 50 var sum = 0.0
54 val scopeFitnes = scopeObjective.getFitness(context) 51 val scopeFitnes = scopeObjective.getFitness(context)
55 //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] 52 // val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]
56 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) 53 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)
57 54
58 sum+=scopeFitnes 55 sum += scopeFitnes
59 var multiplicity = 0.0 56 var multiplicity = 0.0
60 for(multiplicityObjective : unfinishedMultiplicityObjectives) { 57 for (multiplicityObjective : unfinishedMultiplicityObjectives) {
61 multiplicity+=multiplicityObjective.getFitness(context)//*0.5 58 multiplicity += multiplicityObjective.getFitness(context) // *0.5
62 } 59 }
63 sum+=multiplicity 60 sum += multiplicity
64 sum += unfinishedWFsFitness//*0.5 61 sum += unfinishedWFsFitness // *0.5
65 62 // println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
66 //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
67
68 return sum 63 return sum
69 } 64 }
70 65
71 override getLevel() { 2 } 66 override getWorstPossibleFitness(ThreadContext threadContext) {
72 override getName() { "CompositeUnfinishednessObjective"} 67 Double.POSITIVE_INFINITY
68 }
73 69
70 override getBestPossibleFitness(ThreadContext threadContext) {
71 0.0
72 }
73
74 override getLevel() { 2 }
75
76 override getName() { "CompositeUnfinishednessObjective" }
77
74 override isHardObjective() { true } 78 override isHardObjective() { true }
79
75 override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } 80 override satisifiesHardObjective(Double fitness) { fitness <= 0.001 }
76 81
77
78 override setComparator(Comparator<Double> comparator) { 82 override setComparator(Comparator<Double> comparator) {
79 throw new UnsupportedOperationException("TODO: auto-generated method stub") 83 throw new UnsupportedOperationException("Model generation objective comparator cannot be set.")
80 } 84 }
85
81 override setLevel(int level) { 86 override setLevel(int level) {
82 throw new UnsupportedOperationException("TODO: auto-generated method stub") 87 throw new UnsupportedOperationException("Model generation objective level cannot be set.")
83 } 88 }
84 89}
85} \ 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/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..d036257d
--- /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,74 @@
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
22class SolutionCopier {
23 val copiedSolutions = new LinkedHashMap<Object, CopiedSolution>
24
25 long startTime = System.nanoTime
26 @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0
27
28 def void copySolution(ThreadContext context, Object solutionId) {
29 val existingCopy = copiedSolutions.get(solutionId)
30 if (existingCopy === null) {
31 val copyStart = System.nanoTime
32 val solution = context.model as PartialInterpretation
33 val copier = new EcoreUtil.Copier
34 val copiedPartialInterpretation = copier.copy(solution) as PartialInterpretation
35 copier.copyReferences
36 totalCopierRuntime += System.nanoTime - copyStart
37 val copierRuntime = System.nanoTime - startTime
38 val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime)
39 copiedSolutions.put(solutionId, copiedSolution)
40 } else {
41 existingCopy.current = true
42 }
43 }
44
45 def void markAsObsolete(Object solutionId) {
46 val copiedSolution = copiedSolutions.get(solutionId)
47 if (copiedSolution === null) {
48 throw new IllegalStateException("No solution to mark as obsolete for state code: " + solutionId)
49 }
50 copiedSolution.current = false
51 }
52
53 def List<PartialInterpretation> getPartialInterpretations(boolean currentOnly) {
54 getListOfCopiedSolutions(currentOnly).map[partialInterpretations]
55 }
56
57 def List<Map<EObject, EObject>> getTraces(boolean currentOnly) {
58 getListOfCopiedSolutions(currentOnly).map[trace]
59 }
60
61 def List<Long> getAllCopierRuntimes(boolean currentOnly) {
62 getListOfCopiedSolutions(currentOnly).map[copierRuntime]
63 }
64
65 def List<CopiedSolution> getListOfCopiedSolutions(boolean currentOnly) {
66 val values = copiedSolutions.values
67 val filteredSolutions = if (currentOnly) {
68 values.filter[current]
69 } else {
70 values
71 }
72 ImmutableList.copyOf(filteredSolutions)
73 }
74}
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
deleted file mode 100644
index a8b7301e..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
+++ /dev/null
@@ -1,52 +0,0 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.List
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import java.util.LinkedList
6import org.eclipse.emf.ecore.EObject
7import java.util.Map
8import org.eclipse.emf.ecore.util.EcoreUtil
9import org.eclipse.viatra.dse.base.ThreadContext
10import java.util.TreeMap
11import java.util.SortedMap
12
13class SolutionStoreWithCopy {
14
15 long runtime = 0
16 List<PartialInterpretation> solutions = new LinkedList
17 //public List<SortedMap<String,Integer>> additionalMatches = new LinkedList
18 List<Map<EObject,EObject>> copyTraces = new LinkedList
19
20 long sartTime = System.nanoTime
21 List<Long> solutionTimes = new LinkedList
22
23 /*def newSolution(ThreadContext context, SortedMap<String,Integer> additonalMatch) {
24 additionalMatches+= additonalMatch
25 newSolution(context)
26 }*/
27
28 def newSolution(ThreadContext context) {
29 //print(System.nanoTime-initTime + ";")
30 val copyStart = System.nanoTime
31 val solution = context.model as PartialInterpretation
32 val copier = new EcoreUtil.Copier
33 val solutionCopy = copier.copy(solution) as PartialInterpretation
34 copier.copyReferences
35 solutions.add(solutionCopy)
36 copyTraces.add(copier)
37 runtime += System.nanoTime - copyStart
38 solutionTimes.add(System.nanoTime-sartTime)
39 }
40 def getSumRuntime() {
41 return runtime
42 }
43 def getAllRuntimes() {
44 return solutionTimes
45 }
46 def getSolutions() {
47 solutions
48 }
49 def getCopyTraces() {
50 return copyTraces
51 }
52} \ 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/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..f54a31ca
--- /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,29 @@
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 if (solutionSaver !== null) {
13 return
14 }
15 }
16
17 override createNew() {
18 this
19 }
20
21 override getName() {
22 class.name
23 }
24
25 override checkGlobalConstraint(ThreadContext context) {
26 val bestFitness = DseUtils.caclulateBestPossibleFitness(context)
27 bestFitness.satisifiesHardObjectives && solutionSaver.fitnessMayBeSaved(bestFitness)
28 }
29}
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 aad9a448..7d0a7884 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
@@ -9,7 +9,7 @@ import org.eclipse.viatra.dse.objectives.Comparators
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
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..6bffeb59
--- /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,137 @@
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 */
18class ViatraReasonerSolutionSaver implements ISolutionSaver {
19 @Accessors val solutionCopier = new SolutionCopier
20 @Accessors val DiversityChecker diversityChecker
21 val boolean hasExtremalObjectives
22 val int numberOfRequiredSolutions
23 val ObjectiveComparatorHelper comparatorHelper
24 val Map<SolutionTrajectory, Fitness> trajectories = new HashMap
25
26 @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection
27
28 new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) {
29 this.diversityChecker = diversityChecker
30 comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives)
31 hasExtremalObjectives = leveledExtremalObjectives.exists[!empty]
32 this.numberOfRequiredSolutions = numberOfRequiredSolutions
33 }
34
35 override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
36 if (hasExtremalObjectives) {
37 saveBestSolutionOnly(context, id, solutionTrajectory)
38 } else {
39 saveAnyDiverseSolution(context, id, solutionTrajectory)
40 }
41 }
42
43 private def saveBestSolutionOnly(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
44 val fitness = context.lastFitness
45 if (!fitness.satisifiesHardObjectives) {
46 return false
47 }
48 val dominatedTrajectories = newArrayList
49 for (entry : trajectories.entrySet) {
50 val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value)
51 if (isLastFitnessBetter < 0) {
52 // Found a trajectory that dominates the current one, no need to save
53 return false
54 }
55 if (isLastFitnessBetter > 0) {
56 dominatedTrajectories += entry.key
57 }
58 }
59 if (dominatedTrajectories.size == 0 && !needsMoreSolutionsWithSameFitness) {
60 return false
61 }
62 if (!diversityChecker.newSolution(context, id, dominatedTrajectories.map[solution.stateCode])) {
63 return false
64 }
65 // We must save the new trajectory before removing dominated trajectories
66 // to avoid removing the current solution when it is reachable only via dominated trajectories.
67 val solutionSaved = basicSaveSolution(context, id, solutionTrajectory, fitness)
68 for (dominatedTrajectory : dominatedTrajectories) {
69 trajectories -= dominatedTrajectory
70 val dominatedSolution = dominatedTrajectory.solution
71 if (!dominatedSolution.trajectories.remove(dominatedTrajectory)) {
72 throw new DSEException(
73 "Dominated solution is not reachable from dominated trajectory. This should never happen!")
74 }
75 if (dominatedSolution.trajectories.empty) {
76 val dominatedSolutionId = dominatedSolution.stateCode
77 solutionCopier.markAsObsolete(dominatedSolutionId)
78 solutionsCollection -= dominatedSolutionId
79 }
80 }
81 solutionSaved
82 }
83
84 private def saveAnyDiverseSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
85 val fitness = context.lastFitness
86 if (!fitness.satisifiesHardObjectives) {
87 return false
88 }
89 if (!diversityChecker.newSolution(context, id, emptyList)) {
90 return false
91 }
92 basicSaveSolution(context, id, solutionTrajectory, fitness)
93 }
94
95 private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, Fitness fitness) {
96 var boolean solutionSaved = false
97 var dseSolution = solutionsCollection.get(id)
98 if (dseSolution === null) {
99 solutionCopier.copySolution(context, id)
100 dseSolution = new Solution(id, solutionTrajectory)
101 solutionsCollection.put(id, dseSolution)
102 solutionSaved = true
103 } else {
104 solutionSaved = dseSolution.trajectories.add(solutionTrajectory)
105 }
106 if (solutionSaved) {
107 solutionTrajectory.solution = dseSolution
108 trajectories.put(solutionTrajectory, fitness)
109 }
110 solutionSaved
111 }
112
113 def fitnessMayBeSaved(Fitness fitness) {
114 if (!hasExtremalObjectives) {
115 return true
116 }
117 var boolean mayDominate
118 for (existingFitness : trajectories.values) {
119 val isNewFitnessBetter = comparatorHelper.compare(fitness, existingFitness)
120 if (isNewFitnessBetter < 0) {
121 return false
122 }
123 if (isNewFitnessBetter > 0) {
124 mayDominate = true
125 }
126 }
127 mayDominate || needsMoreSolutionsWithSameFitness
128 }
129
130 private def boolean needsMoreSolutionsWithSameFitness() {
131 if (solutionsCollection === null) {
132 // The solutions collection will only be initialized upon saving the first solution.
133 return true
134 }
135 solutionsCollection.size < numberOfRequiredSolutions
136 }
137}
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..63d78220 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,35 @@ 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 UNFINISHED_WFS_NAME = "unfinishedWFs"
17 static val INVALIDATED_WFS_NAME = "invalidatedWFs"
18
16 def createCompletenessObjective( 19 def createCompletenessObjective(
17 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) 20 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) {
18 { 21 // createConstraintObjective(UNFINISHED_WFS_NAME, unfinishedWF)
19 val res = new ConstraintsObjective('''unfinishedWFs''', 22 new UnfinishedWFObjective(unfinishedWF)
20 unfinishedWF.map[ 23 }
21 new QueryConstraint(it.fullyQualifiedName,it,2.0) 24
22 ].toList 25 def createInvalidationObjective(
26 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {
27 createConstraintObjective(INVALIDATED_WFS_NAME, invalidatedByWF)
28 }
29
30 def IGlobalConstraint createInvalidationGlobalConstraint(
31 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {
32 new ModelQueriesGlobalConstraint(INVALIDATED_WFS_NAME, new ArrayList(invalidatedByWF))
33 }
34
35 private def createConstraintObjective(String name,
36 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries) {
37 val res = new ConstraintsObjective(
38 name,
39 ImmutableList.copyOf(queries.map [
40 new QueryConstraint(it.fullyQualifiedName, it, 1.0)
41 ])
23 ) 42 )
24 res.withComparator(Comparators.LOWER_IS_BETTER) 43 res.withComparator(Comparators.LOWER_IS_BETTER)
25 res.level = 2 44 res.level = 2
26 return res 45 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 } 46 }
36} \ No newline at end of file 47}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-17 01:51:28 +0000