aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend227
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend44
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java70
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DiversityChecker.xtend184
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend66
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/LoggerSolutionFoundHandler.xtend24
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend78
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend74
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithCopy.xtend52
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionStoreWithDiversityDescriptor.xtend120
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SurelyViolatedObjectiveGlobalConstraint.xtend29
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedMultiplicityObjective.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend137
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend45
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend102
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend10
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java36
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend85
18 files changed, 1010 insertions, 375 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
index 6639e5f3..edcca676 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
2 2
3import com.google.common.collect.ImmutableList
4import com.google.common.collect.Lists
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel 5import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
4import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner 6import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException 7import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
@@ -17,12 +19,17 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory 19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory 20import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory
19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration 21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration
22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler
20import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective 24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective
21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation 25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation
22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective 26import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective
27import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective 28import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedWFObjective 29import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver
25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter 30import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter
31import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement
32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective
26import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 33import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
27import java.util.List 34import java.util.List
28import java.util.Map 35import java.util.Map
@@ -31,44 +38,41 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer
31import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel 38import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel
32import org.eclipse.viatra.dse.solutionstore.SolutionStore 39import org.eclipse.viatra.dse.solutionstore.SolutionStore
33import org.eclipse.viatra.dse.statecode.IStateCoderFactory 40import org.eclipse.viatra.dse.statecode.IStateCoderFactory
34import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SolutionStoreWithDiversityDescriptor
35import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityGranularity
36 41
37class ViatraReasoner extends LogicReasoner{ 42class ViatraReasoner extends LogicReasoner {
38 val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() 43 val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()
39 val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider 44 val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider
40 val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE 45 val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE
41 val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter 46 val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter
42 47
43 48 override solve(LogicProblem problem, LogicSolverConfiguration configuration,
44 override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { 49 ReasonerWorkspace workspace) throws LogicReasonerException {
45 val viatraConfig = configuration.asConfig 50 val viatraConfig = configuration.asConfig
46 51
47 if(viatraConfig.debugCongiguration.logging) { 52 if (viatraConfig.debugConfiguration.logging) {
48 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL) 53 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL)
49 } else { 54 } else {
50 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN) 55 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN)
51 } 56 }
52 57
53 val DesignSpaceExplorer dse = new DesignSpaceExplorer(); 58 val DesignSpaceExplorer dse = new DesignSpaceExplorer();
54 59
55 dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE) 60 dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE)
56 dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE) 61 dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE)
57 dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE) 62 dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE)
58 63
59 val transformationStartTime = System.nanoTime 64 val transformationStartTime = System.nanoTime
60 65
61 66 val emptySolution = initialiser.initialisePartialInterpretation(problem, viatraConfig.typeScopes).output
62 67 if ((viatraConfig.documentationLevel == DocumentationLevel::FULL ||
63 val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output 68 viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {
64 if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { 69 workspace.writeModel(emptySolution, "init.partialmodel")
65 workspace.writeModel(emptySolution,"init.partialmodel") 70 }
66 }
67 emptySolution.problemConainer = problem 71 emptySolution.problemConainer = problem
68 72
69 val ScopePropagator scopePropagator = new ScopePropagator(emptySolution) 73 val ScopePropagator scopePropagator = new ScopePropagator(emptySolution)
70 scopePropagator.propagateAllScopeConstraints 74 scopePropagator.propagateAllScopeConstraints
71 75
72 val method = modelGenerationMethodProvider.createModelGenerationMethod( 76 val method = modelGenerationMethodProvider.createModelGenerationMethod(
73 problem, 77 problem,
74 emptySolution, 78 emptySolution,
@@ -78,138 +82,185 @@ class ViatraReasoner extends LogicReasoner{
78 scopePropagator, 82 scopePropagator,
79 viatraConfig.documentationLevel 83 viatraConfig.documentationLevel
80 ) 84 )
81 85
82 dse.addObjective(new ModelGenerationCompositeObjective( 86 dse.addObjective(new ModelGenerationCompositeObjective(
83 new ScopeObjective, 87 new ScopeObjective,
84 method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], 88 method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)],
85 new UnfinishedWFObjective(method.unfinishedWF) 89 wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF)
86 )) 90 ))
87 91
88 dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF)) 92 val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size)
89 for(additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) { 93 for (entry : viatraConfig.costObjectives.indexed) {
90 dse.addGlobalConstraint(additionalConstraint.apply(method)) 94 val objectiveName = '''costObjective«entry.key»'''
95 val objectiveConfig = entry.value
96 val elementsBuilder = ImmutableList.builder
97 for (elementConfig : objectiveConfig.elements) {
98 val relationName = elementConfig.patternQualifiedName
99 val modalQueries = method.modalRelationQueries.get(relationName)
100 if (modalQueries === null) {
101 throw new IllegalArgumentException("Unknown relation: " + relationName)
102 }
103 elementsBuilder.add(new ThreeValuedCostElement(
104 modalQueries.currentQuery,
105 modalQueries.mayQuery,
106 modalQueries.mustQuery,
107 elementConfig.weight
108 ))
109 }
110 val costElements = elementsBuilder.build
111 val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind,
112 objectiveConfig.threshold, 3)
113 dse.addObjective(costObjective)
114 if (objectiveConfig.findExtremum) {
115 extremalObjectives += costObjective
116 }
91 } 117 }
92 118
93 dse.setInitialModel(emptySolution,false) 119 val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions
94 120 val solutionStore = if (extremalObjectives.empty) {
95 val IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) { 121 new SolutionStore(numberOfRequiredSolutions)
96 new NeighbourhoodBasedStateCoderFactory 122 } else {
97 } else { 123 new SolutionStore()
98 new IdentifierBasedStateCoderFactory 124 }
125 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))
126 val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement)
127 val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions,
128 diversityChecker)
129 val solutionCopier = solutionSaver.solutionCopier
130 solutionStore.withSolutionSaver(solutionSaver)
131 dse.solutionStore = solutionStore
132
133 dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationGlobalConstraint(method.invalidWF))
134 dse.addGlobalConstraint(new SurelyViolatedObjectiveGlobalConstraint(solutionSaver))
135 for (additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) {
136 dse.addGlobalConstraint(additionalConstraint.apply(method))
99 } 137 }
138
139 dse.setInitialModel(emptySolution, false)
140
141 val IStateCoderFactory statecoder = if (viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) {
142 new NeighbourhoodBasedStateCoderFactory
143 } else {
144 new IdentifierBasedStateCoderFactory
145 }
100 dse.stateCoderFactory = statecoder 146 dse.stateCoderFactory = statecoder
101 147
102 dse.maxNumberOfThreads = 1 148 dse.maxNumberOfThreads = 1
103 149
104 val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolution) 150 for (rule : method.relationRefinementRules) {
105 dse.solutionStore = solutionStore
106
107 for(rule : method.relationRefinementRules) {
108 dse.addTransformationRule(rule) 151 dse.addTransformationRule(rule)
109 } 152 }
110 for(rule : method.objectRefinementRules) { 153 for (rule : method.objectRefinementRules) {
111 dse.addTransformationRule(rule) 154 dse.addTransformationRule(rule)
112 } 155 }
113 156
114 val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) 157 val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method)
115 viatraConfig.progressMonitor.workedForwardTransformation 158 viatraConfig.progressMonitor.workedForwardTransformation
116 159
117 val transformationTime = System.nanoTime - transformationStartTime 160 val transformationTime = System.nanoTime - transformationStartTime
118 val solverStartTime = System.nanoTime 161 val solverStartTime = System.nanoTime
119 162
120 var boolean stoppedByTimeout 163 var boolean stoppedByTimeout
121 var boolean stoppedByException 164 try {
122 try{ 165 stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000);
123 stoppedByTimeout = dse.startExplorationWithTimeout(strategy,configuration.runtimeLimit*1000);
124 stoppedByException = false
125 } catch (NullPointerException npe) { 166 } catch (NullPointerException npe) {
126 stoppedByTimeout = false 167 stoppedByTimeout = false
127 stoppedByException = true
128 } 168 }
129 val solverTime = System.nanoTime - solverStartTime 169 val solverTime = System.nanoTime - solverStartTime
130 viatraConfig.progressMonitor.workedSearchFinished 170 viatraConfig.progressMonitor.workedSearchFinished
131 171
132 //additionalMatches = strategy.solutionStoreWithCopy.additionalMatches 172 // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches
133 val statistics = createStatistics => [ 173 val statistics = createStatistics => [
134 //it.solverTime = viatraConfig.runtimeLimit 174 // it.solverTime = viatraConfig.runtimeLimit
135 it.solverTime = (solverTime/1000000) as int 175 it.solverTime = (solverTime / 1000000) as int
136 it.transformationTime = (transformationTime/1000000) as int 176 it.transformationTime = (transformationTime / 1000000) as int
137 for(x : 0..<strategy.solutionStoreWithCopy.allRuntimes.size) { 177 for (pair : solutionCopier.getAllCopierRuntimes(true).indexed) {
138 it.entries += createIntStatisticEntry => [ 178 it.entries += createIntStatisticEntry => [
139 it.name = '''_Solution«x»FoundAt''' 179 it.name = '''_Solution«pair.key»FoundAt'''
140 it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int 180 it.value = (pair.value / 1000000) as int
141 ] 181 ]
142 } 182 }
143 it.entries += createIntStatisticEntry => [ 183 it.entries += createIntStatisticEntry => [
144 it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int 184 it.name = "TransformationExecutionTime"
185 it.value = (method.statistics.transformationExecutionTime / 1000000) as int
145 ] 186 ]
146 it.entries += createIntStatisticEntry => [ 187 it.entries += createIntStatisticEntry => [
147 it.name = "TypeAnalysisTime" it.value = (method.statistics.PreliminaryTypeAnalisisTime/1000000) as int 188 it.name = "TypeAnalysisTime"
189 it.value = (method.statistics.PreliminaryTypeAnalisisTime / 1000000) as int
148 ] 190 ]
149 it.entries += createIntStatisticEntry => [ 191 it.entries += createIntStatisticEntry => [
150 it.name = "StateCoderTime" it.value = (statecoder.runtime/1000000) as int 192 it.name = "StateCoderTime"
193 it.value = (statecoder.runtime / 1000000) as int
151 ] 194 ]
152 it.entries += createIntStatisticEntry => [ 195 it.entries += createIntStatisticEntry => [
153 it.name = "StateCoderFailCount" it.value = strategy.numberOfStatecoderFail 196 it.name = "StateCoderFailCount"
197 it.value = strategy.numberOfStatecoderFail
154 ] 198 ]
155 it.entries += createIntStatisticEntry => [ 199 it.entries += createIntStatisticEntry => [
156 it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int 200 it.name = "SolutionCopyTime"
201 it.value = (solutionCopier.getTotalCopierRuntime / 1000000) as int
157 ] 202 ]
158 if(strategy.solutionStoreWithDiversityDescriptor.isActive) { 203 if (diversityChecker.isActive) {
159 it.entries += createIntStatisticEntry => [ 204 it.entries += createIntStatisticEntry => [
160 it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int 205 it.name = "SolutionDiversityCheckTime"
206 it.value = (diversityChecker.totalRuntime / 1000000) as int
161 ] 207 ]
162 it.entries += createRealStatisticEntry => [ 208 it.entries += createRealStatisticEntry => [
163 it.name = "SolutionDiversitySuccessRate" it.value = strategy.solutionStoreWithDiversityDescriptor.successRate 209 it.name = "SolutionDiversitySuccessRate"
210 it.value = diversityChecker.successRate
164 ] 211 ]
165 } 212 }
166 ] 213 ]
167 214
168 viatraConfig.progressMonitor.workedBackwardTransformationFinished 215 viatraConfig.progressMonitor.workedBackwardTransformationFinished
169 216
170 if(stoppedByTimeout) { 217 if (stoppedByTimeout) {
171 return createInsuficientResourcesResult=>[ 218 return createInsuficientResourcesResult => [
172 it.problem = problem 219 it.problem = problem
173 it.resourceName="time" 220 it.resourceName = "time"
174 it.representation += strategy.solutionStoreWithCopy.solutions 221 it.representation += solutionCopier.getPartialInterpretations(true)
175 it.statistics = statistics 222 it.statistics = statistics
176 ] 223 ]
177 } else { 224 } else {
178 if(solutionStore.solutions.empty) { 225 if (solutionStore.solutions.empty) {
179 return createInconsistencyResult => [ 226 return createInconsistencyResult => [
180 it.problem = problem 227 it.problem = problem
181 it.representation += strategy.solutionStoreWithCopy.solutions 228 it.representation += solutionCopier.getPartialInterpretations(true)
182 it.statistics = statistics 229 it.statistics = statistics
183 ] 230 ]
184 } else { 231 } else {
185 return createModelResult => [ 232 return createModelResult => [
186 it.problem = problem 233 it.problem = problem
187 it.trace = strategy.solutionStoreWithCopy.copyTraces 234 it.trace = solutionCopier.getTraces(true)
188 it.representation += strategy.solutionStoreWithCopy.solutions 235 it.representation += solutionCopier.getPartialInterpretations(true)
189 it.statistics = statistics 236 it.statistics = statistics
190 ] 237 ]
191 } 238 }
192 } 239 }
193 } 240 }
194 241
195 private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) { 242 private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) {
196 sc.sumStatecoderRuntime 243 sc.sumStatecoderRuntime
197 } 244 }
198 245
199 private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) { 246 private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) {
200 sc.sumStatecoderRuntime 247 sc.sumStatecoderRuntime
201 } 248 }
202 249
203 override getInterpretations(ModelResult modelResult) { 250 override getInterpretations(ModelResult modelResult) {
204 val indexes = 0..<modelResult.representation.size 251 val indexes = 0 ..< modelResult.representation.size
205 val traces = modelResult.trace as List<Map<EObject, EObject>>; 252 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 253 val res = indexes.map [ i |
254 new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation,
255 traces.get(i))
256 ].toList
207 return res 257 return res
208 } 258 }
209 259
210 private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) { 260 private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) {
211 if(configuration instanceof ViatraReasonerConfiguration) { 261 if (configuration instanceof ViatraReasonerConfiguration) {
212 return configuration 262 return configuration
213 } else throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''') 263 } else
264 throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''')
214 } 265 }
215} 266}
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..e6aee20c 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
@@ -7,18 +7,22 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod 7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod 8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser 9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser
10import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
11import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
10import java.util.LinkedList 12import java.util.LinkedList
11import java.util.List 13import java.util.List
12import java.util.Set 14import java.util.Set
13import org.eclipse.xtext.xbase.lib.Functions.Function1 15import org.eclipse.xtext.xbase.lib.Functions.Function1
14 16
15public enum StateCoderStrategy { 17enum StateCoderStrategy {
16 Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity 18 Neighbourhood,
19 NeighbourhoodWithEquivalence,
20 IDBased,
21 DefinedByDiversity
17} 22}
18 23
19class ViatraReasonerConfiguration extends LogicSolverConfiguration{ 24class ViatraReasonerConfiguration extends LogicSolverConfiguration {
20 //public var Iterable<PQuery> existingQueries 25 // public var Iterable<PQuery> existingQueries
21
22 public var nameNewElements = false 26 public var nameNewElements = false
23 public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood 27 public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood
24 public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis 28 public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
@@ -26,7 +30,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
26 * Once per 1/randomBacktrackChance the search selects a random state. 30 * Once per 1/randomBacktrackChance the search selects a random state.
27 */ 31 */
28 public var int randomBacktrackChance = 20; 32 public var int randomBacktrackChance = 20;
29 33
30 /** 34 /**
31 * Describes the required diversity between the solutions. 35 * Describes the required diversity between the solutions.
32 * Null means that the solutions have to have different state codes only. 36 * Null means that the solutions have to have different state codes only.
@@ -40,14 +44,16 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
40 /** 44 /**
41 * Configuration for debugging support. 45 * Configuration for debugging support.
42 */ 46 */
43 public var DebugConfiguration debugCongiguration = new DebugConfiguration 47 public var DebugConfiguration debugConfiguration = new DebugConfiguration
44 /** 48 /**
45 * Configuration for cutting search space. 49 * Configuration for cutting search space.
46 */ 50 */
47 public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint 51 public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint
52
53 public var List<CostObjectiveConfiguration> costObjectives = newArrayList
48} 54}
49 55
50public class DiversityDescriptor { 56class DiversityDescriptor {
51 public var ensureDiversity = false 57 public var ensureDiversity = false
52 public static val FixPointRange = -1 58 public static val FixPointRange = -1
53 public var int range = FixPointRange 59 public var int range = FixPointRange
@@ -57,20 +63,32 @@ public class DiversityDescriptor {
57 public var Set<RelationDeclaration> relevantRelations = null 63 public var Set<RelationDeclaration> relevantRelations = null
58} 64}
59 65
60public class DebugConfiguration { 66class DebugConfiguration {
61 public var logging = false 67 public var logging = false
62 public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null; 68 public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null;
63 public var partalInterpretationVisualisationFrequency = 1 69 public var partalInterpretationVisualisationFrequency = 1
64} 70}
65 71
66public class InternalConsistencyCheckerConfiguration { 72class InternalConsistencyCheckerConfiguration {
67 public var LogicReasoner internalIncosnsitencyDetector = null 73 public var LogicReasoner internalIncosnsitencyDetector = null
68 public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null 74 public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null
69 public var incternalConsistencyCheckingFrequency = 1 75 public var incternalConsistencyCheckingFrequency = 1
70} 76}
71 77
72public class SearchSpaceConstraint { 78class SearchSpaceConstraint {
73 public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE 79 public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE
74 public var int maxDepth = UNLIMITED_MAXDEPTH 80 public var int maxDepth = UNLIMITED_MAXDEPTH
75 public var List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList 81 public var List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList
76} \ No newline at end of file 82}
83
84class CostObjectiveConfiguration {
85 public var List<CostObjectiveElementConfiguration> elements = newArrayList
86 public var ObjectiveKind kind
87 public var ObjectiveThreshold threshold
88 public var boolean findExtremum
89}
90
91class CostObjectiveElementConfiguration {
92 public var String patternQualifiedName
93 public var int weight
94}
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..6ff867d7 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
@@ -75,8 +75,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
75 // Running 75 // Running
76 private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore; 76 private PriorityQueue<TrajectoryWithFitness> trajectoiresToExplore;
77 private SolutionStore solutionStore; 77 private SolutionStore solutionStore;
78 private SolutionStoreWithCopy solutionStoreWithCopy;
79 private SolutionStoreWithDiversityDescriptor solutionStoreWithDiversityDescriptor;
80 private volatile boolean isInterrupted = false; 78 private volatile boolean isInterrupted = false;
81 private ModelResult modelResultByInternalSolver = null; 79 private ModelResult modelResultByInternalSolver = null;
82 private Random random = new Random(); 80 private Random random = new Random();
@@ -97,12 +95,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
97 this.method = method; 95 this.method = method;
98 } 96 }
99 97
100 public SolutionStoreWithCopy getSolutionStoreWithCopy() {
101 return solutionStoreWithCopy;
102 }
103 public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
104 return solutionStoreWithDiversityDescriptor;
105 }
106 public int getNumberOfStatecoderFail() { 98 public int getNumberOfStatecoderFail() {
107 return numberOfStatecoderFail; 99 return numberOfStatecoderFail;
108 } 100 }
@@ -121,9 +113,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
121 matchers.add(matcher); 113 matchers.add(matcher);
122 } 114 }
123 115
124 this.solutionStoreWithCopy = new SolutionStoreWithCopy();
125 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
126
127 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); 116 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
128 this.comparator = new Comparator<TrajectoryWithFitness>() { 117 this.comparator = new Comparator<TrajectoryWithFitness>() {
129 @Override 118 @Override
@@ -146,13 +135,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
146 return; 135 return;
147 } 136 }
148 137
149 final Fitness firstFittness = context.calculateFitness(); 138 final Fitness firstfitness = context.calculateFitness();
150 checkForSolution(firstFittness); 139 solutionStore.newSolution(context);
151 140
152 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); 141 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
153 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); 142 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
154 TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness); 143 TrajectoryWithFitness currentTrajectoryWithfitness = new TrajectoryWithFitness(firstTrajectory, firstfitness);
155 trajectoiresToExplore.add(currentTrajectoryWithFittness); 144 trajectoiresToExplore.add(currentTrajectoryWithfitness);
156 145
157 //if(configuration) 146 //if(configuration)
158 visualiseCurrentState(); 147 visualiseCurrentState();
@@ -167,22 +156,22 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
167 156
168 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) { 157 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) {
169 158
170 if (currentTrajectoryWithFittness == null) { 159 if (currentTrajectoryWithfitness == null) {
171 if (trajectoiresToExplore.isEmpty()) { 160 if (trajectoiresToExplore.isEmpty()) {
172 logger.debug("State space is fully traversed."); 161 logger.debug("State space is fully traversed.");
173 return; 162 return;
174 } else { 163 } else {
175 currentTrajectoryWithFittness = selectState(); 164 currentTrajectoryWithfitness = selectState();
176 if (logger.isDebugEnabled()) { 165 if (logger.isDebugEnabled()) {
177 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); 166 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
178 logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness); 167 logger.debug("New trajectory is chosen: " + currentTrajectoryWithfitness);
179 } 168 }
180 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory); 169 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithfitness.trajectory);
181 } 170 }
182 } 171 }
183 172
184// visualiseCurrentState(); 173// visualiseCurrentState();
185// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); 174// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
186// if(consistencyCheckResult == true) { 175// if(consistencyCheckResult == true) {
187// continue mainLoop; 176// continue mainLoop;
188// } 177// }
@@ -194,7 +183,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
194 final Object nextActivation = iterator.next(); 183 final Object nextActivation = iterator.next();
195// if (!iterator.hasNext()) { 184// if (!iterator.hasNext()) {
196// logger.debug("Last untraversed activation of the state."); 185// logger.debug("Last untraversed activation of the state.");
197// trajectoiresToExplore.remove(currentTrajectoryWithFittness); 186// trajectoiresToExplore.remove(currentTrajectoryWithfitness);
198// } 187// }
199 logger.debug("Executing new activation: " + nextActivation); 188 logger.debug("Executing new activation: " + nextActivation);
200 context.executeAcitvationId(nextActivation); 189 context.executeAcitvationId(nextActivation);
@@ -209,7 +198,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
209// System.out.println("---------"); 198// System.out.println("---------");
210// } 199// }
211 200
212 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); 201 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
213 if(consistencyCheckResult == true) { continue mainLoop; } 202 if(consistencyCheckResult == true) { continue mainLoop; }
214 203
215 if (context.isCurrentStateAlreadyTraversed()) { 204 if (context.isCurrentStateAlreadyTraversed()) {
@@ -220,38 +209,38 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
220 context.backtrack(); 209 context.backtrack();
221 } else { 210 } else {
222 final Fitness nextFitness = context.calculateFitness(); 211 final Fitness nextFitness = context.calculateFitness();
223 checkForSolution(nextFitness); 212 solutionStore.newSolution(context);
224 if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) { 213 if (context.getDepth() > configuration.searchSpaceConstraints.maxDepth) {
225 logger.debug("Reached max depth."); 214 logger.debug("Reached max depth.");
226 context.backtrack(); 215 context.backtrack();
227 continue; 216 continue;
228 } 217 }
229 218
230 TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness( 219 TrajectoryWithFitness nextTrajectoryWithfitness = new TrajectoryWithFitness(
231 context.getTrajectory().toArray(), nextFitness); 220 context.getTrajectory().toArray(), nextFitness);
232 trajectoiresToExplore.add(nextTrajectoryWithFittness); 221 trajectoiresToExplore.add(nextTrajectoryWithfitness);
233 222
234 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness, 223 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithfitness.fitness,
235 nextTrajectoryWithFittness.fitness); 224 nextTrajectoryWithfitness.fitness);
236 if (compare < 0) { 225 if (compare < 0) {
237 logger.debug("Better fitness, moving on: " + nextFitness); 226 logger.debug("Better fitness, moving on: " + nextFitness);
238 currentTrajectoryWithFittness = nextTrajectoryWithFittness; 227 currentTrajectoryWithfitness = nextTrajectoryWithfitness;
239 continue mainLoop; 228 continue mainLoop;
240 } else if (compare == 0) { 229 } else if (compare == 0) {
241 logger.debug("Equally good fitness, moving on: " + nextFitness); 230 logger.debug("Equally good fitness, moving on: " + nextFitness);
242 currentTrajectoryWithFittness = nextTrajectoryWithFittness; 231 currentTrajectoryWithfitness = nextTrajectoryWithfitness;
243 continue mainLoop; 232 continue mainLoop;
244 } else { 233 } else {
245 logger.debug("Worse fitness."); 234 logger.debug("Worse fitness.");
246 currentTrajectoryWithFittness = null; 235 currentTrajectoryWithfitness = null;
247 continue mainLoop; 236 continue mainLoop;
248 } 237 }
249 } 238 }
250 } 239 }
251 240
252 logger.debug("State is fully traversed."); 241 logger.debug("State is fully traversed.");
253 trajectoiresToExplore.remove(currentTrajectoryWithFittness); 242 trajectoiresToExplore.remove(currentTrajectoryWithfitness);
254 currentTrajectoryWithFittness = null; 243 currentTrajectoryWithfitness = null;
255 244
256 } 245 }
257 logger.info("Interrupted."); 246 logger.info("Interrupted.");
@@ -269,19 +258,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
269 return activationIds; 258 return activationIds;
270 } 259 }
271 260
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 261 @Override
286 public void interruptStrategy() { 262 public void interruptStrategy() {
287 isInterrupted = true; 263 isInterrupted = true;
@@ -311,11 +287,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
311 } 287 }
312 288
313 public void visualiseCurrentState() { 289 public void visualiseCurrentState() {
314 PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser; 290 PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser;
315 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) { 291 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) {
316 PartialInterpretation p = (PartialInterpretation) (context.getModel()); 292 PartialInterpretation p = (PartialInterpretation) (context.getModel());
317 int id = ++numberOfPrintedModel; 293 int id = ++numberOfPrintedModel;
318 if (id % configuration.debugCongiguration.partalInterpretationVisualisationFrequency == 0) { 294 if (id % configuration.debugConfiguration.partalInterpretationVisualisationFrequency == 0) {
319 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p); 295 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p);
320 visualisation.writeToFile(workspace, String.format("state%09d.png", id)); 296 visualisation.writeToFile(workspace, String.format("state%09d.png", id));
321 } 297 }
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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import com.google.common.collect.HashMultiset
4import com.google.common.collect.ImmutableSet
5import com.google.common.collect.Multiset
6import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.AbstractNodeDescriptor
7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.NeighbourhoodWithTraces
8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
10import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
11import java.util.Collection
12import java.util.HashSet
13import java.util.Map
14import java.util.Set
15import org.eclipse.viatra.dse.base.ThreadContext
16import org.eclipse.xtend.lib.annotations.Accessors
17
18interface 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
54abstract 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
101class 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
144class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective
4import org.eclipse.viatra.dse.base.ThreadContext
5import org.eclipse.viatra.dse.objectives.Comparators
6import org.eclipse.viatra.dse.objectives.Fitness
7import org.eclipse.viatra.dse.objectives.IObjective
8
9final 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/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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
4import org.apache.log4j.Logger
5import org.eclipse.viatra.dse.api.SolutionTrajectory
6import org.eclipse.viatra.dse.base.ThreadContext
7import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler
8import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
9
10@FinalFieldsConstructor
11class 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..9a33753c 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import com.google.common.collect.ImmutableList
4import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective
3import java.util.Comparator 5import java.util.Comparator
4import java.util.List 6import java.util.List
5import org.eclipse.viatra.dse.base.ThreadContext 7import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.dse.objectives.Comparators 8import org.eclipse.viatra.dse.objectives.Comparators
7import org.eclipse.viatra.dse.objectives.IObjective 9import org.eclipse.viatra.dse.objectives.IObjective
8import org.eclipse.viatra.dse.objectives.impl.BaseObjective 10import 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
25class ModelGenerationCompositeObjective implements IObjective{ 27@FinalFieldsConstructor
26 val ScopeObjective scopeObjective 28class 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/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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import com.google.common.collect.ImmutableList
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import java.util.LinkedHashMap
6import java.util.List
7import java.util.Map
8import org.eclipse.emf.ecore.EObject
9import org.eclipse.emf.ecore.util.EcoreUtil
10import org.eclipse.viatra.dse.base.ThreadContext
11import org.eclipse.xtend.lib.annotations.Accessors
12import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
13
14@FinalFieldsConstructor
15class 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
22class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.List
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import java.util.LinkedList
6import org.eclipse.emf.ecore.EObject
7import java.util.Map
8import org.eclipse.emf.ecore.util.EcoreUtil
9import org.eclipse.viatra.dse.base.ThreadContext
10import java.util.TreeMap
11import java.util.SortedMap
12
13class 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.neighbourhood.PartialInterpretation2ImmutableTypeLattice
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
6import java.util.LinkedList
7import java.util.List
8import org.eclipse.viatra.dse.base.ThreadContext
9import java.util.HashSet
10import java.util.Set
11
12enum DiversityGranularity {
13 Nodewise, Graphwise
14}
15
16class 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..f54a31ca
--- /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,29 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import org.eclipse.viatra.dse.base.ThreadContext
4import org.eclipse.viatra.dse.objectives.IGlobalConstraint
5import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
6
7@FinalFieldsConstructor
8class SurelyViolatedObjectiveGlobalConstraint implements IGlobalConstraint {
9 val ViatraReasonerSolutionSaver solutionSaver
10
11 override init(ThreadContext context) {
12 if (solutionSaver !== null) {
13 return
14 }
15 }
16
17 override createNew() {
18 this
19 }
20
21 override getName() {
22 class.name
23 }
24
25 override checkGlobalConstraint(ThreadContext context) {
26 val bestFitness = DseUtils.caclulateBestPossibleFitness(context)
27 bestFitness.satisifiesHardObjectives && solutionSaver.fitnessMayBeSaved(bestFitness)
28 }
29}
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..7d0a7884 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
@@ -9,7 +9,7 @@ import org.eclipse.viatra.dse.objectives.Comparators
9class UnfinishedMultiplicityObjective implements IObjective { 9class 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
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..6bffeb59
--- /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,137 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import java.util.HashMap
4import java.util.Map
5import org.eclipse.viatra.dse.api.DSEException
6import org.eclipse.viatra.dse.api.Solution
7import org.eclipse.viatra.dse.api.SolutionTrajectory
8import org.eclipse.viatra.dse.base.ThreadContext
9import org.eclipse.viatra.dse.objectives.Fitness
10import org.eclipse.viatra.dse.objectives.IObjective
11import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper
12import org.eclipse.viatra.dse.solutionstore.SolutionStore.ISolutionSaver
13import org.eclipse.xtend.lib.annotations.Accessors
14
15/**
16 * Based on {@link SolutionStore.BestSolutionSaver}.
17 */
18class 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 (!fitness.satisifiesHardObjectives) {
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 (!fitness.satisifiesHardObjectives) {
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 basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, Fitness fitness) {
96 var boolean solutionSaved = false
97 var dseSolution = solutionsCollection.get(id)
98 if (dseSolution === null) {
99 solutionCopier.copySolution(context, id)
100 dseSolution = new Solution(id, solutionTrajectory)
101 solutionsCollection.put(id, dseSolution)
102 solutionSaved = true
103 } else {
104 solutionSaved = dseSolution.trajectories.add(solutionTrajectory)
105 }
106 if (solutionSaved) {
107 solutionTrajectory.solution = dseSolution
108 trajectories.put(solutionTrajectory, fitness)
109 }
110 solutionSaved
111 }
112
113 def fitnessMayBeSaved(Fitness fitness) {
114 if (!hasExtremalObjectives) {
115 return true
116 }
117 var boolean mayDominate
118 for (existingFitness : trajectories.values) {
119 val isNewFitnessBetter = comparatorHelper.compare(fitness, existingFitness)
120 if (isNewFitnessBetter < 0) {
121 return false
122 }
123 if (isNewFitnessBetter > 0) {
124 mayDominate = true
125 }
126 }
127 mayDominate || needsMoreSolutionsWithSameFitness
128 }
129
130 private def boolean needsMoreSolutionsWithSameFitness() {
131 if (solutionsCollection === null) {
132 // The solutions collection will only be initialized upon saving the first solution.
133 return true
134 }
135 solutionsCollection.size < numberOfRequiredSolutions
136 }
137}
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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2 2
3import com.google.common.collect.ImmutableList
3import java.util.ArrayList 4import java.util.ArrayList
4import java.util.Collection 5import java.util.Collection
5import org.eclipse.viatra.dse.objectives.Comparators 6import org.eclipse.viatra.dse.objectives.Comparators
@@ -12,25 +13,35 @@ import org.eclipse.viatra.query.runtime.api.IQuerySpecification
12import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher 13import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
13 14
14class WF2ObjectiveConverter { 15class 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..241bef2a
--- /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,102 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2
3import java.util.Comparator
4import org.eclipse.viatra.dse.base.ThreadContext
5import org.eclipse.xtend.lib.annotations.Accessors
6import org.eclipse.xtend.lib.annotations.Data
7
8abstract class ObjectiveThreshold {
9 public static val NO_THRESHOLD = new hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold {
10 override isHard() {
11 false
12 }
13
14 override satisfiesThreshold(double cost, Comparator<Double> comparator) {
15 true
16 }
17 }
18
19 private new() {
20 }
21
22 def boolean isHard() {
23 true
24 }
25
26 def boolean satisfiesThreshold(double cost, Comparator<Double> comparator)
27
28 @Data
29 static class Exclusive extends ObjectiveThreshold {
30 val double threshold
31
32 override satisfiesThreshold(double cost, Comparator<Double> comparator) {
33 comparator.compare(threshold, cost) > 0
34 }
35 }
36
37 @Data
38 static class Inclusive extends ObjectiveThreshold {
39 val double threshold
40
41 override satisfiesThreshold(double cost, Comparator<Double> comparator) {
42 comparator.compare(threshold, cost) >= 0
43 }
44 }
45}
46
47abstract class AbstractThreeValuedObjective implements IThreeValuedObjective {
48 @Accessors val String name
49 @Accessors ObjectiveKind kind
50 @Accessors ObjectiveThreshold threshold
51 @Accessors int level
52
53 protected new(String name, ObjectiveKind kind, ObjectiveThreshold threshold, int level) {
54 this.name = name
55 this.kind = kind
56 this.threshold = threshold
57 this.level = level
58 }
59
60 abstract def double getLowestPossibleFitness(ThreadContext threadContext)
61
62 abstract def double getHighestPossibleFitness(ThreadContext threadContext)
63
64 override getWorstPossibleFitness(ThreadContext threadContext) {
65 switch (kind) {
66 case LOWER_IS_BETTER:
67 getHighestPossibleFitness(threadContext)
68 case HIGHER_IS_BETTER:
69 getLowestPossibleFitness(threadContext)
70 default:
71 throw new IllegalStateException("Unknown three valued objective kind: " + kind)
72 }
73 }
74
75 override getBestPossibleFitness(ThreadContext threadContext) {
76 switch (kind) {
77 case LOWER_IS_BETTER:
78 getLowestPossibleFitness(threadContext)
79 case HIGHER_IS_BETTER:
80 getHighestPossibleFitness(threadContext)
81 default:
82 throw new IllegalStateException("Unknown three valued objective kind: " + kind)
83 }
84 }
85
86 override isHardObjective() {
87 threshold.hard
88 }
89
90 override satisifiesHardObjective(Double fitness) {
91 threshold.satisfiesThreshold(fitness, comparator)
92 }
93
94 override getComparator() {
95 kind.comparator
96 }
97
98 override setComparator(Comparator<Double> comparator) {
99 kind = ObjectiveKind.fromComparator(comparator)
100 }
101
102}
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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2
3import org.eclipse.viatra.dse.base.ThreadContext
4import org.eclipse.viatra.dse.objectives.IObjective
5
6interface 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/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..f65428fe
--- /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,36 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization;
2
3import java.util.Comparator;
4
5import org.eclipse.viatra.dse.objectives.Comparators;
6
7public enum ObjectiveKind {
8 LOWER_IS_BETTER {
9
10 @Override
11 public Comparator<Double> getComparator() {
12 return Comparators.LOWER_IS_BETTER;
13 }
14
15 },
16 HIGHER_IS_BETTER {
17
18 @Override
19 public Comparator<Double> getComparator() {
20 return Comparators.HIGHER_IS_BETTER;
21 }
22
23 };
24
25 public abstract Comparator<Double> getComparator();
26
27 public static ObjectiveKind fromComparator(Comparator<Double> comparator) {
28 if (Comparators.LOWER_IS_BETTER.equals(comparator)) {
29 return ObjectiveKind.LOWER_IS_BETTER;
30 } else if (Comparators.HIGHER_IS_BETTER.equals(comparator)) {
31 return ObjectiveKind.HIGHER_IS_BETTER;
32 } else {
33 throw new IllegalStateException("Only LOWER_IS_BETTER and HIGHER_IS_BETTER comparators are supported.");
34 }
35 }
36}
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..e2585c83
--- /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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization
2
3import com.google.common.collect.ImmutableList
4import java.util.Collection
5import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.query.runtime.api.IPatternMatch
7import org.eclipse.viatra.query.runtime.api.IQuerySpecification
8import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
9import org.eclipse.xtend.lib.annotations.Data
10
11@Data
12class 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
19class 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 getFitness(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}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-03 11:14:06 +0000