aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-08 03:00:08 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-08 03:00:08 -0400
commitf63a94c06268b5233264436cc538062f1f7b01bc (patch)
treecbdc3dcdb34ecbeaba24991c36c34205df79e32e /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src
parentVAMPIRE: Implement Vampire measurement code (diff)
downloadVIATRA-Generator-f63a94c06268b5233264436cc538062f1f7b01bc.tar.gz
VIATRA-Generator-f63a94c06268b5233264436cc538062f1f7b01bc.tar.zst
VIATRA-Generator-f63a94c06268b5233264436cc538062f1f7b01bc.zip
VAMPIRE: fix bug in transformation, further implement measurement code
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend111
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql8
2 files changed, 52 insertions, 67 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
index 057bcf12..cc7f4809 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
@@ -1,10 +1,10 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.FamPatterns 3import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver 4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration 5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
6import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel 7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
7import functionalarchitecture.FunctionalarchitecturePackage
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic 8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration 9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
10import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel 10import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
@@ -12,9 +12,13 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
12import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult 12import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
13import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore 13import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
14import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic 14import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
15import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic 16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
16import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 17import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
17import java.io.PrintWriter 18import java.io.PrintWriter
19import java.text.SimpleDateFormat
20import java.time.LocalDate
21import java.util.Date
18import org.eclipse.emf.ecore.resource.Resource 22import org.eclipse.emf.ecore.resource.Resource
19import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 23import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
20 24
@@ -26,8 +30,12 @@ class YakinduTest {
26 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic 30 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
27 31
28 // Workspace setup 32 // Workspace setup
33 val Date date = new Date(System.currentTimeMillis)
34 val SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss");
35 val formattedDate = format.format(date)
36
29 val inputs = new FileSystemWorkspace('''initialModels/''', "") 37 val inputs = new FileSystemWorkspace('''initialModels/''', "")
30 val workspace = new FileSystemWorkspace('''output/YakinduTest/''', "") 38 val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "")
31 workspace.initAndClear 39 workspace.initAndClear
32 40
33 // Logicproblem writing setup 41 // Logicproblem writing setup
@@ -37,12 +45,12 @@ class YakinduTest {
37 45
38 println("Input and output workspaces are created") 46 println("Input and output workspaces are created")
39 47
40// val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) 48 val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE)
41 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) 49 val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi")
42// val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi") 50 val queries = GeneralTest.loadQueries(metamodel, Patterns.instance)
43 val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") 51// val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)
44// val queries = GeneralTest.loadQueries(metamodel, YakinduPatterns.instance) 52// val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi")
45 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) 53// val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)
46// val queries = null 54// val queries = null
47 println("DSL loaded") 55 println("DSL loaded")
48 56
@@ -50,40 +58,42 @@ class YakinduTest {
50 var START = 10 58 var START = 10
51 var INC = 20 59 var INC = 20
52 var REPS = 1 60 var REPS = 1
53 61
54 val EXACT = -1 62 val EXACT = 50
55 if (EXACT!= -1) { 63 if (EXACT != -1) {
56 MAX = EXACT 64 MAX = EXACT
57 START = EXACT 65 START = EXACT
58 INC = 1 66 INC = 1
59 REPS = 5 67 REPS = 3
60 } 68 }
61 69
62 var writer = new PrintWriter(workspace.workspaceURI + "//yakinduStats.csv") 70 var writer = new PrintWriter(workspace.workspaceURI + "//_yakinduStats.csv")
63 writer.append("size,") 71 writer.append("size,")
64 for (var x = 0; x < REPS; x++) { 72 for (var x = 0; x < REPS; x++) {
65 writer.append("t" + x + ",") 73 writer.append("tTransf" + x + "," + "tSolv" + x + ",")
66 } 74 }
67 writer.append("avg\n") 75 writer.append("medSolv,medTransf\n")
68 var totalTime = 0.0 76 var solverTimes = newArrayList
69 var totFound = 0.0 77 var transformationTimes = newArrayList
70 var modelFound = true 78 var modelFound = true
71 var LogicResult solution = null 79 var LogicResult solution = null
72 for (var i = START; i <= MAX; i += INC) { 80 for (var i = START; i <= MAX; i += INC) {
73 val num = (i - START) / INC 81 val num = (i - START) / INC
74 print("Generation " + num + ": SIZE=" + i + " Attempt: ") 82 print("Generation " + num + ": SIZE=" + i + " Attempt: ")
75 writer.append(i + ",") 83 writer.append(i + ",")
76 totalTime = 0.0 84 solverTimes.clear
77 totFound = 0.0 85 transformationTimes.clear
78 modelFound = true 86 modelFound = true
79 for (var j = 0; j < REPS; j++) { 87 for (var j = 0; j < REPS; j++) {
80 88
81 print(j) 89 print(j)
82 90
83 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) 91 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
84 var problem = modelGenerationProblem.output 92 var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel)
85 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output 93 var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem,
86// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output 94 new Viatra2LogicConfiguration)
95
96 var problem = validModelExtensionProblem.output
87 workspace.writeModel(problem, "Yakindu.logicproblem") 97 workspace.writeModel(problem, "Yakindu.logicproblem")
88 98
89// println("Problem created") 99// println("Problem created")
@@ -110,9 +120,11 @@ class YakinduTest {
110 // Define Config File 120 // Define Config File
111 val size = i 121 val size = i
112 val inc = INC 122 val inc = INC
123 val iter = j
113 val vampireConfig = new VampireSolverConfiguration => [ 124 val vampireConfig = new VampireSolverConfiguration => [
114 // add configuration things, in config file first 125 // add configuration things, in config file first
115 it.documentationLevel = DocumentationLevel::FULL 126 it.documentationLevel = DocumentationLevel::FULL
127 it.iteration = iter
116 128
117 it.typeScopes.minNewElements = size - inc 129 it.typeScopes.minNewElements = size - inc
118 it.typeScopes.maxNewElements = size 130 it.typeScopes.maxNewElements = size
@@ -132,11 +144,12 @@ class YakinduTest {
132// ].isEmpty 144// ].isEmpty
133// 145//
134// if (modelFound) { 146// if (modelFound) {
135 val time = solution.statistics.transformationTime / 1000.0 147 val tTime = solution.statistics.transformationTime / 1000.0
136 writer.append(time + ",") 148 val sTime = solution.statistics.solverTime / 1000.0
137 print("(" + time + ")..") 149 writer.append(tTime + "," + sTime + ",")
138 totalTime += time 150 print("(" + tTime + "/" + sTime + "s)..")
139 totFound += 1 151 solverTimes.add(sTime)
152 transformationTimes.add(tTime)
140// } else { 153// } else {
141// writer.append("MNF" + ",") 154// writer.append("MNF" + ",")
142//// print("MNF") 155//// print("MNF")
@@ -144,55 +157,19 @@ class YakinduTest {
144 // println("Problem solved") 157 // println("Problem solved")
145 // visualisation, see 158 // visualisation, see
146// var interpretations = reasoner.getInterpretations(solution as ModelResult) 159// var interpretations = reasoner.getInterpretations(solution as ModelResult)
147 /* interpretations.get(0) as VampireModelInterpretation
148 * println(ecore2Logic.IsAttributeValue(modelGenerationProblem.trace, )
149 * Literal(modelGenerationProblem.trace, ecore2Logic.allLiteralsInScope(modelGenerationProblem.trace).get(0) )
150 * )
151 * println((ecore2Logic.allAttributesInScope(modelGenerationProblem.trace)).get(0).EAttributeType)
152 print(interpretations.class)*/
153// for (interpretation : interpretations) { 160// for (interpretation : interpretations) {
154// val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) 161// val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace)
155// workspace.writeModel(model, "model.xmi") 162// workspace.writeModel(model, "model.xmi")
156 /* val representation = im2pi.transform(modelGenerationProblem, model.eAllContents.toList, false)//solution.representation.get(0) // TODO: fix for multiple represenations
157 * if (representation instanceof PartialInterpretation) {
158 * val vis1 = new PartialInterpretation2Gml
159 * val gml = vis1.transform(representation)
160 * workspace.writeText("model.gml", gml)
161
162 * val vis2 = new GraphvizVisualiser
163 * val dot = vis2.visualiseConcretization(representation)
164 * dot.writeToFile(workspace, "model.png")
165 * } else {
166 * println("ERROR")
167 * }
168 look here: hu.bme.mit.inf.dslreasoner.application.execution.GenerationTaskExecutor*/
169// } 163// }
170 /*/
171 *
172 * reasoner = new AlloySolver
173 * val alloyConfig = new AlloySolverConfiguration => [
174 * it.typeScopes.maxNewElements = 7
175 * it.typeScopes.minNewElements = 3
176 * it.solutionScope.numberOfRequiredSolution = 1
177 * it.typeScopes.maxNewIntegers = 0
178 * it.documentationLevel = DocumentationLevel::NORMAL
179 * ]
180 * solution = reasoner.solve(problem, alloyConfig, workspace)
181 //*/
182 // /////////////////////////////////////////////////////
183// var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 164// var totalTimeMin = (System.currentTimeMillis - startTime) / 60000
184// var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 165// var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
185// println("Problem solved") 166// println("Problem solved")
186// println("Time was: " + totalTimeMin + ":" + totalTimeSec) 167// println("Time was: " + totalTimeMin + ":" + totalTimeSec)
187 } 168 }
188 println() 169 println()
189 var avg = 0.0 170 var solverMed = solverTimes.sort.get(REPS/2)
190 if (totFound == 0) { 171 var transformationMed = transformationTimes.sort.get(REPS/2)
191 avg = -1 172 writer.append(solverMed.toString + "," + transformationMed.toString)
192 } else {
193 avg = totalTime / totFound
194 }
195 writer.append(avg.toString)
196 writer.append("\n") 173 writer.append("\n")
197 } 174 }
198 writer.close 175 writer.close
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql
index 60679874..d9d6b881 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql
@@ -9,4 +9,12 @@ pattern terminatorAndInformation(T : FAMTerminator, I : InformationLink) = {
9} or { 9} or {
10 InformationLink.to(I,In); 10 InformationLink.to(I,In);
11 FunctionalInput.terminator(In,T); 11 FunctionalInput.terminator(In,T);
12}
13
14pattern rootElements(Model: FunctionalArchitectureModel, Root : Function) = {
15 FunctionalArchitectureModel.rootElements(Model, Root);
16}
17
18pattern parent(Func : Function, Par : Function) = {
19 Function.parent(Func, Par);
12} \ No newline at end of file 20} \ No newline at end of file