diff options
author | 2017-09-27 22:47:51 +0200 | |
---|---|---|
committer | 2017-09-27 22:47:51 +0200 | |
commit | 0d4516ef455e916ffac2702d2bfe727c71789bc0 (patch) | |
tree | cb16562d8c29f2df497d876ab46ca1e1e99f8c0b /Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend | |
parent | Set thread stop signal to volatile (diff) | |
download | VIATRA-Generator-0d4516ef455e916ffac2702d2bfe727c71789bc0.tar.gz VIATRA-Generator-0d4516ef455e916ffac2702d2bfe727c71789bc0.tar.zst VIATRA-Generator-0d4516ef455e916ffac2702d2bfe727c71789bc0.zip |
Research paper measurement configuration updates
Diffstat (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend')
-rw-r--r-- | Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend | 378 |
1 files changed, 378 insertions, 0 deletions
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend new file mode 100644 index 00000000..d8f75b89 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend | |||
@@ -0,0 +1,378 @@ | |||
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.domains.yakindu.sgraph.yakindumm.Statechart | ||
6 | import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | ||
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | ||
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | ||
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.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml | ||
29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy | ||
31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | ||
32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
33 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation | ||
34 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
35 | import java.io.BufferedReader | ||
36 | import java.io.InputStreamReader | ||
37 | import java.util.ArrayList | ||
38 | import java.util.Collections | ||
39 | import java.util.LinkedList | ||
40 | import java.util.List | ||
41 | import java.util.Random | ||
42 | import org.eclipse.emf.ecore.EObject | ||
43 | import org.eclipse.emf.ecore.resource.Resource | ||
44 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
45 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
46 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
47 | import java.lang.invoke.VolatileCallSite | ||
48 | |||
49 | enum PartialModelSource { Homeworks, Random } | ||
50 | enum ValidationTechique {Alloy, Viatra} | ||
51 | |||
52 | class RunModelExtensionMeasurements { | ||
53 | val String id | ||
54 | |||
55 | new(String id) { | ||
56 | this.id = id | ||
57 | inputs = new FileSystemWorkspace('''initialModels/''',"") | ||
58 | workspace = new FileSystemWorkspace('''output_«id»/''',"") | ||
59 | } | ||
60 | |||
61 | // Workspace | ||
62 | val FileSystemWorkspace inputs | ||
63 | val FileSystemWorkspace workspace | ||
64 | |||
65 | // Mappers | ||
66 | val Ecore2Logic ecore2Logic = new Ecore2Logic | ||
67 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | ||
68 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | ||
69 | |||
70 | // Solvers | ||
71 | val SMTSolver smtSolver = new SMTSolver | ||
72 | val ViatraReasoner viatraSolver = new ViatraReasoner | ||
73 | val ViatraReasoner viatraWithSmtSolver = new ViatraReasoner | ||
74 | val AlloySolver alloyReasoner = new AlloySolver | ||
75 | |||
76 | def dslLoader(Domain dsl) { | ||
77 | if(dsl == Domain::FAM) { | ||
78 | return new FAMLoader(inputs) | ||
79 | } else if(dsl == Domain::Yakindu) { | ||
80 | return new YakinduLoader(inputs) =>[it.useSynchronization = false useComplexStates = true] | ||
81 | } else if(dsl == Domain::FileSystem){ | ||
82 | return new FileSystemLoader(inputs) | ||
83 | } else if(dsl == Domain::Ecore) { | ||
84 | return new EcoreLoader(inputs) | ||
85 | }else throw new IllegalArgumentException('''Unknown domain: «dsl»''') | ||
86 | } | ||
87 | def static init() { | ||
88 | LogiclanguagePackage.eINSTANCE.class | ||
89 | LogicproblemPackage.eINSTANCE.class | ||
90 | PartialinterpretationPackage.eINSTANCE.class | ||
91 | Ecore2logicannotationsPackage.eINSTANCE.class | ||
92 | Viatra2LogicAnnotationsPackage.eINSTANCE.class | ||
93 | YakindummPackage.eINSTANCE.class | ||
94 | Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("*",new XMIResourceFactoryImpl) | ||
95 | } | ||
96 | |||
97 | def transformMMtoLogic(EcoreMetamodelDescriptor mm) { | ||
98 | ecore2Logic.transformMetamodel(mm,new Ecore2LogicConfiguration()) | ||
99 | } | ||
100 | def transformPSToLogic(List<EObject> objects, TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelProblem) { | ||
101 | instanceModel2Logic.transform(metamodelProblem,objects) | ||
102 | } | ||
103 | def transformQueriesToLogic(ViatraQuerySetDescriptor descriptor, TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelProblem) { | ||
104 | viatra2Logic.transformQueries(descriptor,metamodelProblem,new Viatra2LogicConfiguration) | ||
105 | } | ||
106 | |||
107 | def executeSolver( | ||
108 | LogicProblem problem, | ||
109 | ViatraQuerySetDescriptor vq, | ||
110 | MetamodelLoader loader, | ||
111 | DiversityDescriptor diversityRequirement, | ||
112 | int size, | ||
113 | UseSolver solver) | ||
114 | { | ||
115 | if(solver == UseSolver.Smt) { | ||
116 | val smtConfig = new SmtSolverConfiguration() => [ | ||
117 | it.typeScopes.maxNewElements = size | ||
118 | it.typeScopes.minNewElements = size | ||
119 | it.solutionScope.numberOfRequiredSolution = 1 | ||
120 | it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"''' | ||
121 | ] | ||
122 | val solution = this.smtSolver.solve( | ||
123 | problem, | ||
124 | smtConfig, | ||
125 | this.workspace | ||
126 | ) | ||
127 | return solution | ||
128 | } if(solver==UseSolver::Alloy) { | ||
129 | val alloyConfig = new AlloySolverConfiguration => [ | ||
130 | it.typeScopes.maxNewElements = size | ||
131 | it.typeScopes.minNewElements = size | ||
132 | it.solutionScope.numberOfRequiredSolution = 1 | ||
133 | it.typeScopes.maxNewIntegers = 0 | ||
134 | it.writeToFile = true | ||
135 | ] | ||
136 | val solution = this.alloyReasoner.solve( | ||
137 | problem, | ||
138 | alloyConfig, | ||
139 | this.workspace | ||
140 | ) | ||
141 | return solution | ||
142 | } else { | ||
143 | val viatraConfig = new ViatraReasonerConfiguration => [ | ||
144 | it.runtimeLimit = 400 | ||
145 | it.typeScopes.maxNewElements = size | ||
146 | it.typeScopes.minNewElements = size | ||
147 | it.solutionScope.numberOfRequiredSolution = 1 | ||
148 | it.existingQueries = vq.patterns.map[it.internalQueryRepresentation] | ||
149 | it.nameNewElements = false | ||
150 | it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis | ||
151 | it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints | ||
152 | it.stateCoderStrategy = StateCoderStrategy::Neighbourhood | ||
153 | it.debugCongiguration.partalInterpretationVisualisationFrequency = 100 | ||
154 | //it.debugCongiguration.partialInterpretatioVisualiser = | ||
155 | //new GraphvizVisualisation | ||
156 | //new PartialInterpretationSizePrinter | ||
157 | ] | ||
158 | viatraConfig.diversityRequirement = diversityRequirement | ||
159 | if (solver == UseSolver.Viatra) { | ||
160 | val solution = this.viatraSolver.solve( | ||
161 | problem, | ||
162 | viatraConfig, | ||
163 | this.workspace | ||
164 | ) | ||
165 | return solution | ||
166 | } else if(solver == UseSolver.ViatraWithSmt) { | ||
167 | val inconsistency = new SmtSolverConfiguration() => [ | ||
168 | it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"''' | ||
169 | it.runtimeLimit = 10 | ||
170 | ] | ||
171 | val solution = this.viatraWithSmtSolver.solve( | ||
172 | problem, | ||
173 | viatraConfig =>[ | ||
174 | it.internalConsistencyCheckerConfiguration.internalIncosnsitencyDetector = smtSolver | ||
175 | it.internalConsistencyCheckerConfiguration.internalInconsistencDetectorConfiguration = inconsistency | ||
176 | ], | ||
177 | this.workspace | ||
178 | ) | ||
179 | return solution | ||
180 | } | ||
181 | } | ||
182 | } | ||
183 | |||
184 | def public static loadPartialModels(int size, int max) { | ||
185 | if(partialModelSource === PartialModelSource::Homeworks) { | ||
186 | val hfs = new FileSystemWorkspace("D:/Eclipse/GIT/RemoHF/Extracted/output","") | ||
187 | val allFileNames = hfs.allFiles.toList | ||
188 | |||
189 | |||
190 | val models = allFileNames.map[hfs.readModel(Statechart,it)] | ||
191 | //println("loaded") | ||
192 | val filtered = if(size===-1) { | ||
193 | models | ||
194 | } else { | ||
195 | models.filter[it.eAllContents.size + 1 >= size].toList | ||
196 | } | ||
197 | //println("filtered") | ||
198 | |||
199 | val selected = if(max!==-1) { | ||
200 | Collections.shuffle(filtered); | ||
201 | filtered.subList(0,max) | ||
202 | } else { | ||
203 | filtered | ||
204 | } | ||
205 | //println("selected "+ selected.size) | ||
206 | val collected = selected.map[ | ||
207 | val r = new LinkedList | ||
208 | r.add(it) | ||
209 | r.addAll(it.eAllContents.toIterable) | ||
210 | return r | ||
211 | ].toList | ||
212 | //println("collected to lists") | ||
213 | |||
214 | val list = new ArrayList(collected.size) | ||
215 | for(s : collected) { | ||
216 | list.add(s.prune(size)) | ||
217 | } | ||
218 | //println("pruned to " + size) | ||
219 | |||
220 | return list | ||
221 | } else if(partialModelSource === PartialModelSource::Random) { | ||
222 | |||
223 | } | ||
224 | } | ||
225 | |||
226 | static val Random pruningRandom = new Random(0) | ||
227 | // def private void prune(EObject root, int targetSize) { | ||
228 | // var size = root.eAllContents.size + 1 | ||
229 | // while(size>targetSize) { | ||
230 | // val leafs = root.eAllContents.filter[it.eContents.empty].toList | ||
231 | // val leafToRemove = leafs.get(pruningRandom.nextInt(leafs.size)) | ||
232 | // EcoreUtil.delete(leafToRemove) | ||
233 | // size-- | ||
234 | // } | ||
235 | // } | ||
236 | def static private prune(List<EObject> objects, int targetSize) { | ||
237 | if(targetSize !== -1) { | ||
238 | var size = objects.size | ||
239 | while(size>targetSize) { | ||
240 | val leafs = objects.filter[!it.eAllContents.toList.exists[child | objects.contains(child)]].toList | ||
241 | if(leafs.exists[it instanceof Statechart]) { | ||
242 | println("Gebasz!") | ||
243 | } | ||
244 | objects.remove(leafs.get(pruningRandom.nextInt(leafs.size))) | ||
245 | size-- | ||
246 | } | ||
247 | if(!objects.exists[it instanceof Statechart]) { | ||
248 | println("Gebasz2!") | ||
249 | } | ||
250 | |||
251 | } | ||
252 | return objects; | ||
253 | } | ||
254 | |||
255 | static val partialModelSource = PartialModelSource::Homeworks | ||
256 | static val monitoring = false | ||
257 | static val clean = true | ||
258 | public static var sizes = #[-1/*,5,10,15,20,25,30,35,40,45,50*/] | ||
259 | |||
260 | def static void waitForEnter() { | ||
261 | if(monitoring) { | ||
262 | println(''' Press ENTER to continue''') | ||
263 | (new BufferedReader(new InputStreamReader(System.in))).readLine | ||
264 | } | ||
265 | } | ||
266 | |||
267 | def static runMeasure(String id, int size){ | ||
268 | init | ||
269 | |||
270 | val partialModels = loadPartialModels(size,-1) | ||
271 | var pmIndex = 1 | ||
272 | |||
273 | for(partialModel : partialModels) { | ||
274 | |||
275 | val pmID = id+"_"+(pmIndex++) | ||
276 | val r = new RunModelExtensionMeasurements(pmID) | ||
277 | r.workspace.initAndClear | ||
278 | print(pmID + ";") | ||
279 | print(partialModel.size + ";") | ||
280 | //println("- init") | ||
281 | val dsl = r.dslLoader(Domain::Yakindu) | ||
282 | val mm = dsl.loadMetamodel() | ||
283 | val vq = dsl.loadQueries(mm) | ||
284 | //println("- Queries loaded") | ||
285 | |||
286 | val metamodelProblem = r.transformMMtoLogic(mm) | ||
287 | r.transformPSToLogic(partialModel,metamodelProblem) | ||
288 | r.transformQueriesToLogic(vq,metamodelProblem) | ||
289 | val logicProblem = metamodelProblem.output | ||
290 | |||
291 | //println("- DSL -> Logic problem transformation finished") | ||
292 | |||
293 | waitForEnter | ||
294 | |||
295 | val ValidationTechique validationTechnique = ValidationTechique::Viatra | ||
296 | if(validationTechnique === ValidationTechique::Alloy) { | ||
297 | val solution = r.executeSolver(logicProblem, vq, dsl, null, 0, UseSolver::Alloy) | ||
298 | |||
299 | print(solution.class.simpleName+";"); | ||
300 | print(solution.statistics.transformationTime+";") | ||
301 | print(solution.statistics.solverTime+";") | ||
302 | print((new StatisticSections2Print).transformStatisticDatas2CSV(solution.statistics.entries)) | ||
303 | |||
304 | waitForEnter | ||
305 | |||
306 | if(solution instanceof ModelResult) { | ||
307 | val representations = solution.representation | ||
308 | for(representationIndex : 0..<representations.size) { | ||
309 | val representation = representations.get(representationIndex) | ||
310 | val representationNumber = representationIndex + 1 | ||
311 | if(representation instanceof PartialInterpretation) { | ||
312 | r.workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''') | ||
313 | val partialInterpretation2GML = new PartialInterpretation2Gml | ||
314 | val gml = partialInterpretation2GML.transform(representation) | ||
315 | r.workspace.writeText('''solution«representationNumber».gml''',gml) | ||
316 | if(representation.newElements.size <160) { | ||
317 | val visualiser = new GraphvizVisualisation | ||
318 | val visualisation = visualiser.visualiseConcretization(representation) | ||
319 | visualisation.writeToFile(r.workspace,'''solution«representationNumber»''') | ||
320 | } | ||
321 | |||
322 | } else { | ||
323 | r.workspace.writeText('''solution«representationNumber».txt''',representation.toString) | ||
324 | } | ||
325 | } | ||
326 | println('''saved''') | ||
327 | } else { | ||
328 | val partial = logicProblem//.eContainer | ||
329 | r.workspace.writeModel(partial, "solution.partialinterpretation") | ||
330 | println('''saved''') | ||
331 | } | ||
332 | } else if(validationTechnique === ValidationTechique::Viatra) { | ||
333 | val validationPatterns = vq.validationPatterns | ||
334 | val resource = partialModel.head.eResource | ||
335 | |||
336 | val startTime = System.currentTimeMillis | ||
337 | val ViatraQueryEngine engine = ViatraQueryEngine.on(new EMFScope(resource) ) | ||
338 | val matchers = new ArrayList(validationPatterns.size) | ||
339 | val validationResult = new ArrayList(validationPatterns.size) | ||
340 | for(validationPattern : validationPatterns) { | ||
341 | val matcher = validationPattern.getMatcher(engine) | ||
342 | matchers += matcher | ||
343 | validationResult += matcher.hasMatch | ||
344 | } | ||
345 | val finishTime = System.currentTimeMillis-startTime | ||
346 | |||
347 | print(finishTime + ";") | ||
348 | print(!validationResult.exists[it] + ";") | ||
349 | for(patternResult : validationResult) { | ||
350 | print(patternResult + ";") | ||
351 | } | ||
352 | println | ||
353 | } | ||
354 | |||
355 | System.gc System.gc System.gc | ||
356 | Thread.sleep(2000) | ||
357 | } | ||
358 | } | ||
359 | |||
360 | def static void main(String[] args) { | ||
361 | //val id = 50//args.get(0) | ||
362 | for(size : sizes) { | ||
363 | val run = (1..1).map['''r«it»'''] | ||
364 | for(runIndex : run) { | ||
365 | val runID = runIndex+"_"+size | ||
366 | |||
367 | |||
368 | try { | ||
369 | runMeasure(runID,size) | ||
370 | } catch(Exception e) {e.printStackTrace} | ||
371 | |||
372 | System.gc System.gc System.gc | ||
373 | Thread.sleep(2000) | ||
374 | } | ||
375 | } | ||
376 | |||
377 | } | ||
378 | } \ No newline at end of file | ||