diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu')
6 files changed, 190 insertions, 58 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index bafe78f6..df3ccee5 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | |||
@@ -82,7 +82,8 @@ class ViatraReasoner extends LogicReasoner{ | |||
82 | dse.addObjective(new ModelGenerationCompositeObjective( | 82 | dse.addObjective(new ModelGenerationCompositeObjective( |
83 | new ScopeObjective, | 83 | new ScopeObjective, |
84 | method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], | 84 | method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], |
85 | new UnfinishedWFObjective(method.unfinishedWF) | 85 | new UnfinishedWFObjective(method.unfinishedWF), |
86 | viatraConfig | ||
86 | )) | 87 | )) |
87 | 88 | ||
88 | dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF)) | 89 | dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF)) |
@@ -113,8 +114,9 @@ class ViatraReasoner extends LogicReasoner{ | |||
113 | 114 | ||
114 | val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) | 115 | val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) |
115 | viatraConfig.progressMonitor.workedForwardTransformation | 116 | viatraConfig.progressMonitor.workedForwardTransformation |
117 | val transformationFinished = System.nanoTime | ||
118 | val transformationTime = transformationFinished - transformationStartTime | ||
116 | 119 | ||
117 | val transformationTime = System.nanoTime - transformationStartTime | ||
118 | val solverStartTime = System.nanoTime | 120 | val solverStartTime = System.nanoTime |
119 | 121 | ||
120 | var boolean stoppedByTimeout | 122 | var boolean stoppedByTimeout |
@@ -136,10 +138,19 @@ class ViatraReasoner extends LogicReasoner{ | |||
136 | it.transformationTime = (transformationTime/1000000) as int | 138 | it.transformationTime = (transformationTime/1000000) as int |
137 | for(x : 0..<strategy.solutionStoreWithCopy.allRuntimes.size) { | 139 | for(x : 0..<strategy.solutionStoreWithCopy.allRuntimes.size) { |
138 | it.entries += createIntStatisticEntry => [ | 140 | it.entries += createIntStatisticEntry => [ |
139 | it.name = '''_Solution«x»FoundAt''' | 141 | it.name = '''Solution«x+1»FoundAt''' |
140 | it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int | 142 | it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int |
141 | ] | 143 | ] |
142 | } | 144 | } |
145 | for(x: 0..<strategy.times.size) { | ||
146 | it.entries += createStringStatisticEntry => [ | ||
147 | it.name = '''Solution«x+1»DetailedStatistics''' | ||
148 | it.value = strategy.times.get(x) | ||
149 | ] | ||
150 | } | ||
151 | it.entries += createIntStatisticEntry => [ | ||
152 | it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int | ||
153 | ] | ||
143 | it.entries += createIntStatisticEntry => [ | 154 | it.entries += createIntStatisticEntry => [ |
144 | it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int | 155 | it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int |
145 | ] | 156 | ] |
@@ -159,7 +170,16 @@ class ViatraReasoner extends LogicReasoner{ | |||
159 | it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int | 170 | it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int |
160 | ] | 171 | ] |
161 | it.entries += createIntStatisticEntry => [ | 172 | it.entries += createIntStatisticEntry => [ |
162 | it.name = "NumericalSolverTime" it.value = (strategy.numericSolver.runtime/1000000) as int | 173 | it.name = "NumericalSolverSumTime" it.value = (strategy.numericSolver.runtime/1000000) as int |
174 | ] | ||
175 | it.entries += createIntStatisticEntry => [ | ||
176 | it.name = "NumericalSolverProblemFormingTime" it.value = (strategy.numericSolver.solverFormingProblem/1000000) as int | ||
177 | ] | ||
178 | it.entries += createIntStatisticEntry => [ | ||
179 | it.name = "NumericalSolverSolvingTime" it.value = (strategy.numericSolver.solverSolvingProblem/1000000) as int | ||
180 | ] | ||
181 | it.entries += createIntStatisticEntry => [ | ||
182 | it.name = "NumericalSolverInterpretingSolution" it.value = (strategy.numericSolver.solverSolution/1000000) as int | ||
163 | ] | 183 | ] |
164 | it.entries += createIntStatisticEntry => [ | 184 | it.entries += createIntStatisticEntry => [ |
165 | it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int | 185 | it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index c4d7e231..7369344c 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend | |||
@@ -44,7 +44,15 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{ | |||
44 | /** | 44 | /** |
45 | * Configuration for cutting search space. | 45 | * Configuration for cutting search space. |
46 | */ | 46 | */ |
47 | public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint | 47 | public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint |
48 | |||
49 | public var runIntermediateNumericalConsistencyChecks = true | ||
50 | |||
51 | public var punishSize = true | ||
52 | public var scopeWeight = 1 | ||
53 | public var conaintmentWeight = 2 | ||
54 | public var nonContainmentWeight = 1 | ||
55 | public var unfinishedWFWeight = 1 | ||
48 | } | 56 | } |
49 | 57 | ||
50 | public class DiversityDescriptor { | 58 | public class DiversityDescriptor { |
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 18fe94e4..8035c947 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,6 +9,9 @@ | |||
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; | ||
12 | import java.util.ArrayList; | 15 | import java.util.ArrayList; |
13 | import java.util.Arrays; | 16 | import java.util.Arrays; |
14 | import java.util.Collection; | 17 | import java.util.Collection; |
@@ -44,6 +47,7 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver; | |||
44 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; | 47 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; |
45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; | 48 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; |
46 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; | 49 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; |
50 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder; | ||
47 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; | 51 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; |
48 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; | 52 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; |
49 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; | 53 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; |
@@ -91,6 +95,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
91 | private int numberOfPrintedModel = 0; | 95 | private int numberOfPrintedModel = 0; |
92 | private int numberOfSolverCalls = 0; | 96 | private int numberOfSolverCalls = 0; |
93 | 97 | ||
98 | public long explorationStarted = 0; | ||
94 | 99 | ||
95 | public BestFirstStrategyForModelGeneration( | 100 | public BestFirstStrategyForModelGeneration( |
96 | ReasonerWorkspace workspace, | 101 | ReasonerWorkspace workspace, |
@@ -111,7 +116,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
111 | public int getNumberOfStatecoderFail() { | 116 | public int getNumberOfStatecoderFail() { |
112 | return numberOfStatecoderFail; | 117 | return numberOfStatecoderFail; |
113 | } | 118 | } |
114 | 119 | //LinkedList<ViatraQueryMatcher<? extends IPatternMatch>> matchers; | |
115 | @Override | 120 | @Override |
116 | public void initStrategy(ThreadContext context) { | 121 | public void initStrategy(ThreadContext context) { |
117 | this.context = context; | 122 | this.context = context; |
@@ -137,17 +142,25 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
137 | } | 142 | } |
138 | }; | 143 | }; |
139 | 144 | ||
140 | this.numericSolver = new NumericSolver(context, method, false); | 145 | this.numericSolver = new NumericSolver(context, method, false,this.configuration.runIntermediateNumericalConsistencyChecks); |
141 | 146 | ||
142 | trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); | 147 | trajectoiresToExplore = new PriorityQueue<TrajectoryWithFitness>(11, comparator); |
143 | } | 148 | } |
144 | 149 | ||
145 | @Override | 150 | @Override |
146 | public void explore() { | 151 | public void explore() { |
152 | // System.out.println("press enter"); | ||
153 | // try { | ||
154 | // new BufferedReader(new InputStreamReader(System.in)).readLine(); | ||
155 | // } catch (IOException e) { | ||
156 | // // TODO Auto-generated catch block | ||
157 | // e.printStackTrace(); | ||
158 | // } | ||
159 | this.explorationStarted=System.nanoTime(); | ||
147 | if (!context.checkGlobalConstraints()) { | 160 | if (!context.checkGlobalConstraints()) { |
148 | logger.info("Global contraint is not satisifed in the first state. Terminate."); | 161 | logger.info("Global contraint is not satisifed in the first state. Terminate."); |
149 | return; | 162 | return; |
150 | } else if(!numericSolver.isSatisfiable()) { | 163 | } else if(!numericSolver.maySatisfiable()) { |
151 | logger.info("Numeric contraints are not satisifed in the first state. Terminate."); | 164 | logger.info("Numeric contraints are not satisifed in the first state. Terminate."); |
152 | return; | 165 | return; |
153 | } | 166 | } |
@@ -211,12 +224,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
211 | 224 | ||
212 | visualiseCurrentState(); | 225 | visualiseCurrentState(); |
213 | // for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { | 226 | // for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { |
214 | // System.out.println(matcher.getPatternName()); | 227 | // int c = matcher.countMatches(); |
215 | // System.out.println("---------"); | 228 | // if(c>=100) { |
216 | // for(IPatternMatch m : matcher.getAllMatches()) { | 229 | // System.out.println(c+ " " +matcher.getPatternName()); |
217 | // System.out.println(m); | ||
218 | // } | 230 | // } |
219 | // System.out.println("---------"); | 231 | // |
220 | // } | 232 | // } |
221 | 233 | ||
222 | boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); | 234 | boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); |
@@ -228,7 +240,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
228 | } else if (!context.checkGlobalConstraints()) { | 240 | } else if (!context.checkGlobalConstraints()) { |
229 | logger.debug("Global contraint is not satisifed."); | 241 | logger.debug("Global contraint is not satisifed."); |
230 | context.backtrack(); | 242 | context.backtrack(); |
231 | } else if (!numericSolver.isSatisfiable()) { | 243 | } else if (!numericSolver.maySatisfiable()) { |
232 | logger.debug("Numeric constraints are not satisifed."); | 244 | logger.debug("Numeric constraints are not satisifed."); |
233 | context.backtrack(); | 245 | context.backtrack(); |
234 | } else { | 246 | } else { |
@@ -284,16 +296,38 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
284 | private void checkForSolution(final Fitness fittness) { | 296 | private void checkForSolution(final Fitness fittness) { |
285 | if (fittness.isSatisifiesHardObjectives()) { | 297 | if (fittness.isSatisifiesHardObjectives()) { |
286 | if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { | 298 | if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { |
287 | Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context); | 299 | if(numericSolver.currentSatisfiable()) { |
288 | numericSolver.fillSolutionCopy(trace); | 300 | Map<EObject, EObject> trace = solutionStoreWithCopy.newSolution(context); |
289 | solutionStoreWithDiversityDescriptor.newSolution(context); | 301 | numericSolver.fillSolutionCopy(trace); |
290 | solutionStore.newSolution(context); | 302 | solutionStoreWithDiversityDescriptor.newSolution(context); |
291 | configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); | 303 | solutionStore.newSolution(context); |
292 | 304 | configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); | |
293 | logger.debug("Found a solution."); | 305 | saveTimes(); |
306 | logger.debug("Found a solution."); | ||
307 | } | ||
294 | } | 308 | } |
295 | } | 309 | } |
296 | } | 310 | } |
311 | public List<String> times = new LinkedList<String>(); | ||
312 | private void saveTimes() { | ||
313 | long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder)this.context.getStateCoder()).getStatecoderRuntime()/1000000; | ||
314 | long solutionCopy = solutionStoreWithCopy.getSumRuntime()/1000000; | ||
315 | long activationSelection = this.activationSelector.getRuntime()/1000000; | ||
316 | long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000; | ||
317 | long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000; | ||
318 | long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000; | ||
319 | long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000; | ||
320 | this.times.add( | ||
321 | "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ | ||
322 | "|StateCoderTime:"+statecoderTime+ | ||
323 | "|SolutionCopyTime:"+solutionCopy+ | ||
324 | "|ActivationSelectionTime:"+activationSelection+ | ||
325 | "|NumericalSolverSumTime:"+numericalSolverSumTime+ | ||
326 | "|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+ | ||
327 | "|NumericalSolverSolvingTime:"+numericalSolverSolving+ | ||
328 | "|NumericalSolverInterpretingSolution:"+numericalSolverInterpreting+")"); | ||
329 | |||
330 | } | ||
297 | 331 | ||
298 | @Override | 332 | @Override |
299 | public void interruptStrategy() { | 333 | public void interruptStrategy() { |
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 a75ddf76..a10530c7 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 | |||
@@ -6,6 +6,8 @@ import org.eclipse.viatra.dse.base.ThreadContext | |||
6 | import org.eclipse.viatra.dse.objectives.Comparators | 6 | import org.eclipse.viatra.dse.objectives.Comparators |
7 | import org.eclipse.viatra.dse.objectives.IObjective | 7 | import org.eclipse.viatra.dse.objectives.IObjective |
8 | import org.eclipse.viatra.dse.objectives.impl.BaseObjective | 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 | ||
9 | 11 | ||
10 | //class ViatraReasonerNumbers { | 12 | //class ViatraReasonerNumbers { |
11 | // public static val scopePriority = 2 | 13 | // public static val scopePriority = 2 |
@@ -26,18 +28,48 @@ class ModelGenerationCompositeObjective implements IObjective{ | |||
26 | val ScopeObjective scopeObjective | 28 | val ScopeObjective scopeObjective |
27 | val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives | 29 | val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives |
28 | val UnfinishedWFObjective unfinishedWFObjective | 30 | val UnfinishedWFObjective unfinishedWFObjective |
31 | var PartialInterpretation model=null; | ||
32 | val boolean punishSize | ||
33 | val int scopeWeight | ||
34 | val int conaintmentWeight | ||
35 | val int nonContainmentWeight | ||
36 | val int unfinishedWFWeight | ||
29 | 37 | ||
30 | public new( | 38 | new( |
31 | ScopeObjective scopeObjective, | 39 | ScopeObjective scopeObjective, |
32 | List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives, | 40 | List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives, |
33 | UnfinishedWFObjective unfinishedWFObjective) | 41 | UnfinishedWFObjective unfinishedWFObjective, |
42 | ViatraReasonerConfiguration configuration) | ||
34 | { | 43 | { |
35 | this.scopeObjective = scopeObjective | 44 | this.scopeObjective = scopeObjective |
36 | this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives | 45 | this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives |
37 | this.unfinishedWFObjective = unfinishedWFObjective | 46 | this.unfinishedWFObjective = unfinishedWFObjective |
47 | |||
48 | this.punishSize = configuration.punishSize | ||
49 | this.scopeWeight = configuration.scopeWeight | ||
50 | this.conaintmentWeight = configuration.conaintmentWeight | ||
51 | this.nonContainmentWeight = configuration.nonContainmentWeight | ||
52 | this.unfinishedWFWeight = configuration.unfinishedWFWeight | ||
53 | } | ||
54 | new( | ||
55 | ScopeObjective scopeObjective, | ||
56 | List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives, | ||
57 | UnfinishedWFObjective unfinishedWFObjective, | ||
58 | boolean punishSize, int scopeWeight, int conaintmentWeight, int nonContainmentWeight, int unfinishedWFWeight) | ||
59 | { | ||
60 | this.scopeObjective = scopeObjective | ||
61 | this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives | ||
62 | this.unfinishedWFObjective = unfinishedWFObjective | ||
63 | |||
64 | this.punishSize = punishSize | ||
65 | this.scopeWeight = scopeWeight | ||
66 | this.conaintmentWeight = conaintmentWeight | ||
67 | this.nonContainmentWeight = nonContainmentWeight | ||
68 | this.unfinishedWFWeight = unfinishedWFWeight | ||
38 | } | 69 | } |
39 | 70 | ||
40 | override init(ThreadContext context) { | 71 | override init(ThreadContext context) { |
72 | model = context.model as PartialInterpretation | ||
41 | this.scopeObjective.init(context) | 73 | this.scopeObjective.init(context) |
42 | this.unfinishedMultiplicityObjectives.forEach[it.init(context)] | 74 | this.unfinishedMultiplicityObjectives.forEach[it.init(context)] |
43 | this.unfinishedWFObjective.init(context) | 75 | this.unfinishedWFObjective.init(context) |
@@ -45,7 +77,8 @@ class ModelGenerationCompositeObjective implements IObjective{ | |||
45 | 77 | ||
46 | override createNew() { | 78 | override createNew() { |
47 | return new ModelGenerationCompositeObjective( | 79 | return new ModelGenerationCompositeObjective( |
48 | this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective) | 80 | this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective, |
81 | this.punishSize, this.scopeWeight, this.conaintmentWeight, this.nonContainmentWeight, this.unfinishedWFWeight) | ||
49 | } | 82 | } |
50 | 83 | ||
51 | override getComparator() { Comparators.LOWER_IS_BETTER } | 84 | override getComparator() { Comparators.LOWER_IS_BETTER } |
@@ -55,17 +88,29 @@ class ModelGenerationCompositeObjective implements IObjective{ | |||
55 | //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] | 88 | //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] |
56 | val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) | 89 | val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) |
57 | 90 | ||
58 | 91 | var containmentMultiplicity = 0.0 | |
59 | var multiplicity = 0.0 | 92 | var nonContainmentMultiplicity = 0.0 |
60 | for(multiplicityObjective : unfinishedMultiplicityObjectives) { | 93 | for(multiplicityObjective : unfinishedMultiplicityObjectives) { |
61 | multiplicity+=multiplicityObjective.getFitness(context) | 94 | if(multiplicityObjective.containment) { |
95 | containmentMultiplicity+=multiplicityObjective.getFitness(context) | ||
96 | } else { | ||
97 | nonContainmentMultiplicity+=multiplicityObjective.getFitness(context) | ||
98 | } | ||
99 | } | ||
100 | val size = if(punishSize) { | ||
101 | 0.9/model.newElements.size | ||
102 | } else { | ||
103 | 0 | ||
62 | } | 104 | } |
105 | |||
63 | var sum = 0.0 | 106 | var sum = 0.0 |
64 | sum += scopeFitnes | 107 | sum += scopeFitnes*scopeWeight |
65 | sum +=Math.sqrt(multiplicity *0.1) | 108 | sum += containmentMultiplicity*conaintmentWeight |
66 | sum += unfinishedWFsFitness//*0.5 | 109 | sum += nonContainmentMultiplicity*nonContainmentWeight |
110 | sum += unfinishedWFsFitness*unfinishedWFWeight | ||
111 | sum+=size | ||
67 | 112 | ||
68 | println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') | 113 | //println('''Sum=«sum»|Scope=«scopeFitnes»|ContainmentMultiplicity=«containmentMultiplicity»|NonContainmentMultiplicity=«nonContainmentMultiplicity»|WFs=«unfinishedWFsFitness»''') |
69 | 114 | ||
70 | return sum | 115 | return sum |
71 | } | 116 | } |
@@ -74,7 +119,7 @@ class ModelGenerationCompositeObjective implements IObjective{ | |||
74 | override getName() { "CompositeUnfinishednessObjective"} | 119 | override getName() { "CompositeUnfinishednessObjective"} |
75 | 120 | ||
76 | override isHardObjective() { true } | 121 | override isHardObjective() { true } |
77 | override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } | 122 | override satisifiesHardObjective(Double fitness) { fitness < 0.95 } |
78 | 123 | ||
79 | 124 | ||
80 | override setComparator(Comparator<Double> comparator) { | 125 | override setComparator(Comparator<Double> comparator) { |
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 71793aa6..ed8bdae3 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 | |||
@@ -1,32 +1,32 @@ | |||
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.viatra2logic.NumericProblemSolver | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
5 | import java.util.HashMap | ||
6 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
7 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
9 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
10 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | 3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator |
11 | import org.eclipse.viatra.dse.base.ThreadContext | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod |
12 | import org.eclipse.emf.ecore.EObject | ||
13 | import java.util.Map | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement |
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
20 | import java.util.List | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement |
21 | import java.math.BigDecimal | 11 | import java.math.BigDecimal |
22 | import java.util.LinkedHashSet | 12 | import java.util.HashMap |
23 | import java.util.LinkedHashMap | 13 | import java.util.LinkedHashMap |
14 | import java.util.LinkedHashSet | ||
15 | import java.util.List | ||
16 | import java.util.Map | ||
17 | import org.eclipse.emf.ecore.EObject | ||
18 | import org.eclipse.viatra.dse.base.ThreadContext | ||
19 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
20 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
21 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
24 | 22 | ||
25 | class NumericSolver { | 23 | class NumericSolver { |
26 | val ThreadContext threadContext; | 24 | val ThreadContext threadContext; |
27 | val constraint2UnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | 25 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> |
26 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | ||
28 | NumericTranslator t = new NumericTranslator | 27 | NumericTranslator t = new NumericTranslator |
29 | 28 | ||
29 | val boolean intermediateConsistencyCheck | ||
30 | val boolean caching; | 30 | val boolean caching; |
31 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | 31 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap |
32 | 32 | ||
@@ -35,15 +35,23 @@ class NumericSolver { | |||
35 | var int numberOfSolverCalls = 0 | 35 | var int numberOfSolverCalls = 0 |
36 | var int numberOfCachedSolverCalls = 0 | 36 | var int numberOfCachedSolverCalls = 0 |
37 | 37 | ||
38 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean caching) { | 38 | new(ThreadContext threadContext, ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) { |
39 | this.threadContext = threadContext | 39 | this.threadContext = threadContext |
40 | val engine = threadContext.queryEngine | 40 | val engine = threadContext.queryEngine |
41 | for(entry : method.unitPropagationPreconditions.entrySet) { | 41 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { |
42 | val constraint = entry.key | ||
43 | val querySpec = entry.value | ||
44 | val matcher = querySpec.getMatcher(engine); | ||
45 | constraint2MustUnitPropagationPrecondition.put(constraint,matcher) | ||
46 | } | ||
47 | for(entry : method.currentUnitPropagationPreconditions.entrySet) { | ||
42 | val constraint = entry.key | 48 | val constraint = entry.key |
43 | val querySpec = entry.value | 49 | val querySpec = entry.value |
44 | val matcher = querySpec.getMatcher(engine); | 50 | val matcher = querySpec.getMatcher(engine); |
45 | constraint2UnitPropagationPrecondition.put(constraint,matcher) | 51 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) |
46 | } | 52 | } |
53 | this.intermediateConsistencyCheck = true | ||
54 | println() | ||
47 | this.caching = caching | 55 | this.caching = caching |
48 | } | 56 | } |
49 | 57 | ||
@@ -51,15 +59,29 @@ class NumericSolver { | |||
51 | def getCachingTime(){cachingTime} | 59 | def getCachingTime(){cachingTime} |
52 | def getNumberOfSolverCalls(){numberOfSolverCalls} | 60 | def getNumberOfSolverCalls(){numberOfSolverCalls} |
53 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} | 61 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} |
62 | def getSolverFormingProblem(){this.t.formingProblemTime} | ||
63 | def getSolverSolvingProblem(){this.t.solvingProblemTime} | ||
64 | def getSolverSolution(){this.t.formingSolutionTime} | ||
54 | 65 | ||
55 | def boolean isSatisfiable() { | 66 | def boolean maySatisfiable() { |
67 | if(intermediateConsistencyCheck) { | ||
68 | return isSatisfiable(this.constraint2MustUnitPropagationPrecondition) | ||
69 | } else { | ||
70 | return true | ||
71 | } | ||
72 | } | ||
73 | def boolean currentSatisfiable() { | ||
74 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition) | ||
75 | } | ||
76 | |||
77 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { | ||
56 | val start = System.nanoTime | 78 | val start = System.nanoTime |
57 | var boolean finalResult | 79 | var boolean finalResult |
58 | if(constraint2UnitPropagationPrecondition.empty){ | 80 | if(matches.empty){ |
59 | finalResult=true | 81 | finalResult=true |
60 | } else { | 82 | } else { |
61 | val propagatedConstraints = new HashMap | 83 | val propagatedConstraints = new HashMap |
62 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { | 84 | for(entry : matches.entrySet) { |
63 | val constraint = entry.key | 85 | val constraint = entry.key |
64 | //println(constraint) | 86 | //println(constraint) |
65 | val allMatches = entry.value.allMatches.map[it.toArray] | 87 | val allMatches = entry.value.allMatches.map[it.toArray] |
@@ -92,7 +114,7 @@ class NumericSolver { | |||
92 | this.numberOfSolverCalls++ | 114 | this.numberOfSolverCalls++ |
93 | } | 115 | } |
94 | } | 116 | } |
95 | } | 117 | } |
96 | this.runtime+=System.nanoTime-start | 118 | this.runtime+=System.nanoTime-start |
97 | return finalResult | 119 | return finalResult |
98 | } | 120 | } |
@@ -108,11 +130,11 @@ class NumericSolver { | |||
108 | def fillSolutionCopy(Map<EObject, EObject> trace) { | 130 | def fillSolutionCopy(Map<EObject, EObject> trace) { |
109 | val model = threadContext.getModel as PartialInterpretation | 131 | val model = threadContext.getModel as PartialInterpretation |
110 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | 132 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList |
111 | if(constraint2UnitPropagationPrecondition.empty) { | 133 | if(constraint2CurrentUnitPropagationPrecondition.empty) { |
112 | fillWithDefaultValues(dataObjects,trace) | 134 | fillWithDefaultValues(dataObjects,trace) |
113 | } else { | 135 | } else { |
114 | val propagatedConstraints = new HashMap | 136 | val propagatedConstraints = new HashMap |
115 | for(entry : constraint2UnitPropagationPrecondition.entrySet) { | 137 | for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { |
116 | val constraint = entry.key | 138 | val constraint = entry.key |
117 | val allMatches = entry.value.allMatches.map[it.toArray] | 139 | val allMatches = entry.value.allMatches.map[it.toArray] |
118 | propagatedConstraints.put(constraint,allMatches) | 140 | propagatedConstraints.put(constraint,allMatches) |
@@ -142,7 +164,7 @@ class NumericSolver { | |||
142 | def protected dispatch getDefaultValue(RealElement e) {0.0} | 164 | def protected dispatch getDefaultValue(RealElement e) {0.0} |
143 | def protected dispatch getDefaultValue(StringElement e) {""} | 165 | def protected dispatch getDefaultValue(StringElement e) {""} |
144 | 166 | ||
145 | def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Integer> solution, Map<EObject, EObject> trace) { | 167 | def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) { |
146 | for(element : elements) { | 168 | for(element : elements) { |
147 | if(element.valueSet==false) { | 169 | if(element.valueSet==false) { |
148 | if(solution.containsKey(element)) { | 170 | if(solution.containsKey(element)) { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend index aad9a448..2b0807d6 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 | |||
@@ -34,4 +34,7 @@ class UnfinishedMultiplicityObjective implements IObjective { | |||
34 | override setLevel(int level) { | 34 | override setLevel(int level) { |
35 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 35 | throw new UnsupportedOperationException("TODO: auto-generated method stub") |
36 | } | 36 | } |
37 | def isContainment() { | ||
38 | return this.unfinishedMultiplicity.containment | ||
39 | } | ||
37 | } \ No newline at end of file | 40 | } \ No newline at end of file |