aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
diff options
context:
space:
mode:
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend214
1 files changed, 132 insertions, 82 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 c35b200e..9121367b 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,6 +1,7 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse 1package ca.mcgill.ecse.dslreasoner.vampire.icse
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns 3import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver 5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration 6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
6import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement 7import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement
@@ -11,6 +12,8 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
11import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration 12import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel 13import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
13import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult 14import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
15import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry
16import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry
14import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore 17import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
15import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic 18import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
16import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration 19import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
@@ -32,10 +35,11 @@ class YakinduTest {
32 35
33 // Workspace setup 36 // Workspace setup
34 val Date date = new Date(System.currentTimeMillis) 37 val Date date = new Date(System.currentTimeMillis)
35 val SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss"); 38 val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm");
36 val formattedDate = format.format(date) 39 val formattedDate = format.format(date)
37 40
38 val inputs = new FileSystemWorkspace('''initialModels/''', "") 41 val inputs = new FileSystemWorkspace('''initialModels/''', "")
42 val dataWorkspace = new FileSystemWorkspace('''output/YakinduTest/''', "")
39 val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "") 43 val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "")
40 workspace.initAndClear 44 workspace.initAndClear
41 45
@@ -55,89 +59,120 @@ class YakinduTest {
55// val queries = null 59// val queries = null
56 println("DSL loaded") 60 println("DSL loaded")
57 61
58 var SZ_TOP = 10 62 var SZ_TOP = 30
59 var SZ_BOT = 126 63 var SZ_BOT = 5
60 var INC = 1 64 var INC = 5
61 var REPS = 1 65 var REPS = 1
62
63 val RANGE = 3
64 66
65 val EXACT = 10 67 val RUNTIME = 20
68
69 val EXACT = -1
66 if (EXACT != -1) { 70 if (EXACT != -1) {
67 SZ_TOP = EXACT 71 SZ_TOP = EXACT
68 SZ_BOT = EXACT 72 SZ_BOT = EXACT
69 INC = 1 73 INC = 1
70 REPS = 1 74 REPS = 10
71 } 75 }
76 val BACKENDSOLVERS = newArrayList(
77// BackendSolver::CVC4
78// ,
79// BackendSolver::DARWINFM
80// ,
81// BackendSolver::EDARWIN
82// ,
83// BackendSolver::GEOIII
84// ,
85 BackendSolver::IPROVER
86// ,
87// BackendSolver::PARADOX
88// ,
89// BackendSolver::VAMPIRE
90// ,
91// BackendSolver::Z3
92 )
93
72 94
73 var writer = new PrintWriter(workspace.workspaceURI + "//_yakinduStats.csv") 95 var str = ""
74 writer.append("size,") 96
75 for (var x = 0; x < REPS; x++) { 97 for (solver : BACKENDSOLVERS) {
76 writer.append("tTransf" + x + "," + "tSolv" + x + ",") 98 str += solver.name.substring(0, 1)
77 } 99 }
78 writer.append("medSolv,medTransf\n") 100
101 var writer = new PrintWriter(
102 dataWorkspace.workspaceURI + "//_stats" + formattedDate + "-" + str + SZ_BOT + "to" + SZ_TOP + "by" + INC +
103 "x" + REPS + ".csv")
104 writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n")
79 var solverTimes = newArrayList 105 var solverTimes = newArrayList
80 var transformationTimes = newArrayList 106 var transformationTimes = newArrayList
81 var modelFound = true
82 var LogicResult solution = null 107 var LogicResult solution = null
83 for (var i = SZ_BOT; i <= SZ_TOP; i += INC) {
84 val num = (i - SZ_BOT) / INC
85 print("Generation " + num + ": SIZE=" + i + " Attempt: ")
86 writer.append(i + ",")
87 solverTimes.clear
88 transformationTimes.clear
89 modelFound = true
90 for (var j = 0; j < REPS; j++) {
91 108
92 print(j) 109 for (BESOLVER : BACKENDSOLVERS) {
93 110
94 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) 111 for (var i = SZ_BOT; i <= SZ_TOP; i += INC) {
95 var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel) 112 val num = (i - SZ_BOT) / INC
96 var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, 113 println()
97 new Viatra2LogicConfiguration) 114 println("SOLVER: " + BESOLVER.name + ", SIZE=" + i)
115 println()
98 116
99 var problem = modelGenerationProblem.output 117 solverTimes.clear
100 workspace.writeModel(problem, "Yakindu.logicproblem") 118 transformationTimes.clear
119 for (var j = 0; j < REPS; j++) {
101 120
121 print("<<Run number " + j + ">> :")
122
123 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,
124 new Ecore2LogicConfiguration())
125 var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel)
126 var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem,
127 new Viatra2LogicConfiguration)
128
129 var problem = modelGenerationProblem.output
130// workspace.writeModel(problem, "Yakindu.logicproblem")
102// println("Problem created") 131// println("Problem created")
103// Start Time 132// Start Time
104 var startTime = System.currentTimeMillis 133 var startTime = System.currentTimeMillis
105 134
106 var VampireSolver reasoner 135 var VampireSolver reasoner
107 // * 136 // *
108 reasoner = new VampireSolver 137 reasoner = new VampireSolver
109 138
110 // ///////////////////////////////////////////////////// 139 // /////////////////////////////////////////////////////
111 // Minimum Scope 140 // Minimum Scope
112 val classMapMin = new HashMap<Class, Integer> 141 val classMapMin = new HashMap<Class, Integer>
113 classMapMin.put(Region, 1) 142 classMapMin.put(Region, 1)
114 classMapMin.put(Transition, 2) 143 classMapMin.put(Transition, 2)
115 classMapMin.put(CompositeElement, 3) 144 classMapMin.put(CompositeElement, 3)
116 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) 145 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic,
117 // Maximum Scope 146 modelGenerationProblem.trace)
118 val classMapMax = new HashMap<Class, Integer> 147 // Maximum Scope
119 classMapMax.put(Region, 5) 148 val classMapMax = new HashMap<Class, Integer>
120 classMapMax.put(Transition, 2) 149 classMapMax.put(Region, 5)
121 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) 150 classMapMax.put(Transition, 2)
122 // Define Config File 151 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic,
123 val size = i 152 modelGenerationProblem.trace)
124 val inc = INC 153 // Define Config File
125 val iter = j 154 val size = i
126 val vampireConfig = new VampireSolverConfiguration => [ 155 val inc = INC
127 // add configuration things, in config file first 156 val iter = j
128 it.documentationLevel = DocumentationLevel::FULL 157 val vampireConfig = new VampireSolverConfiguration => [
129 it.iteration = iter 158 // add configuration things, in config file first
130 it.runtimeLimit = 60 159 it.documentationLevel = DocumentationLevel::FULL
131 it.typeScopes.maxNewElements = -1 160 it.iteration = iter
132 it.typeScopes.minNewElements = size 161 it.runtimeLimit = RUNTIME
133 it.genModel = false 162// it.typeScopes.maxNewElements = size
134 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin 163 it.typeScopes.minNewElements = size
135 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax 164
136 it.contCycleLevel = 5 165 it.genModel = true
137 it.uniquenessDuplicates = false 166 it.server = true
138 ] 167 it.solver = BESOLVER
139 168
140 solution = reasoner.solve(problem, vampireConfig, workspace) 169// if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
170// if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
171 it.contCycleLevel = 5
172 it.uniquenessDuplicates = false
173 ]
174
175 solution = reasoner.solve(problem, vampireConfig, workspace)
141// print((solution as ModelResult).representation.get(0)) 176// print((solution as ModelResult).representation.get(0))
142// val soln = ((solution as ModelResult).representation.get(0) as VampireModel) 177// val soln = ((solution as ModelResult).representation.get(0) as VampireModel)
143// println(soln.confirmations) 178// println(soln.confirmations)
@@ -145,20 +180,35 @@ class YakinduTest {
145// modelFound = !soln.confirmations.filter [ 180// modelFound = !soln.confirmations.filter [
146// class == VLSFiniteModelImpl 181// class == VLSFiniteModelImpl
147// ].isEmpty 182// ].isEmpty
148// 183// ADD TO CSV
149// if (modelFound) { 184 writer.append(vampireConfig.solver.name + ",")
150 val tTime = solution.statistics.transformationTime / 1000.0 185 writer.append(size + ",")
151 val sTime = solution.statistics.solverTime / 1000.0 186 writer.append(solution.statistics.transformationTime / 1000.0 + ",")
152 writer.append(tTime + "," + sTime + ",") 187
153 print("(" + tTime + "/" + sTime + "s)..") 188 val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry).
154 solverTimes.add(sTime) 189 value
155 transformationTimes.add(tTime) 190 val satTime = (solution.statistics.entries.filter[name == "satTime"].get(0) as RealStatisticEntry).
191 value
192 val modOut = (solution.statistics.entries.filter[name == "modOut"].get(0) as StringStatisticEntry).
193 value
194 val modTime = (solution.statistics.entries.filter[name == "modTime"].get(0) as RealStatisticEntry).
195 value
196
197 writer.append(satOut + ",")
198 writer.append(satTime + ",")
199 writer.append(modOut + ",")
200 writer.append(modTime + ",")
201 writer.append("\n")
202
203// print("(" + tTime + "/" + sTime + "s)..")
204// solverTimes.add(sTime)
205// transformationTimes.add(tTime)
156// } else { 206// } else {
157// writer.append("MNF" + ",") 207// writer.append("MNF" + ",")
158//// print("MNF") 208//// print("MNF")
159// } 209// }
160 // println("Problem solved") 210 // println("Problem solved")
161 // visualisation, see 211 // visualisation, see
162// var interpretations = reasoner.getInterpretations(solution as ModelResult) 212// var interpretations = reasoner.getInterpretations(solution as ModelResult)
163// for (interpretation : interpretations) { 213// for (interpretation : interpretations) {
164// val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) 214// val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace)
@@ -168,15 +218,15 @@ class YakinduTest {
168// var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 218// var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60
169// println("Problem solved") 219// println("Problem solved")
170// println("Time was: " + totalTimeMin + ":" + totalTimeSec) 220// println("Time was: " + totalTimeMin + ":" + totalTimeSec)
221 }
222// println()
223// var solverMed = solverTimes.sort.get(REPS / 2)
224// var transformationMed = transformationTimes.sort.get(REPS / 2)
225// writer.append(solverMed.toString + "," + transformationMed.toString)
171 } 226 }
172 println() 227
173 var solverMed = solverTimes.sort.get(REPS / 2)
174 var transformationMed = transformationTimes.sort.get(REPS / 2)
175 writer.append(solverMed.toString + "," + transformationMed.toString)
176 writer.append("\n")
177 } 228 }
178 writer.close 229 writer.close
179
180 } 230 }
181 231
182} 232}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-17 16:16:14 +0000