diff options
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.xtend | 205 |
1 files changed, 205 insertions, 0 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 new file mode 100644 index 00000000..38cc9459 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | |||
@@ -0,0 +1,205 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PartialModelAsLogicInterpretation | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedWFObjective | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter | ||
23 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
24 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer | ||
25 | import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel | ||
26 | import org.eclipse.viatra.dse.solutionstore.SolutionStore | ||
27 | import org.eclipse.viatra.dse.statecode.IStateCoderFactory | ||
28 | |||
29 | class ViatraReasoner extends LogicReasoner{ | ||
30 | val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser() | ||
31 | val ModelGenerationMethodProvider modelGenerationMethodProvider = new ModelGenerationMethodProvider | ||
32 | val extension LogicresultFactory factory = LogicresultFactory.eINSTANCE | ||
33 | val WF2ObjectiveConverter wf2ObjectiveConverter = new WF2ObjectiveConverter | ||
34 | |||
35 | val LogicReasoner inconsistencyDetector | ||
36 | |||
37 | public new() { | ||
38 | this.inconsistencyDetector=null | ||
39 | } | ||
40 | |||
41 | public new(LogicReasoner inconsistencyDetector) { | ||
42 | this.inconsistencyDetector = inconsistencyDetector | ||
43 | } | ||
44 | |||
45 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | ||
46 | val viatraConfig = configuration.asConfig | ||
47 | val DesignSpaceExplorer dse = new DesignSpaceExplorer(); | ||
48 | |||
49 | /* | ||
50 | DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.VERBOSE_FULL) | ||
51 | /*/ | ||
52 | DesignSpaceExplorer.turnOnLogging(DseLoggingLevel.WARN) | ||
53 | //*/ | ||
54 | |||
55 | dse.addMetaModelPackage(LogiclanguagePackage.eINSTANCE) | ||
56 | dse.addMetaModelPackage(LogicproblemPackage.eINSTANCE) | ||
57 | dse.addMetaModelPackage(PartialinterpretationPackage.eINSTANCE) | ||
58 | |||
59 | val transformationStartTime = System.nanoTime | ||
60 | |||
61 | val emptySolution = initialiser.initialisePartialInterpretation(problem, | ||
62 | viatraConfig.typeScopes.minNewElements, | ||
63 | viatraConfig.typeScopes.maxNewElements).output | ||
64 | emptySolution.problemConainer = problem | ||
65 | |||
66 | val method = modelGenerationMethodProvider.createModelGenerationMethod( | ||
67 | problem, | ||
68 | emptySolution, | ||
69 | viatraConfig.existingQueries, | ||
70 | workspace, | ||
71 | viatraConfig.nameNewElements, | ||
72 | viatraConfig.typeInferenceMethod | ||
73 | ) | ||
74 | |||
75 | dse.addObjective(new ModelGenerationCompositeObjective( | ||
76 | new ScopeObjective, | ||
77 | method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)], | ||
78 | new UnfinishedWFObjective(method.unfinishedWF) | ||
79 | )) | ||
80 | |||
81 | dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationObjective(method.invalidWF)) | ||
82 | for(additionalConstraint : configuration.asConfig.additionalGlobalConstraints) { | ||
83 | dse.addGlobalConstraint(additionalConstraint.apply(method)) | ||
84 | } | ||
85 | |||
86 | dse.setInitialModel(emptySolution) | ||
87 | |||
88 | var IStateCoderFactory statecoder = if(viatraConfig.stateCoderStrategy == StateCoderStrategy.Neighbourhood) { | ||
89 | new NeighbourhoodBasedStateCoderFactory | ||
90 | } else { | ||
91 | new IdentifierBasedStateCoderFactory | ||
92 | } | ||
93 | dse.stateCoderFactory = statecoder | ||
94 | |||
95 | dse.maxNumberOfThreads = 1 | ||
96 | |||
97 | val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolution) | ||
98 | dse.solutionStore = solutionStore | ||
99 | |||
100 | for(rule : method.relationRefinementRules) { | ||
101 | dse.addTransformationRule(rule) | ||
102 | } | ||
103 | for(rule : method.objectRefinementRules) { | ||
104 | dse.addTransformationRule(rule) | ||
105 | } | ||
106 | |||
107 | val strategy = new BestFirstStrategyForModelGeneration( | ||
108 | workspace,inconsistencyDetector, | ||
109 | viatraConfig.inconsistencDetectorConfiguration, | ||
110 | viatraConfig.diversityRequirement) | ||
111 | |||
112 | val transformationTime = System.nanoTime - transformationStartTime | ||
113 | val solverStartTime = System.nanoTime | ||
114 | var boolean stoppedByTimeout | ||
115 | var boolean stoppedByException | ||
116 | try{ | ||
117 | stoppedByTimeout = dse.startExplorationWithTimeout(strategy,configuration.runtimeLimit*1000); | ||
118 | stoppedByException = false | ||
119 | } catch (NullPointerException npe) { | ||
120 | stoppedByTimeout = false | ||
121 | stoppedByException = true | ||
122 | } | ||
123 | |||
124 | val solverTime = System.nanoTime - solverStartTime | ||
125 | |||
126 | val statecoderFinal = statecoder | ||
127 | val statistics = createStatistics => [ | ||
128 | //it.solverTime = viatraConfig.runtimeLimit | ||
129 | it.solverTime = (solverTime/1000000) as int | ||
130 | it.transformationTime = (transformationTime/1000000) as int | ||
131 | it.entries += createIntStatisticEntry => [ | ||
132 | it.name = "TransformationExecutionTime" it.value = (method.statistics.transformationExecutionTime/1000000) as int | ||
133 | ] | ||
134 | it.entries += createIntStatisticEntry => [ | ||
135 | it.name = "TypeAnalysisTime" it.value = (method.statistics.PreliminaryTypeAnalisisTime/1000000) as int | ||
136 | ] | ||
137 | it.entries += createIntStatisticEntry => [ | ||
138 | it.name = "StateCoderTime" it.value = (statecoderFinal.runtime/1000000) as int | ||
139 | ] | ||
140 | it.entries += createIntStatisticEntry => [ | ||
141 | it.name = "StateCoderFailCount" it.value = strategy.numberOfStatecoderFaiL | ||
142 | ] | ||
143 | it.entries += createIntStatisticEntry => [ | ||
144 | it.name = "SolutionCopyTime" it.value = (strategy.solutionStoreWithCopy.sumRuntime/1000000) as int | ||
145 | ] | ||
146 | if(strategy.solutionStoreWithDiversityDescriptor.isActive) { | ||
147 | it.entries += createIntStatisticEntry => [ | ||
148 | it.name = "SolutionDiversityCheckTime" it.value = (strategy.solutionStoreWithDiversityDescriptor.sumRuntime/1000000) as int | ||
149 | ] | ||
150 | it.entries += createRealStatisticEntry => [ | ||
151 | it.name = "SolutionDiversitySuccessRate" it.value = strategy.solutionStoreWithDiversityDescriptor.successRate | ||
152 | ] | ||
153 | } | ||
154 | ] | ||
155 | |||
156 | if(stoppedByTimeout) { | ||
157 | return createInsuficientResourcesResult=>[ | ||
158 | it.problem = problem | ||
159 | it.resourceName="time" | ||
160 | it.statistics = statistics | ||
161 | ] | ||
162 | } else { | ||
163 | if(solutionStore.solutions.empty) { | ||
164 | return createInconsistencyResult => [ | ||
165 | it.problem = problem | ||
166 | it.statistics = statistics | ||
167 | ] | ||
168 | } else { | ||
169 | |||
170 | /*solutionStore.solutions.head.trajectories.head | ||
171 | solutionTrajectory.doTransformation(emptySolution) | ||
172 | * | ||
173 | */ | ||
174 | return factory.createModelResult => [ | ||
175 | it.problem = problem | ||
176 | it.trace = null | ||
177 | it.representation += strategy.solutionStoreWithCopy.solutions | ||
178 | it.statistics = statistics | ||
179 | ] | ||
180 | } | ||
181 | } | ||
182 | } | ||
183 | |||
184 | /*private def simpleWeithts(List<IObjective> objectives) { | ||
185 | objectives.map[1.0].toList | ||
186 | }*/ | ||
187 | |||
188 | private def dispatch long runtime(NeighbourhoodBasedStateCoderFactory sc) { | ||
189 | sc.sumStatecoderRuntime | ||
190 | } | ||
191 | |||
192 | private def dispatch long runtime(IdentifierBasedStateCoderFactory sc) { | ||
193 | sc.sumStatecoderRuntime | ||
194 | } | ||
195 | |||
196 | override getInterpretation(ModelResult modelResult) { | ||
197 | return new PartialModelAsLogicInterpretation | ||
198 | } | ||
199 | |||
200 | def ViatraReasonerConfiguration asConfig(LogicSolverConfiguration configuration) { | ||
201 | if(configuration instanceof ViatraReasonerConfiguration) { | ||
202 | return configuration | ||
203 | } else throw new IllegalArgumentException('''Wrong configuration. Expected: «ViatraReasonerConfiguration.name», but got: «configuration.class.name»"''') | ||
204 | } | ||
205 | } | ||