diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca')
-rw-r--r-- | Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend | 51 |
1 files changed, 31 insertions, 20 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 f26a1c91..adea57d4 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 | |||
@@ -59,12 +59,12 @@ class YakinduTest { | |||
59 | // val queries = null | 59 | // val queries = null |
60 | println("DSL loaded") | 60 | println("DSL loaded") |
61 | 61 | ||
62 | var SZ_TOP = 25 | 62 | var SZ_TOP = 120 |
63 | var SZ_BOT = 5 | 63 | var SZ_BOT = 60 |
64 | var INC = 5 | 64 | var INC = 20 |
65 | var REPS = 5 | 65 | var REPS =25 |
66 | 66 | ||
67 | val RUNTIME = 60 | 67 | val RUNTIME = 300 |
68 | 68 | ||
69 | val EXACT = -1 | 69 | val EXACT = -1 |
70 | if (EXACT != -1) { | 70 | if (EXACT != -1) { |
@@ -91,8 +91,7 @@ class YakinduTest { | |||
91 | // BackendSolver::Z3 | 91 | // BackendSolver::Z3 |
92 | // , | 92 | // , |
93 | BackendSolver::LOCVAMP | 93 | BackendSolver::LOCVAMP |
94 | ) | 94 | ) |
95 | |||
96 | 95 | ||
97 | var str = "" | 96 | var str = "" |
98 | 97 | ||
@@ -100,10 +99,6 @@ class YakinduTest { | |||
100 | str += solver.name.substring(0, 1) | 99 | str += solver.name.substring(0, 1) |
101 | } | 100 | } |
102 | 101 | ||
103 | var writer = new PrintWriter( | ||
104 | dataWorkspace.workspaceURI + "//_stats" + formattedDate + "-" + str + SZ_BOT + "to" + SZ_TOP + "by" + INC + | ||
105 | "x" + REPS + ".csv") | ||
106 | writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n") | ||
107 | var solverTimes = newArrayList | 102 | var solverTimes = newArrayList |
108 | var transformationTimes = newArrayList | 103 | var transformationTimes = newArrayList |
109 | var LogicResult solution = null | 104 | var LogicResult solution = null |
@@ -111,6 +106,13 @@ class YakinduTest { | |||
111 | for (BESOLVER : BACKENDSOLVERS) { | 106 | for (BESOLVER : BACKENDSOLVERS) { |
112 | 107 | ||
113 | for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { | 108 | for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { |
109 | // var writer = new PrintWriter( | ||
110 | // dataWorkspace.workspaceURI + "//_stats" + formattedDate + "-" + str + "sz" + i + "x" + REPS + | ||
111 | // ".csv") | ||
112 | var writer = new PrintWriter( | ||
113 | dataWorkspace.workspaceURI + "//_vampire" + i + "x" + REPS + "-" + formattedDate + ".csv") | ||
114 | writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n") | ||
115 | |||
114 | val num = (i - SZ_BOT) / INC | 116 | val num = (i - SZ_BOT) / INC |
115 | println() | 117 | println() |
116 | println("SOLVER: " + BESOLVER.name + ", SIZE=" + i) | 118 | println("SOLVER: " + BESOLVER.name + ", SIZE=" + i) |
@@ -161,17 +163,16 @@ class YakinduTest { | |||
161 | it.documentationLevel = DocumentationLevel::FULL | 163 | it.documentationLevel = DocumentationLevel::FULL |
162 | it.iteration = iter | 164 | it.iteration = iter |
163 | it.runtimeLimit = RUNTIME | 165 | it.runtimeLimit = RUNTIME |
164 | // it.typeScopes.maxNewElements = size | 166 | it.typeScopes.maxNewElements = size |
165 | it.typeScopes.minNewElements = size | 167 | it.typeScopes.minNewElements = size |
166 | 168 | ||
167 | it.genModel = true | 169 | it.genModel = true |
168 | it.server = false | 170 | it.server = false |
169 | if(it.server){ | 171 | if (it.server) { |
170 | it.solver = BESOLVER | 172 | it.solver = BESOLVER |
171 | } else{ | 173 | } else { |
172 | it.solver = BackendSolver::LOCVAMP | 174 | it.solver = BackendSolver::LOCVAMP |
173 | } | 175 | } |
174 | |||
175 | 176 | ||
176 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 177 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
177 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 178 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
@@ -194,12 +195,12 @@ class YakinduTest { | |||
194 | 195 | ||
195 | val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry). | 196 | val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry). |
196 | value | 197 | value |
197 | val satTime = (solution.statistics.entries.filter[name == "satTime"].get(0) as StringStatisticEntry). | 198 | val satTime = (solution.statistics.entries.filter[name == "satTime"]. |
198 | value | 199 | get(0) as StringStatisticEntry).value |
199 | val modOut = (solution.statistics.entries.filter[name == "modOut"].get(0) as StringStatisticEntry). | 200 | val modOut = (solution.statistics.entries.filter[name == "modOut"].get(0) as StringStatisticEntry). |
200 | value | 201 | value |
201 | val modTime = (solution.statistics.entries.filter[name == "modTime"].get(0) as StringStatisticEntry). | 202 | val modTime = (solution.statistics.entries.filter[name == "modTime"]. |
202 | value | 203 | get(0) as StringStatisticEntry).value |
203 | 204 | ||
204 | writer.append(satOut + ",") | 205 | writer.append(satOut + ",") |
205 | writer.append(satTime + ",") | 206 | writer.append(satTime + ",") |
@@ -207,6 +208,15 @@ class YakinduTest { | |||
207 | writer.append(modTime + "") | 208 | writer.append(modTime + "") |
208 | writer.append("\n") | 209 | writer.append("\n") |
209 | 210 | ||
211 | println("->" + modOut + " ... " + modTime) | ||
212 | |||
213 | // Run Garbage Collector | ||
214 | val Runtime r = Runtime.getRuntime(); | ||
215 | r.gc(); | ||
216 | r.gc(); | ||
217 | r.gc(); | ||
218 | Thread.sleep(3000) | ||
219 | |||
210 | // print("(" + tTime + "/" + sTime + "s)..") | 220 | // print("(" + tTime + "/" + sTime + "s)..") |
211 | // solverTimes.add(sTime) | 221 | // solverTimes.add(sTime) |
212 | // transformationTimes.add(tTime) | 222 | // transformationTimes.add(tTime) |
@@ -230,10 +240,11 @@ class YakinduTest { | |||
230 | // var solverMed = solverTimes.sort.get(REPS / 2) | 240 | // var solverMed = solverTimes.sort.get(REPS / 2) |
231 | // var transformationMed = transformationTimes.sort.get(REPS / 2) | 241 | // var transformationMed = transformationTimes.sort.get(REPS / 2) |
232 | // writer.append(solverMed.toString + "," + transformationMed.toString) | 242 | // writer.append(solverMed.toString + "," + transformationMed.toString) |
243 | writer.close | ||
233 | } | 244 | } |
234 | 245 | ||
235 | } | 246 | } |
236 | writer.close | 247 | |
237 | } | 248 | } |
238 | 249 | ||
239 | } | 250 | } |