aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
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/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
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/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend188
1 files changed, 100 insertions, 88 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}