aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend28
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend10
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java66
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend67
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend74
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend3
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
50public class DiversityDescriptor { 58public 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 *******************************************************************************/
10package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse; 10package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse;
11 11
12import java.io.BufferedReader;
13import java.io.IOException;
14import java.io.InputStreamReader;
12import java.util.ArrayList; 15import java.util.ArrayList;
13import java.util.Arrays; 16import java.util.Arrays;
14import java.util.Collection; 17import java.util.Collection;
@@ -44,6 +47,7 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver;
44import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; 47import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod;
45import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; 48import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic;
46import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; 49import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
50import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder;
47import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; 51import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation;
48import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; 52import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser;
49import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; 53import 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
6import org.eclipse.viatra.dse.objectives.Comparators 6import org.eclipse.viatra.dse.objectives.Comparators
7import org.eclipse.viatra.dse.objectives.IObjective 7import org.eclipse.viatra.dse.objectives.IObjective
8import org.eclipse.viatra.dse.objectives.impl.BaseObjective 8import org.eclipse.viatra.dse.objectives.impl.BaseObjective
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
10import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericProblemSolver
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
5import java.util.HashMap
6import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
7import org.eclipse.viatra.query.runtime.api.IPatternMatch
8import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
9import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
10import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator 3import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator
11import org.eclipse.viatra.dse.base.ThreadContext 4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
12import org.eclipse.emf.ecore.EObject
13import java.util.Map
14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement 5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement 6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement 7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement 9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement
20import java.util.List 10import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement
21import java.math.BigDecimal 11import java.math.BigDecimal
22import java.util.LinkedHashSet 12import java.util.HashMap
23import java.util.LinkedHashMap 13import java.util.LinkedHashMap
14import java.util.LinkedHashSet
15import java.util.List
16import java.util.Map
17import org.eclipse.emf.ecore.EObject
18import org.eclipse.viatra.dse.base.ThreadContext
19import org.eclipse.viatra.query.runtime.api.IPatternMatch
20import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
21import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
24 22
25class NumericSolver { 23class 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
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-18 02:45:01 +0000