diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner')
28 files changed, 1527 insertions, 415 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF index 2a271acf..4ad61ccb 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/META-INF/MANIFEST.MF | |||
@@ -3,7 +3,8 @@ Bundle-ManifestVersion: 2 | |||
3 | Bundle-Name: Reasoner | 3 | Bundle-Name: Reasoner |
4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | 4 | Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner |
5 | Bundle-Version: 1.0.0.qualifier | 5 | Bundle-Version: 1.0.0.qualifier |
6 | Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | 6 | Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner, |
7 | hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
7 | Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | 8 | Require-Bundle: hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", |
8 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | 9 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", |
9 | hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", | 10 | hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", |
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 6639e5f3..aa02cd30 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 | |||
@@ -1,5 +1,7 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.Lists | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException |
@@ -10,19 +12,28 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | |||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider | 14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ScopePropagator | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser |
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage |
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.AbstractNeighbourhoodBasedStateCoderFactory | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory | 20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory | 21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedHashStateCoderFactory |
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration | 24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration |
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker | ||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint | ||
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective | 28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective |
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation | 29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation |
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective | 30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective |
31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective | 32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective |
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedWFObjective | 33 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver |
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter | 34 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter |
35 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement | ||
36 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective | ||
26 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 37 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
27 | import java.util.List | 38 | import java.util.List |
28 | import java.util.Map | 39 | import java.util.Map |
@@ -31,185 +42,263 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer | |||
31 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel | 42 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel |
32 | import org.eclipse.viatra.dse.solutionstore.SolutionStore | 43 | import org.eclipse.viatra.dse.solutionstore.SolutionStore |
33 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory | 44 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory |
34 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SolutionStoreWithDiversityDescriptor | ||
35 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityGranularity | ||
36 | 45 | ||
37 | class ViatraReasoner extends LogicReasoner{ | 46 | class ViatraReasoner extends LogicReasoner { |
38 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() | 47 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() |
39 | val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider | 48 | val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider |
40 | val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE | 49 | val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE |
41 | val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter | 50 | val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter |
42 | 51 | ||
43 | 52 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, | |
44 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | 53 | ReasonerWorkspace workspace) throws LogicReasonerException { |
45 | val viatraConfig = configuration.asConfig | 54 | val viatraConfig = configuration.asConfig |
46 | 55 | ||
47 | if(viatraConfig.debugCongiguration.logging) { | 56 | if (viatraConfig.documentationLevel == DocumentationLevel.FULL) { |
48 | DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL) | 57 | DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL) |
49 | } else { | 58 | } else { |
50 | DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN) | 59 | DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN) |
51 | } | 60 | } |
52 | 61 | ||
53 | val DesignSpaceExplorer dse = new DesignSpaceExplorer(); | 62 | val DesignSpaceExplorer dse = new DesignSpaceExplorer(); |
54 | 63 | ||
55 | dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE) | 64 | dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE) |
56 | dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE) | 65 | dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE) |
57 | dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE) | 66 | dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE) |
58 | 67 | ||
59 | val transformationStartTime = System.nanoTime | 68 | val transformationStartTime = System.nanoTime |
60 | 69 | ||
61 | 70 | val emptySolution = initialiser.initialisePartialInterpretation(problem, viatraConfig.typeScopes).output | |
62 | 71 | if ((viatraConfig.documentationLevel == DocumentationLevel::FULL || | |
63 | val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output | 72 | viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { |
64 | if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { | 73 | workspace.writeModel(emptySolution, "init.partialmodel") |
65 | workspace.writeModel(emptySolution,"init.partialmodel") | 74 | } |
66 | } | ||
67 | emptySolution.problemConainer = problem | 75 | emptySolution.problemConainer = problem |
68 | 76 | var BasicScopeGlobalConstraint basicScopeGlobalConstraint = null | |
69 | val ScopePropagator scopePropagator = new ScopePropagator(emptySolution) | 77 | if (viatraConfig.scopePropagatorStrategy == ScopePropagatorStrategy.None) { |
70 | scopePropagator.propagateAllScopeConstraints | 78 | basicScopeGlobalConstraint = new BasicScopeGlobalConstraint(emptySolution) |
71 | 79 | emptySolution.scopes.clear | |
80 | } | ||
81 | |||
72 | val method = modelGenerationMethodProvider.createModelGenerationMethod( | 82 | val method = modelGenerationMethodProvider.createModelGenerationMethod( |
73 | problem, | 83 | problem, |
74 | emptySolution, | 84 | emptySolution, |
75 | workspace, | 85 | workspace, |
76 | viatraConfig.nameNewElements, | 86 | viatraConfig.nameNewElements, |
77 | viatraConfig.typeInferenceMethod, | 87 | viatraConfig.typeInferenceMethod, |
78 | scopePropagator, | 88 | viatraConfig.scopePropagatorStrategy, |
89 | viatraConfig.hints, | ||
79 | viatraConfig.documentationLevel | 90 | viatraConfig.documentationLevel |
80 | ) | 91 | ) |
81 | 92 | ||
82 | dse.addObjective(new ModelGenerationCompositeObjective( | 93 | dse.addObjective(new ModelGenerationCompositeObjective( |
83 | new ScopeObjective, | 94 | basicScopeGlobalConstraint ?: new ScopeObjective, |
84 | method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], | 95 | method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], |
85 | new UnfinishedWFObjective(method.unfinishedWF) | 96 | wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF) |
86 | )) | 97 | )) |
87 | 98 | ||
88 | dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF)) | 99 | val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size) |
89 | for(additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) { | 100 | for (entry : viatraConfig.costObjectives.indexed) { |
101 | val objectiveName = '''costObjective«entry.key»''' | ||
102 | val objectiveConfig = entry.value | ||
103 | val elementsBuilder = ImmutableList.builder | ||
104 | for (elementConfig : objectiveConfig.elements) { | ||
105 | val relationName = elementConfig.patternQualifiedName | ||
106 | val modalQueries = method.modalRelationQueries.get(relationName) | ||
107 | if (modalQueries === null) { | ||
108 | throw new IllegalArgumentException("Unknown relation: " + relationName) | ||
109 | } | ||
110 | elementsBuilder.add(new ThreeValuedCostElement( | ||
111 | modalQueries.currentQuery, | ||
112 | modalQueries.mayQuery, | ||
113 | modalQueries.mustQuery, | ||
114 | elementConfig.weight | ||
115 | )) | ||
116 | } | ||
117 | val costElements = elementsBuilder.build | ||
118 | val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind, | ||
119 | objectiveConfig.threshold, 3) | ||
120 | dse.addObjective(costObjective) | ||
121 | if (objectiveConfig.findExtremum) { | ||
122 | extremalObjectives += costObjective | ||
123 | } | ||
124 | } | ||
125 | |||
126 | val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions | ||
127 | val solutionStore = if (extremalObjectives.empty) { | ||
128 | new SolutionStore(numberOfRequiredSolutions) | ||
129 | } else { | ||
130 | new SolutionStore() | ||
131 | } | ||
132 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) | ||
133 | val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement) | ||
134 | val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions, | ||
135 | diversityChecker) | ||
136 | val solutionCopier = solutionSaver.solutionCopier | ||
137 | solutionStore.withSolutionSaver(solutionSaver) | ||
138 | dse.solutionStore = solutionStore | ||
139 | |||
140 | dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationGlobalConstraint(method.invalidWF)) | ||
141 | dse.addGlobalConstraint(new SurelyViolatedObjectiveGlobalConstraint(solutionSaver)) | ||
142 | dse.addGlobalConstraint(new InconsistentScopeGlobalConstraint) | ||
143 | if (basicScopeGlobalConstraint !== null) { | ||
144 | dse.addGlobalConstraint(basicScopeGlobalConstraint) | ||
145 | } | ||
146 | for (additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) { | ||
90 | dse.addGlobalConstraint(additionalConstraint.apply(method)) | 147 | dse.addGlobalConstraint(additionalConstraint.apply(method)) |
91 | } | 148 | } |
92 | 149 | ||
93 | dse.setInitialModel(emptySolution,false) | 150 | dse.setInitialModel(emptySolution, false) |
94 | 151 | ||
95 | val IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) { | 152 | val IStateCoderFactory statecoder = switch (viatraConfig.stateCoderStrategy) { |
96 | new NeighbourhoodBasedStateCoderFactory | 153 | case Neighbourhood: |
97 | } else { | 154 | new NeighbourhoodBasedHashStateCoderFactory |
98 | new IdentifierBasedStateCoderFactory | 155 | case PairwiseNeighbourhood: |
156 | new PairwiseNeighbourhoodBasedStateCoderFactory | ||
157 | default: | ||
158 | new IdentifierBasedStateCoderFactory | ||
99 | } | 159 | } |
100 | dse.stateCoderFactory = statecoder | 160 | dse.stateCoderFactory = statecoder |
101 | 161 | ||
102 | dse.maxNumberOfThreads = 1 | 162 | dse.maxNumberOfThreads = 1 |
103 | 163 | ||
104 | val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolution) | 164 | for (rule : method.relationRefinementRules) { |
105 | dse.solutionStore = solutionStore | ||
106 | |||
107 | for(rule : method.relationRefinementRules) { | ||
108 | dse.addTransformationRule(rule) | 165 | dse.addTransformationRule(rule) |
109 | } | 166 | } |
110 | for(rule : method.objectRefinementRules) { | 167 | for (rule : method.objectRefinementRules) { |
111 | dse.addTransformationRule(rule) | 168 | dse.addTransformationRule(rule) |
112 | } | 169 | } |
113 | 170 | ||
114 | val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) | 171 | val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method) |
115 | viatraConfig.progressMonitor.workedForwardTransformation | 172 | viatraConfig.progressMonitor.workedForwardTransformation |
116 | 173 | ||
117 | val transformationTime = System.nanoTime - transformationStartTime | 174 | val transformationTime = System.nanoTime - transformationStartTime |
118 | val solverStartTime = System.nanoTime | 175 | val solverStartTime = System.nanoTime |
119 | 176 | ||
120 | var boolean stoppedByTimeout | 177 | var boolean stoppedByTimeout |
121 | var boolean stoppedByException | 178 | try { |
122 | try{ | 179 | stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000); |
123 | stoppedByTimeout = dse.startExplorationWithTimeout(strategy,configuration.runtimeLimit*1000); | ||
124 | stoppedByException = false | ||
125 | } catch (NullPointerException npe) { | 180 | } catch (NullPointerException npe) { |
126 | stoppedByTimeout = false | 181 | stoppedByTimeout = false |
127 | stoppedByException = true | ||
128 | } | 182 | } |
129 | val solverTime = System.nanoTime - solverStartTime | 183 | val solverTime = System.nanoTime - solverStartTime |
130 | viatraConfig.progressMonitor.workedSearchFinished | 184 | viatraConfig.progressMonitor.workedSearchFinished |
131 | 185 | ||
132 | //additionalMatches = strategy.solutionStoreWithCopy.additionalMatches | 186 | // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches |
133 | val statistics = createStatistics => [ | 187 | val statistics = createStatistics => [ |
134 | //it.solverTime = viatraConfig.runtimeLimit | 188 | // it.solverTime = viatraConfig.runtimeLimit |
135 | it.solverTime = (solverTime/1000000) as int | 189 | it.solverTime = (solverTime / 1000000) as int |
136 | it.transformationTime = (transformationTime/1000000) as int | 190 | it.transformationTime = (transformationTime / 1000000) as int |
137 | for(x : 0..<strategy.solutionStoreWithCopy.allRuntimes.size) { | 191 | for (pair : solutionCopier.getAllCopierRuntimes(true).indexed) { |
138 | it.entries += createIntStatisticEntry => [ | 192 | it.entries += createIntStatisticEntry => [ |
139 | it.name = '''_Solution«x»FoundAt''' | 193 | it.name = '''_Solution«pair.key»FoundAt''' |
140 | it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int | 194 | it.value = (pair.value / 1000000) as int |
141 | ] | 195 | ] |
142 | } | 196 | } |
143 | it.entries += createIntStatisticEntry => [ | 197 | it.entries += createIntStatisticEntry => [ |
144 | it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int | 198 | it.name = "TransformationExecutionTime" |
199 | it.value = (method.statistics.transformationExecutionTime / 1000000) as int | ||
200 | ] | ||
201 | it.entries += createIntStatisticEntry => [ | ||
202 | it.name = "ScopePropagationTime" | ||
203 | it.value = (method.statistics.scopePropagationTime / 1000000) as int | ||
204 | ] | ||
205 | it.entries += createIntStatisticEntry => [ | ||
206 | it.name = "TypeAnalysisTime" | ||
207 | it.value = (method.statistics.preliminaryTypeAnalisisTime / 1000000) as int | ||
208 | ] | ||
209 | it.entries += createIntStatisticEntry => [ | ||
210 | it.name = "StateCoderTime" | ||
211 | it.value = (statecoder.runtime / 1000000) as int | ||
145 | ] | 212 | ] |
146 | it.entries += createIntStatisticEntry => [ | 213 | it.entries += createIntStatisticEntry => [ |
147 | it.name = "TypeAnalysisTime" it.value = (method.statistics.PreliminaryTypeAnalisisTime/1000000) as int | 214 | it.name = "StateCoderFailCount" |
215 | it.value = strategy.numberOfStatecoderFail | ||
148 | ] | 216 | ] |
149 | it.entries += createIntStatisticEntry => [ | 217 | it.entries += createIntStatisticEntry => [ |
150 | it.name = "StateCoderTime" it.value = (statecoder.runtime/1000000) as int | 218 | it.name = "SolutionCopyTime" |
219 | it.value = (solutionCopier.getTotalCopierRuntime / 1000000) as int | ||
151 | ] | 220 | ] |
152 | it.entries += createIntStatisticEntry => [ | 221 | it.entries += createIntStatisticEntry => [ |
153 | it.name = "StateCoderFailCount" it.value = strategy.numberOfStatecoderFail | 222 | it.name = "States" |
223 | it.value = dse.numberOfStates as int | ||
154 | ] | 224 | ] |
155 | it.entries += createIntStatisticEntry => [ | 225 | it.entries += createIntStatisticEntry => [ |
156 | it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int | 226 | it.name = "Decisions" |
227 | it.value = method.statistics.decisionsTried | ||
157 | ] | 228 | ] |
158 | if(strategy.solutionStoreWithDiversityDescriptor.isActive) { | 229 | it.entries += createIntStatisticEntry => [ |
230 | it.name = "Transformations" | ||
231 | it.value = method.statistics.transformationInvocations | ||
232 | ] | ||
233 | it.entries += createIntStatisticEntry => [ | ||
234 | it.name = "ScopePropagations" | ||
235 | it.value = method.statistics.scopePropagatorInvocations | ||
236 | ] | ||
237 | it.entries += createIntStatisticEntry => [ | ||
238 | it.name = "ScopePropagationsSolverCalls" | ||
239 | it.value = method.statistics.scopePropagatorSolverInvocations | ||
240 | ] | ||
241 | if (diversityChecker.isActive) { | ||
159 | it.entries += createIntStatisticEntry => [ | 242 | it.entries += createIntStatisticEntry => [ |
160 | it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int | 243 | it.name = "SolutionDiversityCheckTime" |
244 | it.value = (diversityChecker.totalRuntime / 1000000) as int | ||
161 | ] | 245 | ] |
162 | it.entries += createRealStatisticEntry => [ | 246 | it.entries += createRealStatisticEntry => [ |
163 | it.name = "SolutionDiversitySuccessRate" it.value = strategy.solutionStoreWithDiversityDescriptor.successRate | 247 | it.name = "SolutionDiversitySuccessRate" |
248 | it.value = diversityChecker.successRate | ||
164 | ] | 249 | ] |
165 | } | 250 | } |
166 | ] | 251 | ] |
167 | 252 | ||
168 | viatraConfig.progressMonitor.workedBackwardTransformationFinished | 253 | viatraConfig.progressMonitor.workedBackwardTransformationFinished |
169 | 254 | ||
170 | if(stoppedByTimeout) { | 255 | if (stoppedByTimeout) { |
171 | return createInsuficientResourcesResult=>[ | 256 | return createInsuficientResourcesResult => [ |
172 | it.problem = problem | 257 | it.problem = problem |
173 | it.resourceName="time" | 258 | it.resourceName = "time" |
174 | it.representation += strategy.solutionStoreWithCopy.solutions | 259 | it.representation += solutionCopier.getPartialInterpretations(true) |
175 | it.statistics = statistics | 260 | it.statistics = statistics |
176 | ] | 261 | ] |
177 | } else { | 262 | } else { |
178 | if(solutionStore.solutions.empty) { | 263 | if (solutionStore.solutions.empty) { |
179 | return createInconsistencyResult => [ | 264 | return createInconsistencyResult => [ |
180 | it.problem = problem | 265 | it.problem = problem |
181 | it.representation += strategy.solutionStoreWithCopy.solutions | 266 | it.representation += solutionCopier.getPartialInterpretations(true) |
182 | it.statistics = statistics | 267 | it.statistics = statistics |
183 | ] | 268 | ] |
184 | } else { | 269 | } else { |
185 | return createModelResult => [ | 270 | return createModelResult => [ |
186 | it.problem = problem | 271 | it.problem = problem |
187 | it.trace = strategy.solutionStoreWithCopy.copyTraces | 272 | it.trace = solutionCopier.getTraces(true) |
188 | it.representation += strategy.solutionStoreWithCopy.solutions | 273 | it.representation += solutionCopier.getPartialInterpretations(true) |
189 | it.statistics = statistics | 274 | it.statistics = statistics |
190 | ] | 275 | ] |
191 | } | 276 | } |
192 | } | 277 | } |
193 | } | 278 | } |
194 | 279 | ||
195 | private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) { | 280 | private def dispatch long runtime(AbstractNeighbourhoodBasedStateCoderFactory sc) { |
196 | sc.sumStatecoderRuntime | 281 | sc.sumStatecoderRuntime |
197 | } | 282 | } |
198 | 283 | ||
199 | private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) { | 284 | private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) { |
200 | sc.sumStatecoderRuntime | 285 | sc.sumStatecoderRuntime |
201 | } | 286 | } |
202 | 287 | ||
203 | override getInterpretations(ModelResult modelResult) { | 288 | override getInterpretations(ModelResult modelResult) { |
204 | val indexes = 0..<modelResult.representation.size | 289 | val indexes = 0 ..< modelResult.representation.size |
205 | val traces = modelResult.trace as List<Map<EObject, EObject>>; | 290 | val traces = modelResult.trace as List<Map<EObject, EObject>>; |
206 | val res = indexes.map[i | new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation,traces.get(i))].toList | 291 | val res = indexes.map [ i | |
292 | new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation, | ||
293 | traces.get(i)) | ||
294 | ].toList | ||
207 | return res | 295 | return res |
208 | } | 296 | } |
209 | 297 | ||
210 | private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) { | 298 | private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) { |
211 | if(configuration instanceof ViatraReasonerConfiguration) { | 299 | if (configuration instanceof ViatraReasonerConfiguration) { |
212 | return configuration | 300 | return configuration |
213 | } else throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''') | 301 | } else |
302 | throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''') | ||
214 | } | 303 | } |
215 | } | 304 | } |
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..6f38d261 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 | |||
@@ -6,19 +6,28 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | |||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold | ||
10 | import java.util.LinkedList | 15 | import java.util.LinkedList |
11 | import java.util.List | 16 | import java.util.List |
12 | import java.util.Set | 17 | import java.util.Set |
13 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 18 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
14 | 20 | ||
15 | public enum StateCoderStrategy { | 21 | enum StateCoderStrategy { |
16 | Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity | 22 | Neighbourhood, |
23 | PairwiseNeighbourhood, | ||
24 | NeighbourhoodWithEquivalence, | ||
25 | IDBased, | ||
26 | DefinedByDiversity | ||
17 | } | 27 | } |
18 | 28 | ||
19 | class ViatraReasonerConfiguration extends LogicSolverConfiguration{ | 29 | class ViatraReasonerConfiguration extends LogicSolverConfiguration { |
20 | //public var Iterable<PQuery> existingQueries | 30 | // public var Iterable<PQuery> existingQueries |
21 | |||
22 | public var nameNewElements = false | 31 | public var nameNewElements = false |
23 | public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood | 32 | public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood |
24 | public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis | 33 | public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis |
@@ -26,7 +35,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{ | |||
26 | * Once per 1/randomBacktrackChance the search selects a random state. | 35 | * Once per 1/randomBacktrackChance the search selects a random state. |
27 | */ | 36 | */ |
28 | public var int randomBacktrackChance = 20; | 37 | public var int randomBacktrackChance = 20; |
29 | 38 | ||
30 | /** | 39 | /** |
31 | * Describes the required diversity between the solutions. | 40 | * Describes the required diversity between the solutions. |
32 | * Null means that the solutions have to have different state codes only. | 41 | * Null means that the solutions have to have different state codes only. |
@@ -40,14 +49,21 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{ | |||
40 | /** | 49 | /** |
41 | * Configuration for debugging support. | 50 | * Configuration for debugging support. |
42 | */ | 51 | */ |
43 | public var DebugConfiguration debugCongiguration = new DebugConfiguration | 52 | public var DebugConfiguration debugConfiguration = new DebugConfiguration |
44 | /** | 53 | /** |
45 | * Configuration for cutting search space. | 54 | * Configuration for cutting search space. |
46 | */ | 55 | */ |
47 | public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint | 56 | public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint |
57 | |||
58 | public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral( | ||
59 | PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp) | ||
60 | |||
61 | public var List<LinearTypeConstraintHint> hints = newArrayList | ||
62 | |||
63 | public var List<CostObjectiveConfiguration> costObjectives = newArrayList | ||
48 | } | 64 | } |
49 | 65 | ||
50 | public class DiversityDescriptor { | 66 | class DiversityDescriptor { |
51 | public var ensureDiversity = false | 67 | public var ensureDiversity = false |
52 | public static val FixPointRange = -1 | 68 | public static val FixPointRange = -1 |
53 | public var int range = FixPointRange | 69 | public var int range = FixPointRange |
@@ -57,20 +73,31 @@ public class DiversityDescriptor { | |||
57 | public var Set<RelationDeclaration> relevantRelations = null | 73 | public var Set<RelationDeclaration> relevantRelations = null |
58 | } | 74 | } |
59 | 75 | ||
60 | public class DebugConfiguration { | 76 | class DebugConfiguration { |
61 | public var logging = false | 77 | public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null |
62 | public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null; | ||
63 | public var partalInterpretationVisualisationFrequency = 1 | 78 | public var partalInterpretationVisualisationFrequency = 1 |
64 | } | 79 | } |
65 | 80 | ||
66 | public class InternalConsistencyCheckerConfiguration { | 81 | class InternalConsistencyCheckerConfiguration { |
67 | public var LogicReasoner internalIncosnsitencyDetector = null | 82 | public var LogicReasoner internalIncosnsitencyDetector = null |
68 | public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null | 83 | public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null |
69 | public var incternalConsistencyCheckingFrequency = 1 | 84 | public var incternalConsistencyCheckingFrequency = 1 |
70 | } | 85 | } |
71 | 86 | ||
72 | public class SearchSpaceConstraint { | 87 | class SearchSpaceConstraint { |
73 | public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE | 88 | public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE |
74 | public var int maxDepth = UNLIMITED_MAXDEPTH | 89 | public var int maxDepth = UNLIMITED_MAXDEPTH |
75 | public var List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList | 90 | public var List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList |
76 | } \ No newline at end of file | 91 | } |
92 | |||
93 | class CostObjectiveConfiguration { | ||
94 | public var List<CostObjectiveElementConfiguration> elements = newArrayList | ||
95 | public var ObjectiveKind kind | ||
96 | public var ObjectiveThreshold threshold | ||
97 | public var boolean findExtremum | ||
98 | } | ||
99 | |||
100 | class CostObjectiveElementConfiguration { | ||
101 | public var String patternQualifiedName | ||
102 | public var int weight | ||
103 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend new file mode 100644 index 00000000..67f447ed --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend | |||
@@ -0,0 +1,103 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | ||
6 | import java.util.Comparator | ||
7 | import java.util.List | ||
8 | import org.eclipse.viatra.dse.base.ThreadContext | ||
9 | import org.eclipse.viatra.dse.objectives.Comparators | ||
10 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | ||
11 | import org.eclipse.viatra.dse.objectives.IObjective | ||
12 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
13 | |||
14 | class BasicScopeGlobalConstraint implements IGlobalConstraint, IObjective { | ||
15 | val PartialInterpretation p | ||
16 | val List<ScopeAssertion> assertions | ||
17 | |||
18 | new(PartialInterpretation p) { | ||
19 | this.p = p | ||
20 | assertions = ImmutableList.copyOf(p.scopes.map [ | ||
21 | val currentSize = targetTypeInterpretation.elements.size | ||
22 | val minElements = minNewElements + currentSize | ||
23 | val maxElements = if (maxNewElements < 0) { | ||
24 | -1 | ||
25 | } else { | ||
26 | maxNewElements + currentSize | ||
27 | } | ||
28 | new ScopeAssertion(minElements, maxElements, targetTypeInterpretation) | ||
29 | ]) | ||
30 | } | ||
31 | |||
32 | override init(ThreadContext context) { | ||
33 | if (context.model != p) { | ||
34 | throw new IllegalArgumentException( | ||
35 | "Partial model must be passed to the constructor of BasicScopeGlobalConstraint") | ||
36 | } | ||
37 | } | ||
38 | |||
39 | override checkGlobalConstraint(ThreadContext context) { | ||
40 | assertions.forall[upperBoundSatisfied] | ||
41 | } | ||
42 | |||
43 | override getFitness(ThreadContext context) { | ||
44 | var double fitness = p.minNewElements | ||
45 | for (assertion : assertions) { | ||
46 | if (!assertion.lowerBoundSatisfied) { | ||
47 | fitness += 1 | ||
48 | } | ||
49 | } | ||
50 | fitness | ||
51 | } | ||
52 | |||
53 | override satisifiesHardObjective(Double fitness) { | ||
54 | fitness <= 0.01 | ||
55 | } | ||
56 | |||
57 | override BasicScopeGlobalConstraint createNew() { | ||
58 | this | ||
59 | } | ||
60 | |||
61 | override getName() { | ||
62 | class.name | ||
63 | } | ||
64 | |||
65 | override getComparator() { | ||
66 | Comparators.LOWER_IS_BETTER | ||
67 | } | ||
68 | |||
69 | override getLevel() { | ||
70 | 2 | ||
71 | } | ||
72 | |||
73 | override isHardObjective() { | ||
74 | true | ||
75 | } | ||
76 | |||
77 | override setComparator(Comparator<Double> comparator) { | ||
78 | throw new UnsupportedOperationException | ||
79 | } | ||
80 | |||
81 | override setLevel(int level) { | ||
82 | throw new UnsupportedOperationException | ||
83 | } | ||
84 | |||
85 | @FinalFieldsConstructor | ||
86 | private static class ScopeAssertion { | ||
87 | val int lowerBound | ||
88 | val int upperBound | ||
89 | val PartialTypeInterpratation typeDefinitions | ||
90 | |||
91 | private def getCount() { | ||
92 | typeDefinitions.elements.size | ||
93 | } | ||
94 | |||
95 | private def isLowerBoundSatisfied() { | ||
96 | count >= lowerBound | ||
97 | } | ||
98 | |||
99 | private def isUpperBoundSatisfied() { | ||
100 | upperBound < 0 || count <= upperBound | ||
101 | } | ||
102 | } | ||
103 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index 60f46033..081e48fa 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 | |||
@@ -21,6 +21,7 @@ import java.util.PriorityQueue; | |||
21 | import java.util.Random; | 21 | import java.util.Random; |
22 | 22 | ||
23 | import org.apache.log4j.Logger; | 23 | import org.apache.log4j.Logger; |
24 | import org.eclipse.emf.ecore.EObject; | ||
24 | import org.eclipse.emf.ecore.util.EcoreUtil; | 25 | import org.eclipse.emf.ecore.util.EcoreUtil; |
25 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; | 26 | import org.eclipse.viatra.dse.api.strategy.interfaces.IStrategy; |
26 | import org.eclipse.viatra.dse.base.ThreadContext; | 27 | import org.eclipse.viatra.dse.base.ThreadContext; |
@@ -75,8 +76,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
75 | // Running | 76 | // Running |
76 | private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore; | 77 | private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore; |
77 | private SolutionStore solutionStore; | 78 | private SolutionStore solutionStore; |
78 | private SolutionStoreWithCopy solutionStoreWithCopy; | ||
79 | private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor; | ||
80 | private volatile boolean isInterrupted = false; | 79 | private volatile boolean isInterrupted = false; |
81 | private ModelResult modelResultByInternalSolver = null; | 80 | private ModelResult modelResultByInternalSolver = null; |
82 | private Random random = new Random(); | 81 | private Random random = new Random(); |
@@ -95,14 +94,9 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
95 | this.workspace = workspace; | 94 | this.workspace = workspace; |
96 | this.configuration = configuration; | 95 | this.configuration = configuration; |
97 | this.method = method; | 96 | this.method = method; |
97 | //logger.setLevel(Level.DEBUG); | ||
98 | } | 98 | } |
99 | 99 | ||
100 | public SolutionStoreWithCopy getSolutionStoreWithCopy() { | ||
101 | return solutionStoreWithCopy; | ||
102 | } | ||
103 | public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() { | ||
104 | return solutionStoreWithDiversityDescriptor; | ||
105 | } | ||
106 | public int getNumberOfStatecoderFail() { | 100 | public int getNumberOfStatecoderFail() { |
107 | return numberOfStatecoderFail; | 101 | return numberOfStatecoderFail; |
108 | } | 102 | } |
@@ -121,9 +115,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
121 | matchers.add(matcher); | 115 | matchers.add(matcher); |
122 | } | 116 | } |
123 | 117 | ||
124 | this.solutionStoreWithCopy = new SolutionStoreWithCopy(); | ||
125 | this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement); | ||
126 | |||
127 | final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); | 118 | final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); |
128 | this.comparator = new Comparator<TrajectoryWithFitness>() { | 119 | this.comparator = new Comparator<TrajectoryWithFitness>() { |
129 | @Override | 120 | @Override |
@@ -146,13 +137,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
146 | return; | 137 | return; |
147 | } | 138 | } |
148 | 139 | ||
149 | final Fitness firstFittness = context.calculateFitness(); | 140 | final Fitness firstfitness = context.calculateFitness(); |
150 | checkForSolution(firstFittness); | 141 | solutionStore.newSolution(context); |
151 | 142 | ||
152 | final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); | 143 | final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); |
153 | final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); | 144 | final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); |
154 | TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness); | 145 | TrajectoryWithFitness currentTrajectoryWithfitness = new TrajectoryWithFitness(firstTrajectory, firstfitness); |
155 | trajectoiresToExplore.add(currentTrajectoryWithFittness); | 146 | trajectoiresToExplore.add(currentTrajectoryWithfitness); |
156 | 147 | ||
157 | //if(configuration) | 148 | //if(configuration) |
158 | visualiseCurrentState(); | 149 | visualiseCurrentState(); |
@@ -167,22 +158,22 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
167 | 158 | ||
168 | mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) { | 159 | mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) { |
169 | 160 | ||
170 | if (currentTrajectoryWithFittness == null) { | 161 | if (currentTrajectoryWithfitness == null) { |
171 | if (trajectoiresToExplore.isEmpty()) { | 162 | if (trajectoiresToExplore.isEmpty()) { |
172 | logger.debug("State space is fully traversed."); | 163 | logger.debug("State space is fully traversed."); |
173 | return; | 164 | return; |
174 | } else { | 165 | } else { |
175 | currentTrajectoryWithFittness = selectState(); | 166 | currentTrajectoryWithfitness = selectState(); |
176 | if (logger.isDebugEnabled()) { | 167 | if (logger.isDebugEnabled()) { |
177 | logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); | 168 | logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); |
178 | logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness); | 169 | logger.debug("New trajectory is chosen: " + currentTrajectoryWithfitness); |
179 | } | 170 | } |
180 | context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory); | 171 | context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithfitness.trajectory); |
181 | } | 172 | } |
182 | } | 173 | } |
183 | 174 | ||
184 | // visualiseCurrentState(); | 175 | // visualiseCurrentState(); |
185 | // boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); | 176 | // boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness); |
186 | // if(consistencyCheckResult == true) { | 177 | // if(consistencyCheckResult == true) { |
187 | // continue mainLoop; | 178 | // continue mainLoop; |
188 | // } | 179 | // } |
@@ -194,10 +185,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
194 | final Object nextActivation = iterator.next(); | 185 | final Object nextActivation = iterator.next(); |
195 | // if (!iterator.hasNext()) { | 186 | // if (!iterator.hasNext()) { |
196 | // logger.debug("Last untraversed activation of the state."); | 187 | // logger.debug("Last untraversed activation of the state."); |
197 | // trajectoiresToExplore.remove(currentTrajectoryWithFittness); | 188 | // trajectoiresToExplore.remove(currentTrajectoryWithfitness); |
198 | // } | 189 | // } |
199 | logger.debug("Executing new activation: " + nextActivation); | 190 | logger.debug("Executing new activation: " + nextActivation); |
200 | context.executeAcitvationId(nextActivation); | 191 | context.executeAcitvationId(nextActivation); |
192 | method.getStatistics().incrementDecisionCount(); | ||
201 | 193 | ||
202 | visualiseCurrentState(); | 194 | visualiseCurrentState(); |
203 | // for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { | 195 | // for(ViatraQueryMatcher<? extends IPatternMatch> matcher : matchers) { |
@@ -209,7 +201,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
209 | // System.out.println("---------"); | 201 | // System.out.println("---------"); |
210 | // } | 202 | // } |
211 | 203 | ||
212 | boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); | 204 | boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness); |
213 | if(consistencyCheckResult == true) { continue mainLoop; } | 205 | if(consistencyCheckResult == true) { continue mainLoop; } |
214 | 206 | ||
215 | if (context.isCurrentStateAlreadyTraversed()) { | 207 | if (context.isCurrentStateAlreadyTraversed()) { |
@@ -220,38 +212,38 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
220 | context.backtrack(); | 212 | context.backtrack(); |
221 | } else { | 213 | } else { |
222 | final Fitness nextFitness = context.calculateFitness(); | 214 | final Fitness nextFitness = context.calculateFitness(); |
223 | checkForSolution(nextFitness); | 215 | solutionStore.newSolution(context); |
224 | if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) { | 216 | if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) { |
225 | logger.debug("Reached max depth."); | 217 | logger.debug("Reached max depth."); |
226 | context.backtrack(); | 218 | context.backtrack(); |
227 | continue; | 219 | continue; |
228 | } | 220 | } |
229 | 221 | ||
230 | TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness( | 222 | TrajectoryWithFitness nextTrajectoryWithfitness = new TrajectoryWithFitness( |
231 | context.getTrajectory().toArray(), nextFitness); | 223 | context.getTrajectory().toArray(), nextFitness); |
232 | trajectoiresToExplore.add(nextTrajectoryWithFittness); | 224 | trajectoiresToExplore.add(nextTrajectoryWithfitness); |
233 | 225 | ||
234 | int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness, | 226 | int compare = objectiveComparatorHelper.compare(currentTrajectoryWithfitness.fitness, |
235 | nextTrajectoryWithFittness.fitness); | 227 | nextTrajectoryWithfitness.fitness); |
236 | if (compare < 0) { | 228 | if (compare < 0) { |
237 | logger.debug("Better fitness, moving on: " + nextFitness); | 229 | logger.debug("Better fitness, moving on: " + nextFitness); |
238 | currentTrajectoryWithFittness = nextTrajectoryWithFittness; | 230 | currentTrajectoryWithfitness = nextTrajectoryWithfitness; |
239 | continue mainLoop; | 231 | continue mainLoop; |
240 | } else if (compare == 0) { | 232 | } else if (compare == 0) { |
241 | logger.debug("Equally good fitness, moving on: " + nextFitness); | 233 | logger.debug("Equally good fitness, moving on: " + nextFitness); |
242 | currentTrajectoryWithFittness = nextTrajectoryWithFittness; | 234 | currentTrajectoryWithfitness = nextTrajectoryWithfitness; |
243 | continue mainLoop; | 235 | continue mainLoop; |
244 | } else { | 236 | } else { |
245 | logger.debug("Worse fitness."); | 237 | logger.debug("Worse fitness."); |
246 | currentTrajectoryWithFittness = null; | 238 | currentTrajectoryWithfitness = null; |
247 | continue mainLoop; | 239 | continue mainLoop; |
248 | } | 240 | } |
249 | } | 241 | } |
250 | } | 242 | } |
251 | 243 | ||
252 | logger.debug("State is fully traversed."); | 244 | logger.debug("State is fully traversed."); |
253 | trajectoiresToExplore.remove(currentTrajectoryWithFittness); | 245 | trajectoiresToExplore.remove(currentTrajectoryWithfitness); |
254 | currentTrajectoryWithFittness = null; | 246 | currentTrajectoryWithfitness = null; |
255 | 247 | ||
256 | } | 248 | } |
257 | logger.info("Interrupted."); | 249 | logger.info("Interrupted."); |
@@ -263,25 +255,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
263 | activationIds = new ArrayList<Object>(context.getUntraversedActivationIds()); | 255 | activationIds = new ArrayList<Object>(context.getUntraversedActivationIds()); |
264 | Collections.shuffle(activationIds); | 256 | Collections.shuffle(activationIds); |
265 | } catch (NullPointerException e) { | 257 | } catch (NullPointerException e) { |
258 | // logger.warn("Unexpected state code: " + context.getDesignSpaceManager().getCurrentState()); | ||
266 | numberOfStatecoderFail++; | 259 | numberOfStatecoderFail++; |
267 | activationIds = Collections.emptyList(); | 260 | activationIds = Collections.emptyList(); |
268 | } | 261 | } |
269 | return activationIds; | 262 | return activationIds; |
270 | } | 263 | } |
271 | 264 | ||
272 | private void checkForSolution(final Fitness fittness) { | ||
273 | if (fittness.isSatisifiesHardObjectives()) { | ||
274 | if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { | ||
275 | solutionStoreWithCopy.newSolution(context); | ||
276 | solutionStoreWithDiversityDescriptor.newSolution(context); | ||
277 | solutionStore.newSolution(context); | ||
278 | configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution); | ||
279 | |||
280 | logger.debug("Found a solution."); | ||
281 | } | ||
282 | } | ||
283 | } | ||
284 | |||
285 | @Override | 265 | @Override |
286 | public void interruptStrategy() { | 266 | public void interruptStrategy() { |
287 | isInterrupted = true; | 267 | isInterrupted = true; |
@@ -311,13 +291,16 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
311 | } | 291 | } |
312 | 292 | ||
313 | public void visualiseCurrentState() { | 293 | public void visualiseCurrentState() { |
314 | PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser; | 294 | PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser; |
315 | if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) { | 295 | if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) { |
316 | PartialInterpretation p = (PartialInterpretation) (context.getModel()); | 296 | PartialInterpretation p = (PartialInterpretation) (context.getModel()); |
317 | int id = ++numberOfPrintedModel; | 297 | int id = ++numberOfPrintedModel; |
318 | if (id % configuration.debugCongiguration.partalInterpretationVisualisationFrequency == 0) { | 298 | if (id % configuration.debugConfiguration.partalInterpretationVisualisationFrequency == 0) { |
319 | PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p); | 299 | PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p); |
320 | visualisation.writeToFile(workspace, String.format("state%09d.png", id)); | 300 | logger.debug("Visualizing state: " + id + " (" + context.getDesignSpaceManager().getCurrentState() + ")"); |
301 | String name = String.format("state%09d", id); | ||
302 | visualisation.writeToFile(workspace, name + ".png"); | ||
303 | workspace.writeModel((EObject) context.getModel(), name + ".xmi"); | ||
321 | } | 304 | } |
322 | } | 305 | } |
323 | } | 306 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend new file mode 100644 index 00000000..fb1b2066 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend | |||
@@ -0,0 +1,184 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import com.google.common.collect.HashMultiset | ||
4 | import com.google.common.collect.ImmutableSet | ||
5 | import com.google.common.collect.Multiset | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.NeighbourhoodWithTraces | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
11 | import java.util.Collection | ||
12 | import java.util.HashSet | ||
13 | import java.util.Map | ||
14 | import java.util.Set | ||
15 | import org.eclipse.viatra.dse.base.ThreadContext | ||
16 | import org.eclipse.xtend.lib.annotations.Accessors | ||
17 | |||
18 | interface DiversityChecker { | ||
19 | public static val NO_DIVERSITY_CHECKER = new DiversityChecker { | ||
20 | override isActive() { | ||
21 | false | ||
22 | } | ||
23 | |||
24 | override getTotalRuntime() { | ||
25 | 0 | ||
26 | } | ||
27 | |||
28 | override getSuccessRate() { | ||
29 | 1.0 | ||
30 | } | ||
31 | |||
32 | override newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) { | ||
33 | true | ||
34 | } | ||
35 | } | ||
36 | |||
37 | def boolean isActive() | ||
38 | |||
39 | def long getTotalRuntime() | ||
40 | |||
41 | def double getSuccessRate() | ||
42 | |||
43 | def boolean newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) | ||
44 | |||
45 | static def of(DiversityDescriptor descriptor) { | ||
46 | if (descriptor.ensureDiversity) { | ||
47 | new NodewiseDiversityChecker(descriptor) | ||
48 | } else { | ||
49 | NO_DIVERSITY_CHECKER | ||
50 | } | ||
51 | } | ||
52 | } | ||
53 | |||
54 | abstract class AbstractDiversityChecker implements DiversityChecker { | ||
55 | val DiversityDescriptor descriptor | ||
56 | val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice | ||
57 | |||
58 | @Accessors(PUBLIC_GETTER) var long totalRuntime = 0 | ||
59 | var int allCheckCount = 0 | ||
60 | var int successfulCheckCount = 0 | ||
61 | |||
62 | protected new(DiversityDescriptor descriptor) { | ||
63 | if (!descriptor.ensureDiversity) { | ||
64 | throw new IllegalArgumentException( | ||
65 | "Diversity description should enforce diversity or NO_DIVERSITY_CHECKER should be used instead.") | ||
66 | } | ||
67 | this.descriptor = descriptor | ||
68 | } | ||
69 | |||
70 | override isActive() { | ||
71 | true | ||
72 | } | ||
73 | |||
74 | override getTotalRuntime() { | ||
75 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
76 | } | ||
77 | |||
78 | override getSuccessRate() { | ||
79 | (allCheckCount as double) / (successfulCheckCount as double) | ||
80 | } | ||
81 | |||
82 | override newSolution(ThreadContext threadContext, Object solutionId, Collection<Object> dominatedSolutionIds) { | ||
83 | val start = System.nanoTime | ||
84 | val model = threadContext.model as PartialInterpretation | ||
85 | val representation = solutionCoder.createRepresentation(model, descriptor.range, descriptor.parallels, | ||
86 | descriptor.maxNumber, descriptor.relevantTypes, descriptor.relevantRelations) | ||
87 | val isDifferent = internalNewSolution(representation, solutionId, dominatedSolutionIds) | ||
88 | totalRuntime += System.nanoTime - start | ||
89 | allCheckCount++ | ||
90 | if (isDifferent) { | ||
91 | successfulCheckCount++ | ||
92 | } | ||
93 | isDifferent | ||
94 | } | ||
95 | |||
96 | protected abstract def boolean internalNewSolution( | ||
97 | NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation, | ||
98 | Object solutionId, Collection<Object> dominatedSolutionIds) | ||
99 | } | ||
100 | |||
101 | class NodewiseDiversityChecker extends AbstractDiversityChecker { | ||
102 | var Multiset<Integer> nodeCodes = HashMultiset.create | ||
103 | val Map<Object, Set<Integer>> tracedNodeCodes = newHashMap | ||
104 | |||
105 | new(DiversityDescriptor descriptor) { | ||
106 | super(descriptor) | ||
107 | } | ||
108 | |||
109 | override protected internalNewSolution( | ||
110 | NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation, | ||
111 | Object solutionId, Collection<Object> dominatedSolutionIds) { | ||
112 | val nodeCodesInSolution = ImmutableSet.copyOf(representation.modelRepresentation.keySet.map[hashCode]) | ||
113 | val remainingNodeCodes = if (dominatedSolutionIds.empty) { | ||
114 | nodeCodes | ||
115 | } else { | ||
116 | getRemainingNodeCodes(dominatedSolutionIds) | ||
117 | } | ||
118 | val hasNewCode = nodeCodesInSolution.exists[!remainingNodeCodes.contains(it)] | ||
119 | if (hasNewCode) { | ||
120 | nodeCodes = remainingNodeCodes | ||
121 | nodeCodes.addAll(nodeCodesInSolution) | ||
122 | for (dominatedSolutionId : dominatedSolutionIds) { | ||
123 | tracedNodeCodes.remove(dominatedSolutionId) | ||
124 | } | ||
125 | tracedNodeCodes.put(solutionId, nodeCodesInSolution) | ||
126 | } | ||
127 | hasNewCode | ||
128 | } | ||
129 | |||
130 | private def getRemainingNodeCodes(Collection<Object> dominatedSolutionIds) { | ||
131 | // TODO Optimize multiset operations. | ||
132 | val copyOfNodeCodes = HashMultiset.create(nodeCodes) | ||
133 | for (dominatedSolutionId : dominatedSolutionIds) { | ||
134 | val dominatedModelCode = tracedNodeCodes.get(dominatedSolutionId) | ||
135 | if (dominatedModelCode === null) { | ||
136 | throw new IllegalArgumentException("Unknown dominated solution: " + dominatedSolutionId) | ||
137 | } | ||
138 | copyOfNodeCodes.removeAll(dominatedModelCode) | ||
139 | } | ||
140 | copyOfNodeCodes | ||
141 | } | ||
142 | } | ||
143 | |||
144 | class GraphwiseDiversityChecker extends AbstractDiversityChecker { | ||
145 | var Set<Integer> modelCodes = newHashSet | ||
146 | val Map<Object, Integer> tracedModelCodes = newHashMap | ||
147 | |||
148 | new(DiversityDescriptor descriptor) { | ||
149 | super(descriptor) | ||
150 | } | ||
151 | |||
152 | override protected internalNewSolution( | ||
153 | NeighbourhoodWithTraces<Map<? extends AbstractNodeDescriptor, Integer>, AbstractNodeDescriptor> representation, | ||
154 | Object solutionId, Collection<Object> dominatedSolutionIds) { | ||
155 | val modelCodeOfSolution = representation.modelRepresentation.hashCode | ||
156 | val remainingModelCodes = if (dominatedSolutionIds.empty) { | ||
157 | modelCodes | ||
158 | } else { | ||
159 | getRemainingModelCodes(dominatedSolutionIds) | ||
160 | } | ||
161 | val isNewCode = !remainingModelCodes.contains(modelCodeOfSolution) | ||
162 | if (isNewCode) { | ||
163 | modelCodes = remainingModelCodes | ||
164 | modelCodes += modelCodeOfSolution | ||
165 | for (dominatedSolutionId : dominatedSolutionIds) { | ||
166 | tracedModelCodes.remove(dominatedSolutionId) | ||
167 | } | ||
168 | tracedModelCodes.put(solutionId, modelCodeOfSolution) | ||
169 | } | ||
170 | isNewCode | ||
171 | } | ||
172 | |||
173 | private def getRemainingModelCodes(Collection<Object> dominatedSolutionIds) { | ||
174 | val copyOfModelCodes = new HashSet(modelCodes) | ||
175 | for (dominatedSolutionId : dominatedSolutionIds) { | ||
176 | val dominatedModelCode = tracedModelCodes.get(dominatedSolutionId) | ||
177 | if (dominatedModelCode === null) { | ||
178 | throw new IllegalArgumentException("Unknown dominated solution: " + dominatedSolutionId) | ||
179 | } | ||
180 | copyOfModelCodes -= dominatedModelCode | ||
181 | } | ||
182 | copyOfModelCodes | ||
183 | } | ||
184 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend new file mode 100644 index 00000000..3c2e3319 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend | |||
@@ -0,0 +1,66 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective | ||
4 | import org.eclipse.viatra.dse.base.ThreadContext | ||
5 | import org.eclipse.viatra.dse.objectives.Comparators | ||
6 | import org.eclipse.viatra.dse.objectives.Fitness | ||
7 | import org.eclipse.viatra.dse.objectives.IObjective | ||
8 | |||
9 | final class DseUtils { | ||
10 | private new() { | ||
11 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly.") | ||
12 | } | ||
13 | |||
14 | static def calculateFitness(ThreadContext it, (IObjective)=>Double getFitness) { | ||
15 | val result = new Fitness | ||
16 | var boolean satisifiesHardObjectives = true | ||
17 | for (objective : objectives) { | ||
18 | val fitness = getFitness.apply(objective) | ||
19 | result.put(objective.name, fitness) | ||
20 | if (objective.isHardObjective() && !objective.satisifiesHardObjective(fitness)) { | ||
21 | satisifiesHardObjectives = false | ||
22 | } | ||
23 | } | ||
24 | result.satisifiesHardObjectives = satisifiesHardObjectives | ||
25 | result | ||
26 | } | ||
27 | |||
28 | static def caclulateBestPossibleFitness(ThreadContext threadContext) { | ||
29 | threadContext.calculateFitness [ objective | | ||
30 | if (objective instanceof IThreeValuedObjective) { | ||
31 | objective.getBestPossibleFitness(threadContext) | ||
32 | } else { | ||
33 | switch (objective.comparator) { | ||
34 | case Comparators.LOWER_IS_BETTER: | ||
35 | Double.NEGATIVE_INFINITY | ||
36 | case Comparators.HIGHER_IS_BETTER: | ||
37 | Double.POSITIVE_INFINITY | ||
38 | case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER: | ||
39 | 0.0 | ||
40 | default: | ||
41 | throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " + | ||
42 | objective.name) | ||
43 | } | ||
44 | } | ||
45 | ] | ||
46 | } | ||
47 | |||
48 | static def caclulateWorstPossibleFitness(ThreadContext threadContext) { | ||
49 | threadContext.calculateFitness [ objective | | ||
50 | if (objective instanceof IThreeValuedObjective) { | ||
51 | objective.getWorstPossibleFitness(threadContext) | ||
52 | } else { | ||
53 | switch (objective.comparator) { | ||
54 | case Comparators.LOWER_IS_BETTER, | ||
55 | case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER: | ||
56 | Double.POSITIVE_INFINITY | ||
57 | case Comparators.HIGHER_IS_BETTER: | ||
58 | Double.NEGATIVE_INFINITY | ||
59 | default: | ||
60 | throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " + | ||
61 | objective.name) | ||
62 | } | ||
63 | } | ||
64 | ] | ||
65 | } | ||
66 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend new file mode 100644 index 00000000..2e039ca2 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/InconsistentScopeGlobalConstraint.xtend | |||
@@ -0,0 +1,25 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | ||
4 | import org.eclipse.viatra.dse.base.ThreadContext | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
6 | |||
7 | class InconsistentScopeGlobalConstraint implements IGlobalConstraint { | ||
8 | |||
9 | override init(ThreadContext context) { | ||
10 | // Nothing to initialize. | ||
11 | } | ||
12 | |||
13 | override createNew() { | ||
14 | this | ||
15 | } | ||
16 | |||
17 | override getName() { | ||
18 | class.name | ||
19 | } | ||
20 | |||
21 | override checkGlobalConstraint(ThreadContext context) { | ||
22 | val partialModel = context.model as PartialInterpretation | ||
23 | partialModel.minNewElements <= partialModel.maxNewElements || partialModel.maxNewElements < 0 | ||
24 | } | ||
25 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend new file mode 100644 index 00000000..39ef5f9a --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend | |||
@@ -0,0 +1,24 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
4 | import org.apache.log4j.Logger | ||
5 | import org.eclipse.viatra.dse.api.SolutionTrajectory | ||
6 | import org.eclipse.viatra.dse.base.ThreadContext | ||
7 | import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler | ||
8 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
9 | |||
10 | @FinalFieldsConstructor | ||
11 | class LoggerSolutionFoundHandler implements ISolutionFoundHandler { | ||
12 | val ViatraReasonerConfiguration configuration | ||
13 | |||
14 | val logger = Logger.getLogger(SolutionCopier) | ||
15 | |||
16 | override solutionFound(ThreadContext context, SolutionTrajectory trajectory) { | ||
17 | configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolutions) | ||
18 | logger.debug("Found a solution.") | ||
19 | } | ||
20 | |||
21 | override solutionTriedToSave(ThreadContext context, SolutionTrajectory trajectory) { | ||
22 | // We are not interested in invalid solutions, ignore. | ||
23 | } | ||
24 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend index 2489c751..2976bebe 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,11 +1,13 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective | ||
3 | import java.util.Comparator | 5 | import java.util.Comparator |
4 | import java.util.List | 6 | import java.util.List |
5 | import org.eclipse.viatra.dse.base.ThreadContext | 7 | import org.eclipse.viatra.dse.base.ThreadContext |
6 | import org.eclipse.viatra.dse.objectives.Comparators | 8 | import org.eclipse.viatra.dse.objectives.Comparators |
7 | import org.eclipse.viatra.dse.objectives.IObjective | 9 | import org.eclipse.viatra.dse.objectives.IObjective |
8 | import org.eclipse.viatra.dse.objectives.impl.BaseObjective | 10 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
9 | 11 | ||
10 | //class ViatraReasonerNumbers { | 12 | //class ViatraReasonerNumbers { |
11 | // public static val scopePriority = 2 | 13 | // public static val scopePriority = 2 |
@@ -22,64 +24,66 @@ import org.eclipse.viatra.dse.objectives.impl.BaseObjective | |||
22 | // public static val compositePriority = 2 | 24 | // public static val compositePriority = 2 |
23 | //} | 25 | //} |
24 | 26 | ||
25 | class ModelGenerationCompositeObjective implements IObjective{ | 27 | @FinalFieldsConstructor |
26 | val ScopeObjective scopeObjective | 28 | class ModelGenerationCompositeObjective implements IThreeValuedObjective { |
27 | val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives | 29 | val IObjective scopeObjective |
28 | val UnfinishedWFObjective unfinishedWFObjective | 30 | val List<IObjective> unfinishedMultiplicityObjectives |
29 | 31 | val IObjective unfinishedWFObjective | |
30 | public new( | 32 | |
31 | ScopeObjective scopeObjective, | ||
32 | List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives, | ||
33 | UnfinishedWFObjective unfinishedWFObjective) | ||
34 | { | ||
35 | this.scopeObjective = scopeObjective | ||
36 | this.unfinishedMultiplicityObjectives = unfinishedMultiplicityObjectives | ||
37 | this.unfinishedWFObjective = unfinishedWFObjective | ||
38 | } | ||
39 | |||
40 | override init(ThreadContext context) { | 33 | override init(ThreadContext context) { |
41 | this.scopeObjective.init(context) | 34 | this.scopeObjective.init(context) |
42 | this.unfinishedMultiplicityObjectives.forEach[it.init(context)] | 35 | this.unfinishedMultiplicityObjectives.forEach[it.init(context)] |
43 | this.unfinishedWFObjective.init(context) | 36 | this.unfinishedWFObjective.init(context) |
44 | } | 37 | } |
45 | 38 | ||
46 | override createNew() { | 39 | override createNew() { |
47 | return new ModelGenerationCompositeObjective( | 40 | return new ModelGenerationCompositeObjective( |
48 | this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective) | 41 | scopeObjective.createNew, |
42 | ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew]), | ||
43 | unfinishedWFObjective.createNew | ||
44 | ) | ||
49 | } | 45 | } |
50 | 46 | ||
51 | override getComparator() { Comparators.LOWER_IS_BETTER } | 47 | override getComparator() { Comparators.LOWER_IS_BETTER } |
48 | |||
52 | override getFitness(ThreadContext context) { | 49 | override getFitness(ThreadContext context) { |
53 | var sum = 0.0 | 50 | var sum = 0.0 |
54 | val scopeFitnes = scopeObjective.getFitness(context) | 51 | val scopeFitnes = scopeObjective.getFitness(context) |
55 | //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] | 52 | // val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] |
56 | val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) | 53 | val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) |
57 | 54 | ||
58 | sum+=scopeFitnes | 55 | sum += scopeFitnes |
59 | var multiplicity = 0.0 | 56 | var multiplicity = 0.0 |
60 | for(multiplicityObjective : unfinishedMultiplicityObjectives) { | 57 | for (multiplicityObjective : unfinishedMultiplicityObjectives) { |
61 | multiplicity+=multiplicityObjective.getFitness(context)//*0.5 | 58 | multiplicity += multiplicityObjective.getFitness(context) // *0.5 |
62 | } | 59 | } |
63 | sum+=multiplicity | 60 | sum += multiplicity |
64 | sum += unfinishedWFsFitness//*0.5 | 61 | sum += unfinishedWFsFitness // *0.5 |
65 | 62 | // println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') | |
66 | //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''') | ||
67 | |||
68 | return sum | 63 | return sum |
69 | } | 64 | } |
70 | 65 | ||
71 | override getLevel() { 2 } | 66 | override getWorstPossibleFitness(ThreadContext threadContext) { |
72 | override getName() { "CompositeUnfinishednessObjective"} | 67 | Double.POSITIVE_INFINITY |
68 | } | ||
73 | 69 | ||
70 | override getBestPossibleFitness(ThreadContext threadContext) { | ||
71 | 0.0 | ||
72 | } | ||
73 | |||
74 | override getLevel() { 2 } | ||
75 | |||
76 | override getName() { "CompositeUnfinishednessObjective" } | ||
77 | |||
74 | override isHardObjective() { true } | 78 | override isHardObjective() { true } |
79 | |||
75 | override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } | 80 | override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } |
76 | 81 | ||
77 | |||
78 | override setComparator(Comparator<Double> comparator) { | 82 | override setComparator(Comparator<Double> comparator) { |
79 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 83 | throw new UnsupportedOperationException("Model generation objective comparator cannot be set.") |
80 | } | 84 | } |
85 | |||
81 | override setLevel(int level) { | 86 | override setLevel(int level) { |
82 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 87 | throw new UnsupportedOperationException("Model generation objective level cannot be set.") |
83 | } | 88 | } |
84 | 89 | } | |
85 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend index f61c7333..b63bfe8b 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 | |||
@@ -163,4 +163,4 @@ class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | |||
163 | override getAllStringsInStructure() { | 163 | override getAllStringsInStructure() { |
164 | new TreeSet(this.stringForwardTrace.keySet) | 164 | new TreeSet(this.stringForwardTrace.keySet) |
165 | } | 165 | } |
166 | } \ No newline at end of file | 166 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend index 69efe0d7..69a734f8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend | |||
@@ -23,9 +23,9 @@ class ScopeObjective implements IObjective{ | |||
23 | 23 | ||
24 | override getFitness(ThreadContext context) { | 24 | override getFitness(ThreadContext context) { |
25 | val interpretation = context.model as PartialInterpretation | 25 | val interpretation = context.model as PartialInterpretation |
26 | var res = interpretation.minNewElements.doubleValue | 26 | var res = interpretation.minNewElementsHeuristic.doubleValue |
27 | for(scope : interpretation.scopes) { | 27 | for(scope : interpretation.scopes) { |
28 | res += scope.minNewElements*2 | 28 | res += scope.minNewElementsHeuristic*2 |
29 | } | 29 | } |
30 | return res | 30 | return res |
31 | } | 31 | } |
@@ -41,4 +41,4 @@ class ScopeObjective implements IObjective{ | |||
41 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 41 | throw new UnsupportedOperationException("TODO: auto-generated method stub") |
42 | } | 42 | } |
43 | override getLevel() { 2 } | 43 | override getLevel() { 2 } |
44 | } \ No newline at end of file | 44 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend new file mode 100644 index 00000000..d036257d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend | |||
@@ -0,0 +1,74 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import java.util.LinkedHashMap | ||
6 | import java.util.List | ||
7 | import java.util.Map | ||
8 | import org.eclipse.emf.ecore.EObject | ||
9 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
10 | import org.eclipse.viatra.dse.base.ThreadContext | ||
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
13 | |||
14 | @FinalFieldsConstructor | ||
15 | class CopiedSolution { | ||
16 | @Accessors val PartialInterpretation partialInterpretations | ||
17 | @Accessors val Map<EObject, EObject> trace | ||
18 | @Accessors val long copierRuntime | ||
19 | @Accessors var boolean current = true | ||
20 | } | ||
21 | |||
22 | class SolutionCopier { | ||
23 | val copiedSolutions = new LinkedHashMap<Object, CopiedSolution> | ||
24 | |||
25 | long startTime = System.nanoTime | ||
26 | @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 | ||
27 | |||
28 | def void copySolution(ThreadContext context, Object solutionId) { | ||
29 | val existingCopy = copiedSolutions.get(solutionId) | ||
30 | if (existingCopy === null) { | ||
31 | val copyStart = System.nanoTime | ||
32 | val solution = context.model as PartialInterpretation | ||
33 | val copier = new EcoreUtil.Copier | ||
34 | val copiedPartialInterpretation = copier.copy(solution) as PartialInterpretation | ||
35 | copier.copyReferences | ||
36 | totalCopierRuntime += System.nanoTime - copyStart | ||
37 | val copierRuntime = System.nanoTime - startTime | ||
38 | val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime) | ||
39 | copiedSolutions.put(solutionId, copiedSolution) | ||
40 | } else { | ||
41 | existingCopy.current = true | ||
42 | } | ||
43 | } | ||
44 | |||
45 | def void markAsObsolete(Object solutionId) { | ||
46 | val copiedSolution = copiedSolutions.get(solutionId) | ||
47 | if (copiedSolution === null) { | ||
48 | throw new IllegalStateException("No solution to mark as obsolete for state code: " + solutionId) | ||
49 | } | ||
50 | copiedSolution.current = false | ||
51 | } | ||
52 | |||
53 | def List<PartialInterpretation> getPartialInterpretations(boolean currentOnly) { | ||
54 | getListOfCopiedSolutions(currentOnly).map[partialInterpretations] | ||
55 | } | ||
56 | |||
57 | def List<Map<EObject, EObject>> getTraces(boolean currentOnly) { | ||
58 | getListOfCopiedSolutions(currentOnly).map[trace] | ||
59 | } | ||
60 | |||
61 | def List<Long> getAllCopierRuntimes(boolean currentOnly) { | ||
62 | getListOfCopiedSolutions(currentOnly).map[copierRuntime] | ||
63 | } | ||
64 | |||
65 | def List<CopiedSolution> getListOfCopiedSolutions(boolean currentOnly) { | ||
66 | val values = copiedSolutions.values | ||
67 | val filteredSolutions = if (currentOnly) { | ||
68 | values.filter[current] | ||
69 | } else { | ||
70 | values | ||
71 | } | ||
72 | ImmutableList.copyOf(filteredSolutions) | ||
73 | } | ||
74 | } | ||
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 deleted file mode 100644 index a8b7301e..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend +++ /dev/null | |||
@@ -1,52 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.List | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import java.util.LinkedList | ||
6 | import org.eclipse.emf.ecore.EObject | ||
7 | import java.util.Map | ||
8 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
9 | import org.eclipse.viatra.dse.base.ThreadContext | ||
10 | import java.util.TreeMap | ||
11 | import java.util.SortedMap | ||
12 | |||
13 | class SolutionStoreWithCopy { | ||
14 | |||
15 | long runtime = 0 | ||
16 | List<PartialInterpretation> solutions = new LinkedList | ||
17 | //public List<SortedMap<String,Integer>> additionalMatches = new LinkedList | ||
18 | List<Map<EObject,EObject>> copyTraces = new LinkedList | ||
19 | |||
20 | long sartTime = System.nanoTime | ||
21 | List<Long> solutionTimes = new LinkedList | ||
22 | |||
23 | /*def newSolution(ThreadContext context, SortedMap<String,Integer> additonalMatch) { | ||
24 | additionalMatches+= additonalMatch | ||
25 | newSolution(context) | ||
26 | }*/ | ||
27 | |||
28 | def newSolution(ThreadContext context) { | ||
29 | //print(System.nanoTime-initTime + ";") | ||
30 | val copyStart = System.nanoTime | ||
31 | val solution = context.model as PartialInterpretation | ||
32 | val copier = new EcoreUtil.Copier | ||
33 | val solutionCopy = copier.copy(solution) as PartialInterpretation | ||
34 | copier.copyReferences | ||
35 | solutions.add(solutionCopy) | ||
36 | copyTraces.add(copier) | ||
37 | runtime += System.nanoTime - copyStart | ||
38 | solutionTimes.add(System.nanoTime-sartTime) | ||
39 | } | ||
40 | def getSumRuntime() { | ||
41 | return runtime | ||
42 | } | ||
43 | def getAllRuntimes() { | ||
44 | return solutionTimes | ||
45 | } | ||
46 | def getSolutions() { | ||
47 | solutions | ||
48 | } | ||
49 | def getCopyTraces() { | ||
50 | return copyTraces | ||
51 | } | ||
52 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend deleted file mode 100644 index 1e7f18a8..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend +++ /dev/null | |||
@@ -1,120 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
6 | import java.util.LinkedList | ||
7 | import java.util.List | ||
8 | import org.eclipse.viatra.dse.base.ThreadContext | ||
9 | import java.util.HashSet | ||
10 | import java.util.Set | ||
11 | |||
12 | enum DiversityGranularity { | ||
13 | Nodewise, Graphwise | ||
14 | } | ||
15 | |||
16 | class SolutionStoreWithDiversityDescriptor { | ||
17 | val DiversityDescriptor descriptor | ||
18 | DiversityGranularity granularity | ||
19 | val PartialInterpretation2ImmutableTypeLattice solutionCoder = new PartialInterpretation2ImmutableTypeLattice | ||
20 | val Set<Integer> solutionCodeList = new HashSet | ||
21 | |||
22 | var long runtime | ||
23 | var int allCheck | ||
24 | var int successfulCheck | ||
25 | |||
26 | new(DiversityDescriptor descriptor) { | ||
27 | if(descriptor.ensureDiversity) { | ||
28 | this.descriptor = descriptor | ||
29 | this.granularity = DiversityGranularity::Nodewise | ||
30 | } else { | ||
31 | this.descriptor = null | ||
32 | this.granularity = DiversityGranularity::Nodewise | ||
33 | } | ||
34 | } | ||
35 | |||
36 | def public isActive() { | ||
37 | descriptor!==null | ||
38 | } | ||
39 | |||
40 | def getSumRuntime() { | ||
41 | return runtime | ||
42 | } | ||
43 | def getSuccessRate() { | ||
44 | return successfulCheck as double / allCheck | ||
45 | } | ||
46 | |||
47 | def isDifferent(ThreadContext context) { | ||
48 | if(active) { | ||
49 | val start = System.nanoTime | ||
50 | val model = context.model as PartialInterpretation | ||
51 | var boolean isDifferent | ||
52 | if(this.granularity == DiversityGranularity::Graphwise) { | ||
53 | val code = solutionCoder.createRepresentation(model, | ||
54 | descriptor.range, | ||
55 | descriptor.parallels, | ||
56 | descriptor.maxNumber, | ||
57 | descriptor.relevantTypes, | ||
58 | descriptor.relevantRelations).modelRepresentation.hashCode | ||
59 | |||
60 | isDifferent = !solutionCodeList.contains(code) | ||
61 | } else if(this.granularity == DiversityGranularity::Nodewise){ | ||
62 | val codes = solutionCoder.createRepresentation(model, | ||
63 | descriptor.range, | ||
64 | descriptor.parallels, | ||
65 | descriptor.maxNumber, | ||
66 | descriptor.relevantTypes, | ||
67 | descriptor.relevantRelations).modelRepresentation.keySet.map[hashCode].toList | ||
68 | val differentCodes = codes.filter[!solutionCodeList.contains(it)] | ||
69 | //println(differentCodes.size) | ||
70 | |||
71 | isDifferent = differentCodes.size>=1 | ||
72 | } else { | ||
73 | throw new UnsupportedOperationException('''Unsupported diversity type: «this.granularity»''') | ||
74 | } | ||
75 | |||
76 | runtime += System.nanoTime - start | ||
77 | allCheck++ | ||
78 | if(isDifferent) { successfulCheck++ } | ||
79 | return isDifferent | ||
80 | } else { | ||
81 | allCheck++ | ||
82 | successfulCheck++ | ||
83 | return true | ||
84 | } | ||
85 | } | ||
86 | |||
87 | def canBeDifferent(ThreadContext context) { | ||
88 | return true | ||
89 | } | ||
90 | |||
91 | def newSolution(ThreadContext context) { | ||
92 | if(active) { | ||
93 | val start = System.nanoTime | ||
94 | val model = context.model as PartialInterpretation | ||
95 | if(this.granularity == DiversityGranularity::Graphwise) { | ||
96 | val code = solutionCoder.createRepresentation(model, | ||
97 | descriptor.range, | ||
98 | descriptor.parallels, | ||
99 | descriptor.maxNumber, | ||
100 | descriptor.relevantTypes, | ||
101 | descriptor.relevantRelations).modelRepresentation.hashCode | ||
102 | |||
103 | solutionCodeList += code.hashCode | ||
104 | } else if(this.granularity == DiversityGranularity::Nodewise){ | ||
105 | val codes = solutionCoder.createRepresentation(model, | ||
106 | descriptor.range, | ||
107 | descriptor.parallels, | ||
108 | descriptor.maxNumber, | ||
109 | descriptor.relevantTypes, | ||
110 | descriptor.relevantRelations).modelRepresentation.keySet.map[hashCode].toList | ||
111 | |||
112 | solutionCodeList += codes.map[it.hashCode] | ||
113 | } else { | ||
114 | throw new UnsupportedOperationException('''Unsupported diversity type: «this.granularity»''') | ||
115 | } | ||
116 | |||
117 | runtime += System.nanoTime - start | ||
118 | } | ||
119 | } | ||
120 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend new file mode 100644 index 00000000..8ed3e912 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend | |||
@@ -0,0 +1,27 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import org.eclipse.viatra.dse.base.ThreadContext | ||
4 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | ||
5 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
6 | |||
7 | @FinalFieldsConstructor | ||
8 | class SurelyViolatedObjectiveGlobalConstraint implements IGlobalConstraint { | ||
9 | val ViatraReasonerSolutionSaver solutionSaver | ||
10 | |||
11 | override init(ThreadContext context) { | ||
12 | // Nothing to initialize. | ||
13 | } | ||
14 | |||
15 | override createNew() { | ||
16 | this | ||
17 | } | ||
18 | |||
19 | override getName() { | ||
20 | class.name | ||
21 | } | ||
22 | |||
23 | override checkGlobalConstraint(ThreadContext context) { | ||
24 | val bestFitness = DseUtils.caclulateBestPossibleFitness(context) | ||
25 | bestFitness.satisifiesHardObjectives && solutionSaver.fitnessMayBeSaved(bestFitness) | ||
26 | } | ||
27 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend index aad9a448..9f0c642f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend | |||
@@ -1,15 +1,15 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator |
4 | import java.util.Comparator | 4 | import java.util.Comparator |
5 | import org.eclipse.viatra.dse.base.ThreadContext | 5 | import org.eclipse.viatra.dse.base.ThreadContext |
6 | import org.eclipse.viatra.dse.objectives.IObjective | ||
7 | import org.eclipse.viatra.dse.objectives.Comparators | 6 | import org.eclipse.viatra.dse.objectives.Comparators |
7 | import org.eclipse.viatra.dse.objectives.IObjective | ||
8 | 8 | ||
9 | class UnfinishedMultiplicityObjective implements IObjective { | 9 | class UnfinishedMultiplicityObjective implements IObjective { |
10 | val MultiplicityGoalConstraintCalculator unfinishedMultiplicity; | 10 | val MultiplicityGoalConstraintCalculator unfinishedMultiplicity; |
11 | 11 | ||
12 | public new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) { | 12 | new(MultiplicityGoalConstraintCalculator unfinishedMultiplicity) { |
13 | this.unfinishedMultiplicity = unfinishedMultiplicity | 13 | this.unfinishedMultiplicity = unfinishedMultiplicity |
14 | } | 14 | } |
15 | 15 | ||
@@ -29,9 +29,9 @@ class UnfinishedMultiplicityObjective implements IObjective { | |||
29 | override satisifiesHardObjective(Double fitness) { return fitness <=0.01 } | 29 | override satisifiesHardObjective(Double fitness) { return fitness <=0.01 } |
30 | 30 | ||
31 | override setComparator(Comparator<Double> comparator) { | 31 | override setComparator(Comparator<Double> comparator) { |
32 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 32 | throw new UnsupportedOperationException |
33 | } | 33 | } |
34 | override setLevel(int level) { | 34 | override setLevel(int level) { |
35 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 35 | throw new UnsupportedOperationException |
36 | } | 36 | } |
37 | } \ No newline at end of file | 37 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend index e0111cf6..1b61ffa5 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend | |||
@@ -1,56 +1,64 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import org.eclipse.viatra.dse.objectives.IObjective | 3 | import java.util.ArrayList |
4 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
5 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
6 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
7 | import java.util.Collection | 4 | import java.util.Collection |
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 5 | import java.util.Comparator |
9 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
10 | import org.eclipse.viatra.dse.base.ThreadContext | ||
11 | import java.util.List | 6 | import java.util.List |
7 | import org.eclipse.viatra.dse.base.ThreadContext | ||
12 | import org.eclipse.viatra.dse.objectives.Comparators | 8 | import org.eclipse.viatra.dse.objectives.Comparators |
13 | import java.util.ArrayList | 9 | import org.eclipse.viatra.dse.objectives.IObjective |
14 | import java.util.Comparator | 10 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
11 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
12 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
15 | 13 | ||
16 | class UnfinishedWFObjective implements IObjective { | 14 | class UnfinishedWFObjective implements IObjective { |
17 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs | 15 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs |
18 | val List<ViatraQueryMatcher<?>> matchers | 16 | val List<ViatraQueryMatcher<?>> matchers |
19 | 17 | ||
20 | public new(Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) { | 18 | new( |
19 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) { | ||
21 | this.unfinishedWFs = unfinishedWFs | 20 | this.unfinishedWFs = unfinishedWFs |
22 | matchers = new ArrayList(unfinishedWFs.size) | 21 | matchers = new ArrayList(unfinishedWFs.size) |
23 | } | 22 | } |
23 | |||
24 | override getName() '''unfinishedWFs''' | 24 | override getName() '''unfinishedWFs''' |
25 | |||
25 | override createNew() { | 26 | override createNew() { |
26 | return new UnfinishedWFObjective(unfinishedWFs) | 27 | return new UnfinishedWFObjective(unfinishedWFs) |
27 | } | 28 | } |
29 | |||
28 | override init(ThreadContext context) { | 30 | override init(ThreadContext context) { |
29 | val engine = context.queryEngine//ViatraQueryEngine.on(new EMFScope(context.model)) | 31 | val engine = context.queryEngine // ViatraQueryEngine.on(new EMFScope(context.model)) |
30 | for(unfinishedWF : unfinishedWFs) { | 32 | for (unfinishedWF : unfinishedWFs) { |
31 | matchers += unfinishedWF.getMatcher(engine) | 33 | matchers += unfinishedWF.getMatcher(engine) |
32 | } | 34 | } |
33 | } | 35 | } |
34 | 36 | ||
35 | override getComparator() { Comparators.LOWER_IS_BETTER } | 37 | override getComparator() { Comparators.LOWER_IS_BETTER } |
38 | |||
36 | override getFitness(ThreadContext context) { | 39 | override getFitness(ThreadContext context) { |
37 | var sumOfMatches = 0 | 40 | var sumOfMatches = 0 |
38 | for(matcher : matchers) { | 41 | for (matcher : matchers) { |
39 | val number = matcher.countMatches | 42 | val number = matcher.countMatches |
40 | //println('''«matcher.patternName» = «number»''') | 43 | // if (number > 0) { |
41 | sumOfMatches+=number | 44 | // println('''«matcher.patternName» = «number»''') |
45 | // } | ||
46 | sumOfMatches += number | ||
42 | } | 47 | } |
43 | return sumOfMatches.doubleValue | 48 | return sumOfMatches.doubleValue |
44 | } | 49 | } |
45 | 50 | ||
46 | override getLevel() { 2 } | 51 | override getLevel() { 2 } |
52 | |||
47 | override isHardObjective() { true } | 53 | override isHardObjective() { true } |
48 | override satisifiesHardObjective(Double fitness) { return fitness <=0.01 } | 54 | |
49 | 55 | override satisifiesHardObjective(Double fitness) { return fitness <= 0.01 } | |
56 | |||
50 | override setComparator(Comparator<Double> comparator) { | 57 | override setComparator(Comparator<Double> comparator) { |
51 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 58 | throw new UnsupportedOperationException() |
52 | } | 59 | } |
60 | |||
53 | override setLevel(int level) { | 61 | override setLevel(int level) { |
54 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 62 | throw new UnsupportedOperationException() |
55 | } | 63 | } |
56 | } \ No newline at end of file | 64 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend new file mode 100644 index 00000000..74500cc2 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend | |||
@@ -0,0 +1,142 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.HashMap | ||
4 | import java.util.Map | ||
5 | import org.eclipse.viatra.dse.api.DSEException | ||
6 | import org.eclipse.viatra.dse.api.Solution | ||
7 | import org.eclipse.viatra.dse.api.SolutionTrajectory | ||
8 | import org.eclipse.viatra.dse.base.ThreadContext | ||
9 | import org.eclipse.viatra.dse.objectives.Fitness | ||
10 | import org.eclipse.viatra.dse.objectives.IObjective | ||
11 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper | ||
12 | import org.eclipse.viatra.dse.solutionstore.SolutionStore.ISolutionSaver | ||
13 | import org.eclipse.xtend.lib.annotations.Accessors | ||
14 | |||
15 | /** | ||
16 | * Based on {@link SolutionStore.BestSolutionSaver}. | ||
17 | */ | ||
18 | class ViatraReasonerSolutionSaver implements ISolutionSaver { | ||
19 | @Accessors val solutionCopier = new SolutionCopier | ||
20 | @Accessors val DiversityChecker diversityChecker | ||
21 | val boolean hasExtremalObjectives | ||
22 | val int numberOfRequiredSolutions | ||
23 | val ObjectiveComparatorHelper comparatorHelper | ||
24 | val Map<SolutionTrajectory, Fitness> trajectories = new HashMap | ||
25 | |||
26 | @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection | ||
27 | |||
28 | new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) { | ||
29 | this.diversityChecker = diversityChecker | ||
30 | comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) | ||
31 | hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] | ||
32 | this.numberOfRequiredSolutions = numberOfRequiredSolutions | ||
33 | } | ||
34 | |||
35 | override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { | ||
36 | if (hasExtremalObjectives) { | ||
37 | saveBestSolutionOnly(context, id, solutionTrajectory) | ||
38 | } else { | ||
39 | saveAnyDiverseSolution(context, id, solutionTrajectory) | ||
40 | } | ||
41 | } | ||
42 | |||
43 | private def saveBestSolutionOnly(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { | ||
44 | val fitness = context.lastFitness | ||
45 | if (!shouldSaveSolution(fitness, context)) { | ||
46 | return false | ||
47 | } | ||
48 | val dominatedTrajectories = newArrayList | ||
49 | for (entry : trajectories.entrySet) { | ||
50 | val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) | ||
51 | if (isLastFitnessBetter < 0) { | ||
52 | // Found a trajectory that dominates the current one, no need to save | ||
53 | return false | ||
54 | } | ||
55 | if (isLastFitnessBetter > 0) { | ||
56 | dominatedTrajectories += entry.key | ||
57 | } | ||
58 | } | ||
59 | if (dominatedTrajectories.size == 0 && !needsMoreSolutionsWithSameFitness) { | ||
60 | return false | ||
61 | } | ||
62 | if (!diversityChecker.newSolution(context, id, dominatedTrajectories.map[solution.stateCode])) { | ||
63 | return false | ||
64 | } | ||
65 | // We must save the new trajectory before removing dominated trajectories | ||
66 | // to avoid removing the current solution when it is reachable only via dominated trajectories. | ||
67 | val solutionSaved = basicSaveSolution(context, id, solutionTrajectory, fitness) | ||
68 | for (dominatedTrajectory : dominatedTrajectories) { | ||
69 | trajectories -= dominatedTrajectory | ||
70 | val dominatedSolution = dominatedTrajectory.solution | ||
71 | if (!dominatedSolution.trajectories.remove(dominatedTrajectory)) { | ||
72 | throw new DSEException( | ||
73 | "Dominated solution is not reachable from dominated trajectory. This should never happen!") | ||
74 | } | ||
75 | if (dominatedSolution.trajectories.empty) { | ||
76 | val dominatedSolutionId = dominatedSolution.stateCode | ||
77 | solutionCopier.markAsObsolete(dominatedSolutionId) | ||
78 | solutionsCollection -= dominatedSolutionId | ||
79 | } | ||
80 | } | ||
81 | solutionSaved | ||
82 | } | ||
83 | |||
84 | private def saveAnyDiverseSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { | ||
85 | val fitness = context.lastFitness | ||
86 | if (!shouldSaveSolution(fitness, context)) { | ||
87 | return false | ||
88 | } | ||
89 | if (!diversityChecker.newSolution(context, id, emptyList)) { | ||
90 | return false | ||
91 | } | ||
92 | basicSaveSolution(context, id, solutionTrajectory, fitness) | ||
93 | } | ||
94 | |||
95 | private def shouldSaveSolution(Fitness fitness, ThreadContext context) { | ||
96 | return fitness.satisifiesHardObjectives | ||
97 | } | ||
98 | |||
99 | private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, | ||
100 | Fitness fitness) { | ||
101 | var boolean solutionSaved = false | ||
102 | var dseSolution = solutionsCollection.get(id) | ||
103 | if (dseSolution === null) { | ||
104 | solutionCopier.copySolution(context, id) | ||
105 | dseSolution = new Solution(id, solutionTrajectory) | ||
106 | solutionsCollection.put(id, dseSolution) | ||
107 | solutionSaved = true | ||
108 | } else { | ||
109 | solutionSaved = dseSolution.trajectories.add(solutionTrajectory) | ||
110 | } | ||
111 | if (solutionSaved) { | ||
112 | solutionTrajectory.solution = dseSolution | ||
113 | trajectories.put(solutionTrajectory, fitness) | ||
114 | } | ||
115 | solutionSaved | ||
116 | } | ||
117 | |||
118 | def fitnessMayBeSaved(Fitness fitness) { | ||
119 | if (!hasExtremalObjectives) { | ||
120 | return true | ||
121 | } | ||
122 | var boolean mayDominate | ||
123 | for (existingFitness : trajectories.values) { | ||
124 | val isNewFitnessBetter = comparatorHelper.compare(fitness, existingFitness) | ||
125 | if (isNewFitnessBetter < 0) { | ||
126 | return false | ||
127 | } | ||
128 | if (isNewFitnessBetter > 0) { | ||
129 | mayDominate = true | ||
130 | } | ||
131 | } | ||
132 | mayDominate || needsMoreSolutionsWithSameFitness | ||
133 | } | ||
134 | |||
135 | private def boolean needsMoreSolutionsWithSameFitness() { | ||
136 | if (solutionsCollection === null) { | ||
137 | // The solutions collection will only be initialized upon saving the first solution. | ||
138 | return true | ||
139 | } | ||
140 | solutionsCollection.size < numberOfRequiredSolutions | ||
141 | } | ||
142 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend index 5a528a9e..63d78220 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend | |||
@@ -1,5 +1,6 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
3 | import java.util.ArrayList | 4 | import java.util.ArrayList |
4 | import java.util.Collection | 5 | import java.util.Collection |
5 | import org.eclipse.viatra.dse.objectives.Comparators | 6 | import org.eclipse.viatra.dse.objectives.Comparators |
@@ -12,25 +13,35 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification | |||
12 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 13 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
13 | 14 | ||
14 | class WF2ObjectiveConverter { | 15 | class WF2ObjectiveConverter { |
15 | 16 | static val UNFINISHED_WFS_NAME = "unfinishedWFs" | |
17 | static val INVALIDATED_WFS_NAME = "invalidatedWFs" | ||
18 | |||
16 | def createCompletenessObjective( | 19 | def createCompletenessObjective( |
17 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) | 20 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF) { |
18 | { | 21 | // createConstraintObjective(UNFINISHED_WFS_NAME, unfinishedWF) |
19 | val res = new ConstraintsObjective('''unfinishedWFs''', | 22 | new UnfinishedWFObjective(unfinishedWF) |
20 | unfinishedWF.map[ | 23 | } |
21 | new QueryConstraint(it.fullyQualifiedName,it,2.0) | 24 | |
22 | ].toList | 25 | def createInvalidationObjective( |
26 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) { | ||
27 | createConstraintObjective(INVALIDATED_WFS_NAME, invalidatedByWF) | ||
28 | } | ||
29 | |||
30 | def IGlobalConstraint createInvalidationGlobalConstraint( | ||
31 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) { | ||
32 | new ModelQueriesGlobalConstraint(INVALIDATED_WFS_NAME, new ArrayList(invalidatedByWF)) | ||
33 | } | ||
34 | |||
35 | private def createConstraintObjective(String name, | ||
36 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries) { | ||
37 | val res = new ConstraintsObjective( | ||
38 | name, | ||
39 | ImmutableList.copyOf(queries.map [ | ||
40 | new QueryConstraint(it.fullyQualifiedName, it, 1.0) | ||
41 | ]) | ||
23 | ) | 42 | ) |
24 | res.withComparator(Comparators.LOWER_IS_BETTER) | 43 | res.withComparator(Comparators.LOWER_IS_BETTER) |
25 | res.level = 2 | 44 | res.level = 2 |
26 | return res | 45 | res |
27 | } | ||
28 | |||
29 | def IGlobalConstraint createInvalidationObjective( | ||
30 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) | ||
31 | { | ||
32 | return new ModelQueriesGlobalConstraint('''invalidatedWFs''', | ||
33 | new ArrayList(invalidatedByWF) | ||
34 | ) | ||
35 | } | 46 | } |
36 | } \ No newline at end of file | 47 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend new file mode 100644 index 00000000..cd911ab5 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend | |||
@@ -0,0 +1,35 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import org.eclipse.viatra.dse.base.ThreadContext | ||
4 | |||
5 | abstract class AbstractThreeValuedObjective extends DirectionalThresholdObjective implements IThreeValuedObjective { | ||
6 | protected new(String name, ObjectiveKind kind, ObjectiveThreshold threshold, int level) { | ||
7 | super(name, kind, threshold, level) | ||
8 | } | ||
9 | |||
10 | abstract def double getLowestPossibleFitness(ThreadContext threadContext) | ||
11 | |||
12 | abstract def double getHighestPossibleFitness(ThreadContext threadContext) | ||
13 | |||
14 | override getWorstPossibleFitness(ThreadContext threadContext) { | ||
15 | switch (kind) { | ||
16 | case LOWER_IS_BETTER: | ||
17 | getHighestPossibleFitness(threadContext) | ||
18 | case HIGHER_IS_BETTER: | ||
19 | getLowestPossibleFitness(threadContext) | ||
20 | default: | ||
21 | throw new IllegalStateException("Unknown three valued objective kind: " + kind) | ||
22 | } | ||
23 | } | ||
24 | |||
25 | override getBestPossibleFitness(ThreadContext threadContext) { | ||
26 | switch (kind) { | ||
27 | case LOWER_IS_BETTER: | ||
28 | getLowestPossibleFitness(threadContext) | ||
29 | case HIGHER_IS_BETTER: | ||
30 | getHighestPossibleFitness(threadContext) | ||
31 | default: | ||
32 | throw new IllegalStateException("Unknown three valued objective kind: " + kind) | ||
33 | } | ||
34 | } | ||
35 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CompositeDirectionalThresholdObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CompositeDirectionalThresholdObjective.xtend new file mode 100644 index 00000000..0aa442f5 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CompositeDirectionalThresholdObjective.xtend | |||
@@ -0,0 +1,62 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import java.util.Collection | ||
5 | import org.eclipse.viatra.dse.base.ThreadContext | ||
6 | |||
7 | class CompositeDirectionalThresholdObjective extends DirectionalThresholdObjective { | ||
8 | val Collection<DirectionalThresholdObjective> objectives | ||
9 | |||
10 | new(String name, Collection<DirectionalThresholdObjective> objectives) { | ||
11 | this(name, objectives, getKind(objectives), getThreshold(objectives), getLevel(objectives)) | ||
12 | } | ||
13 | |||
14 | new(String name, DirectionalThresholdObjective... objectives) { | ||
15 | this(name, objectives as Collection<DirectionalThresholdObjective>) | ||
16 | } | ||
17 | |||
18 | protected new(String name, Iterable<DirectionalThresholdObjective> objectives, ObjectiveKind kind, | ||
19 | ObjectiveThreshold threshold, int level) { | ||
20 | super(name, kind, threshold, level) | ||
21 | this.objectives = ImmutableList.copyOf(objectives) | ||
22 | } | ||
23 | |||
24 | override createNew() { | ||
25 | new CompositeDirectionalThresholdObjective(name, objectives.map[createNew as DirectionalThresholdObjective], | ||
26 | kind, threshold, level) | ||
27 | } | ||
28 | |||
29 | override init(ThreadContext context) { | ||
30 | for (objective : objectives) { | ||
31 | objective.init(context) | ||
32 | } | ||
33 | } | ||
34 | |||
35 | override protected getRawFitness(ThreadContext context) { | ||
36 | var double fitness = 0 | ||
37 | for (objective : objectives) { | ||
38 | fitness += objective.getFitness(context) | ||
39 | } | ||
40 | fitness | ||
41 | } | ||
42 | |||
43 | private static def getKind(Collection<DirectionalThresholdObjective> objectives) { | ||
44 | val kinds = objectives.map[kind].toSet | ||
45 | if (kinds.size != 1) { | ||
46 | throw new IllegalArgumentException("Passed objectives must have the same kind") | ||
47 | } | ||
48 | kinds.head | ||
49 | } | ||
50 | |||
51 | private static def getThreshold(Collection<DirectionalThresholdObjective> objectives) { | ||
52 | objectives.map[threshold].reduce[a, b|a.merge(b)] | ||
53 | } | ||
54 | |||
55 | private static def int getLevel(Collection<DirectionalThresholdObjective> objectives) { | ||
56 | val levels = objectives.map[level].toSet | ||
57 | if (levels.size != 1) { | ||
58 | throw new IllegalArgumentException("Passed objectives must have the same level") | ||
59 | } | ||
60 | levels.head | ||
61 | } | ||
62 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/DirectionalThresholdObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/DirectionalThresholdObjective.xtend new file mode 100644 index 00000000..376e3d1a --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/DirectionalThresholdObjective.xtend | |||
@@ -0,0 +1,164 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import java.util.Comparator | ||
4 | import org.eclipse.viatra.dse.base.ThreadContext | ||
5 | import org.eclipse.viatra.dse.objectives.IObjective | ||
6 | import org.eclipse.xtend.lib.annotations.Accessors | ||
7 | import org.eclipse.xtend.lib.annotations.Data | ||
8 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
9 | |||
10 | abstract class ObjectiveThreshold { | ||
11 | public static val NO_THRESHOLD = new ObjectiveThreshold { | ||
12 | override isHard() { | ||
13 | false | ||
14 | } | ||
15 | |||
16 | override satisfiesThreshold(double cost, Comparator<Double> comparator) { | ||
17 | true | ||
18 | } | ||
19 | |||
20 | override protected postProcessSatisfactoryCost(double cost, ObjectiveKind kind) { | ||
21 | cost | ||
22 | } | ||
23 | |||
24 | override ObjectiveThreshold merge(ObjectiveThreshold other) { | ||
25 | if (other == NO_THRESHOLD) { | ||
26 | NO_THRESHOLD | ||
27 | } else { | ||
28 | throw new IllegalArgumentException("Merged thresholds must have the same type") | ||
29 | } | ||
30 | } | ||
31 | } | ||
32 | |||
33 | private new() { | ||
34 | } | ||
35 | |||
36 | def boolean isHard() { | ||
37 | true | ||
38 | } | ||
39 | |||
40 | def boolean satisfiesThreshold(double cost, ObjectiveKind kind) { | ||
41 | satisfiesThreshold(cost, kind.comparator) | ||
42 | } | ||
43 | |||
44 | def boolean satisfiesThreshold(double cost, Comparator<Double> comparator) | ||
45 | |||
46 | def double postProcessCost(double cost, ObjectiveKind kind) { | ||
47 | if (satisfiesThreshold(cost, kind)) { | ||
48 | postProcessSatisfactoryCost(cost, kind) | ||
49 | } else { | ||
50 | cost | ||
51 | } | ||
52 | } | ||
53 | |||
54 | protected def double postProcessSatisfactoryCost(double cost, ObjectiveKind kind) | ||
55 | |||
56 | def ObjectiveThreshold merge(ObjectiveThreshold other) | ||
57 | |||
58 | @Data | ||
59 | static class Exclusive extends ObjectiveThreshold { | ||
60 | static val EPSILON = 0.1 | ||
61 | |||
62 | val double threshold | ||
63 | val boolean clampToThreshold | ||
64 | |||
65 | @FinalFieldsConstructor | ||
66 | new() { | ||
67 | } | ||
68 | |||
69 | new(double threshold) { | ||
70 | this(threshold, true) | ||
71 | } | ||
72 | |||
73 | override satisfiesThreshold(double cost, Comparator<Double> comparator) { | ||
74 | comparator.compare(threshold, cost) < 0 | ||
75 | } | ||
76 | |||
77 | override protected postProcessSatisfactoryCost(double cost, ObjectiveKind kind) { | ||
78 | if (clampToThreshold) { | ||
79 | threshold + Math.signum(kind.satisfiedValue) * EPSILON | ||
80 | } else { | ||
81 | cost | ||
82 | } | ||
83 | } | ||
84 | |||
85 | override ObjectiveThreshold merge(ObjectiveThreshold other) { | ||
86 | if (other instanceof Exclusive) { | ||
87 | new Exclusive(threshold + other.threshold) | ||
88 | } else { | ||
89 | throw new IllegalArgumentException("Merged thresholds must have the same type") | ||
90 | } | ||
91 | } | ||
92 | } | ||
93 | |||
94 | @Data | ||
95 | static class Inclusive extends ObjectiveThreshold { | ||
96 | val double threshold | ||
97 | val boolean clampToThreshold | ||
98 | |||
99 | @FinalFieldsConstructor | ||
100 | new() { | ||
101 | } | ||
102 | |||
103 | new(double threshold) { | ||
104 | this(threshold, true) | ||
105 | } | ||
106 | |||
107 | override satisfiesThreshold(double cost, Comparator<Double> comparator) { | ||
108 | comparator.compare(threshold, cost) <= 0 | ||
109 | } | ||
110 | |||
111 | override protected postProcessSatisfactoryCost(double cost, ObjectiveKind kind) { | ||
112 | if (clampToThreshold) { | ||
113 | threshold | ||
114 | } else { | ||
115 | cost | ||
116 | } | ||
117 | } | ||
118 | |||
119 | override ObjectiveThreshold merge(ObjectiveThreshold other) { | ||
120 | if (other instanceof Inclusive) { | ||
121 | new Inclusive(threshold + other.threshold) | ||
122 | } else { | ||
123 | throw new IllegalArgumentException("Merged thresholds must have the same type") | ||
124 | } | ||
125 | } | ||
126 | } | ||
127 | } | ||
128 | |||
129 | abstract class DirectionalThresholdObjective implements IObjective { | ||
130 | @Accessors val String name | ||
131 | @Accessors ObjectiveKind kind | ||
132 | @Accessors ObjectiveThreshold threshold | ||
133 | @Accessors int level | ||
134 | |||
135 | protected new(String name, ObjectiveKind kind, ObjectiveThreshold threshold, int level) { | ||
136 | this.name = name | ||
137 | this.kind = kind | ||
138 | this.threshold = threshold | ||
139 | this.level = level | ||
140 | } | ||
141 | |||
142 | override isHardObjective() { | ||
143 | threshold.hard | ||
144 | } | ||
145 | |||
146 | override satisifiesHardObjective(Double fitness) { | ||
147 | threshold.satisfiesThreshold(fitness, comparator) | ||
148 | } | ||
149 | |||
150 | override getComparator() { | ||
151 | kind.comparator | ||
152 | } | ||
153 | |||
154 | override setComparator(Comparator<Double> comparator) { | ||
155 | kind = ObjectiveKind.fromComparator(comparator) | ||
156 | } | ||
157 | |||
158 | override getFitness(ThreadContext context) { | ||
159 | val fitness = getRawFitness(context) | ||
160 | threshold.postProcessCost(fitness, kind) | ||
161 | } | ||
162 | |||
163 | protected def double getRawFitness(ThreadContext context) | ||
164 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend new file mode 100644 index 00000000..4a870a3e --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend | |||
@@ -0,0 +1,10 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import org.eclipse.viatra.dse.base.ThreadContext | ||
4 | import org.eclipse.viatra.dse.objectives.IObjective | ||
5 | |||
6 | interface IThreeValuedObjective extends IObjective { | ||
7 | def Double getWorstPossibleFitness(ThreadContext threadContext) | ||
8 | |||
9 | def Double getBestPossibleFitness(ThreadContext threadContext) | ||
10 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/MatchCostObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/MatchCostObjective.xtend new file mode 100644 index 00000000..a0c6a2c1 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/MatchCostObjective.xtend | |||
@@ -0,0 +1,52 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import java.util.Collection | ||
5 | import org.eclipse.viatra.dse.base.ThreadContext | ||
6 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
7 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
9 | import org.eclipse.xtend.lib.annotations.Data | ||
10 | |||
11 | @Data | ||
12 | class MatchCostElement { | ||
13 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> querySpecification | ||
14 | val double weight | ||
15 | } | ||
16 | |||
17 | class MatchCostObjective extends DirectionalThresholdObjective { | ||
18 | val Collection<MatchCostElement> costElements | ||
19 | Collection<CostElementMatcher> matchers | ||
20 | |||
21 | new(String name, Collection<MatchCostElement> costElements, ObjectiveKind kind, ObjectiveThreshold threshold, | ||
22 | int level) { | ||
23 | super(name, kind, threshold, level) | ||
24 | this.costElements = costElements | ||
25 | } | ||
26 | |||
27 | override createNew() { | ||
28 | new MatchCostObjective(name, costElements, kind, threshold, level) | ||
29 | } | ||
30 | |||
31 | override init(ThreadContext context) { | ||
32 | val queryEngine = context.queryEngine | ||
33 | matchers = ImmutableList.copyOf(costElements.map [ | ||
34 | val matcher = querySpecification.getMatcher(queryEngine) | ||
35 | new CostElementMatcher(matcher, weight) | ||
36 | ]) | ||
37 | } | ||
38 | |||
39 | override protected getRawFitness(ThreadContext context) { | ||
40 | var double cost = 0 | ||
41 | for (it : matchers) { | ||
42 | cost += weight * matcher.countMatches | ||
43 | } | ||
44 | cost | ||
45 | } | ||
46 | |||
47 | @Data | ||
48 | private static class CostElementMatcher { | ||
49 | val ViatraQueryMatcher<? extends IPatternMatch> matcher | ||
50 | val double weight | ||
51 | } | ||
52 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java new file mode 100644 index 00000000..cbbaaafd --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java | |||
@@ -0,0 +1,60 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization; | ||
2 | |||
3 | import java.util.Comparator; | ||
4 | |||
5 | import org.eclipse.viatra.dse.objectives.Comparators; | ||
6 | |||
7 | public enum ObjectiveKind { | ||
8 | LOWER_IS_BETTER { | ||
9 | |||
10 | @Override | ||
11 | public Comparator<Double> getComparator() { | ||
12 | return Comparators.LOWER_IS_BETTER; | ||
13 | } | ||
14 | |||
15 | @Override | ||
16 | public double getInvalidValue() { | ||
17 | return Double.POSITIVE_INFINITY; | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public double getSatisfiedValue() { | ||
22 | return Double.NEGATIVE_INFINITY; | ||
23 | } | ||
24 | |||
25 | }, | ||
26 | HIGHER_IS_BETTER { | ||
27 | |||
28 | @Override | ||
29 | public Comparator<Double> getComparator() { | ||
30 | return Comparators.HIGHER_IS_BETTER; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | public double getInvalidValue() { | ||
35 | return Double.NEGATIVE_INFINITY; | ||
36 | } | ||
37 | |||
38 | @Override | ||
39 | public double getSatisfiedValue() { | ||
40 | return Double.POSITIVE_INFINITY; | ||
41 | } | ||
42 | |||
43 | }; | ||
44 | |||
45 | public abstract Comparator<Double> getComparator(); | ||
46 | |||
47 | public abstract double getInvalidValue(); | ||
48 | |||
49 | public abstract double getSatisfiedValue(); | ||
50 | |||
51 | public static ObjectiveKind fromComparator(Comparator<Double> comparator) { | ||
52 | if (Comparators.LOWER_IS_BETTER.equals(comparator)) { | ||
53 | return ObjectiveKind.LOWER_IS_BETTER; | ||
54 | } else if (Comparators.HIGHER_IS_BETTER.equals(comparator)) { | ||
55 | return ObjectiveKind.HIGHER_IS_BETTER; | ||
56 | } else { | ||
57 | throw new IllegalStateException("Only LOWER_IS_BETTER and HIGHER_IS_BETTER comparators are supported."); | ||
58 | } | ||
59 | } | ||
60 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/QueryBasedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/QueryBasedObjective.xtend new file mode 100644 index 00000000..d355f5be --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/QueryBasedObjective.xtend | |||
@@ -0,0 +1,48 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import org.eclipse.viatra.dse.base.ThreadContext | ||
4 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
5 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
6 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
7 | |||
8 | class QueryBasedObjective extends DirectionalThresholdObjective { | ||
9 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> querySpecification | ||
10 | ViatraQueryMatcher<? extends IPatternMatch> matcher | ||
11 | |||
12 | new(IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> querySpecification, | ||
13 | ObjectiveKind kind, ObjectiveThreshold threshold, int level) { | ||
14 | super(querySpecification.simpleName + " objective", kind, threshold, level) | ||
15 | if (querySpecification.parameters.size != 1) { | ||
16 | throw new IllegalArgumentException("Objective query must have a single parameter") | ||
17 | } | ||
18 | this.querySpecification = querySpecification | ||
19 | } | ||
20 | |||
21 | override createNew() { | ||
22 | new QueryBasedObjective(querySpecification, kind, threshold, level) | ||
23 | } | ||
24 | |||
25 | override init(ThreadContext context) { | ||
26 | matcher = querySpecification.getMatcher(context.queryEngine) | ||
27 | } | ||
28 | |||
29 | override protected getRawFitness(ThreadContext context) { | ||
30 | val iterator = matcher.allMatches.iterator | ||
31 | if (!iterator.hasNext) { | ||
32 | return invalidValue | ||
33 | } | ||
34 | val value = iterator.next.get(0) | ||
35 | if (iterator.hasNext) { | ||
36 | throw new IllegalStateException("Multiple matches for objective query") | ||
37 | } | ||
38 | if (value instanceof Number) { | ||
39 | value.doubleValue | ||
40 | } else { | ||
41 | throw new IllegalStateException("Objective value is not an instance of Number") | ||
42 | } | ||
43 | } | ||
44 | |||
45 | private def getInvalidValue() { | ||
46 | kind.invalidValue | ||
47 | } | ||
48 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend new file mode 100644 index 00000000..0a6fd55b --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend | |||
@@ -0,0 +1,85 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import java.util.Collection | ||
5 | import org.eclipse.viatra.dse.base.ThreadContext | ||
6 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
7 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
9 | import org.eclipse.xtend.lib.annotations.Data | ||
10 | |||
11 | @Data | ||
12 | class ThreeValuedCostElement { | ||
13 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentMatchQuery | ||
14 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayMatchQuery | ||
15 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustMatchQuery | ||
16 | val int weight | ||
17 | } | ||
18 | |||
19 | class ThreeValuedCostObjective extends AbstractThreeValuedObjective { | ||
20 | val Collection<ThreeValuedCostElement> costElements | ||
21 | Collection<CostElementMatchers> matchers | ||
22 | |||
23 | new(String name, Collection<ThreeValuedCostElement> costElements, ObjectiveKind kind, ObjectiveThreshold threshold, | ||
24 | int level) { | ||
25 | super(name, kind, threshold, level) | ||
26 | this.costElements = costElements | ||
27 | } | ||
28 | |||
29 | override createNew() { | ||
30 | new ThreeValuedCostObjective(name, costElements, kind, threshold, level) | ||
31 | } | ||
32 | |||
33 | override init(ThreadContext context) { | ||
34 | val queryEngine = context.queryEngine | ||
35 | matchers = ImmutableList.copyOf(costElements.map [ element | | ||
36 | new CostElementMatchers( | ||
37 | queryEngine.getMatcher(element.currentMatchQuery), | ||
38 | queryEngine.getMatcher(element.mayMatchQuery), | ||
39 | queryEngine.getMatcher(element.mustMatchQuery), | ||
40 | element.weight | ||
41 | ) | ||
42 | ]) | ||
43 | } | ||
44 | |||
45 | override getRawFitness(ThreadContext context) { | ||
46 | var int cost = 0 | ||
47 | for (matcher : matchers) { | ||
48 | cost += matcher.weight * matcher.currentMatcher.countMatches | ||
49 | } | ||
50 | cost as double | ||
51 | } | ||
52 | |||
53 | override getLowestPossibleFitness(ThreadContext threadContext) { | ||
54 | var int cost = 0 | ||
55 | for (matcher : matchers) { | ||
56 | if (matcher.weight >= 0) { | ||
57 | cost += matcher.weight * matcher.mustMatcher.countMatches | ||
58 | } else if (matcher.mayMatcher.countMatches > 0) { | ||
59 | // TODO Count may matches. | ||
60 | return Double.NEGATIVE_INFINITY | ||
61 | } | ||
62 | } | ||
63 | cost as double | ||
64 | } | ||
65 | |||
66 | override getHighestPossibleFitness(ThreadContext threadContext) { | ||
67 | var int cost = 0 | ||
68 | for (matcher : matchers) { | ||
69 | if (matcher.weight <= 0) { | ||
70 | cost += matcher.weight * matcher.mustMatcher.countMatches | ||
71 | } else if (matcher.mayMatcher.countMatches > 0) { | ||
72 | return Double.POSITIVE_INFINITY | ||
73 | } | ||
74 | } | ||
75 | cost as double | ||
76 | } | ||
77 | |||
78 | @Data | ||
79 | private static class CostElementMatchers { | ||
80 | val ViatraQueryMatcher<? extends IPatternMatch> currentMatcher | ||
81 | val ViatraQueryMatcher<? extends IPatternMatch> mayMatcher | ||
82 | val ViatraQueryMatcher<? extends IPatternMatch> mustMatcher | ||
83 | val int weight | ||
84 | } | ||
85 | } | ||