aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-11 15:51:49 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-11 15:51:49 -0400
commit17d6aa5028bff14c80f0be6a042c6a68fe8b61b0 (patch)
tree0c156ad34304a1ac296690fd4c3bf1c438245456 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src
parentimplement http requests for the TPTP server (diff)
downloadVIATRA-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')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend59
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend214
2 files changed, 132 insertions, 141 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
index 5225fb89..26ed10e3 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend
@@ -26,65 +26,6 @@ import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
26import org.eclipse.viatra.query.runtime.api.IQueryGroup 26import org.eclipse.viatra.query.runtime.api.IQueryGroup
27 27
28class GeneralTest { 28class GeneralTest {
29 val static USER_AGENT = "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36"
30
31 def static void main(String[] args) {
32 val form = makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300)
33
34// val x =sendPost("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\ntester
35//
36//\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n
37//
38//------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___Paradox---4.0\"\r\n\r\nParadox---4.0\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___Paradox---4.0\"\r\n\r\nparadox --no-progress --time %d --tstp --model %s\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--")
39 val x = sendPost(form)
40 print(x.toString)
41 }
42
43 def static makeForm(String formula, String solver, String cmd, int time) {
44 return header + addSpec(formula) + addOptions + addSolver(solver, cmd.replace("%d", time.toString)) + addEnd
45 }
46
47 def static sendPost(String formData ) throws Exception {
48
49 val OkHttpClient client = new OkHttpClient()
50
51 val MediaType mediaType = MediaType.parse(
52 "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA")
53 val RequestBody body = RequestBody.create(mediaType, formData)
54 val Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).
55 addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin",
56 "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type",
57 "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent",
58 "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").
59 addHeader("Accept",
60 "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").
61 addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding",
62 "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token",
63 "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host",
64 "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build()
65
66 val Response response = client.newCall(request).execute()
67// TimeUnit.SECONDS.sleep(5)
68// return newArrayList( response.body.string.split("\n"))
69return response.body.string
70
71 // case 1:
72 }
73 def static getHeader() {
74 return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n"
75 }
76 def static addSpec(String spec) {
77 return spec.replace("\n", "\r\n")
78 }
79 def static addOptions() {
80 return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n"
81 }
82 def static addSolver(String ID, String cmd) {
83 return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + "\"\r\n\r\n" + ID + "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + "\"\r\n\r\n" + cmd + "\r\n"
84 }
85 def static addEnd() {
86 return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"
87 }
88 29
89 def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, 30 def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel,
90 Ecore2Logic e2l, Ecore2Logic_Trace trace) { 31 Ecore2Logic e2l, Ecore2Logic_Trace trace) {
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-30 23:32:05 +0000