aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-04-07 13:46:36 +0200
committerLibravatar Kristóf Marussy <kris7topher@gmail.com>2019-04-07 13:46:36 +0200
commit3f9b1c92cc35fa4ed9672a2b8601f4c22af24921 (patch)
tree927c41492ff3b50b3d998a4fbe87861187d85912 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu
parentAdd reliability probability and mtff objectives (diff)
downloadVIATRA-Generator-3f9b1c92cc35fa4ed9672a2b8601f4c22af24921.tar.gz
VIATRA-Generator-3f9b1c92cc35fa4ed9672a2b8601f4c22af24921.tar.zst
VIATRA-Generator-3f9b1c92cc35fa4ed9672a2b8601f4c22af24921.zip
Infrastructure for objective functions
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend188
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend12
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java57
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend65
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend10
-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.xtend77
-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/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/UnfinishedWFObjective.xtend56
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend99
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/WF2ObjectiveConverter.xtend44
14 files changed, 499 insertions, 290 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..8831b0ff 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
@@ -17,11 +17,13 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory 17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory 18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory
19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration 19import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration
20import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler
20import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective 21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective
21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation 22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation
22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective 23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective 25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedWFObjective 26import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver
25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter 27import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter
26import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 28import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
27import java.util.List 29import java.util.List
@@ -31,44 +33,41 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer
31import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel 33import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel
32import org.eclipse.viatra.dse.solutionstore.SolutionStore 34import org.eclipse.viatra.dse.solutionstore.SolutionStore
33import org.eclipse.viatra.dse.statecode.IStateCoderFactory 35import 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 36
37class ViatraReasoner extends LogicReasoner{ 37class ViatraReasoner extends LogicReasoner {
38 val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() 38 val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()
39 val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider 39 val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider
40 val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE 40 val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE
41 val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter 41 val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter
42 42
43 43 override solve(LogicProblem problem, LogicSolverConfiguration configuration,
44 override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { 44 ReasonerWorkspace workspace) throws LogicReasonerException {
45 val viatraConfig = configuration.asConfig 45 val viatraConfig = configuration.asConfig
46 46
47 if(viatraConfig.debugCongiguration.logging) { 47 if (viatraConfig.debugConfiguration.logging) {
48 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL) 48 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL)
49 } else { 49 } else {
50 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN) 50 DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN)
51 } 51 }
52 52
53 val DesignSpaceExplorer dse = new DesignSpaceExplorer(); 53 val DesignSpaceExplorer dse = new DesignSpaceExplorer();
54 54
55 dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE) 55 dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE)
56 dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE) 56 dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE)
57 dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE) 57 dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE)
58 58
59 val transformationStartTime = System.nanoTime 59 val transformationStartTime = System.nanoTime
60 60
61 61 val emptySolution = initialiser.initialisePartialInterpretation(problem, viatraConfig.typeScopes).output
62 62 if ((viatraConfig.documentationLevel == DocumentationLevel::FULL ||
63 val emptySolution = initialiser.initialisePartialInterpretation(problem,viatraConfig.typeScopes).output 63 viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) {
64 if((viatraConfig.documentationLevel == DocumentationLevel::FULL || viatraConfig.documentationLevel == DocumentationLevel::NORMAL) && workspace !== null) { 64 workspace.writeModel(emptySolution, "init.partialmodel")
65 workspace.writeModel(emptySolution,"init.partialmodel") 65 }
66 }
67 emptySolution.problemConainer = problem 66 emptySolution.problemConainer = problem
68 67
69 val ScopePropagator scopePropagator = new ScopePropagator(emptySolution) 68 val ScopePropagator scopePropagator = new ScopePropagator(emptySolution)
70 scopePropagator.propagateAllScopeConstraints 69 scopePropagator.propagateAllScopeConstraints
71 70
72 val method = modelGenerationMethodProvider.createModelGenerationMethod( 71 val method = modelGenerationMethodProvider.createModelGenerationMethod(
73 problem, 72 problem,
74 emptySolution, 73 emptySolution,
@@ -78,138 +77,151 @@ class ViatraReasoner extends LogicReasoner{
78 scopePropagator, 77 scopePropagator,
79 viatraConfig.documentationLevel 78 viatraConfig.documentationLevel
80 ) 79 )
81 80
82 dse.addObjective(new ModelGenerationCompositeObjective( 81 dse.addObjective(new ModelGenerationCompositeObjective(
83 new ScopeObjective, 82 new ScopeObjective,
84 method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], 83 method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)],
85 new UnfinishedWFObjective(method.unfinishedWF) 84 wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF)
86 )) 85 ))
87 86
88 dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF)) 87 val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolutions)
89 for(additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) { 88 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))
89 val solutionSaver = new ViatraReasonerSolutionSaver(newArrayOfSize(0, 0))
90 val solutionCopier = solutionSaver.solutionCopier
91 solutionStore.withSolutionSaver(solutionSaver)
92 dse.solutionStore = solutionStore
93
94 dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationGlobalConstraint(method.invalidWF))
95 dse.addGlobalConstraint(new SurelyViolatedObjectiveGlobalConstraint(solutionSaver))
96 for (additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) {
90 dse.addGlobalConstraint(additionalConstraint.apply(method)) 97 dse.addGlobalConstraint(additionalConstraint.apply(method))
91 } 98 }
92 99
93 dse.setInitialModel(emptySolution,false) 100 dse.setInitialModel(emptySolution, false)
94 101
95 val IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) { 102 val IStateCoderFactory statecoder = if (viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) {
96 new NeighbourhoodBasedStateCoderFactory 103 new NeighbourhoodBasedStateCoderFactory
97 } else { 104 } else {
98 new IdentifierBasedStateCoderFactory 105 new IdentifierBasedStateCoderFactory
99 } 106 }
100 dse.stateCoderFactory = statecoder 107 dse.stateCoderFactory = statecoder
101 108
102 dse.maxNumberOfThreads = 1 109 dse.maxNumberOfThreads = 1
103 110
104 val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolution) 111 for (rule : method.relationRefinementRules) {
105 dse.solutionStore = solutionStore
106
107 for(rule : method.relationRefinementRules) {
108 dse.addTransformationRule(rule) 112 dse.addTransformationRule(rule)
109 } 113 }
110 for(rule : method.objectRefinementRules) { 114 for (rule : method.objectRefinementRules) {
111 dse.addTransformationRule(rule) 115 dse.addTransformationRule(rule)
112 } 116 }
113 117
114 val strategy = new BestFirstStrategyForModelGeneration(workspace,viatraConfig,method) 118 val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method)
115 viatraConfig.progressMonitor.workedForwardTransformation 119 viatraConfig.progressMonitor.workedForwardTransformation
116 120
117 val transformationTime = System.nanoTime - transformationStartTime 121 val transformationTime = System.nanoTime - transformationStartTime
118 val solverStartTime = System.nanoTime 122 val solverStartTime = System.nanoTime
119 123
120 var boolean stoppedByTimeout 124 var boolean stoppedByTimeout
121 var boolean stoppedByException 125 try {
122 try{ 126 stoppedByTimeout = dse.startExplorationWithTimeout(strategy, configuration.runtimeLimit * 1000);
123 stoppedByTimeout = dse.startExplorationWithTimeout(strategy,configuration.runtimeLimit*1000);
124 stoppedByException = false
125 } catch (NullPointerException npe) { 127 } catch (NullPointerException npe) {
126 stoppedByTimeout = false 128 stoppedByTimeout = false
127 stoppedByException = true
128 } 129 }
129 val solverTime = System.nanoTime - solverStartTime 130 val solverTime = System.nanoTime - solverStartTime
130 viatraConfig.progressMonitor.workedSearchFinished 131 viatraConfig.progressMonitor.workedSearchFinished
131 132
132 //additionalMatches = strategy.solutionStoreWithCopy.additionalMatches 133 // additionalMatches = strategy.solutionStoreWithCopy.additionalMatches
133 val statistics = createStatistics => [ 134 val statistics = createStatistics => [
134 //it.solverTime = viatraConfig.runtimeLimit 135 // it.solverTime = viatraConfig.runtimeLimit
135 it.solverTime = (solverTime/1000000) as int 136 it.solverTime = (solverTime / 1000000) as int
136 it.transformationTime = (transformationTime/1000000) as int 137 it.transformationTime = (transformationTime / 1000000) as int
137 for(x : 0..<strategy.solutionStoreWithCopy.allRuntimes.size) { 138 for (pair : solutionCopier.getAllCopierRuntimes(true).indexed) {
138 it.entries += createIntStatisticEntry => [ 139 it.entries += createIntStatisticEntry => [
139 it.name = '''_Solution«x»FoundAt''' 140 it.name = '''_Solution«pair.key»FoundAt'''
140 it.value = (strategy.solutionStoreWithCopy.allRuntimes.get(x)/1000000) as int 141 it.value = (pair.value / 1000000) as int
141 ] 142 ]
142 } 143 }
143 it.entries += createIntStatisticEntry => [ 144 it.entries += createIntStatisticEntry => [
144 it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int 145 it.name = "TransformationExecutionTime"
146 it.value = (method.statistics.transformationExecutionTime / 1000000) as int
145 ] 147 ]
146 it.entries += createIntStatisticEntry => [ 148 it.entries += createIntStatisticEntry => [
147 it.name = "TypeAnalysisTime" it.value = (method.statistics.PreliminaryTypeAnalisisTime/1000000) as int 149 it.name = "TypeAnalysisTime"
150 it.value = (method.statistics.PreliminaryTypeAnalisisTime / 1000000) as int
148 ] 151 ]
149 it.entries += createIntStatisticEntry => [ 152 it.entries += createIntStatisticEntry => [
150 it.name = "StateCoderTime" it.value = (statecoder.runtime/1000000) as int 153 it.name = "StateCoderTime"
154 it.value = (statecoder.runtime / 1000000) as int
151 ] 155 ]
152 it.entries += createIntStatisticEntry => [ 156 it.entries += createIntStatisticEntry => [
153 it.name = "StateCoderFailCount" it.value = strategy.numberOfStatecoderFail 157 it.name = "StateCoderFailCount"
158 it.value = strategy.numberOfStatecoderFail
154 ] 159 ]
155 it.entries += createIntStatisticEntry => [ 160 it.entries += createIntStatisticEntry => [
156 it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int 161 it.name = "SolutionCopyTime"
162 it.value = (solutionCopier.getTotalCopierRuntime / 1000000) as int
157 ] 163 ]
158 if(strategy.solutionStoreWithDiversityDescriptor.isActive) { 164 if (strategy.solutionStoreWithDiversityDescriptor.isActive) {
159 it.entries += createIntStatisticEntry => [ 165 it.entries += createIntStatisticEntry => [
160 it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int 166 it.name = "SolutionDiversityCheckTime"
167 it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime / 1000000) as int
161 ] 168 ]
162 it.entries += createRealStatisticEntry => [ 169 it.entries += createRealStatisticEntry => [
163 it.name = "SolutionDiversitySuccessRate" it.value = strategy.solutionStoreWithDiversityDescriptor.successRate 170 it.name = "SolutionDiversitySuccessRate"
171 it.value = strategy.solutionStoreWithDiversityDescriptor.successRate
164 ] 172 ]
165 } 173 }
166 ] 174 ]
167 175
168 viatraConfig.progressMonitor.workedBackwardTransformationFinished 176 viatraConfig.progressMonitor.workedBackwardTransformationFinished
169 177
170 if(stoppedByTimeout) { 178 if (stoppedByTimeout) {
171 return createInsuficientResourcesResult=>[ 179 return createInsuficientResourcesResult => [
172 it.problem = problem 180 it.problem = problem
173 it.resourceName="time" 181 it.resourceName = "time"
174 it.representation += strategy.solutionStoreWithCopy.solutions 182 it.representation += solutionCopier.getPartialInterpretations(true)
175 it.statistics = statistics 183 it.statistics = statistics
176 ] 184 ]
177 } else { 185 } else {
178 if(solutionStore.solutions.empty) { 186 if (solutionStore.solutions.empty) {
179 return createInconsistencyResult => [ 187 return createInconsistencyResult => [
180 it.problem = problem 188 it.problem = problem
181 it.representation += strategy.solutionStoreWithCopy.solutions 189 it.representation += solutionCopier.getPartialInterpretations(true)
182 it.statistics = statistics 190 it.statistics = statistics
183 ] 191 ]
184 } else { 192 } else {
185 return createModelResult => [ 193 return createModelResult => [
186 it.problem = problem 194 it.problem = problem
187 it.trace = strategy.solutionStoreWithCopy.copyTraces 195 it.trace = solutionCopier.getTraces(true)
188 it.representation += strategy.solutionStoreWithCopy.solutions 196 it.representation += solutionCopier.getPartialInterpretations(true)
189 it.statistics = statistics 197 it.statistics = statistics
190 ] 198 ]
191 } 199 }
192 } 200 }
193 } 201 }
194 202
195 private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) { 203 private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) {
196 sc.sumStatecoderRuntime 204 sc.sumStatecoderRuntime
197 } 205 }
198 206
199 private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) { 207 private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) {
200 sc.sumStatecoderRuntime 208 sc.sumStatecoderRuntime
201 } 209 }
202 210
203 override getInterpretations(ModelResult modelResult) { 211 override getInterpretations(ModelResult modelResult) {
204 val indexes = 0..<modelResult.representation.size 212 val indexes = 0 ..< modelResult.representation.size
205 val traces = modelResult.trace as List<Map<EObject, EObject>>; 213 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 214 val res = indexes.map [ i |
215 new PartialModelAsLogicInterpretation(modelResult.representation.get(i) as PartialInterpretation,
216 traces.get(i))
217 ].toList
207 return res 218 return res
208 } 219 }
209 220
210 private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) { 221 private def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) {
211 if(configuration instanceof ViatraReasonerConfiguration) { 222 if (configuration instanceof ViatraReasonerConfiguration) {
212 return configuration 223 return configuration
213 } else throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''') 224 } else
225 throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''')
214 } 226 }
215} 227}
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..9ef23c59 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
@@ -12,7 +12,7 @@ import java.util.List
12import java.util.Set 12import java.util.Set
13import org.eclipse.xtext.xbase.lib.Functions.Function1 13import org.eclipse.xtext.xbase.lib.Functions.Function1
14 14
15public enum StateCoderStrategy { 15enum StateCoderStrategy {
16 Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity 16 Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity
17} 17}
18 18
@@ -40,14 +40,14 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{
40 /** 40 /**
41 * Configuration for debugging support. 41 * Configuration for debugging support.
42 */ 42 */
43 public var DebugConfiguration debugCongiguration = new DebugConfiguration 43 public var DebugConfiguration debugConfiguration = new DebugConfiguration
44 /** 44 /**
45 * Configuration for cutting search space. 45 * Configuration for cutting search space.
46 */ 46 */
47 public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint 47 public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint
48} 48}
49 49
50public class DiversityDescriptor { 50class DiversityDescriptor {
51 public var ensureDiversity = false 51 public var ensureDiversity = false
52 public static val FixPointRange = -1 52 public static val FixPointRange = -1
53 public var int range = FixPointRange 53 public var int range = FixPointRange
@@ -57,19 +57,19 @@ public class DiversityDescriptor {
57 public var Set<RelationDeclaration> relevantRelations = null 57 public var Set<RelationDeclaration> relevantRelations = null
58} 58}
59 59
60public class DebugConfiguration { 60class DebugConfiguration {
61 public var logging = false 61 public var logging = false
62 public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null; 62 public var PartialInterpretationVisualiser partialInterpretatioVisualiser = null;
63 public var partalInterpretationVisualisationFrequency = 1 63 public var partalInterpretationVisualisationFrequency = 1
64} 64}
65 65
66public class InternalConsistencyCheckerConfiguration { 66class InternalConsistencyCheckerConfiguration {
67 public var LogicReasoner internalIncosnsitencyDetector = null 67 public var LogicReasoner internalIncosnsitencyDetector = null
68 public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null 68 public var LogicSolverConfiguration internalInconsistencDetectorConfiguration = null
69 public var incternalConsistencyCheckingFrequency = 1 69 public var incternalConsistencyCheckingFrequency = 1
70} 70}
71 71
72public class SearchSpaceConstraint { 72class SearchSpaceConstraint {
73 public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE 73 public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE
74 public var int maxDepth = UNLIMITED_MAXDEPTH 74 public var int maxDepth = UNLIMITED_MAXDEPTH
75 public var List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList 75 public var List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalGlobalConstraints = new LinkedList
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..1234d54b 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,7 +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; 78 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;
@@ -97,9 +96,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
97 this.method = method; 96 this.method = method;
98 } 97 }
99 98
100 public SolutionStoreWithCopy getSolutionStoreWithCopy() {
101 return solutionStoreWithCopy;
102 }
103 public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() { 99 public SolutionStoreWithDiversityDescriptor getSolutionStoreWithDiversityDescriptor() {
104 return solutionStoreWithDiversityDescriptor; 100 return solutionStoreWithDiversityDescriptor;
105 } 101 }
@@ -121,7 +117,6 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
121 matchers.add(matcher); 117 matchers.add(matcher);
122 } 118 }
123 119
124 this.solutionStoreWithCopy = new SolutionStoreWithCopy();
125 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement); 120 this.solutionStoreWithDiversityDescriptor = new SolutionStoreWithDiversityDescriptor(configuration.diversityRequirement);
126 121
127 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); 122 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
@@ -146,13 +141,13 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
146 return; 141 return;
147 } 142 }
148 143
149 final Fitness firstFittness = context.calculateFitness(); 144 final Fitness firstfitness = context.calculateFitness();
150 checkForSolution(firstFittness); 145 checkForSolution(firstfitness);
151 146
152 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper(); 147 final ObjectiveComparatorHelper objectiveComparatorHelper = context.getObjectiveComparatorHelper();
153 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]); 148 final Object[] firstTrajectory = context.getTrajectory().toArray(new Object[0]);
154 TrajectoryWithFitness currentTrajectoryWithFittness = new TrajectoryWithFitness(firstTrajectory, firstFittness); 149 TrajectoryWithFitness currentTrajectoryWithfitness = new TrajectoryWithFitness(firstTrajectory, firstfitness);
155 trajectoiresToExplore.add(currentTrajectoryWithFittness); 150 trajectoiresToExplore.add(currentTrajectoryWithfitness);
156 151
157 //if(configuration) 152 //if(configuration)
158 visualiseCurrentState(); 153 visualiseCurrentState();
@@ -167,22 +162,22 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
167 162
168 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) { 163 mainLoop: while (!isInterrupted && !configuration.progressMonitor.isCancelled()) {
169 164
170 if (currentTrajectoryWithFittness == null) { 165 if (currentTrajectoryWithfitness == null) {
171 if (trajectoiresToExplore.isEmpty()) { 166 if (trajectoiresToExplore.isEmpty()) {
172 logger.debug("State space is fully traversed."); 167 logger.debug("State space is fully traversed.");
173 return; 168 return;
174 } else { 169 } else {
175 currentTrajectoryWithFittness = selectState(); 170 currentTrajectoryWithfitness = selectState();
176 if (logger.isDebugEnabled()) { 171 if (logger.isDebugEnabled()) {
177 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray())); 172 logger.debug("Current trajectory: " + Arrays.toString(context.getTrajectory().toArray()));
178 logger.debug("New trajectory is chosen: " + currentTrajectoryWithFittness); 173 logger.debug("New trajectory is chosen: " + currentTrajectoryWithfitness);
179 } 174 }
180 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithFittness.trajectory); 175 context.getDesignSpaceManager().executeTrajectoryWithMinimalBacktrackWithoutStateCoding(currentTrajectoryWithfitness.trajectory);
181 } 176 }
182 } 177 }
183 178
184// visualiseCurrentState(); 179// visualiseCurrentState();
185// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); 180// boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
186// if(consistencyCheckResult == true) { 181// if(consistencyCheckResult == true) {
187// continue mainLoop; 182// continue mainLoop;
188// } 183// }
@@ -194,7 +189,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
194 final Object nextActivation = iterator.next(); 189 final Object nextActivation = iterator.next();
195// if (!iterator.hasNext()) { 190// if (!iterator.hasNext()) {
196// logger.debug("Last untraversed activation of the state."); 191// logger.debug("Last untraversed activation of the state.");
197// trajectoiresToExplore.remove(currentTrajectoryWithFittness); 192// trajectoiresToExplore.remove(currentTrajectoryWithfitness);
198// } 193// }
199 logger.debug("Executing new activation: " + nextActivation); 194 logger.debug("Executing new activation: " + nextActivation);
200 context.executeAcitvationId(nextActivation); 195 context.executeAcitvationId(nextActivation);
@@ -209,7 +204,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
209// System.out.println("---------"); 204// System.out.println("---------");
210// } 205// }
211 206
212 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFittness); 207 boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithfitness);
213 if(consistencyCheckResult == true) { continue mainLoop; } 208 if(consistencyCheckResult == true) { continue mainLoop; }
214 209
215 if (context.isCurrentStateAlreadyTraversed()) { 210 if (context.isCurrentStateAlreadyTraversed()) {
@@ -227,31 +222,31 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
227 continue; 222 continue;
228 } 223 }
229 224
230 TrajectoryWithFitness nextTrajectoryWithFittness = new TrajectoryWithFitness( 225 TrajectoryWithFitness nextTrajectoryWithfitness = new TrajectoryWithFitness(
231 context.getTrajectory().toArray(), nextFitness); 226 context.getTrajectory().toArray(), nextFitness);
232 trajectoiresToExplore.add(nextTrajectoryWithFittness); 227 trajectoiresToExplore.add(nextTrajectoryWithfitness);
233 228
234 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFittness.fitness, 229 int compare = objectiveComparatorHelper.compare(currentTrajectoryWithfitness.fitness,
235 nextTrajectoryWithFittness.fitness); 230 nextTrajectoryWithfitness.fitness);
236 if (compare < 0) { 231 if (compare < 0) {
237 logger.debug("Better fitness, moving on: " + nextFitness); 232 logger.debug("Better fitness, moving on: " + nextFitness);
238 currentTrajectoryWithFittness = nextTrajectoryWithFittness; 233 currentTrajectoryWithfitness = nextTrajectoryWithfitness;
239 continue mainLoop; 234 continue mainLoop;
240 } else if (compare == 0) { 235 } else if (compare == 0) {
241 logger.debug("Equally good fitness, moving on: " + nextFitness); 236 logger.debug("Equally good fitness, moving on: " + nextFitness);
242 currentTrajectoryWithFittness = nextTrajectoryWithFittness; 237 currentTrajectoryWithfitness = nextTrajectoryWithfitness;
243 continue mainLoop; 238 continue mainLoop;
244 } else { 239 } else {
245 logger.debug("Worse fitness."); 240 logger.debug("Worse fitness.");
246 currentTrajectoryWithFittness = null; 241 currentTrajectoryWithfitness = null;
247 continue mainLoop; 242 continue mainLoop;
248 } 243 }
249 } 244 }
250 } 245 }
251 246
252 logger.debug("State is fully traversed."); 247 logger.debug("State is fully traversed.");
253 trajectoiresToExplore.remove(currentTrajectoryWithFittness); 248 trajectoiresToExplore.remove(currentTrajectoryWithfitness);
254 currentTrajectoryWithFittness = null; 249 currentTrajectoryWithfitness = null;
255 250
256 } 251 }
257 logger.info("Interrupted."); 252 logger.info("Interrupted.");
@@ -269,15 +264,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
269 return activationIds; 264 return activationIds;
270 } 265 }
271 266
272 private void checkForSolution(final Fitness fittness) { 267 private void checkForSolution(final Fitness fitness) {
273 if (fittness.isSatisifiesHardObjectives()) { 268 if (fitness.isSatisifiesHardObjectives()) {
274 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) { 269 if (solutionStoreWithDiversityDescriptor.isDifferent(context)) {
275 solutionStoreWithCopy.newSolution(context);
276 solutionStoreWithDiversityDescriptor.newSolution(context); 270 solutionStoreWithDiversityDescriptor.newSolution(context);
277 solutionStore.newSolution(context); 271 solutionStore.newSolution(context);
278 configuration.progressMonitor.workedModelFound(configuration.solutionScope.numberOfRequiredSolution);
279
280 logger.debug("Found a solution.");
281 } 272 }
282 } 273 }
283 } 274 }
@@ -311,11 +302,11 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
311 } 302 }
312 303
313 public void visualiseCurrentState() { 304 public void visualiseCurrentState() {
314 PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugCongiguration.partialInterpretatioVisualiser; 305 PartialInterpretationVisualiser partialInterpretatioVisualiser = configuration.debugConfiguration.partialInterpretatioVisualiser;
315 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) { 306 if(partialInterpretatioVisualiser != null && this.configuration.documentationLevel == DocumentationLevel.FULL && workspace != null) {
316 PartialInterpretation p = (PartialInterpretation) (context.getModel()); 307 PartialInterpretation p = (PartialInterpretation) (context.getModel());
317 int id = ++numberOfPrintedModel; 308 int id = ++numberOfPrintedModel;
318 if (id % configuration.debugCongiguration.partalInterpretationVisualisationFrequency == 0) { 309 if (id % configuration.debugConfiguration.partalInterpretationVisualisationFrequency == 0) {
319 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p); 310 PartialInterpretationVisualisation visualisation = partialInterpretatioVisualiser.visualiseConcretization(p);
320 visualisation.writeToFile(workspace, String.format("state%09d.png", id)); 311 visualisation.writeToFile(workspace, String.format("state%09d.png", id));
321 } 312 }
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..3a897aa3
--- /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,65 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import org.eclipse.viatra.dse.base.ThreadContext
4import org.eclipse.viatra.dse.objectives.Comparators
5import org.eclipse.viatra.dse.objectives.Fitness
6import org.eclipse.viatra.dse.objectives.IObjective
7
8final class DseUtils {
9 private new() {
10 throw new IllegalStateException("This is a static utility class and should not be instantiated directly.")
11 }
12
13 static def calculateFitness(ThreadContext it, (IObjective)=>Double getFitness) {
14 val result = new Fitness
15 var boolean satisifiesHardObjectives = true
16 for (objective : objectives) {
17 val fitness = getFitness.apply(objective)
18 result.put(objective.name, fitness)
19 if (objective.isHardObjective() && !objective.satisifiesHardObjective(fitness)) {
20 satisifiesHardObjectives = false
21 }
22 }
23 result.satisifiesHardObjectives = satisifiesHardObjectives
24 result
25 }
26
27 static def caclulateBestPossibleFitness(ThreadContext threadContext) {
28 threadContext.calculateFitness [ objective |
29 if (objective instanceof IThreeValuedObjective) {
30 objective.getBestPossibleFitness(threadContext)
31 } else {
32 switch (objective.comparator) {
33 case Comparators.LOWER_IS_BETTER:
34 Double.NEGATIVE_INFINITY
35 case Comparators.HIGHER_IS_BETTER:
36 Double.POSITIVE_INFINITY
37 case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER:
38 0.0
39 default:
40 throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " +
41 objective.name)
42 }
43 }
44 ]
45 }
46
47 static def caclulateWorstPossibleFitness(ThreadContext threadContext) {
48 threadContext.calculateFitness [ objective |
49 if (objective instanceof IThreeValuedObjective) {
50 objective.getWorstPossibleFitness(threadContext)
51 } else {
52 switch (objective.comparator) {
53 case Comparators.LOWER_IS_BETTER,
54 case Comparators.DIFFERENCE_TO_ZERO_IS_BETTER:
55 Double.POSITIVE_INFINITY
56 case Comparators.HIGHER_IS_BETTER:
57 Double.NEGATIVE_INFINITY
58 default:
59 throw new IllegalArgumentException("Unknown comparator for non-three-valued objective: " +
60 objective.name)
61 }
62 }
63 ]
64 }
65}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend
new file mode 100644
index 00000000..8c93d4ec
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend
@@ -0,0 +1,10 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
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/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..af6d1bbd 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,12 @@
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.Comparator 4import java.util.Comparator
4import java.util.List 5import java.util.List
5import org.eclipse.viatra.dse.base.ThreadContext 6import org.eclipse.viatra.dse.base.ThreadContext
6import org.eclipse.viatra.dse.objectives.Comparators 7import org.eclipse.viatra.dse.objectives.Comparators
7import org.eclipse.viatra.dse.objectives.IObjective 8import org.eclipse.viatra.dse.objectives.IObjective
8import org.eclipse.viatra.dse.objectives.impl.BaseObjective 9import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
9 10
10//class ViatraReasonerNumbers { 11//class ViatraReasonerNumbers {
11// public static val scopePriority = 2 12// public static val scopePriority = 2
@@ -22,64 +23,66 @@ import org.eclipse.viatra.dse.objectives.impl.BaseObjective
22// public static val compositePriority = 2 23// public static val compositePriority = 2
23//} 24//}
24 25
25class ModelGenerationCompositeObjective implements IObjective{ 26@FinalFieldsConstructor
26 val ScopeObjective scopeObjective 27class ModelGenerationCompositeObjective implements IThreeValuedObjective {
27 val List<UnfinishedMultiplicityObjective> unfinishedMultiplicityObjectives 28 val IObjective scopeObjective
28 val UnfinishedWFObjective unfinishedWFObjective 29 val List<IObjective> unfinishedMultiplicityObjectives
29 30 val IObjective unfinishedWFObjective
30 public new( 31
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) { 32 override init(ThreadContext context) {
41 this.scopeObjective.init(context) 33 this.scopeObjective.init(context)
42 this.unfinishedMultiplicityObjectives.forEach[it.init(context)] 34 this.unfinishedMultiplicityObjectives.forEach[it.init(context)]
43 this.unfinishedWFObjective.init(context) 35 this.unfinishedWFObjective.init(context)
44 } 36 }
45 37
46 override createNew() { 38 override createNew() {
47 return new ModelGenerationCompositeObjective( 39 return new ModelGenerationCompositeObjective(
48 this.scopeObjective, this.unfinishedMultiplicityObjectives, this.unfinishedWFObjective) 40 scopeObjective.createNew,
41 ImmutableList.copyOf(unfinishedMultiplicityObjectives.map[createNew]),
42 unfinishedWFObjective.createNew
43 )
49 } 44 }
50 45
51 override getComparator() { Comparators.LOWER_IS_BETTER } 46 override getComparator() { Comparators.LOWER_IS_BETTER }
47
52 override getFitness(ThreadContext context) { 48 override getFitness(ThreadContext context) {
53 var sum = 0.0 49 var sum = 0.0
54 val scopeFitnes = scopeObjective.getFitness(context) 50 val scopeFitnes = scopeObjective.getFitness(context)
55 //val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)] 51 // val unfinishedMultiplicitiesFitneses = unfinishedMultiplicityObjectives.map[x|x.getFitness(context)]
56 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context) 52 val unfinishedWFsFitness = unfinishedWFObjective.getFitness(context)
57 53
58 sum+=scopeFitnes 54 sum += scopeFitnes
59 var multiplicity = 0.0 55 var multiplicity = 0.0
60 for(multiplicityObjective : unfinishedMultiplicityObjectives) { 56 for (multiplicityObjective : unfinishedMultiplicityObjectives) {
61 multiplicity+=multiplicityObjective.getFitness(context)//*0.5 57 multiplicity += multiplicityObjective.getFitness(context) // *0.5
62 } 58 }
63 sum+=multiplicity 59 sum += multiplicity
64 sum += unfinishedWFsFitness//*0.5 60 sum += unfinishedWFsFitness // *0.5
65 61 // println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
66 //println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')
67
68 return sum 62 return sum
69 } 63 }
70 64
71 override getLevel() { 2 } 65 override getWorstPossibleFitness(ThreadContext threadContext) {
72 override getName() { "CompositeUnfinishednessObjective"} 66 Double.POSITIVE_INFINITY
67 }
73 68
69 override getBestPossibleFitness(ThreadContext threadContext) {
70 0.0
71 }
72
73 override getLevel() { 2 }
74
75 override getName() { "CompositeUnfinishednessObjective" }
76
74 override isHardObjective() { true } 77 override isHardObjective() { true }
78
75 override satisifiesHardObjective(Double fitness) { fitness <= 0.001 } 79 override satisifiesHardObjective(Double fitness) { fitness <= 0.001 }
76 80
77
78 override setComparator(Comparator<Double> comparator) { 81 override setComparator(Comparator<Double> comparator) {
79 throw new UnsupportedOperationException("TODO: auto-generated method stub") 82 throw new UnsupportedOperationException("Model generation objective comparator cannot be set.")
80 } 83 }
84
81 override setLevel(int level) { 85 override setLevel(int level) {
82 throw new UnsupportedOperationException("TODO: auto-generated method stub") 86 throw new UnsupportedOperationException("Model generation objective level cannot be set.")
83 } 87 }
84 88}
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/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..7fd494a0
--- /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.isFitnessDominated(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/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
deleted file mode 100644
index e0111cf6..00000000
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
+++ /dev/null
@@ -1,56 +0,0 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
2
3import org.eclipse.viatra.dse.objectives.IObjective
4import org.eclipse.viatra.query.runtime.api.IPatternMatch
5import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
6import org.eclipse.viatra.query.runtime.api.IQuerySpecification
7import java.util.Collection
8import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
9import org.eclipse.viatra.query.runtime.emf.EMFScope
10import org.eclipse.viatra.dse.base.ThreadContext
11import java.util.List
12import org.eclipse.viatra.dse.objectives.Comparators
13import java.util.ArrayList
14import java.util.Comparator
15
16class UnfinishedWFObjective implements IObjective {
17 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs
18 val List<ViatraQueryMatcher<?>> matchers
19
20 public new(Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) {
21 this.unfinishedWFs = unfinishedWFs
22 matchers = new ArrayList(unfinishedWFs.size)
23 }
24 override getName() '''unfinishedWFs'''
25 override createNew() {
26 return new UnfinishedWFObjective(unfinishedWFs)
27 }
28 override init(ThreadContext context) {
29 val engine = context.queryEngine//ViatraQueryEngine.on(new EMFScope(context.model))
30 for(unfinishedWF : unfinishedWFs) {
31 matchers += unfinishedWF.getMatcher(engine)
32 }
33 }
34
35 override getComparator() { Comparators.LOWER_IS_BETTER }
36 override getFitness(ThreadContext context) {
37 var sumOfMatches = 0
38 for(matcher : matchers) {
39 val number = matcher.countMatches
40 //println('''«matcher.patternName» = «number»''')
41 sumOfMatches+=number
42 }
43 return sumOfMatches.doubleValue
44 }
45
46 override getLevel() { 2 }
47 override isHardObjective() { true }
48 override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }
49
50 override setComparator(Comparator<Double> comparator) {
51 throw new UnsupportedOperationException("TODO: auto-generated method stub")
52 }
53 override setLevel(int level) {
54 throw new UnsupportedOperationException("TODO: auto-generated method stub")
55 }
56} \ 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/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..5877778e
--- /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,99 @@
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 org.eclipse.viatra.dse.solutionstore.SolutionStore.BestSolutionSaver}.
17 */
18class ViatraReasonerSolutionSaver implements ISolutionSaver {
19 @Accessors val solutionCopier = new SolutionCopier
20 val boolean hasExtremalObjectives
21 val ObjectiveComparatorHelper comparatorHelper
22 val Map<SolutionTrajectory, Fitness> trajectories = new HashMap
23
24 @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection
25
26 new(IObjective[][] leveledExtremalObjectives) {
27 comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives)
28 hasExtremalObjectives = leveledExtremalObjectives.exists[!empty]
29 }
30
31 override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
32 if (hasExtremalObjectives) {
33 saveBestSolutionOnly(context, id, solutionTrajectory)
34 } else {
35 basicSaveSolution(context, id, solutionTrajectory)
36 }
37 }
38
39 private def saveBestSolutionOnly(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
40 val fitness = context.lastFitness
41 val dominatedTrajectories = newArrayList
42 for (entry : trajectories.entrySet) {
43 val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value)
44 if (isLastFitnessBetter < 0) {
45 // Found a trajectory that dominates the current one, no need to save
46 return false
47 }
48 if (isLastFitnessBetter > 0) {
49 dominatedTrajectories += entry.key
50 }
51 }
52 // We must save the new trajectory before removing dominated trajectories
53 // to avoid removing the current solution when it is reachable only via dominated trajectories.
54 val solutionSaved = basicSaveSolution(context, id, solutionTrajectory)
55 for (dominatedTrajectory : dominatedTrajectories) {
56 trajectories -= dominatedTrajectory
57 val dominatedSolution = dominatedTrajectory.solution
58 if (!dominatedSolution.trajectories.remove(dominatedTrajectory)) {
59 throw new DSEException(
60 "Dominated solution is not reachable from dominated trajectory. This should never happen!")
61 }
62 if (dominatedSolution.trajectories.empty) {
63 val dominatedSolutionId = dominatedSolution.stateCode
64 solutionCopier.markAsObsolete(dominatedSolutionId)
65 solutionsCollection -= dominatedSolutionId
66 }
67 }
68 solutionSaved
69 }
70
71 private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
72 val fitness = context.lastFitness
73 var boolean solutionSaved = false
74 var dseSolution = solutionsCollection.get(id)
75 if (dseSolution === null) {
76 solutionCopier.copySolution(context, id)
77 dseSolution = new Solution(id, solutionTrajectory)
78 solutionsCollection.put(id, dseSolution)
79 solutionSaved = true
80 } else {
81 solutionSaved = dseSolution.trajectories.add(solutionTrajectory)
82 }
83 if (solutionSaved) {
84 solutionTrajectory.solution = dseSolution
85 trajectories.put(solutionTrajectory, fitness)
86 }
87 solutionSaved
88 }
89
90 def isFitnessDominated(Fitness fitness) {
91 for (existingFitness : trajectories.values) {
92 val isNewFitnessBetter = comparatorHelper.compare(fitness, existingFitness)
93 if (isNewFitnessBetter < 0) {
94 return true
95 }
96 }
97 false
98 }
99}
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..c601de40 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,34 @@ 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 }
20 unfinishedWF.map[ 23
21 new QueryConstraint(it.fullyQualifiedName,it,2.0) 24 def createInvalidationObjective(
22 ].toList 25 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {
26 createConstraintObjective(INVALIDATED_WFS_NAME, invalidatedByWF)
27 }
28
29 def IGlobalConstraint createInvalidationGlobalConstraint(
30 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidatedByWF) {
31 new ModelQueriesGlobalConstraint(INVALIDATED_WFS_NAME, new ArrayList(invalidatedByWF))
32 }
33
34 private def createConstraintObjective(String name,
35 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries) {
36 val res = new ConstraintsObjective(
37 name,
38 ImmutableList.copyOf(queries.map [
39 new QueryConstraint(it.fullyQualifiedName, it, 1.0)
40 ])
23 ) 41 )
24 res.withComparator(Comparators.LOWER_IS_BETTER) 42 res.withComparator(Comparators.LOWER_IS_BETTER)
25 res.level = 2 43 res.level = 2
26 return res 44 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 } 45 }
36} \ No newline at end of file 46}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 08:23:25 +0000