diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf')
15 files changed, 696 insertions, 104 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend index 28cf986d..9ef5e091 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend | |||
@@ -1,11 +1,11 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner |
2 | 2 | ||
3 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | 3 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod |
5 | 5 | ||
6 | abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint { | 6 | abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint { |
7 | val protected ModelGenerationMethod method | 7 | val protected ModelGenerationMethod method |
8 | new(ModelGenerationMethod method) { | 8 | new(ModelGenerationMethod method) { |
9 | this.method = method | 9 | this.method = method |
10 | } | 10 | } |
11 | } \ No newline at end of file | 11 | } |
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 aa02cd30..3033eca7 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 | |||
@@ -42,6 +42,7 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer | |||
42 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel | 42 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel |
43 | import org.eclipse.viatra.dse.solutionstore.SolutionStore | 43 | import org.eclipse.viatra.dse.solutionstore.SolutionStore |
44 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory | 44 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory |
45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.NumericSolver | ||
45 | 46 | ||
46 | class ViatraReasoner extends LogicReasoner { | 47 | class ViatraReasoner extends LogicReasoner { |
47 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() | 48 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() |
@@ -66,12 +67,12 @@ class ViatraReasoner extends LogicReasoner { | |||
66 | dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE) | 67 | dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE) |
67 | 68 | ||
68 | val transformationStartTime = System.nanoTime | 69 | val transformationStartTime = System.nanoTime |
69 | |||
70 | val emptySolution = initialiser.initialisePartialInterpretation(problem, viatraConfig.typeScopes).output | 70 | val emptySolution = initialiser.initialisePartialInterpretation(problem, viatraConfig.typeScopes).output |
71 | if ((viatraConfig.documentationLevel == DocumentationLevel::FULL || | 71 | if ((viatraConfig.documentationLevel == DocumentationLevel::FULL || |
72 | viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { | 72 | viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { |
73 | workspace.writeModel(emptySolution, "init.partialmodel") | 73 | workspace.writeModel(emptySolution, "init.partialmodel") |
74 | } | 74 | } |
75 | |||
75 | emptySolution.problemConainer = problem | 76 | emptySolution.problemConainer = problem |
76 | var BasicScopeGlobalConstraint basicScopeGlobalConstraint = null | 77 | var BasicScopeGlobalConstraint basicScopeGlobalConstraint = null |
77 | if (viatraConfig.scopePropagatorStrategy == ScopePropagatorStrategy.None) { | 78 | if (viatraConfig.scopePropagatorStrategy == ScopePropagatorStrategy.None) { |
@@ -93,7 +94,8 @@ class ViatraReasoner extends LogicReasoner { | |||
93 | dse.addObjective(new ModelGenerationCompositeObjective( | 94 | dse.addObjective(new ModelGenerationCompositeObjective( |
94 | basicScopeGlobalConstraint ?: new ScopeObjective, | 95 | basicScopeGlobalConstraint ?: new ScopeObjective, |
95 | method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], | 96 | method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], |
96 | wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF) | 97 | wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF), |
98 | viatraConfig | ||
97 | )) | 99 | )) |
98 | 100 | ||
99 | val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size) | 101 | val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size) |
@@ -131,8 +133,9 @@ class ViatraReasoner extends LogicReasoner { | |||
131 | } | 133 | } |
132 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) | 134 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) |
133 | val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement) | 135 | val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement) |
136 | val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) | ||
134 | val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions, | 137 | val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions, |
135 | diversityChecker) | 138 | diversityChecker, numericSolver) |
136 | val solutionCopier = solutionSaver.solutionCopier | 139 | val solutionCopier = solutionSaver.solutionCopier |
137 | solutionStore.withSolutionSaver(solutionSaver) | 140 | solutionStore.withSolutionSaver(solutionSaver) |
138 | dse.solutionStore = solutionStore | 141 | dse.solutionStore = solutionStore |
@@ -168,10 +171,10 @@ class ViatraReasoner extends LogicReasoner { | |||
168 | dse.addTransformationRule(rule) | 171 | dse.addTransformationRule(rule) |
169 | } | 172 | } |
170 | 173 | ||
171 | val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method) | 174 | val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, numericSolver) |
172 | viatraConfig.progressMonitor.workedForwardTransformation | 175 | viatraConfig.progressMonitor.workedForwardTransformation |
173 | 176 | val transformationFinished = System.nanoTime | |
174 | val transformationTime = System.nanoTime - transformationStartTime | 177 | val transformationTime = transformationFinished - transformationStartTime |
175 | val solverStartTime = System.nanoTime | 178 | val solverStartTime = System.nanoTime |
176 | 179 | ||
177 | var boolean stoppedByTimeout | 180 | var boolean stoppedByTimeout |
@@ -194,6 +197,15 @@ class ViatraReasoner extends LogicReasoner { | |||
194 | it.value = (pair.value / 1000000) as int | 197 | it.value = (pair.value / 1000000) as int |
195 | ] | 198 | ] |
196 | } | 199 | } |
200 | for(x: 0..<strategy.times.size) { | ||
201 | it.entries += createStringStatisticEntry => [ | ||
202 | it.name = '''Solution«x+1»DetailedStatistics''' | ||
203 | it.value = strategy.times.get(x) | ||
204 | ] | ||
205 | } | ||
206 | it.entries += createIntStatisticEntry => [ | ||
207 | it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int | ||
208 | ] | ||
197 | it.entries += createIntStatisticEntry => [ | 209 | it.entries += createIntStatisticEntry => [ |
198 | it.name = "TransformationExecutionTime" | 210 | it.name = "TransformationExecutionTime" |
199 | it.value = (method.statistics.transformationExecutionTime / 1000000) as int | 211 | it.value = (method.statistics.transformationExecutionTime / 1000000) as int |
@@ -223,6 +235,24 @@ class ViatraReasoner extends LogicReasoner { | |||
223 | it.value = dse.numberOfStates as int | 235 | it.value = dse.numberOfStates as int |
224 | ] | 236 | ] |
225 | it.entries += createIntStatisticEntry => [ | 237 | it.entries += createIntStatisticEntry => [ |
238 | it.name = "ForwardTime" it.value = (strategy.forwardTime/1000000) as int | ||
239 | ] | ||
240 | it.entries += createIntStatisticEntry => [ | ||
241 | it.name = "BacktrackingTime" it.value = (strategy.backtrackingTime/1000000) as int | ||
242 | ] | ||
243 | it.entries += createIntStatisticEntry => [ | ||
244 | it.name = "GlobalConstraintEvaluationTime" it.value = (strategy.globalConstraintEvaluationTime/1000000) as int | ||
245 | ] | ||
246 | it.entries += createIntStatisticEntry => [ | ||
247 | it.name = "FitnessCalculationTime" it.value = (strategy.fitnessCalculationTime/1000000) as int | ||
248 | ] | ||
249 | it.entries += createIntStatisticEntry => [ | ||
250 | it.name = "SolutionCopyTime" it.value = (solutionSaver.totalCopierRuntime/1000000) as int | ||
251 | ] | ||
252 | it.entries += createIntStatisticEntry => [ | ||
253 | it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int | ||
254 | ] | ||
255 | it.entries += createIntStatisticEntry => [ | ||
226 | it.name = "Decisions" | 256 | it.name = "Decisions" |
227 | it.value = method.statistics.decisionsTried | 257 | it.value = method.statistics.decisionsTried |
228 | ] | 258 | ] |
@@ -238,7 +268,28 @@ class ViatraReasoner extends LogicReasoner { | |||
238 | it.name = "ScopePropagationsSolverCalls" | 268 | it.name = "ScopePropagationsSolverCalls" |
239 | it.value = method.statistics.scopePropagatorSolverInvocations | 269 | it.value = method.statistics.scopePropagatorSolverInvocations |
240 | ] | 270 | ] |
241 | if (diversityChecker.isActive) { | 271 | it.entries += createIntStatisticEntry => [ |
272 | it.name = "NumericalSolverSumTime" it.value = (strategy.numericSolver.runtime/1000000) as int | ||
273 | ] | ||
274 | it.entries += createIntStatisticEntry => [ | ||
275 | it.name = "NumericalSolverProblemFormingTime" it.value = (strategy.numericSolver.solverFormingProblem/1000000) as int | ||
276 | ] | ||
277 | it.entries += createIntStatisticEntry => [ | ||
278 | it.name = "NumericalSolverSolvingTime" it.value = (strategy.numericSolver.solverSolvingProblem/1000000) as int | ||
279 | ] | ||
280 | it.entries += createIntStatisticEntry => [ | ||
281 | it.name = "NumericalSolverInterpretingSolution" it.value = (strategy.numericSolver.solverSolution/1000000) as int | ||
282 | ] | ||
283 | it.entries += createIntStatisticEntry => [ | ||
284 | it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int | ||
285 | ] | ||
286 | it.entries += createIntStatisticEntry => [ | ||
287 | it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls | ||
288 | ] | ||
289 | it.entries += createIntStatisticEntry => [ | ||
290 | it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls | ||
291 | ] | ||
292 | if(diversityChecker.active) { | ||
242 | it.entries += createIntStatisticEntry => [ | 293 | it.entries += createIntStatisticEntry => [ |
243 | it.name = "SolutionDiversityCheckTime" | 294 | it.name = "SolutionDiversityCheckTime" |
244 | it.value = (diversityChecker.totalRuntime / 1000000) as int | 295 | it.value = (diversityChecker.totalRuntime / 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 c0a71c85..ddd25aac 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 | |||
@@ -54,8 +54,16 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
54 | * Configuration for cutting search space. | 54 | * Configuration for cutting search space. |
55 | */ | 55 | */ |
56 | public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint | 56 | public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint |
57 | 57 | ||
58 | public var ScopePropagatorStrategy scopePropagatorStrategy = ScopePropagatorStrategy.Polyhedral( | 58 | public var runIntermediateNumericalConsistencyChecks = true |
59 | |||
60 | public var punishSize = true | ||
61 | public var scopeWeight = 1 | ||
62 | public var conaintmentWeight = 2 | ||
63 | public var nonContainmentWeight = 1 | ||
64 | public var unfinishedWFWeight = 1 | ||
65 | |||
66 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( | ||
59 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) | 67 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) |
60 | 68 | ||
61 | public var List<LinearTypeConstraintHint> hints = newArrayList | 69 | public var List<LinearTypeConstraintHint> hints = newArrayList |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend new file mode 100644 index 00000000..65f9814c --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ActivationSelector.xtend | |||
@@ -0,0 +1,24 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.ArrayList | ||
4 | import java.util.Collection | ||
5 | import java.util.Random | ||
6 | |||
7 | abstract class ActivationSelector { | ||
8 | long runtime = 0 | ||
9 | protected val Random r | ||
10 | new(Random r) { | ||
11 | this.r = r | ||
12 | } | ||
13 | |||
14 | def randomizeActivationIDs(Collection<Object> activationIDs) { | ||
15 | val startTime = System.nanoTime | ||
16 | val res = internalRandomizationOfActivationIDs(activationIDs) | ||
17 | runtime+= System.nanoTime-startTime | ||
18 | return res | ||
19 | } | ||
20 | def protected ArrayList<Object> internalRandomizationOfActivationIDs(Collection<Object> activationIDs); | ||
21 | def getRuntime(){ | ||
22 | return runtime | ||
23 | } | ||
24 | } \ 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/BalancedActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend new file mode 100644 index 00000000..2df9957b --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BalancedActivationSelector.xtend | |||
@@ -0,0 +1,51 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.Collection | ||
4 | import java.util.HashMap | ||
5 | import java.util.Map | ||
6 | import java.util.List | ||
7 | import java.util.Random | ||
8 | import java.util.ArrayList | ||
9 | import java.util.LinkedList | ||
10 | import java.util.Collections | ||
11 | |||
12 | class BalancedActivationSelector extends ActivationSelector{ | ||
13 | val Random r = new Random | ||
14 | |||
15 | new(Random r) { | ||
16 | super(r) | ||
17 | } | ||
18 | |||
19 | override protected internalRandomizationOfActivationIDs(Collection<Object> activationIDs) { | ||
20 | val Map<String,List<Object>> urns = new HashMap | ||
21 | val res = new ArrayList(activationIDs.size) | ||
22 | for(activationID : activationIDs) { | ||
23 | val pair = activationID as Pair<String,? extends Object> | ||
24 | val name = pair.key | ||
25 | val selectedUrn = urns.get(name) | ||
26 | if(selectedUrn!==null) { | ||
27 | selectedUrn.add(activationID) | ||
28 | } else { | ||
29 | val collection = new LinkedList | ||
30 | collection.add(activationID) | ||
31 | urns.put(name,collection) | ||
32 | } | ||
33 | } | ||
34 | |||
35 | for(list:urns.values) { | ||
36 | Collections.shuffle(list,r) | ||
37 | } | ||
38 | |||
39 | while(!urns.empty) { | ||
40 | val randomEntry = urns.entrySet.get(r.nextInt(urns.size)) | ||
41 | val list = randomEntry.value | ||
42 | val removedLast = list.remove(list.size-1) | ||
43 | res.add(removedLast) | ||
44 | if(list.empty) { | ||
45 | urns.remove(randomEntry.key) | ||
46 | } | ||
47 | } | ||
48 | return res | ||
49 | } | ||
50 | |||
51 | } \ 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/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 081e48fa..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,9 +9,7 @@ | |||
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.util.ArrayList; | ||
13 | import java.util.Arrays; | 12 | import java.util.Arrays; |
14 | import java.util.Collection; | ||
15 | import java.util.Collections; | 13 | import java.util.Collections; |
16 | import java.util.Comparator; | 14 | import java.util.Comparator; |
17 | import java.util.Iterator; | 15 | import java.util.Iterator; |
@@ -23,15 +21,13 @@ import java.util.Random; | |||
23 | import org.apache.log4j.Logger; | 21 | import org.apache.log4j.Logger; |
24 | import org.eclipse.emf.ecore.EObject; | 22 | import org.eclipse.emf.ecore.EObject; |
25 | import org.eclipse.emf.ecore.util.EcoreUtil; | 23 | import org.eclipse.emf.ecore.util.EcoreUtil; |
24 | import org.eclipse.viatra.dse.api.SolutionTrajectory; | ||
26 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; | 25 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; |
27 | import org.eclipse.viatra.dse.base.ThreadContext; | 26 | import org.eclipse.viatra.dse.base.ThreadContext; |
28 | import org.eclipse.viatra.dse.objectives.Fitness; | 27 | import org.eclipse.viatra.dse.objectives.Fitness; |
29 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; | 28 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; |
29 | import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler; | ||
30 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; | 30 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; |
31 | import org.eclipse.viatra.query.runtime.api.IPatternMatch; | ||
32 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; | ||
33 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine; | ||
34 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher; | ||
35 | 31 | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 32 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
37 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | 33 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; |
@@ -42,6 +38,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | |||
42 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; | 38 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; |
43 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; | 39 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; |
44 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; | 40 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; |
41 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder; | ||
45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; | 42 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; |
46 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; | 43 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; |
47 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; | 44 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; |
@@ -79,41 +76,70 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
79 | private volatile boolean isInterrupted = false; | 76 | private volatile boolean isInterrupted = false; |
80 | private ModelResult modelResultByInternalSolver = null; | 77 | private ModelResult modelResultByInternalSolver = null; |
81 | private Random random = new Random(); | 78 | private Random random = new Random(); |
82 | private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; | 79 | //private Collection<ViatraQueryMatcher<? extends IPatternMatch>> matchers; |
83 | 80 | public ActivationSelector activationSelector = new EvenActivationSelector(random); | |
81 | public ViatraReasonerSolutionSaver solutionSaver; | ||
82 | public NumericSolver numericSolver; | ||
84 | // Statistics | 83 | // Statistics |
85 | private int numberOfStatecoderFail = 0; | 84 | private int numberOfStatecoderFail = 0; |
86 | private int numberOfPrintedModel = 0; | 85 | private int numberOfPrintedModel = 0; |
87 | private int numberOfSolverCalls = 0; | 86 | private int numberOfSolverCalls = 0; |
87 | public long globalConstraintEvaluationTime = 0; | ||
88 | public long fitnessCalculationTime = 0; | ||
89 | |||
90 | public long explorationStarted = 0; | ||
88 | 91 | ||
89 | public BestFirstStrategyForModelGeneration( | 92 | public BestFirstStrategyForModelGeneration( |
90 | ReasonerWorkspace workspace, | 93 | ReasonerWorkspace workspace, |
91 | ViatraReasonerConfiguration configuration, | 94 | ViatraReasonerConfiguration configuration, |
92 | ModelGenerationMethod method) | 95 | ModelGenerationMethod method, |
93 | { | 96 | ViatraReasonerSolutionSaver solutionSaver, |
97 | NumericSolver numericSolver) { | ||
94 | this.workspace = workspace; | 98 | this.workspace = workspace; |
95 | this.configuration = configuration; | 99 | this.configuration = configuration; |
96 | this.method = method; | 100 | this.method = method; |
101 | this.solutionSaver = solutionSaver; | ||
102 | this.numericSolver = numericSolver; | ||
97 | //logger.setLevel(Level.DEBUG); | 103 | //logger.setLevel(Level.DEBUG); |
98 | } | 104 | } |
99 | 105 | ||
100 | public int getNumberOfStatecoderFail() { | 106 | public int getNumberOfStatecoderFail() { |
101 | return numberOfStatecoderFail; | 107 | return numberOfStatecoderFail; |
102 | } | 108 | } |
109 | public long getForwardTime() { | ||
110 | return context.getDesignSpaceManager().getForwardTime(); | ||
111 | } | ||
112 | public long getBacktrackingTime() { | ||
113 | return context.getDesignSpaceManager().getBacktrackingTime(); | ||
114 | } | ||
103 | 115 | ||
104 | @Override | 116 | @Override |
105 | public void initStrategy(ThreadContext context) { | 117 | public void initStrategy(ThreadContext context) { |
106 | this.context = context; | 118 | this.context = context; |
107 | 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); | ||
108 | 135 | ||
109 | ViatraQueryEngine engine = context.getQueryEngine(); | 136 | // ViatraQueryEngine engine = context.getQueryEngine(); |
110 | // // TODO: visualisation | 137 | // matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); |
111 | matchers = new LinkedList<ViatraQueryMatcher<? extends IPatternMatch>>(); | 138 | // for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) { |
112 | for(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> p : this.method.getAllPatterns()) { | 139 | // //System.out.println(p.getSimpleName()); |
113 | //System.out.println(p.getSimpleName()); | 140 | // ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine); |
114 | ViatraQueryMatcher<? extends IPatternMatch> matcher = p.getMatcher(engine); | 141 | // matchers.add(matcher); |
115 | matchers.add(matcher); | 142 | // } |
116 | } | ||
117 | 143 | ||
118 | final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); | 144 | final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); |
119 | this.comparator = new Comparator<TrajectoryWithFitness>() { | 145 | this.comparator = new Comparator<TrajectoryWithFitness>() { |
@@ -128,23 +154,33 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
128 | 154 | ||
129 | @Override | 155 | @Override |
130 | public void explore() { | 156 | public void explore() { |
131 | if (!context.checkGlobalConstraints()) { | 157 | // System.out.println("press enter"); |
158 | // try { | ||
159 | // new BufferedReader(new InputStreamReader(System.in)).readLine(); | ||
160 | // } catch (IOException e) { | ||
161 | // // TODO Auto-generated catch block | ||
162 | // e.printStackTrace(); | ||
163 | // } | ||
164 | this.explorationStarted=System.nanoTime(); | ||
165 | if (!checkGlobalConstraints()) { | ||
132 | logger.info("Global contraint is not satisifed in the first state. Terminate."); | 166 | logger.info("Global contraint is not satisifed in the first state. Terminate."); |
133 | return; | 167 | return; |
168 | } else if(!numericSolver.maySatisfiable()) { | ||
169 | logger.info("Numeric contraints are not satisifed in the first state. Terminate."); | ||
170 | return; | ||
134 | } | 171 | } |
135 | if (configuration.searchSpaceConstraints.maxDepth == 0) { | 172 | if (configuration.searchSpaceConstraints.maxDepth == 0) { |
136 | logger.info("Maximal depth is reached in the initial solution. Terminate."); | 173 | logger.info("Maximal depth is reached in the initial solution. Terminate."); |
137 | return; | 174 | return; |
138 | } | 175 | } |
139 | 176 | ||
140 | final Fitness firstfitness = context.calculateFitness(); | 177 | final Fitness firstFitness = calculateFitness(); |
141 | solutionStore.newSolution(context); | 178 | checkForSolution(firstFitness); |
142 | 179 | ||
143 | final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); | 180 | final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); |
144 | final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); | 181 | final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); |
145 | TrajectoryWithFitness currentTrajectoryWithfitness = new TrajectoryWithFitness(firstTrajectory, firstfitness); | 182 | TrajectoryWithFitness currentTrajectoryWithFitness = new TrajectoryWithFitness(firstTrajectory, firstFitness); |
146 | trajectoiresToExplore.add(currentTrajectoryWithfitness); | 183 | trajectoiresToExplore.add(currentTrajectoryWithFitness); |
147 | |||
148 | //if(configuration) | 184 | //if(configuration) |
149 | visualiseCurrentState(); | 185 | visualiseCurrentState(); |
150 | // for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { | 186 | // for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { |
@@ -158,17 +194,17 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
158 | 194 | ||
159 | mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) { | 195 | mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) { |
160 | 196 | ||
161 | if (currentTrajectoryWithfitness == null) { | 197 | if (currentTrajectoryWithFitness == null) { |
162 | if (trajectoiresToExplore.isEmpty()) { | 198 | if (trajectoiresToExplore.isEmpty()) { |
163 | logger.debug("State space is fully traversed."); | 199 | logger.debug("State space is fully traversed."); |
164 | return; | 200 | return; |
165 | } else { | 201 | } else { |
166 | currentTrajectoryWithfitness = selectState(); | 202 | currentTrajectoryWithFitness = selectState(); |
167 | if (logger.isDebugEnabled()) { | 203 | if (logger.isDebugEnabled()) { |
168 | logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); | 204 | logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); |
169 | logger.debug("New trajectory is chosen: " + currentTrajectoryWithfitness); | 205 | logger.debug("New trajectory is chosen: " + currentTrajectoryWithFitness); |
170 | } | 206 | } |
171 | context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithfitness.trajectory); | 207 | context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFitness.trajectory); |
172 | } | 208 | } |
173 | } | 209 | } |
174 | 210 | ||
@@ -193,26 +229,28 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
193 | 229 | ||
194 | visualiseCurrentState(); | 230 | visualiseCurrentState(); |
195 | // for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { | 231 | // for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { |
196 | // System.out.println(matcher.getPatternName()); | 232 | // int c = matcher.countMatches(); |
197 | // System.out.println("---------"); | 233 | // if(c>=100) { |
198 | // for(IPatternMatch m : matcher.getAllMatches()) { | 234 | // System.out.println(c+ " " +matcher.getPatternName()); |
199 | // System.out.println(m); | ||
200 | // } | 235 | // } |
201 | // System.out.println("---------"); | 236 | // |
202 | // } | 237 | // } |
203 | 238 | ||
204 | boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness); | 239 | boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness); |
205 | if(consistencyCheckResult == true) { continue mainLoop; } | 240 | if(consistencyCheckResult == true) { continue mainLoop; } |
206 | 241 | ||
207 | if (context.isCurrentStateAlreadyTraversed()) { | 242 | if (context.isCurrentStateAlreadyTraversed()) { |
208 | logger.info("The new state is already visited."); | 243 | logger.info("The new state is already visited."); |
209 | context.backtrack(); | 244 | context.backtrack(); |
210 | } else if (!context.checkGlobalConstraints()) { | 245 | } else if (!checkGlobalConstraints()) { |
211 | logger.debug("Global contraint is not satisifed."); | 246 | logger.debug("Global contraint is not satisifed."); |
212 | context.backtrack(); | 247 | context.backtrack(); |
248 | } else if (!numericSolver.maySatisfiable()) { | ||
249 | logger.debug("Numeric constraints are not satisifed."); | ||
250 | context.backtrack(); | ||
213 | } else { | 251 | } else { |
214 | final Fitness nextFitness = context.calculateFitness(); | 252 | final Fitness nextFitness = context.calculateFitness(); |
215 | solutionStore.newSolution(context); | 253 | checkForSolution(nextFitness); |
216 | if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) { | 254 | if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) { |
217 | logger.debug("Reached max depth."); | 255 | logger.debug("Reached max depth."); |
218 | context.backtrack(); | 256 | context.backtrack(); |
@@ -223,37 +261,50 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
223 | context.getTrajectory().toArray(), nextFitness); | 261 | context.getTrajectory().toArray(), nextFitness); |
224 | trajectoiresToExplore.add(nextTrajectoryWithfitness); | 262 | trajectoiresToExplore.add(nextTrajectoryWithfitness); |
225 | 263 | ||
226 | int compare = objectiveComparatorHelper.compare(currentTrajectoryWithfitness.fitness, | 264 | int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFitness.fitness, |
227 | nextTrajectoryWithfitness.fitness); | 265 | nextTrajectoryWithfitness.fitness); |
228 | if (compare < 0) { | 266 | if (compare < 0) { |
229 | logger.debug("Better fitness, moving on: " + nextFitness); | 267 | logger.debug("Better fitness, moving on: " + nextFitness); |
230 | currentTrajectoryWithfitness = nextTrajectoryWithfitness; | 268 | currentTrajectoryWithFitness = nextTrajectoryWithfitness; |
231 | continue mainLoop; | 269 | continue mainLoop; |
232 | } else if (compare == 0) { | 270 | } else if (compare == 0) { |
233 | logger.debug("Equally good fitness, moving on: " + nextFitness); | 271 | logger.debug("Equally good fitness, moving on: " + nextFitness); |
234 | currentTrajectoryWithfitness = nextTrajectoryWithfitness; | 272 | currentTrajectoryWithFitness = nextTrajectoryWithfitness; |
235 | continue mainLoop; | 273 | continue mainLoop; |
236 | } else { | 274 | } else { |
237 | logger.debug("Worse fitness."); | 275 | logger.debug("Worse fitness."); |
238 | currentTrajectoryWithfitness = null; | 276 | currentTrajectoryWithFitness = null; |
239 | continue mainLoop; | 277 | continue mainLoop; |
240 | } | 278 | } |
241 | } | 279 | } |
242 | } | 280 | } |
243 | 281 | ||
244 | logger.debug("State is fully traversed."); | 282 | logger.debug("State is fully traversed."); |
245 | trajectoiresToExplore.remove(currentTrajectoryWithfitness); | 283 | trajectoiresToExplore.remove(currentTrajectoryWithFitness); |
246 | currentTrajectoryWithfitness = null; | 284 | currentTrajectoryWithFitness = null; |
247 | 285 | ||
248 | } | 286 | } |
249 | logger.info("Interrupted."); | 287 | logger.info("Interrupted."); |
250 | } | 288 | } |
251 | 289 | ||
290 | private boolean checkGlobalConstraints() { | ||
291 | long start = System.nanoTime(); | ||
292 | boolean result = context.checkGlobalConstraints(); | ||
293 | globalConstraintEvaluationTime += System.nanoTime() - start; | ||
294 | return result; | ||
295 | } | ||
296 | |||
297 | private Fitness calculateFitness() { | ||
298 | long start = System.nanoTime(); | ||
299 | Fitness fitness = context.calculateFitness(); | ||
300 | fitnessCalculationTime += System.nanoTime() - start; | ||
301 | return fitness; | ||
302 | } | ||
303 | |||
252 | private List<Object> selectActivation() { | 304 | private List<Object> selectActivation() { |
253 | List<Object> activationIds; | 305 | List<Object> activationIds; |
254 | try { | 306 | try { |
255 | activationIds = new ArrayList<Object>(context.getUntraversedActivationIds()); | 307 | activationIds = this.activationSelector.randomizeActivationIDs(context.getUntraversedActivationIds()); |
256 | Collections.shuffle(activationIds); | ||
257 | } catch (NullPointerException e) { | 308 | } catch (NullPointerException e) { |
258 | // logger.warn("Unexpected state code: " + context.getDesignSpaceManager().getCurrentState()); | 309 | // logger.warn("Unexpected state code: " + context.getDesignSpaceManager().getCurrentState()); |
259 | numberOfStatecoderFail++; | 310 | numberOfStatecoderFail++; |
@@ -262,6 +313,37 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
262 | return activationIds; | 313 | return activationIds; |
263 | } | 314 | } |
264 | 315 | ||
316 | private void checkForSolution(final Fitness fittness) { | ||
317 | solutionStore.newSolution(context); | ||
318 | } | ||
319 | |||
320 | public List<String> times = new LinkedList<String>(); | ||
321 | private void saveTimes() { | ||
322 | long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder<?, ?>)this.context.getStateCoder()).getStatecoderRuntime()/1000000; | ||
323 | long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000; | ||
324 | long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000; | ||
325 | long activationSelection = this.activationSelector.getRuntime()/1000000; | ||
326 | long solutionCopierTime = this.solutionSaver.getTotalCopierRuntime()/1000000; | ||
327 | long numericalSolverSumTime = this.numericSolver.getRuntime()/1000000; | ||
328 | long numericalSolverProblemForming = this.numericSolver.getSolverSolvingProblem()/1000000; | ||
329 | long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000; | ||
330 | long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000; | ||
331 | this.times.add( | ||
332 | "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ | ||
333 | "|StateCoderTime:"+statecoderTime+ | ||
334 | "|ForwardTime:"+forwardTime+ | ||
335 | "|Backtrackingtime:"+backtrackingTime+ | ||
336 | "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+ | ||
337 | "|FitnessCalculationTime:"+(fitnessCalculationTime/1000000)+ | ||
338 | "|ActivationSelectionTime:"+activationSelection+ | ||
339 | "|SolutionCopyTime:"+solutionCopierTime+ | ||
340 | "|NumericalSolverSumTime:"+numericalSolverSumTime+ | ||
341 | "|NumericalSolverProblemFormingTime:"+numericalSolverProblemForming+ | ||
342 | "|NumericalSolverSolvingTime:"+numericalSolverSolving+ | ||
343 | "|NumericalSolverInterpretingSolution:"+numericalSolverInterpreting+")"); | ||
344 | |||
345 | } | ||
346 | |||
265 | @Override | 347 | @Override |
266 | public void interruptStrategy() { | 348 | public void interruptStrategy() { |
267 | isInterrupted = true; | 349 | isInterrupted = true; |
@@ -288,7 +370,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
288 | } else { | 370 | } else { |
289 | return trajectoiresToExplore.element(); | 371 | return trajectoiresToExplore.element(); |
290 | } | 372 | } |
291 | } | 373 | } |
292 | 374 | ||
293 | public void visualiseCurrentState() { | 375 | public void visualiseCurrentState() { |
294 | PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser; | 376 | PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser; |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend new file mode 100644 index 00000000..82a5f32d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/EvenActivationSelector.xtend | |||
@@ -0,0 +1,20 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.Random | ||
4 | import java.util.Collection | ||
5 | import java.util.Collections | ||
6 | import java.util.ArrayList | ||
7 | |||
8 | class EvenActivationSelector extends ActivationSelector { | ||
9 | |||
10 | new(Random r) { | ||
11 | super(r) | ||
12 | } | ||
13 | |||
14 | override protected internalRandomizationOfActivationIDs(Collection<Object> activationIDs) { | ||
15 | val toShuffle = new ArrayList<Object>(activationIDs); | ||
16 | Collections.shuffle(toShuffle); | ||
17 | return toShuffle | ||
18 | } | ||
19 | |||
20 | } \ 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/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 2976bebe..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,36 +1,58 @@ | |||
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 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 | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective |
5 | import java.util.Comparator | 7 | import java.util.Comparator |
6 | import java.util.List | 8 | import java.util.List |
7 | import org.eclipse.viatra.dse.base.ThreadContext | 9 | import org.eclipse.viatra.dse.base.ThreadContext |
8 | import org.eclipse.viatra.dse.objectives.Comparators | 10 | import org.eclipse.viatra.dse.objectives.Comparators |
9 | import org.eclipse.viatra.dse.objectives.IObjective | 11 | import org.eclipse.viatra.dse.objectives.IObjective |
10 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
11 | 12 | ||
12 | //class ViatraReasonerNumbers { | ||
13 | // public static val scopePriority = 2 | ||
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 | @FinalFieldsConstructor | ||
28 | class ModelGenerationCompositeObjective implements IThreeValuedObjective { | 13 | class ModelGenerationCompositeObjective implements IThreeValuedObjective { |
29 | val IObjective scopeObjective | 14 | val IObjective scopeObjective |
30 | val List<IObjective> unfinishedMultiplicityObjectives | 15 | val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives |
31 | val IObjective unfinishedWFObjective | 16 | val UnfinishedWFObjective unfinishedWFObjective |
17 | var PartialInterpretation model = null | ||
18 | val boolean punishSize | ||
19 | val int scopeWeight | ||
20 | val int conaintmentWeight | ||
21 | val int nonContainmentWeight | ||
22 | val int unfinishedWFWeight | ||
23 | |||
24 | new( | ||
25 | IObjective scopeObjective, | ||
26 | List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives, | ||
27 | UnfinishedWFObjective unfinishedWFObjective, | ||
28 | ViatraReasonerConfiguration configuration) | ||
29 | { | ||
30 | this( | ||
31 | scopeObjective, unfinishedMultiplicityObjectives, unfinishedWFObjective, configuration.punishSize, | ||
32 | configuration.scopeWeight, configuration.conaintmentWeight, configuration.nonContainmentWeight, | ||
33 | configuration.unfinishedWFWeight | ||
34 | ) | ||
35 | } | ||
32 | 36 | ||
37 | new( | ||
38 | IObjective scopeObjective, | ||
39 | List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives, | ||
40 | UnfinishedWFObjective unfinishedWFObjective, | ||
41 | boolean punishSize, int scopeWeight, int conaintmentWeight, int nonContainmentWeight, int unfinishedWFWeight) | ||
42 | { | ||
43 | this.scopeObjective = scopeObjective | ||
44 | this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives | ||
45 | this.unfinishedWFObjective = unfinishedWFObjective | ||
46 | |||
47 | this.punishSize = punishSize | ||
48 | this.scopeWeight = scopeWeight | ||
49 | this.conaintmentWeight = conaintmentWeight | ||
50 | this.nonContainmentWeight = nonContainmentWeight | ||
51 | this.unfinishedWFWeight = unfinishedWFWeight | ||
52 | } | ||
53 | |||
33 | override init(ThreadContext context) { | 54 | override init(ThreadContext context) { |
55 | model = context.model as PartialInterpretation | ||
34 | this.scopeObjective.init(context) | 56 | this.scopeObjective.init(context) |
35 | this.unfinishedMultiplicityObjectives.forEach[it.init(context)] | 57 | this.unfinishedMultiplicityObjectives.forEach[it.init(context)] |
36 | this.unfinishedWFObjective.init(context) | 58 | this.unfinishedWFObjective.init(context) |
@@ -39,27 +61,40 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective { | |||
39 | override createNew() { | 61 | override createNew() { |
40 | return new ModelGenerationCompositeObjective( | 62 | return new ModelGenerationCompositeObjective( |
41 | scopeObjective.createNew, | 63 | scopeObjective.createNew, |
42 | ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew]), | 64 | ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew as UnfinishedMultiplicityObjective]), |
43 | unfinishedWFObjective.createNew | 65 | unfinishedWFObjective.createNew as UnfinishedWFObjective, |
66 | punishSize, scopeWeight, conaintmentWeight, nonContainmentWeight, unfinishedWFWeight | ||
44 | ) | 67 | ) |
45 | } | 68 | } |
46 | 69 | ||
47 | override getComparator() { Comparators.LOWER_IS_BETTER } | 70 | override getComparator() { Comparators.LOWER_IS_BETTER } |
48 | 71 | ||
49 | override getFitness(ThreadContext context) { | 72 | override getFitness(ThreadContext context) { |
50 | var sum = 0.0 | 73 | |
51 | val scopeFitnes = scopeObjective.getFitness(context) | 74 | val scopeFitnes = scopeObjective.getFitness(context) |
52 | // val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] | ||
53 | val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) | 75 | val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) |
54 | 76 | ||
55 | sum += scopeFitnes | 77 | var containmentMultiplicity = 0.0 |
56 | var multiplicity = 0.0 | 78 | var nonContainmentMultiplicity = 0.0 |
57 | for (multiplicityObjective : unfinishedMultiplicityObjectives) { | 79 | for(multiplicityObjective : unfinishedMultiplicityObjectives) { |
58 | multiplicity += multiplicityObjective.getFitness(context) // *0.5 | 80 | if(multiplicityObjective.containment) { |
81 | containmentMultiplicity+=multiplicityObjective.getFitness(context) | ||
82 | } else { | ||
83 | nonContainmentMultiplicity+=multiplicityObjective.getFitness(context) | ||
84 | } | ||
59 | } | 85 | } |
60 | sum += multiplicity | 86 | val size = if(punishSize) { |
61 | sum += unfinishedWFsFitness // *0.5 | 87 | 0.9/model.newElements.size |
62 | // println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') | 88 | } else { |
89 | 0 | ||
90 | } | ||
91 | |||
92 | var sum = 0.0 | ||
93 | sum += scopeFitnes*scopeWeight | ||
94 | sum += containmentMultiplicity*conaintmentWeight | ||
95 | sum += nonContainmentMultiplicity*nonContainmentWeight | ||
96 | sum += unfinishedWFsFitness*unfinishedWFWeight | ||
97 | sum+=size | ||
63 | return sum | 98 | return sum |
64 | } | 99 | } |
65 | 100 | ||
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 new file mode 100644 index 00000000..066040a0 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | |||
@@ -0,0 +1,192 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | ||
11 | import java.math.BigDecimal | ||
12 | import java.util.HashMap | ||
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 | ||
22 | |||
23 | class NumericSolver { | ||
24 | val ModelGenerationMethod method | ||
25 | var ThreadContext threadContext | ||
26 | val constraint2MustUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | ||
27 | val constraint2CurrentUnitPropagationPrecondition = new HashMap<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> | ||
28 | NumericTranslator t = new NumericTranslator | ||
29 | |||
30 | val boolean intermediateConsistencyCheck | ||
31 | val boolean caching; | ||
32 | Map<LinkedHashMap<PConstraint, Iterable<List<Integer>>>,Boolean> satisfiabilityCache = new HashMap | ||
33 | |||
34 | var long runtime = 0 | ||
35 | var long cachingTime = 0 | ||
36 | var int numberOfSolverCalls = 0 | ||
37 | var int numberOfCachedSolverCalls = 0 | ||
38 | |||
39 | new(ModelGenerationMethod method, boolean intermediateConsistencyCheck, boolean caching) { | ||
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 | ||
49 | val engine = threadContext.queryEngine | ||
50 | for(entry : method.mustUnitPropagationPreconditions.entrySet) { | ||
51 | val constraint = entry.key | ||
52 | val querySpec = entry.value | ||
53 | val matcher = querySpec.getMatcher(engine); | ||
54 | constraint2MustUnitPropagationPrecondition.put(constraint,matcher) | ||
55 | } | ||
56 | for(entry : method.currentUnitPropagationPreconditions.entrySet) { | ||
57 | val constraint = entry.key | ||
58 | val querySpec = entry.value | ||
59 | val matcher = querySpec.getMatcher(engine); | ||
60 | constraint2CurrentUnitPropagationPrecondition.put(constraint,matcher) | ||
61 | } | ||
62 | } | ||
63 | |||
64 | def getRuntime(){runtime} | ||
65 | def getCachingTime(){cachingTime} | ||
66 | def getNumberOfSolverCalls(){numberOfSolverCalls} | ||
67 | def getNumberOfCachedSolverCalls(){numberOfCachedSolverCalls} | ||
68 | def getSolverFormingProblem(){this.t.formingProblemTime} | ||
69 | def getSolverSolvingProblem(){this.t.solvingProblemTime} | ||
70 | def getSolverSolution(){this.t.formingSolutionTime} | ||
71 | |||
72 | def boolean maySatisfiable() { | ||
73 | if(intermediateConsistencyCheck) { | ||
74 | return isSatisfiable(this.constraint2MustUnitPropagationPrecondition) | ||
75 | } else { | ||
76 | return true | ||
77 | } | ||
78 | } | ||
79 | def boolean currentSatisfiable() { | ||
80 | isSatisfiable(this.constraint2CurrentUnitPropagationPrecondition) | ||
81 | } | ||
82 | |||
83 | private def boolean isSatisfiable(Map<PConstraint,ViatraQueryMatcher<? extends IPatternMatch>> matches) { | ||
84 | val start = System.nanoTime | ||
85 | var boolean finalResult | ||
86 | if(matches.empty){ | ||
87 | finalResult=true | ||
88 | } else { | ||
89 | val propagatedConstraints = new HashMap | ||
90 | for(entry : matches.entrySet) { | ||
91 | val constraint = entry.key | ||
92 | //println(constraint) | ||
93 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
94 | //println(allMatches.toList) | ||
95 | propagatedConstraints.put(constraint,allMatches) | ||
96 | } | ||
97 | if(propagatedConstraints.values.forall[empty]) { | ||
98 | finalResult=true | ||
99 | } else { | ||
100 | if(caching) { | ||
101 | val code = getCode(propagatedConstraints) | ||
102 | val cachedResult = satisfiabilityCache.get(code) | ||
103 | if(cachedResult === null) { | ||
104 | // println('''new problem, call solver''') | ||
105 | // for(entry : code.entrySet) { | ||
106 | // println('''«entry.key» -> «entry.value»''') | ||
107 | // } | ||
108 | //println(code.hashCode) | ||
109 | this.numberOfSolverCalls++ | ||
110 | val res = t.delegateIsSatisfiable(propagatedConstraints) | ||
111 | satisfiabilityCache.put(code,res) | ||
112 | finalResult=res | ||
113 | } else { | ||
114 | //println('''similar problem, answer from cache''') | ||
115 | finalResult=cachedResult | ||
116 | this.numberOfCachedSolverCalls++ | ||
117 | } | ||
118 | } else { | ||
119 | finalResult= t.delegateIsSatisfiable(propagatedConstraints) | ||
120 | this.numberOfSolverCalls++ | ||
121 | } | ||
122 | } | ||
123 | } | ||
124 | this.runtime+=System.nanoTime-start | ||
125 | return finalResult | ||
126 | } | ||
127 | |||
128 | def getCode(HashMap<PConstraint, Iterable<Object[]>> propagatedConstraints) { | ||
129 | val start = System.nanoTime | ||
130 | val involvedObjects = new LinkedHashSet(propagatedConstraints.values.flatten.map[toList].flatten.toList).toList | ||
131 | val res = new LinkedHashMap(propagatedConstraints.mapValues[matches | matches.map[objects | objects.map[object | involvedObjects.indexOf(object)].toList]]) | ||
132 | this.cachingTime += System.nanoTime-start | ||
133 | return res | ||
134 | } | ||
135 | |||
136 | def fillSolutionCopy(Map<EObject, EObject> trace) { | ||
137 | val model = threadContext.getModel as PartialInterpretation | ||
138 | val dataObjects = model.newElements.filter(PrimitiveElement).filter[!model.openWorldElements.contains(it)].toList | ||
139 | if(constraint2CurrentUnitPropagationPrecondition.empty) { | ||
140 | fillWithDefaultValues(dataObjects,trace) | ||
141 | } else { | ||
142 | val propagatedConstraints = new HashMap | ||
143 | for(entry : constraint2CurrentUnitPropagationPrecondition.entrySet) { | ||
144 | val constraint = entry.key | ||
145 | val allMatches = entry.value.allMatches.map[it.toArray] | ||
146 | propagatedConstraints.put(constraint,allMatches) | ||
147 | } | ||
148 | |||
149 | if(propagatedConstraints.values.forall[empty]) { | ||
150 | fillWithDefaultValues(dataObjects,trace) | ||
151 | } else { | ||
152 | val solution = t.delegateGetSolution(dataObjects,propagatedConstraints) | ||
153 | fillWithSolutions(dataObjects,solution,trace) | ||
154 | } | ||
155 | } | ||
156 | } | ||
157 | |||
158 | def protected fillWithDefaultValues(List<PrimitiveElement> elements, Map<EObject, EObject> trace) { | ||
159 | for(element : elements) { | ||
160 | if(element.valueSet==false) { | ||
161 | val value = getDefaultValue(element) | ||
162 | val target = trace.get(element) as PrimitiveElement | ||
163 | target.fillWithValue(value) | ||
164 | } | ||
165 | } | ||
166 | } | ||
167 | |||
168 | def protected dispatch getDefaultValue(BooleanElement e) {false} | ||
169 | def protected dispatch getDefaultValue(IntegerElement e) {0} | ||
170 | def protected dispatch getDefaultValue(RealElement e) {0.0} | ||
171 | def protected dispatch getDefaultValue(StringElement e) {""} | ||
172 | |||
173 | def protected fillWithSolutions(List<PrimitiveElement> elements, Map<PrimitiveElement, Number> solution, Map<EObject, EObject> trace) { | ||
174 | for(element : elements) { | ||
175 | if(element.valueSet==false) { | ||
176 | if(solution.containsKey(element)) { | ||
177 | val value = solution.get(element) | ||
178 | val target = trace.get(element) as PrimitiveElement | ||
179 | target.fillWithValue(value) | ||
180 | } else { | ||
181 | val target = trace.get(element) as PrimitiveElement | ||
182 | target.fillWithValue(target.defaultValue) | ||
183 | } | ||
184 | } | ||
185 | } | ||
186 | } | ||
187 | |||
188 | def protected dispatch fillWithValue(BooleanElement e, Object value) {e.valueSet=true e.value=value as Boolean} | ||
189 | def protected dispatch fillWithValue(IntegerElement e, Object value) {e.valueSet=true e.value=value as Integer} | ||
190 | def protected dispatch fillWithValue(RealElement e, Object value) {e.valueSet=true e.value=BigDecimal.valueOf(value as Double) } | ||
191 | def protected dispatch fillWithValue(StringElement e, Object value) {e.valueSet=true e.value=value as String} | ||
192 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend index b63bfe8b..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 | |||
@@ -153,14 +153,70 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | |||
153 | } | 153 | } |
154 | 154 | ||
155 | override getAllIntegersInStructure() { | 155 | override getAllIntegersInStructure() { |
156 | new TreeSet(this.integerForwardTrace.keySet) | 156 | new TreeSet(allIntegersWithInterpretation.values) |
157 | } | ||
158 | |||
159 | override getAllIntegersWithInterpretation() { | ||
160 | val builder = new HashMap | ||
161 | for (entry : integerForwardTrace.entrySet) { | ||
162 | builder.put(entry.value, entry.key) | ||
163 | } | ||
164 | for (element : partialInterpretation.newElements) { | ||
165 | if (element instanceof IntegerElement) { | ||
166 | builder.put(element, element.value) | ||
167 | } | ||
168 | } | ||
169 | builder | ||
157 | } | 170 | } |
158 | 171 | ||
159 | override getAllRealsInStructure() { | 172 | override getAllRealsInStructure() { |
160 | new TreeSet(this.realForwardTrace.keySet) | 173 | new TreeSet(allRealsWithInterpretation.values) |
174 | } | ||
175 | |||
176 | override getAllRealsWithInterpretation() { | ||
177 | val builder = new HashMap | ||
178 | for (entry : realForwardTrace.entrySet) { | ||
179 | builder.put(entry.value, entry.key) | ||
180 | } | ||
181 | for (element : partialInterpretation.newElements) { | ||
182 | if (element instanceof RealElement) { | ||
183 | builder.put(element, element.value) | ||
184 | } | ||
185 | } | ||
186 | builder | ||
161 | } | 187 | } |
162 | 188 | ||
163 | override getAllStringsInStructure() { | 189 | override getAllStringsInStructure() { |
164 | new TreeSet(this.stringForwardTrace.keySet) | 190 | new TreeSet(allStringsWithInterpretation.values) |
191 | } | ||
192 | |||
193 | override getAllStringsWithInterpretation() { | ||
194 | val builder = new HashMap | ||
195 | for (entry : stringForwardTrace.entrySet) { | ||
196 | builder.put(entry.value, entry.key) | ||
197 | } | ||
198 | for (element : partialInterpretation.newElements) { | ||
199 | if (element instanceof StringElement) { | ||
200 | builder.put(element, element.value) | ||
201 | } | ||
202 | } | ||
203 | builder | ||
204 | } | ||
205 | |||
206 | override getAllBooleansInStructure() { | ||
207 | new TreeSet(allBooleansWithInterpretation.values) | ||
208 | } | ||
209 | |||
210 | override getAllBooleansWithInterpretation() { | ||
211 | val builder = new HashMap | ||
212 | for (entry : booleanForwardTrace.entrySet) { | ||
213 | builder.put(entry.value, entry.key) | ||
214 | } | ||
215 | for (element : partialInterpretation.newElements) { | ||
216 | if (element instanceof BooleanElement) { | ||
217 | builder.put(element, element.value) | ||
218 | } | ||
219 | } | ||
220 | builder | ||
165 | } | 221 | } |
166 | } | 222 | } |
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 index d036257d..38c8f5a1 100644 --- 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 | |||
@@ -19,12 +19,23 @@ class CopiedSolution { | |||
19 | @Accessors var boolean current = true | 19 | @Accessors var boolean current = true |
20 | } | 20 | } |
21 | 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 | */ | ||
22 | class SolutionCopier { | 28 | class SolutionCopier { |
29 | val NumericSolver numericSolver | ||
23 | val copiedSolutions = new LinkedHashMap<Object, CopiedSolution> | 30 | val copiedSolutions = new LinkedHashMap<Object, CopiedSolution> |
24 | 31 | ||
25 | long startTime = System.nanoTime | 32 | long startTime = System.nanoTime |
26 | @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 | 33 | @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 |
27 | 34 | ||
35 | new(NumericSolver numericSolver) { | ||
36 | this.numericSolver = numericSolver | ||
37 | } | ||
38 | |||
28 | def void copySolution(ThreadContext context, Object solutionId) { | 39 | def void copySolution(ThreadContext context, Object solutionId) { |
29 | val existingCopy = copiedSolutions.get(solutionId) | 40 | val existingCopy = copiedSolutions.get(solutionId) |
30 | if (existingCopy === null) { | 41 | if (existingCopy === null) { |
@@ -36,6 +47,7 @@ class SolutionCopier { | |||
36 | totalCopierRuntime += System.nanoTime - copyStart | 47 | totalCopierRuntime += System.nanoTime - copyStart |
37 | val copierRuntime = System.nanoTime - startTime | 48 | val copierRuntime = System.nanoTime - startTime |
38 | val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime) | 49 | val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime) |
50 | numericSolver.fillSolutionCopy(copiedSolution.trace) | ||
39 | copiedSolutions.put(solutionId, copiedSolution) | 51 | copiedSolutions.put(solutionId, copiedSolution) |
40 | } else { | 52 | } else { |
41 | existingCopy.current = true | 53 | existingCopy.current = true |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend new file mode 100644 index 00000000..4bd2c349 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend | |||
@@ -0,0 +1,51 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
4 | import java.util.LinkedList | ||
5 | import java.util.List | ||
6 | import java.util.Map | ||
7 | import org.eclipse.emf.ecore.EObject | ||
8 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
9 | import org.eclipse.viatra.dse.base.ThreadContext | ||
10 | |||
11 | class SolutionStoreWithCopy { | ||
12 | |||
13 | long runtime = 0 | ||
14 | List<PartialInterpretation> solutions = new LinkedList | ||
15 | //public List<SortedMap<String,Integer>> additionalMatches = new LinkedList | ||
16 | List<Map<EObject,EObject>> copyTraces = new LinkedList | ||
17 | |||
18 | long sartTime = System.nanoTime | ||
19 | List<Long> solutionTimes = new LinkedList | ||
20 | |||
21 | /*def newSolution(ThreadContext context, SortedMap<String,Integer> additonalMatch) { | ||
22 | additionalMatches+= additonalMatch | ||
23 | newSolution(context) | ||
24 | }*/ | ||
25 | |||
26 | def Map<EObject,EObject> newSolution(ThreadContext context) { | ||
27 | //print(System.nanoTime-initTime + ";") | ||
28 | val copyStart = System.nanoTime | ||
29 | val solution = context.model as PartialInterpretation | ||
30 | val copier = new EcoreUtil.Copier | ||
31 | val solutionCopy = copier.copy(solution) as PartialInterpretation | ||
32 | copier.copyReferences | ||
33 | solutions.add(solutionCopy) | ||
34 | copyTraces.add(copier) | ||
35 | runtime += System.nanoTime - copyStart | ||
36 | solutionTimes.add(System.nanoTime-sartTime) | ||
37 | return copier | ||
38 | } | ||
39 | def getSumRuntime() { | ||
40 | return runtime | ||
41 | } | ||
42 | def getAllRuntimes() { | ||
43 | return solutionTimes | ||
44 | } | ||
45 | def getSolutions() { | ||
46 | solutions | ||
47 | } | ||
48 | def getCopyTraces() { | ||
49 | return copyTraces | ||
50 | } | ||
51 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend index 9f0c642f..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 | |||
@@ -7,7 +7,7 @@ import org.eclipse.viatra.dse.objectives.Comparators | |||
7 | import org.eclipse.viatra.dse.objectives.IObjective | 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 | new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) { | 12 | new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) { |
13 | this.unfinishedMultiplicity = unfinishedMultiplicity | 13 | this.unfinishedMultiplicity = unfinishedMultiplicity |
@@ -34,4 +34,8 @@ class UnfinishedMultiplicityObjective implements IObjective { | |||
34 | override setLevel(int level) { | 34 | override setLevel(int level) { |
35 | throw new UnsupportedOperationException | 35 | throw new UnsupportedOperationException |
36 | } | 36 | } |
37 | |||
38 | def isContainment() { | ||
39 | return this.unfinishedMultiplicity.containment | ||
40 | } | ||
37 | } | 41 | } |
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 index 74500cc2..d879d4cc 100644 --- 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 | |||
@@ -14,9 +14,12 @@ import org.eclipse.xtend.lib.annotations.Accessors | |||
14 | 14 | ||
15 | /** | 15 | /** |
16 | * Based on {@link SolutionStore.BestSolutionSaver}. | 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}. | ||
17 | */ | 20 | */ |
18 | class ViatraReasonerSolutionSaver implements ISolutionSaver { | 21 | class ViatraReasonerSolutionSaver implements ISolutionSaver { |
19 | @Accessors val solutionCopier = new SolutionCopier | 22 | @Accessors val SolutionCopier solutionCopier |
20 | @Accessors val DiversityChecker diversityChecker | 23 | @Accessors val DiversityChecker diversityChecker |
21 | val boolean hasExtremalObjectives | 24 | val boolean hasExtremalObjectives |
22 | val int numberOfRequiredSolutions | 25 | val int numberOfRequiredSolutions |
@@ -25,11 +28,12 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { | |||
25 | 28 | ||
26 | @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection | 29 | @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection |
27 | 30 | ||
28 | new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) { | 31 | new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker, NumericSolver numericSolver) { |
29 | this.diversityChecker = diversityChecker | 32 | this.diversityChecker = diversityChecker |
30 | comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) | 33 | comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) |
31 | hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] | 34 | hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] |
32 | this.numberOfRequiredSolutions = numberOfRequiredSolutions | 35 | this.numberOfRequiredSolutions = numberOfRequiredSolutions |
36 | this.solutionCopier = new SolutionCopier(numericSolver) | ||
33 | } | 37 | } |
34 | 38 | ||
35 | override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { | 39 | override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { |
@@ -139,4 +143,8 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { | |||
139 | } | 143 | } |
140 | solutionsCollection.size < numberOfRequiredSolutions | 144 | solutionsCollection.size < numberOfRequiredSolutions |
141 | } | 145 | } |
146 | |||
147 | def getTotalCopierRuntime() { | ||
148 | solutionCopier.totalCopierRuntime | ||
149 | } | ||
142 | } | 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 63d78220..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 | |||
@@ -13,12 +13,10 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification | |||
13 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 13 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
14 | 14 | ||
15 | class WF2ObjectiveConverter { | 15 | class WF2ObjectiveConverter { |
16 | static val UNFINISHED_WFS_NAME = "unfinishedWFs" | ||
17 | static val INVALIDATED_WFS_NAME = "invalidatedWFs" | 16 | static val INVALIDATED_WFS_NAME = "invalidatedWFs" |
18 | 17 | ||
19 | def createCompletenessObjective( | 18 | def createCompletenessObjective( |
20 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) { | 19 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) { |
21 | // createConstraintObjective(UNFINISHED_WFS_NAME, unfinishedWF) | ||
22 | new UnfinishedWFObjective(unfinishedWF) | 20 | new UnfinishedWFObjective(unfinishedWF) |
23 | } | 21 | } |
24 | 22 | ||