diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-11 15:51:49 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-11 15:51:49 -0400 |
commit | 17d6aa5028bff14c80f0be6a042c6a68fe8b61b0 (patch) | |
tree | 0c156ad34304a1ac296690fd4c3bf1c438245456 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend | |
parent | implement http requests for the TPTP server (diff) | |
download | VIATRA-Generator-17d6aa5028bff14c80f0be6a042c6a68fe8b61b0.tar.gz VIATRA-Generator-17d6aa5028bff14c80f0be6a042c6a68fe8b61b0.tar.zst VIATRA-Generator-17d6aa5028bff14c80f0be6a042c6a68fe8b61b0.zip |
VAMPIRE: complete testing setup
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.xtend | 214 |
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns | 3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
6 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement | 7 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement |
@@ -11,6 +12,8 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | |||
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry | ||
14 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | 17 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore |
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | 18 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic |
16 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | 19 | import 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 | } |