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.java372
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend85
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend30
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend41
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend35
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend77
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend37
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend56
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend36
9 files changed, 769 insertions, 0 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
new file mode 100644
index 00000000..5a6fee2c
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
@@ -0,0 +1,372 @@
1/*******************************************************************************
2 * Copyright (c) 2010-2017, Andras Szabolcs Nagy and Daniel Varro
3 * All rights reserved. This program and the accompanying materials
4 * are made available under the terms of the Eclipse Public License v1.0
5 * which accompanies this distribution, and is available at
6 * http://www.eclipse.org/legal/epl-v10.html
7 * Contributors:
8 * Andras Szabolcs Nagy - initial API and implementation
9 *******************************************************************************/
10package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse;
11
12import java.util.ArrayList;
13import java.util.Arrays;
14import java.util.Collections;
15import java.util.Comparator;
16import java.util.Iterator;
17import java.util.List;
18import java.util.PriorityQueue;
19import java.util.Random;
20
21import org.apache.log4j.Logger;
22import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy;
23import org.eclipse.viatra.dse.base.ThreadContext;
24import org.eclipse.viatra.dse.objectives.Fitness;
25import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper;
26import org.eclipse.viatra.dse.solutionstore.SolutionStore;
27
28import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner;
29import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
30import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
31import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
32import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
33import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml;
34import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor;
35import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
36
37/**
38 * This exploration strategy eventually explorers the whole design space but goes in the most promising directions
39 * first, based on the {@link Fitness}.
40 *
41 * There are a few parameter to tune such as
42 * <ul>
43 * <li>maximum depth</li>
44 * <li>continue the exploration from a state that satisfies the hard objectives (the default that it will
45 * backtrack),</li>
46 * <li>whether to continue the exploration from the newly explored state if it is at least equally good than the
47 * previous one or only if it is better (default is "at least equally good").</li>
48 * </ul>
49 *
50 * @author Andras Szabolcs Nagy
51 *
52 */
53public class BestFirstStrategyForModelGeneration implements IStrategy {
54
55 private ThreadContext context;
56 private SolutionStore solutionStore;
57 private SolutionStoreWithCopy solutionStoreWithCopy;
58 private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor;
59 private int numberOfStatecoderFail=0;
60
61 private int maxDepth = Integer.MAX_VALUE;
62 private boolean isInterrupted = false;
63 //private boolean backTrackIfSolution = true;
64 private boolean onlyBetterFirst = false;
65
66 private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore;
67 private Logger logger = Logger.getLogger(IStrategy.class);
68
69 private static class TrajectoryWithFitness {
70
71 public Object[] trajectory;
72 public Fitness fitness;
73
74 public TrajectoryWithFitness(Object[] trajectory, Fitness fitness) {
75 super();
76 this.trajectory = trajectory;
77 this.fitness = fitness;
78 }
79
80 @Override
81 public String toString() {
82 return Arrays.toString(trajectory) + fitness.toString();
83 }
84
85 }
86
87 public BestFirstStrategyForModelGeneration(ReasonerWorkspace workspace, LogicReasoner reasoner, LogicSolverConfiguration configuration, DiversityDescriptor descriptor) {
88 this.maxDepth = Integer.MAX_VALUE;
89 this.workspace = workspace;
90 this.reasoner = reasoner;
91 this.configuration = configuration;
92 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(descriptor);
93 }
94
95 @Override
96 public void initStrategy(ThreadContext context) {
97 this.context = context;
98 this.solutionStore = context.getGlobalContext().getSolutionStore();
99 this.solutionStoreWithCopy = new SolutionStoreWithCopy();
100
101
102 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
103
104 Comparator<TrajectoryWithFitness> comparator = new Comparator<BestFirstStrategyForModelGeneration.TrajectoryWithFitness>() {
105
106 @Override
107 public int compare(TrajectoryWithFitness o1, TrajectoryWithFitness o2) {
108 return objectiveComparatorHelper.compare(o2.fitness, o1.fitness);
109 }
110 };
111
112 trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator);
113
114 }
115
116 public SolutionStoreWithCopy getSolutionStoreWithCopy() {
117 return solutionStoreWithCopy;
118 }
119
120 public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
121 return solutionStoreWithDiversityDescriptor;
122 }
123
124 public int getNumberOfStatecoderFaiL() {
125 return numberOfStatecoderFail;
126 }
127
128 @Override
129 public void explore() {
130 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
131
132 boolean globalConstraintsAreSatisfied = context.checkGlobalConstraints();
133 if (!globalConstraintsAreSatisfied) {
134 logger.info("Global contraint is not satisifed in the first state. Terminate.");
135 return;
136 }
137
138 final Fitness firstFittness = context.calculateFitness();
139 if (firstFittness.isSatisifiesHardObjectives()) {
140 context.newSolution();
141 logger.info("First state is a solution. Terminate.");
142 return;
143 }
144
145 if (maxDepth == 0) {
146 return;
147 }
148
149 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
150 TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness);
151 trajectoiresToExplore.add(currentTrajectoryWithFittness);
152
153 mainLoop: while (!isInterrupted) {
154
155 if (currentTrajectoryWithFittness == null) {
156 if (trajectoiresToExplore.isEmpty()) {
157 logger.debug("State space is fully traversed.");
158 return;
159 } else {
160 currentTrajectoryWithFittness = selectRandomState();// trajectoiresToExplore.element();
161 if (logger.isDebugEnabled()) {
162 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
163 logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness);
164 }
165// context.backtrackUntilRoot();
166// context.executeTrajectoryWithoutStateCoding(currentTrajectoryWithFittness.trajectory);
167 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory);
168 }
169
170 }
171
172 List<Object> activationIds;
173 try {
174 activationIds = new ArrayList<Object>(context.getUntraversedActivationIds());
175 Collections.shuffle(activationIds);
176 } catch (NullPointerException e) {
177 numberOfStatecoderFail++;
178 activationIds = Collections.emptyList();
179 }
180
181 Iterator<Object> iterator = activationIds.iterator();
182
183// writeCurrentState();
184// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness);
185// if(consistencyCheckResult == true) {
186// continue mainLoop;
187// }
188
189 while (!isInterrupted && iterator.hasNext()) {
190 final Object nextActivation = iterator.next();
191 if (!iterator.hasNext()) {
192 logger.debug("Last untraversed activation of the state.");
193 trajectoiresToExplore.remove(currentTrajectoryWithFittness);
194 }
195
196 if (logger.isDebugEnabled()) {
197 logger.debug("Executing new activation: " + nextActivation);
198 }
199 context.executeAcitvationId(nextActivation);
200
201// writeCurrentState();
202
203 if (context.isCurrentStateAlreadyTraversed()) {
204 logger.info("The new state is already visited.");
205 context.backtrack();
206 } else if (!context.checkGlobalConstraints()) {
207 logger.debug("Global contraint is not satisifed.");
208 context.backtrack();
209 } else {
210 final Fitness nextFitness = context.calculateFitness();
211 if (nextFitness.isSatisifiesHardObjectives()) {
212 if(solutionStoreWithDiversityDescriptor.isDifferent(context)) {
213 solutionStoreWithCopy.newSolution(context);
214 solutionStoreWithDiversityDescriptor.newSolution(context);
215 solutionStore.newSolution(context);
216 logger.debug("Found a solution.");
217 }
218 }
219 if (context.getDepth() > maxDepth) {
220 logger.debug("Reached max depth.");
221 context.backtrack();
222 continue;
223 }
224
225 TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness(
226 context.getTrajectory().toArray(), nextFitness);
227 trajectoiresToExplore.add(nextTrajectoryWithFittness);
228
229 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness,
230 nextTrajectoryWithFittness.fitness);
231 if (compare < 0) {
232 logger.debug("Better fitness, moving on: " + nextFitness);
233 currentTrajectoryWithFittness = nextTrajectoryWithFittness;
234 continue mainLoop;
235 } else if (compare == 0) {
236 if (onlyBetterFirst) {
237 logger.debug("Equally good fitness, backtrack: " + nextFitness);
238 context.backtrack();
239 continue;
240 } else {
241 logger.debug("Equally good fitness, moving on: " + nextFitness);
242 currentTrajectoryWithFittness = nextTrajectoryWithFittness;
243 continue mainLoop;
244 }
245 } else {
246 logger.debug("Worse fitness.");
247// context.backtrack();
248 currentTrajectoryWithFittness = null;
249 continue mainLoop;
250 }
251 }
252 }
253
254 logger.debug("State is fully traversed.");
255 trajectoiresToExplore.remove(currentTrajectoryWithFittness);
256 currentTrajectoryWithFittness = null;
257
258 }
259 logger.info("Interrupted.");
260 }
261
262 @Override
263 public void interruptStrategy() {
264 isInterrupted = true;
265 }
266
267 Random random = new Random();
268 private TrajectoryWithFitness selectRandomState() {
269 int randomNumber = random.nextInt(100);
270 if(randomNumber < 5) {
271 int elements = trajectoiresToExplore.size();
272 int randomElementIndex = random.nextInt(elements);
273 logger.debug("Randomly backtract to the " + randomElementIndex + " best solution...");
274 Iterator<TrajectoryWithFitness> iterator = trajectoiresToExplore.iterator();
275 while(randomElementIndex!=0) {
276 iterator.next();
277 randomElementIndex--;
278 }
279 TrajectoryWithFitness res = iterator.next();
280 if(res == null) {
281 return trajectoiresToExplore.element();
282 } else {
283 return res;
284 }
285 } else {
286 return trajectoiresToExplore.element();
287 }
288 }
289
290 private PartialInterpretation2Logic partialInterpretation2Logic = new PartialInterpretation2Logic();
291 private LogicReasoner reasoner;
292 private PartialInterpretation2Gml partialInterpretation2Gml = new PartialInterpretation2Gml();
293 private ReasonerWorkspace workspace;
294 private LogicSolverConfiguration configuration;
295 int numberOfPrintedModel = 0;
296 public ModelResult modelResultByTheSolver = null;
297 public void writeCurrentState() {
298 PartialInterpretation p = (PartialInterpretation)(context.getModel());
299 int id= ++numberOfPrintedModel;
300 if(id%100 == 1) {
301 String text = this.partialInterpretation2Gml.transform(p);
302 this.workspace.writeText(id+".gml", text);
303 this.workspace.writeModel(p, id+".partialinterpretation");
304 logger.debug("State "+id+" is saved.");
305 }
306 }
307
308// int numberOfSolverCalls = 0;
309//
310// protected boolean checkConsistency(TrajectoryWithFitness t) {
311// if (reasoner != null) {
312// int id = ++numberOfSolverCalls;
313// if (id % 100 == 1) {
314// try {
315// PartialInterpretation interpretation = (PartialInterpretation) (context.getModel());
316// PartialInterpretation copied = EcoreUtil.copy(interpretation);
317// this.partialInterpretation2Logic.transformPartialIntepretation2Logic(copied.getProblem(), copied);
318// LogicProblem newProblem = copied.getProblem();
319//
320// this.configuration.typeScopes.maxNewElements = interpretation.getMaxNewElements();
321// this.configuration.typeScopes.minNewElements = interpretation.getMinNewElements();
322// LogicResult result = reasoner.solve(newProblem, configuration, workspace);
323// if (result instanceof InconsistencyResult) {
324// logger.debug("Solver found an Inconsistency!");
325// removeSubtreeFromQueue(t);
326// return true;
327// } else if (result instanceof ModelResult) {
328// logger.debug("Solver found a model!");
329// solutionStore.newSolution(context);
330
331// modelResultByTheSolver = (ModelResult) result;
332// return true;
333// } else {
334// logger.debug("Failed consistency check.");
335// return false;
336// }
337// } catch (Exception e) {
338// // TODO Auto-generated catch block
339// e.printStackTrace();
340// return false;
341// }
342// }
343//
344// }
345// return false;
346// }
347//
348// protected void removeSubtreeFromQueue(TrajectoryWithFitness t) {
349// PriorityQueue<TrajectoryWithFitness> previous = this.trajectoiresToExplore;
350// this.trajectoiresToExplore = new PriorityQueue<>(this.comparator);
351// for (TrajectoryWithFitness trajectoryWithFitness : previous) {
352// if(! containsAsSubstring(trajectoryWithFitness.trajectory,t.trajectory)) {
353// this.trajectoiresToExplore.add(trajectoryWithFitness);
354// } else {
355// logger.debug("State has been excluded due to inherent inconsistency");
356// }
357// }
358// }
359//
360// private boolean containsAsSubstring(Object[] full, Object[] substring) {
361// if(substring.length > full.length) {
362// return false;
363// } else if(substring.length == full.length) {
364// return Arrays.equals(full, substring);
365// } else {
366// Object[] part = Arrays.copyOfRange(full, 0, substring.length);
367// return Arrays.equals(part, substring);
368// }
369// }
370//
371
372}
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
new file mode 100644
index 00000000..1ca2343f
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend
@@ -0,0 +1,85 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.Comparator
4import java.util.List
5import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.dse.objectives.Comparators
7import org.eclipse.viatra.dse.objectives.IObjective
8import org.eclipse.viatra.dse.objectives.impl.BaseObjective
9
10//class ViatraReasonerNumbers {
11// public static val scopePriority = 2
12// public static val unfinishedMultiplicityPriority = 2
13// public static val unifinshedWFPriority = 2
14// //public static val complexityPriority = 4
15//
16// public static val scopeWeigth = 1.0
17// public static val unfinishedMultiplicityWeigth = 1.5
18// public static val unfinishedWFWeigth = 1.5
19// //public static val complexityWeigth = 0.1
20//
21// public static val useCompositeObjective = true
22// public static val compositePriority = 2
23//}
24
25class ModelGenerationCompositeObjective implements IObjective{
26 val ScopeObjective scopeObjective
27 val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives
28 val UnfinishedWFObjective unfinishedWFObjective
29
30 public new(
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) {
41 this.scopeObjective.init(context)
42 this.unfinishedMultiplicityObjectives.forEach[it.init(context)]
43 this.unfinishedWFObjective.init(context)
44 }
45
46 override createNew() {
47 return new ModelGenerationCompositeObjective(
48 this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective)
49 }
50
51 override getComparator() { Comparators.LOWER_IS_BETTER }
52 override getFitness(ThreadContext context) {
53 var sum = 0.0
54 val scopeFitnes = scopeObjective.getFitness(context)
55 //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]
56 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)
57
58 sum+=scopeFitnes
59 var multiplicity = 0.0
60 for(multiplicityObjective : unfinishedMultiplicityObjectives) {
61 multiplicity+=multiplicityObjective.getFitness(context)//*0.5
62 }
63 sum+=multiplicity
64 sum += unfinishedWFsFitness//*0.5
65
66// println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
67
68 return sum
69 }
70
71 override getLevel() { 2 }
72 override getName() { "CompositeUnfinishednessObjective"}
73
74 override isHardObjective() { true }
75 override satisifiesHardObjective(Double fitness) { fitness <= 0.001 }
76
77
78 override setComparator(Comparator<Double> comparator) {
79 throw new UnsupportedOperationException("TODO: auto-generated method stub")
80 }
81 override setLevel(int level) {
82 throw new UnsupportedOperationException("TODO: auto-generated method stub")
83 }
84
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/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
new file mode 100644
index 00000000..b2a7e3f5
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend
@@ -0,0 +1,30 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
8
9class PartialModelAsLogicInterpretation implements LogicModelInterpretation{
10
11
12 override getElements(Type type) {
13 throw new UnsupportedOperationException("TODO: auto-generated method stub")
14 }
15
16 override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
17 throw new UnsupportedOperationException("TODO: auto-generated method stub")
18 }
19
20 override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
21 throw new UnsupportedOperationException("TODO: auto-generated method stub")
22 }
23
24 override getInterpretation(ConstantDeclaration constant) {
25 throw new UnsupportedOperationException("TODO: auto-generated method stub")
26 }
27
28 override getMinimalInteger() { 0 }
29 override getMaximalInteger() {0 }
30} \ 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/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
new file mode 100644
index 00000000..d3497ef2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
@@ -0,0 +1,41 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import org.eclipse.viatra.dse.objectives.IObjective
4import org.eclipse.viatra.dse.base.ThreadContext
5import java.util.Comparator
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
7
8class ScopeObjective implements IObjective{
9 static val comparator = new Comparator<Double>() {
10 override compare(Double o1, Double o2) {
11
12 return o2.compareTo(o1)
13 }
14 }
15
16 //val static scopeLevel = 3
17
18 override createNew() { return new ScopeObjective }
19 override getName() { '''ScopeConstraint''' }
20 override init(ThreadContext context) { }
21
22 override getComparator() { comparator }
23
24 override getFitness(ThreadContext context) {
25 val interpretation = context.model as PartialInterpretation
26 val res = interpretation.minNewElements
27 return res.doubleValue
28 }
29
30 override isHardObjective() { true }
31 override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }
32
33 override setComparator(Comparator<Double> comparator) {
34 throw new UnsupportedOperationException("TODO: auto-generated method stub")
35 }
36
37 override setLevel(int level) {
38 throw new UnsupportedOperationException("TODO: auto-generated method stub")
39 }
40 override getLevel() { 2 }
41} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
new file mode 100644
index 00000000..2892723b
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend
@@ -0,0 +1,35 @@
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
10
11class SolutionStoreWithCopy {
12 long runtime = 0
13 List<PartialInterpretation> solutions = new LinkedList
14 List<Map<EObject,EObject>> copyTraces = new LinkedList
15
16 long initTime = System.nanoTime
17
18 def newSolution(ThreadContext context) {
19 //print(System.nanoTime-initTime + ";")
20 val copyStart = System.nanoTime
21 val solution = context.model as PartialInterpretation
22 val copier = new EcoreUtil.Copier
23 val solutionCopy = copier.copy(solution) as PartialInterpretation
24 copier.copyReferences
25 solutions.add(solutionCopy)
26 copyTraces.add(copier)
27 runtime += System.nanoTime - copyStart
28 }
29 def getSumRuntime() {
30 return runtime
31 }
32 def getSolutions() {
33 solutions
34 }
35} \ 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
new file mode 100644
index 00000000..ca39cada
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend
@@ -0,0 +1,77 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.NeighbourhoodWithTraces
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
7import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
8import java.util.LinkedList
9import java.util.List
10import java.util.Map
11import org.eclipse.viatra.dse.base.ThreadContext
12
13class SolutionStoreWithDiversityDescriptor {
14 val DiversityDescriptor descriptor
15 val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice
16 val List<NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor>> solutionCodeList = new LinkedList
17
18 var long runtime
19 var int allCheck
20 var int successfulCheck
21
22 public new(DiversityDescriptor descriptor) {
23 this.descriptor = descriptor
24 }
25
26 def public isActive() {
27 descriptor!==null
28 }
29
30 def getSumRuntime() {
31 return runtime
32 }
33 def getSuccessRate() {
34 return successfulCheck as double / allCheck
35 }
36
37 def isDifferent(ThreadContext context) {
38 if(active) {
39 val start = System.nanoTime
40 val model = context.model as PartialInterpretation
41 val code = solutionCoder.createRepresentation(model,
42 descriptor.range,
43 descriptor.parallels,
44 descriptor.maxNumber,
45 descriptor.relevantTypes,
46 descriptor.relevantRelations)
47 val isDifferent = solutionCodeList.forall[previous | ! code.equals(previous)]
48 runtime += System.nanoTime - start
49 allCheck++
50 if(isDifferent) { successfulCheck++ }
51 return isDifferent
52 } else {
53 allCheck++
54 successfulCheck++
55 return true
56 }
57 }
58
59 def canBeDifferent(ThreadContext context) {
60 return true
61 }
62
63 def newSolution(ThreadContext context) {
64 if(active) {
65 val start = System.nanoTime
66 val model = context.model as PartialInterpretation
67 val code = solutionCoder.createRepresentation(model,
68 descriptor.range,
69 descriptor.parallels,
70 descriptor.maxNumber,
71 descriptor.relevantTypes,
72 descriptor.relevantRelations)
73 solutionCodeList += code
74 runtime += System.nanoTime - start
75 }
76 }
77} \ 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/UnfinishedMultiplicityObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
new file mode 100644
index 00000000..aad9a448
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend
@@ -0,0 +1,37 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator
4import java.util.Comparator
5import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.dse.objectives.IObjective
7import org.eclipse.viatra.dse.objectives.Comparators
8
9class UnfinishedMultiplicityObjective implements IObjective {
10 val MultiplicityGoalConstraintCalculator unfinishedMultiplicity;
11
12 public new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) {
13 this.unfinishedMultiplicity = unfinishedMultiplicity
14 }
15
16 override getName() '''unfinishedMultiplicity «unfinishedMultiplicity.name»'''
17 override createNew() {
18 return new UnfinishedMultiplicityObjective(new MultiplicityGoalConstraintCalculator(this.unfinishedMultiplicity))
19 }
20
21 override getComparator() { Comparators.LOWER_IS_BETTER }
22 override getFitness(ThreadContext context) {
23 val unfinishedMultiplicity = unfinishedMultiplicity.calculateValue
24 return unfinishedMultiplicity.doubleValue
25 }
26 override getLevel() { 2 }
27 override init(ThreadContext context) { unfinishedMultiplicity.init(context.model) }
28 override isHardObjective() { true }
29 override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }
30
31 override setComparator(Comparator<Double> comparator) {
32 throw new UnsupportedOperationException("TODO: auto-generated method stub")
33 }
34 override setLevel(int level) {
35 throw new UnsupportedOperationException("TODO: auto-generated method stub")
36 }
37} \ 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/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
new file mode 100644
index 00000000..0fd20fa3
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
@@ -0,0 +1,56 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import org.eclipse.viatra.dse.objectives.IObjective
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
8import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
9import org.eclipse.viatra.query.runtime.emf.EMFScope
10import org.eclipse.viatra.dse.base.ThreadContext
11import java.util.List
12import org.eclipse.viatra.dse.objectives.Comparators
13import java.util.ArrayList
14import java.util.Comparator
15
16class UnfinishedWFObjective implements IObjective {
17 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs
18 val List<ViatraQueryMatcher<?>> matchers
19
20 public new(Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) {
21 this.unfinishedWFs = unfinishedWFs
22 matchers = new ArrayList(unfinishedWFs.size)
23 }
24 override getName() '''unfinishedWFs'''
25 override createNew() {
26 return new UnfinishedWFObjective(unfinishedWFs)
27 }
28 override init(ThreadContext context) {
29 val engine = context.queryEngine//ViatraQueryEngine.on(new EMFScope(context.model))
30 for(unfinishedWF : unfinishedWFs) {
31 matchers += unfinishedWF.getMatcher(engine)
32 }
33 }
34
35 override getComparator() { Comparators.LOWER_IS_BETTER }
36 override getFitness(ThreadContext context) {
37 var sumOfMatches = 0
38 for(matcher : matchers) {
39 val number = matcher.countMatches
40// println('''«matcher.patternName» = «number»''')
41 sumOfMatches+=number
42 }
43 return sumOfMatches.doubleValue
44 }
45
46 override getLevel() { 2 }
47 override isHardObjective() { true }
48 override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }
49
50 override setComparator(Comparator<Double> comparator) {
51 throw new UnsupportedOperationException("TODO: auto-generated method stub")
52 }
53 override setLevel(int level) {
54 throw new UnsupportedOperationException("TODO: auto-generated method stub")
55 }
56} \ 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/WF2ObjectiveConverter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
new file mode 100644
index 00000000..4fd297ca
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend
@@ -0,0 +1,36 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.ArrayList
4import java.util.Collection
5import org.eclipse.viatra.dse.objectives.Comparators
6import org.eclipse.viatra.dse.objectives.IGlobalConstraint
7import org.eclipse.viatra.dse.objectives.impl.ConstraintsObjective
8import org.eclipse.viatra.dse.objectives.impl.ConstraintsObjective.QueryConstraint
9import org.eclipse.viatra.dse.objectives.impl.ModelQueriesGlobalConstraint
10import org.eclipse.viatra.query.runtime.api.IPatternMatch
11import org.eclipse.viatra.query.runtime.api.IQuerySpecification
12import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
13
14class WF2ObjectiveConverter {
15
16 def createCompletenessObjective(
17 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF)
18 {
19 val res = new ConstraintsObjective('''unfinishedWFs''',
20 unfinishedWF.map[
21 new QueryConstraint(it.fullyQualifiedName,it,1.0)
22 ].toList
23 )
24 res.withComparator(Comparators.LOWER_IS_BETTER)
25 res.level = 2
26 return 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 }
36} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-08 17:34:02 +0000