diff options
author | 2020-06-25 19:55:10 +0200 | |
---|---|---|
committer | 2020-06-25 19:55:10 +0200 | |
commit | c3a6d4b9cf3657070d180aa65ddbf0459e880329 (patch) | |
tree | 780c4fc61578dcb309af53fb0c164c7627e51676 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse | |
parent | New configuration language parser WIP (diff) | |
parent | Scope unsat benchmarks (diff) | |
download | VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.gz VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.zst VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.zip |
Merge branch 'kris'
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse')
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | ||
6 | import java.util.Comparator | ||
7 | import java.util.List | ||
8 | import org.eclipse.viatra.dse.base.ThreadContext | ||
9 | import org.eclipse.viatra.dse.objectives.Comparators | ||
10 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | ||
11 | import org.eclipse.viatra.dse.objectives.IObjective | ||
12 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
13 | |||
14 | class 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 | *******************************************************************************/ |
10 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse; | 10 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse; |
11 | 11 | ||
12 | import java.io.BufferedReader; | ||
13 | import java.io.IOException; | ||
14 | import java.io.InputStreamReader; | ||
15 | import java.util.ArrayList; | ||
16 | import java.util.Arrays; | 12 | import java.util.Arrays; |
17 | import java.util.Collection; | ||
18 | import java.util.Collections; | 13 | import java.util.Collections; |
19 | import java.util.Comparator; | 14 | import java.util.Comparator; |
20 | import java.util.Iterator; | 15 | import java.util.Iterator; |
21 | import java.util.LinkedList; | 16 | import java.util.LinkedList; |
22 | import java.util.List; | 17 | import java.util.List; |
23 | import java.util.Map; | ||
24 | import java.util.PriorityQueue; | 18 | import java.util.PriorityQueue; |
25 | import java.util.Random; | 19 | import java.util.Random; |
26 | 20 | ||
27 | import org.apache.log4j.Logger; | 21 | import org.apache.log4j.Logger; |
28 | import org.eclipse.emf.ecore.EObject; | 22 | import org.eclipse.emf.ecore.EObject; |
29 | import org.eclipse.emf.ecore.util.EcoreUtil; | 23 | import org.eclipse.emf.ecore.util.EcoreUtil; |
24 | import org.eclipse.viatra.dse.api.SolutionTrajectory; | ||
30 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; | 25 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; |
31 | import org.eclipse.viatra.dse.base.ThreadContext; | 26 | import org.eclipse.viatra.dse.base.ThreadContext; |
32 | import org.eclipse.viatra.dse.objectives.Fitness; | 27 | import org.eclipse.viatra.dse.objectives.Fitness; |
33 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; | 28 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; |
29 | import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler; | ||
34 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; | 30 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; |
35 | import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine; | ||
36 | import org.eclipse.viatra.query.runtime.api.IPatternMatch; | ||
37 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; | ||
38 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine; | ||
39 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher; | ||
40 | 31 | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 32 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
42 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | 33 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; |
@@ -44,7 +35,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | |||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; | 35 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; |
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 36 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 37 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
47 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver; | ||
48 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; | 38 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; |
49 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; | 39 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; |
50 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; | 40 | import 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import com.google.common.collect.HashMultiset | ||
4 | import com.google.common.collect.ImmutableSet | ||
5 | import com.google.common.collect.Multiset | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.NeighbourhoodWithTraces | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
11 | import java.util.Collection | ||
12 | import java.util.HashSet | ||
13 | import java.util.Map | ||
14 | import java.util.Set | ||
15 | import org.eclipse.viatra.dse.base.ThreadContext | ||
16 | import org.eclipse.xtend.lib.annotations.Accessors | ||
17 | |||
18 | interface 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 | |||
54 | abstract 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 | |||
101 | class 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 | |||
144 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective | ||
4 | import org.eclipse.viatra.dse.base.ThreadContext | ||
5 | import org.eclipse.viatra.dse.objectives.Comparators | ||
6 | import org.eclipse.viatra.dse.objectives.Fitness | ||
7 | import org.eclipse.viatra.dse.objectives.IObjective | ||
8 | |||
9 | final 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | ||
4 | import org.eclipse.viatra.dse.base.ThreadContext | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
6 | |||
7 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
4 | import org.apache.log4j.Logger | ||
5 | import org.eclipse.viatra.dse.api.SolutionTrajectory | ||
6 | import org.eclipse.viatra.dse.base.ThreadContext | ||
7 | import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler | ||
8 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
9 | |||
10 | @FinalFieldsConstructor | ||
11 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective | ||
3 | import java.util.Comparator | 7 | import java.util.Comparator |
4 | import java.util.List | 8 | import java.util.List |
5 | import org.eclipse.viatra.dse.base.ThreadContext | 9 | import org.eclipse.viatra.dse.base.ThreadContext |
6 | import org.eclipse.viatra.dse.objectives.Comparators | 10 | import org.eclipse.viatra.dse.objectives.Comparators |
7 | import org.eclipse.viatra.dse.objectives.IObjective | 11 | import org.eclipse.viatra.dse.objectives.IObjective |
8 | import org.eclipse.viatra.dse.objectives.impl.BaseObjective | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
11 | 12 | ||
12 | //class ViatraReasonerNumbers { | 13 | class 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 | |||
27 | class 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 | |||
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | 21 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint |
22 | 22 | ||
23 | class NumericSolver { | 23 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import java.util.LinkedHashMap | ||
6 | import java.util.List | ||
7 | import java.util.Map | ||
8 | import org.eclipse.emf.ecore.EObject | ||
9 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
10 | import org.eclipse.viatra.dse.base.ThreadContext | ||
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
13 | |||
14 | @FinalFieldsConstructor | ||
15 | class 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 | */ | ||
28 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import java.util.List | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
5 | import java.util.LinkedList | 4 | import java.util.LinkedList |
6 | import org.eclipse.emf.ecore.EObject | 5 | import java.util.List |
7 | import java.util.Map | 6 | import java.util.Map |
7 | import org.eclipse.emf.ecore.EObject | ||
8 | import org.eclipse.emf.ecore.util.EcoreUtil | 8 | import org.eclipse.emf.ecore.util.EcoreUtil |
9 | import org.eclipse.viatra.dse.base.ThreadContext | 9 | import org.eclipse.viatra.dse.base.ThreadContext |
10 | import java.util.TreeMap | ||
11 | import java.util.SortedMap | ||
12 | 10 | ||
13 | class SolutionStoreWithCopy { | 11 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
6 | import java.util.LinkedList | ||
7 | import java.util.List | ||
8 | import org.eclipse.viatra.dse.base.ThreadContext | ||
9 | import java.util.HashSet | ||
10 | import java.util.Set | ||
11 | |||
12 | enum DiversityGranularity { | ||
13 | Nodewise, Graphwise | ||
14 | } | ||
15 | |||
16 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import org.eclipse.viatra.dse.base.ThreadContext | ||
4 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | ||
5 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
6 | |||
7 | @FinalFieldsConstructor | ||
8 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator |
4 | import java.util.Comparator | 4 | import java.util.Comparator |
5 | import org.eclipse.viatra.dse.base.ThreadContext | 5 | import org.eclipse.viatra.dse.base.ThreadContext |
6 | import org.eclipse.viatra.dse.objectives.IObjective | ||
7 | import org.eclipse.viatra.dse.objectives.Comparators | 6 | import org.eclipse.viatra.dse.objectives.Comparators |
7 | import org.eclipse.viatra.dse.objectives.IObjective | ||
8 | 8 | ||
9 | class UnfinishedMultiplicityObjective implements IObjective { | 9 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import org.eclipse.viatra.dse.objectives.IObjective | 3 | import java.util.ArrayList |
4 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
5 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
6 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
7 | import java.util.Collection | 4 | import java.util.Collection |
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 5 | import java.util.Comparator |
9 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
10 | import org.eclipse.viatra.dse.base.ThreadContext | ||
11 | import java.util.List | 6 | import java.util.List |
7 | import org.eclipse.viatra.dse.base.ThreadContext | ||
12 | import org.eclipse.viatra.dse.objectives.Comparators | 8 | import org.eclipse.viatra.dse.objectives.Comparators |
13 | import java.util.ArrayList | 9 | import org.eclipse.viatra.dse.objectives.IObjective |
14 | import java.util.Comparator | 10 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
11 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
12 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
15 | 13 | ||
16 | class UnfinishedWFObjective implements IObjective { | 14 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.HashMap | ||
4 | import java.util.Map | ||
5 | import org.eclipse.viatra.dse.api.DSEException | ||
6 | import org.eclipse.viatra.dse.api.Solution | ||
7 | import org.eclipse.viatra.dse.api.SolutionTrajectory | ||
8 | import org.eclipse.viatra.dse.base.ThreadContext | ||
9 | import org.eclipse.viatra.dse.objectives.Fitness | ||
10 | import org.eclipse.viatra.dse.objectives.IObjective | ||
11 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper | ||
12 | import org.eclipse.viatra.dse.solutionstore.SolutionStore.ISolutionSaver | ||
13 | import 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 | */ | ||
21 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
3 | import java.util.ArrayList | 4 | import java.util.ArrayList |
4 | import java.util.Collection | 5 | import java.util.Collection |
5 | import org.eclipse.viatra.dse.objectives.Comparators | 6 | import org.eclipse.viatra.dse.objectives.Comparators |
@@ -12,25 +13,33 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification | |||
12 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 13 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
13 | 14 | ||
14 | class WF2ObjectiveConverter { | 15 | class 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 | } |