aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-07 00:35:42 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-07 00:35:42 -0400
commit5d1165ceef23e20c4bbe46fe6f88e95f317234b5 (patch)
tree9ed155a9e8d74b0f1ce7173aacd50e0e01c96f22 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse
parentVAMPIRE: fix model generation (diff)
downloadVIATRA-Generator-5d1165ceef23e20c4bbe46fe6f88e95f317234b5.tar.gz
VIATRA-Generator-5d1165ceef23e20c4bbe46fe6f88e95f317234b5.tar.zst
VIATRA-Generator-5d1165ceef23e20c4bbe46fe6f88e95f317234b5.zip
VAMPIRE: Implement Vampire measurement code
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend2
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend15
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend236
3 files changed, 173 insertions, 80 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend
index 70ded02d..35b76350 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend
@@ -50,7 +50,7 @@ class EcoreTest {
50 it.documentationLevel = DocumentationLevel::FULL 50 it.documentationLevel = DocumentationLevel::FULL
51 ] 51 ]
52 52
53 solution = reasoner.solve(logicProblem, vampireConfig, workspace, "ECO") 53 solution = reasoner.solve(logicProblem, vampireConfig, workspace)
54 54
55 println("Problem solved") 55 println("Problem solved")
56 56
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
index 5143641b..a7da818c 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
@@ -2,12 +2,13 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver 3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration 4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
5import functionalarchitecture.FAMTerminator
5import functionalarchitecture.Function 6import functionalarchitecture.Function
6import functionalarchitecture.FunctionalArchitectureModel 7import functionalarchitecture.FunctionalArchitectureModel
7import functionalarchitecture.FunctionalInterface 8import functionalarchitecture.FunctionalInterface
8import functionalarchitecture.FunctionalOutput 9import functionalarchitecture.FunctionalOutput
9import functionalarchitecture.FunctionalarchitecturePackage 10import functionalarchitecture.FunctionalarchitecturePackage
10import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns 11//import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns
11import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic 12import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
12import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration 13import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
13import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel 14import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
@@ -22,7 +23,6 @@ import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
22import java.util.HashMap 23import java.util.HashMap
23import org.eclipse.emf.ecore.resource.Resource 24import org.eclipse.emf.ecore.resource.Resource
24import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 25import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
25import functionalarchitecture.FAMTerminator
26 26
27class FAMTest { 27class FAMTest {
28 def static void main(String[] args) { 28 def static void main(String[] args) {
@@ -47,15 +47,15 @@ class FAMTest {
47 // Load DSL 47 // Load DSL
48 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) 48 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)
49 val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") 49 val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi")
50 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) 50// val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)
51// val queries = null 51 val queries = null
52 52
53 println("DSL loaded") 53 println("DSL loaded")
54 54
55 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) 55 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
56 var problem = modelGenerationProblem.output 56 var problem = modelGenerationProblem.output
57 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output 57 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
58 problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output 58// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
59 workspace.writeModel(problem, "Fam.logicproblem") 59 workspace.writeModel(problem, "Fam.logicproblem")
60 60
61 println("Problem created") 61 println("Problem created")
@@ -94,14 +94,15 @@ class FAMTest {
94 94
95 it.typeScopes.minNewElements = 8//24 95 it.typeScopes.minNewElements = 8//24
96 it.typeScopes.maxNewElements = 10//25 96 it.typeScopes.maxNewElements = 10//25
97 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin 97// if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
98// if(typeMapMax.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax 98// if(typeMapMax.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
99 it.contCycleLevel = 5 99 it.contCycleLevel = 5
100 it.uniquenessDuplicates = false 100 it.uniquenessDuplicates = false
101 ] 101 ]
102 102
103 var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) 103 var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace)
104 104
105 println("Problem solved")
105 // visualisation, see 106 // visualisation, see
106 var interpretations = reasoner.getInterpretations(solution as ModelResult) 107 var interpretations = reasoner.getInterpretations(solution as ModelResult)
107// interpretations.get(0) as VampireModelInterpretation 108// interpretations.get(0) as VampireModelInterpretation
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 fb1bdb59..057bcf12 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,25 +1,27 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage 3import ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.FamPatterns
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.vampireLanguage.VampireModel
7import functionalarchitecture.FunctionalarchitecturePackage
6import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic 8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration 9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
8import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel 10import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
9import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult 11import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
12import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
13import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
11import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic 14import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic 15import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
13import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 16import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
14import java.util.HashMap 17import java.io.PrintWriter
15import org.eclipse.emf.ecore.resource.Resource 18import org.eclipse.emf.ecore.resource.Resource
16import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 19import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
17 20
18import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.*
19
20class YakinduTest { 21class YakinduTest {
21 def static void main(String[] args) { 22 def static void main(String[] args) {
22 val Ecore2Logic ecore2Logic = new Ecore2Logic 23 val Ecore2Logic ecore2Logic = new Ecore2Logic
24 val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic)
23 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) 25 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
24 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic 26 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
25 27
@@ -35,76 +37,166 @@ class YakinduTest {
35 37
36 println("Input and output workspaces are created") 38 println("Input and output workspaces are created")
37 39
38 val metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE) 40// val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE)
39 val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi") 41 val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)
40// val queries = GeneralTest.loadQueries(metamodel, yakinduPatterns.instance) 42// val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi")
41 val queries = null 43 val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi")
42 44// val queries = GeneralTest.loadQueries(metamodel, YakinduPatterns.instance)
45 val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)
46// val queries = null
43 println("DSL loaded") 47 println("DSL loaded")
44 48
45 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) 49 var MAX = 150
46 var problem = modelGenerationProblem.output 50 var START = 10
47 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output 51 var INC = 20
52 var REPS = 1
53
54 val EXACT = -1
55 if (EXACT!= -1) {
56 MAX = EXACT
57 START = EXACT
58 INC = 1
59 REPS = 5
60 }
61
62 var writer = new PrintWriter(workspace.workspaceURI + "//yakinduStats.csv")
63 writer.append("size,")
64 for (var x = 0; x < REPS; x++) {
65 writer.append("t" + x + ",")
66 }
67 writer.append("avg\n")
68 var totalTime = 0.0
69 var totFound = 0.0
70 var modelFound = true
71 var LogicResult solution = null
72 for (var i = START; i <= MAX; i += INC) {
73 val num = (i - START) / INC
74 print("Generation " + num + ": SIZE=" + i + " Attempt: ")
75 writer.append(i + ",")
76 totalTime = 0.0
77 totFound = 0.0
78 modelFound = true
79 for (var j = 0; j < REPS; j++) {
80
81 print(j)
82
83 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
84 var problem = modelGenerationProblem.output
85 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
48// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output 86// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
49 workspace.writeModel(problem, "Yakindu.logicproblem") 87 workspace.writeModel(problem, "Yakindu.logicproblem")
50 88
51 println("Problem created") 89// println("Problem created")
52 90// Start Time
53 // Start Time 91 var startTime = System.currentTimeMillis
54 var startTime = System.currentTimeMillis 92
55 93 var VampireSolver reasoner
56 var VampireSolver reasoner 94 // *
57 // * 95 reasoner = new VampireSolver
58 reasoner = new VampireSolver 96
59 97 // /////////////////////////////////////////////////////
60 // ///////////////////////////////////////////////////// 98 // Minimum Scope
61 // Minimum Scope 99// val classMapMin = new HashMap<Class, Integer>
62 val classMapMin = new HashMap<Class, Integer> 100// classMapMin.put(Region, 1)
63 classMapMin.put(Region, 1) 101// classMapMin.put(Transition, 2)
64 classMapMin.put(Transition, 2) 102// classMapMin.put(CompositeElement, 3)
65 classMapMin.put(CompositeElement, 3) 103// val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
66 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) 104 // Maximum Scope
67 105// val classMapMax = new HashMap<Class, Integer>
68 // Maximum Scope 106// classMapMax.put(Region, 5)
69 val classMapMax = new HashMap<Class, Integer> 107// classMapMax.put(Transition, 2)
70 classMapMax.put(Region, 5) 108// classMapMax.put(Synchronization, 4)
71 classMapMax.put(Transition, 2) 109// val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
72 classMapMax.put(Synchronization, 4) 110 // Define Config File
73 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) 111 val size = i
74 112 val inc = INC
75 // Define Config File 113 val vampireConfig = new VampireSolverConfiguration => [
76 val vampireConfig = new VampireSolverConfiguration => [ 114 // add configuration things, in config file first
77 // add configuration things, in config file first 115 it.documentationLevel = DocumentationLevel::FULL
78 it.documentationLevel = DocumentationLevel::FULL 116
79 117 it.typeScopes.minNewElements = size - inc
80 it.typeScopes.minNewElements = 20 118 it.typeScopes.maxNewElements = size
81 it.typeScopes.maxNewElements = 30 119// if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
82 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin 120// if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
83 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax 121 it.contCycleLevel = 5
84 it.contCycleLevel = 5 122 it.uniquenessDuplicates = false
85 it.uniquenessDuplicates = false 123 ]
86 ] 124
87 125 solution = reasoner.solve(problem, vampireConfig, workspace)
88 var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "YAK") 126// print((solution as ModelResult).representation.get(0))
89 127 val soln = ((solution as ModelResult).representation.get(0) as VampireModel)
90 /*/ 128// println(soln.confirmations)
91 * 129// println((solution as ModelResult).representation)
92 * reasoner = new AlloySolver 130// modelFound = !soln.confirmations.filter [
93 * val alloyConfig = new AlloySolverConfiguration => [ 131// class == VLSFiniteModelImpl
94 * it.typeScopes.maxNewElements = 7 132// ].isEmpty
95 * it.typeScopes.minNewElements = 3 133//
96 * it.solutionScope.numberOfRequiredSolution = 1 134// if (modelFound) {
97 * it.typeScopes.maxNewIntegers = 0 135 val time = solution.statistics.transformationTime / 1000.0
98 * it.documentationLevel = DocumentationLevel::NORMAL 136 writer.append(time + ",")
99 * ] 137 print("(" + time + ")..")
100 * solution = reasoner.solve(problem, alloyConfig, workspace) 138 totalTime += time
101 //*/ 139 totFound += 1
102 // ///////////////////////////////////////////////////// 140// } else {
103 var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 141// writer.append("MNF" + ",")
104 var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 142//// print("MNF")
105 143// }
106 println("Problem solved") 144 // println("Problem solved")
107 println("Time was: " + totalTimeMin + ":" + totalTimeSec) 145 // visualisation, see
146// 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) {
154// val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace)
155// 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// }
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
184// var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
185// println("Problem solved")
186// println("Time was: " + totalTimeMin + ":" + totalTimeSec)
187 }
188 println()
189 var avg = 0.0
190 if (totFound == 0) {
191 avg = -1
192 } else {
193 avg = totalTime / totFound
194 }
195 writer.append(avg.toString)
196 writer.append("\n")
197 }
198 writer.close
199
108 } 200 }
109 201
110} 202}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-26 14:19:50 +0000