diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src')
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.FamPatterns | 3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
6 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel |
7 | import functionalarchitecture.FunctionalarchitecturePackage | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
@@ -12,9 +12,13 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | |||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
13 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | 13 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore |
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | 14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic |
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic |
16 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 17 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
17 | import java.io.PrintWriter | 18 | import java.io.PrintWriter |
19 | import java.text.SimpleDateFormat | ||
20 | import java.time.LocalDate | ||
21 | import java.util.Date | ||
18 | import org.eclipse.emf.ecore.resource.Resource | 22 | import org.eclipse.emf.ecore.resource.Resource |
19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 23 | import 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 | |||
14 | pattern rootElements(Model: FunctionalArchitectureModel, Root : Function) = { | ||
15 | FunctionalArchitectureModel.rootElements(Model, Root); | ||
16 | } | ||
17 | |||
18 | pattern parent(Func : Function, Par : Function) = { | ||
19 | Function.parent(Func, Par); | ||
12 | } \ No newline at end of file | 20 | } \ No newline at end of file |