diff options
Diffstat (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend')
-rw-r--r-- | Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend | 289 |
1 files changed, 289 insertions, 0 deletions
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend new file mode 100644 index 00000000..7ba38ede --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend | |||
@@ -0,0 +1,289 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | ||
2 | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver | ||
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | ||
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.statistics.StatisticSections2Print | ||
18 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver | ||
19 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration | ||
20 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
21 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | ||
22 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor | ||
23 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage | ||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | ||
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | ||
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy | ||
30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | ||
31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
32 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
33 | import java.io.BufferedReader | ||
34 | import java.io.InputStreamReader | ||
35 | import java.util.List | ||
36 | import org.eclipse.emf.ecore.EObject | ||
37 | import org.eclipse.emf.ecore.resource.Resource | ||
38 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
39 | import org.junit.Test | ||
40 | |||
41 | enum UseSolver{Viatra, Smt, ViatraWithSmt, Alloy} | ||
42 | enum Domain{FAM, Yakindu} | ||
43 | enum Diversity{No, Diverse} | ||
44 | |||
45 | class RunMeasurements { | ||
46 | val String id | ||
47 | |||
48 | new(String id) { | ||
49 | this.id = id | ||
50 | inputs = new FileSystemWorkspace('''initialModels/''',"") | ||
51 | workspace = new FileSystemWorkspace('''output_«id»/''',"") | ||
52 | } | ||
53 | |||
54 | // Workspace | ||
55 | val FileSystemWorkspace inputs | ||
56 | val FileSystemWorkspace workspace | ||
57 | |||
58 | // Mappers | ||
59 | val Ecore2Logic ecore2Logic = new Ecore2Logic | ||
60 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | ||
61 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | ||
62 | |||
63 | // Solvers | ||
64 | val SMTSolver smtSolver = new SMTSolver | ||
65 | val ViatraReasoner viatraSolver = new ViatraReasoner | ||
66 | val ViatraReasoner viatraWithSmtSolver = new ViatraReasoner(smtSolver) | ||
67 | val AlloySolver alloyReasoner = new AlloySolver | ||
68 | |||
69 | def dslLoader(Domain dsl) { | ||
70 | if(dsl == Domain::FAM) { | ||
71 | return new FAMLoader(inputs) | ||
72 | } else if(dsl == Domain::Yakindu) { | ||
73 | return new YakinduLoader(inputs) | ||
74 | } else throw new IllegalArgumentException('''Unknown domain: «dsl»''') | ||
75 | } | ||
76 | def static init() { | ||
77 | LogiclanguagePackage.eINSTANCE.class | ||
78 | LogicproblemPackage.eINSTANCE.class | ||
79 | PartialinterpretationPackage.eINSTANCE.class | ||
80 | Ecore2logicannotationsPackage.eINSTANCE.class | ||
81 | Viatra2LogicAnnotationsPackage.eINSTANCE.class | ||
82 | Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("ecore",new XMIResourceFactoryImpl) | ||
83 | Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("logicproblem",new XMIResourceFactoryImpl) | ||
84 | Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("partialinterpretation",new XMIResourceFactoryImpl) | ||
85 | } | ||
86 | |||
87 | def transformMMtoLogic(EcoreMetamodelDescriptor mm) { | ||
88 | ecore2Logic.transformMetamodel(mm,new Ecore2LogicConfiguration()) | ||
89 | } | ||
90 | def transformPSToLogic(List<EObject> objects, TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelProblem) { | ||
91 | instanceModel2Logic.transform(metamodelProblem,objects) | ||
92 | } | ||
93 | def transformQueriesToLogic(ViatraQuerySetDescriptor descriptor, TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelProblem) { | ||
94 | viatra2Logic.transformQueries(descriptor,metamodelProblem,new Viatra2LogicConfiguration) | ||
95 | } | ||
96 | def transformDiversity(MetamodelLoader dsl, Ecore2Logic_Trace trace, EcoreMetamodelDescriptor descriptor) { | ||
97 | if(diverse) { | ||
98 | val relevantClasses = dsl.getRelevantTypes(descriptor) | ||
99 | val relevantReferences = dsl.getRelevantReferences(descriptor) | ||
100 | val relevantTypes = relevantClasses.map[this.ecore2Logic.TypeofEClass(trace,it) as TypeDeclaration].toSet | ||
101 | val relevantRelations = relevantReferences.map[this.ecore2Logic.relationOfReference(trace,it) as RelationDeclaration].toSet | ||
102 | return new DiversityDescriptor => [ | ||
103 | it.relevantTypes = relevantTypes | ||
104 | it.relevantRelations = relevantRelations | ||
105 | it.maxNumber = 2 | ||
106 | it.range = 2 | ||
107 | it.parallels = 2 | ||
108 | ] | ||
109 | } else { | ||
110 | return null | ||
111 | } | ||
112 | } | ||
113 | |||
114 | def executeSolver( | ||
115 | LogicProblem problem, | ||
116 | ViatraQuerySetDescriptor vq, | ||
117 | MetamodelLoader loader, | ||
118 | DiversityDescriptor diversityRequirement, | ||
119 | int size) | ||
120 | { | ||
121 | if(solver == UseSolver.Smt) { | ||
122 | val smtConfig = new SmtSolverConfiguration() => [ | ||
123 | it.typeScopes.maxNewElements = size | ||
124 | it.typeScopes.minNewElements = size | ||
125 | it.solutionScope.numberOfRequiredSolution = number | ||
126 | it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"''' | ||
127 | ] | ||
128 | val solution = this.smtSolver.solve( | ||
129 | problem, | ||
130 | smtConfig, | ||
131 | this.workspace | ||
132 | ) | ||
133 | return solution | ||
134 | } if(solver==UseSolver::Alloy) { | ||
135 | val alloyConfig = new AlloySolverConfiguration => [ | ||
136 | it.typeScopes.maxNewElements = size | ||
137 | it.typeScopes.minNewElements = size | ||
138 | it.solutionScope.numberOfRequiredSolution = number | ||
139 | it.typeScopes.maxIntScope = 0 | ||
140 | it.writeToFile = true | ||
141 | ] | ||
142 | val solution = this.alloyReasoner.solve( | ||
143 | problem, | ||
144 | alloyConfig, | ||
145 | this.workspace | ||
146 | ) | ||
147 | return solution | ||
148 | } else { | ||
149 | val viatraConfig = new ViatraReasonerConfiguration => [ | ||
150 | it.runtimeLimit = 20 | ||
151 | it.typeScopes.maxNewElements = size | ||
152 | it.typeScopes.minNewElements = size | ||
153 | it.solutionScope.numberOfRequiredSolution = number | ||
154 | it.existingQueries = vq.patterns.map[it.internalQueryRepresentation] | ||
155 | it.nameNewElements = false | ||
156 | it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis | ||
157 | it.additionalGlobalConstraints += loader.additionalConstraints | ||
158 | it.stateCoderStrategy = StateCoderStrategy::Neighbourhood | ||
159 | ] | ||
160 | viatraConfig.diversityRequirement = diversityRequirement | ||
161 | if (solver == UseSolver.Viatra) { | ||
162 | val solution = this.viatraSolver.solve( | ||
163 | problem, | ||
164 | viatraConfig, | ||
165 | this.workspace | ||
166 | ) | ||
167 | return solution | ||
168 | } else if(solver == UseSolver.ViatraWithSmt) { | ||
169 | val inconsistency = new SmtSolverConfiguration() => [ | ||
170 | it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"''' | ||
171 | it.runtimeLimit = 10 | ||
172 | ] | ||
173 | val solution = this.viatraWithSmtSolver.solve( | ||
174 | problem, | ||
175 | viatraConfig =>[it.inconsistencDetectorConfiguration = inconsistency], | ||
176 | this.workspace | ||
177 | ) | ||
178 | return solution | ||
179 | } | ||
180 | } | ||
181 | } | ||
182 | |||
183 | @Test | ||
184 | def runAsTest() { | ||
185 | main(#[]) | ||
186 | } | ||
187 | |||
188 | static val monitoring = false | ||
189 | static val clean = false | ||
190 | static val domain = Domain::Yakindu | ||
191 | static val solver = UseSolver::Viatra | ||
192 | static val diverse = false | ||
193 | static val wf = true | ||
194 | public static var sizes = #[50] | ||
195 | static var int number = 10 | ||
196 | |||
197 | def static void waitForEnter() { | ||
198 | if(monitoring) { | ||
199 | println(''' Press ENTER to continue''') | ||
200 | (new BufferedReader(new InputStreamReader(System.in))).readLine | ||
201 | } | ||
202 | } | ||
203 | |||
204 | def static runMeasure(String id, int size) { | ||
205 | val r = new RunMeasurements(id) | ||
206 | r.workspace.initAndClear | ||
207 | init | ||
208 | //println("- init") | ||
209 | val dsl = r.dslLoader(domain) | ||
210 | val mm = dsl.loadMetamodel() | ||
211 | val vq = dsl.loadQueries(mm) | ||
212 | //println("- Queries loaded") | ||
213 | |||
214 | if(!wf) { | ||
215 | mm.attributes.forEach[it.lowerBound = 0] | ||
216 | mm.references.forEach[it.lowerBound = 0] | ||
217 | mm.references.removeAll(vq.derivedFeatures.values) | ||
218 | mm.attributes.removeAll(vq.derivedFeatures.values) | ||
219 | } | ||
220 | |||
221 | val metamodelProblem = r.transformMMtoLogic(mm) | ||
222 | r.transformPSToLogic(dsl.loadPartialModel,metamodelProblem) | ||
223 | if(wf) { | ||
224 | r.transformQueriesToLogic(vq,metamodelProblem) | ||
225 | } | ||
226 | val logicProblem = metamodelProblem.output | ||
227 | |||
228 | //r.workspace.writeModel(logicProblem,"problem.logicproblem") | ||
229 | //resSet.resources += viatraProblem.output.eResource | ||
230 | val diversityRequirement = r.transformDiversity(dsl,metamodelProblem.trace,mm) | ||
231 | |||
232 | //println("- DSL -> Logic problem transformation finished") | ||
233 | |||
234 | waitForEnter | ||
235 | |||
236 | val solution = r.executeSolver(logicProblem, vq, dsl, diversityRequirement, size) | ||
237 | |||
238 | print(solution.class.simpleName+";"); | ||
239 | print(solution.statistics.transformationTime+";") | ||
240 | print(solution.statistics.solverTime+";") | ||
241 | print((new StatisticSections2Print).transformStatisticDatas2CSV(solution.statistics.entries)) | ||
242 | |||
243 | waitForEnter | ||
244 | |||
245 | if(solution instanceof ModelResult) { | ||
246 | val representations = solution.representation | ||
247 | for(representationIndex : 0..<representations.size) { | ||
248 | val representation = representations.get(representationIndex) | ||
249 | val representationNumber = representationIndex + 1 | ||
250 | if(representation instanceof PartialInterpretation) { | ||
251 | r.workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''') | ||
252 | } else { | ||
253 | r.workspace.writeText('''solution«representationNumber».txt''',representation.toString) | ||
254 | } | ||
255 | } | ||
256 | println('''saved''') | ||
257 | } else { | ||
258 | val partial = logicProblem//.eContainer | ||
259 | r.workspace.writeModel(partial, "solution.partialinterpretation") | ||
260 | println('''saved''') | ||
261 | } | ||
262 | } | ||
263 | |||
264 | def static void main(String[] args) { | ||
265 | print("id;") | ||
266 | (1..number).forEach[print("sol"+it+" (nano);")] | ||
267 | print("Solution type (ms);Transformation time (ms);Solver time (ms);TransformationExecutionTime (ms);TypeAnalysisTime (ms);StateCoderTime (ms);SolutionCopyTime (ms);") | ||
268 | if(diverse) { | ||
269 | print("SolutionDiversityCheckTime (ms);SolutionDiversitySuccessRate (%);") | ||
270 | } | ||
271 | println("save") | ||
272 | //val id = 50//args.get(0) | ||
273 | for(size : sizes) { | ||
274 | val run = (1..50).map['''r«it»'''] | ||
275 | for(runIndex : run) { | ||
276 | val runID = runIndex+"_"+size | ||
277 | print(runID + ";") | ||
278 | |||
279 | try { | ||
280 | runMeasure(runID,size) | ||
281 | } catch(Exception e) {} | ||
282 | |||
283 | System.gc System.gc System.gc | ||
284 | Thread.sleep(2000) | ||
285 | } | ||
286 | } | ||
287 | |||
288 | } | ||
289 | } \ No newline at end of file | ||