aboutsummaryrefslogtreecommitdiffstats
path: root/Tests
diff options
context:
space:
mode:
Diffstat (limited to 'Tests')
-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
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbinbin4552 -> 4545 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbinbin6632 -> 6626 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbinbin6207 -> 6201 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbinbin10182 -> 6625 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbinbin8484 -> 8992 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java68
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java250
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbinbin4997 -> 4997 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbinbin687 -> 687 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbinbin6500 -> 6500 bytes
12 files changed, 278 insertions, 313 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}
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
index 93d27b4d..5dc01040 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
index bc2bae6f..e96cf904 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
index 5687258f..688908b9 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
index de68a908..0d18615c 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
index 16a3cd03..cf52d6a6 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
index ce057092..bdea5746 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java
@@ -13,11 +13,6 @@ import java.util.HashMap;
13import java.util.List; 13import java.util.List;
14import java.util.Map; 14import java.util.Map;
15import java.util.Set; 15import java.util.Set;
16import okhttp3.MediaType;
17import okhttp3.OkHttpClient;
18import okhttp3.Request;
19import okhttp3.RequestBody;
20import okhttp3.Response;
21import org.eclipse.emf.common.util.EList; 16import org.eclipse.emf.common.util.EList;
22import org.eclipse.emf.ecore.EAttribute; 17import org.eclipse.emf.ecore.EAttribute;
23import org.eclipse.emf.ecore.EClass; 18import org.eclipse.emf.ecore.EClass;
@@ -33,75 +28,12 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup;
33import org.eclipse.viatra.query.runtime.api.IQuerySpecification; 28import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
34import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; 29import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation;
35import org.eclipse.xtext.xbase.lib.CollectionLiterals; 30import org.eclipse.xtext.xbase.lib.CollectionLiterals;
36import org.eclipse.xtext.xbase.lib.Exceptions;
37import org.eclipse.xtext.xbase.lib.Functions.Function1; 31import org.eclipse.xtext.xbase.lib.Functions.Function1;
38import org.eclipse.xtext.xbase.lib.InputOutput;
39import org.eclipse.xtext.xbase.lib.IterableExtensions; 32import org.eclipse.xtext.xbase.lib.IterableExtensions;
40import org.eclipse.xtext.xbase.lib.ListExtensions; 33import org.eclipse.xtext.xbase.lib.ListExtensions;
41 34
42@SuppressWarnings("all") 35@SuppressWarnings("all")
43public class GeneralTest { 36public class GeneralTest {
44 private final static String 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";
45
46 public static void main(final String[] args) {
47 try {
48 final String form = GeneralTest.makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300);
49 final String x = GeneralTest.sendPost(form);
50 InputOutput.<String>print(x.toString());
51 } catch (Throwable _e) {
52 throw Exceptions.sneakyThrow(_e);
53 }
54 }
55
56 public static String makeForm(final String formula, final String solver, final String cmd, final int time) {
57 String _header = GeneralTest.getHeader();
58 String _addSpec = GeneralTest.addSpec(formula);
59 String _plus = (_header + _addSpec);
60 String _addOptions = GeneralTest.addOptions();
61 String _plus_1 = (_plus + _addOptions);
62 String _addSolver = GeneralTest.addSolver(solver, cmd.replace("%d", Integer.valueOf(time).toString()));
63 String _plus_2 = (_plus_1 + _addSolver);
64 String _addEnd = GeneralTest.addEnd();
65 return (_plus_2 + _addEnd);
66 }
67
68 public static String sendPost(final String formData) throws Exception {
69 final OkHttpClient client = new OkHttpClient();
70 final MediaType mediaType = MediaType.parse(
71 "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA");
72 final RequestBody body = RequestBody.create(mediaType, formData);
73 final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin",
74 "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type",
75 "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent",
76 "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").addHeader("Accept",
77 "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding",
78 "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token",
79 "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host",
80 "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build();
81 final Response response = client.newCall(request).execute();
82 return response.body().string();
83 }
84
85 public static String getHeader() {
86 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";
87 }
88
89 public static String addSpec(final String spec) {
90 return spec.replace("\n", "\r\n");
91 }
92
93 public static String addOptions() {
94 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";
95 }
96
97 public static String addSolver(final String ID, final String cmd) {
98 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");
99 }
100
101 public static String addEnd() {
102 return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--";
103 }
104
105 public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { 37 public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) {
106 final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>(); 38 final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>();
107 final Function1<EClass, String> _function = (EClass s) -> { 39 final Function1<EClass, String> _function = (EClass s) -> {
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
index 3a8f3fb4..1837b768 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
@@ -2,12 +2,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse;
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; 3import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
4import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns; 4import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; 6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; 7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
7import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement; 8import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement;
8import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region; 9import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region;
9import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition; 10import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition;
10import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; 11import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage;
12import com.google.common.base.Objects;
11import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; 13import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
12import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; 14import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;
13import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; 15import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;
@@ -17,6 +19,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; 19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
18import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; 20import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
19import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; 21import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
22import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry;
23import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry;
24import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry;
20import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; 25import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;
21import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; 26import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;
22import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; 27import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration;
@@ -37,7 +42,9 @@ import org.eclipse.emf.ecore.resource.Resource;
37import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; 42import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
38import org.eclipse.xtend2.lib.StringConcatenation; 43import org.eclipse.xtend2.lib.StringConcatenation;
39import org.eclipse.xtext.xbase.lib.CollectionLiterals; 44import org.eclipse.xtext.xbase.lib.CollectionLiterals;
45import org.eclipse.xtext.xbase.lib.Conversions;
40import org.eclipse.xtext.xbase.lib.Exceptions; 46import org.eclipse.xtext.xbase.lib.Exceptions;
47import org.eclipse.xtext.xbase.lib.Functions.Function1;
41import org.eclipse.xtext.xbase.lib.InputOutput; 48import org.eclipse.xtext.xbase.lib.InputOutput;
42import org.eclipse.xtext.xbase.lib.IterableExtensions; 49import org.eclipse.xtext.xbase.lib.IterableExtensions;
43import org.eclipse.xtext.xbase.lib.ObjectExtensions; 50import org.eclipse.xtext.xbase.lib.ObjectExtensions;
@@ -53,17 +60,20 @@ public class YakinduTest {
53 final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); 60 final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();
54 long _currentTimeMillis = System.currentTimeMillis(); 61 long _currentTimeMillis = System.currentTimeMillis();
55 final Date date = new Date(_currentTimeMillis); 62 final Date date = new Date(_currentTimeMillis);
56 final SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss"); 63 final SimpleDateFormat format = new SimpleDateFormat("dd-HHmm");
57 final String formattedDate = format.format(date); 64 final String formattedDate = format.format(date);
58 StringConcatenation _builder = new StringConcatenation(); 65 StringConcatenation _builder = new StringConcatenation();
59 _builder.append("initialModels/"); 66 _builder.append("initialModels/");
60 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); 67 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");
61 StringConcatenation _builder_1 = new StringConcatenation(); 68 StringConcatenation _builder_1 = new StringConcatenation();
62 _builder_1.append("output/YakinduTest/"); 69 _builder_1.append("output/YakinduTest/");
63 String _plus = (_builder_1.toString() + formattedDate); 70 final FileSystemWorkspace dataWorkspace = new FileSystemWorkspace(_builder_1.toString(), "");
64 StringConcatenation _builder_2 = new StringConcatenation(); 71 StringConcatenation _builder_2 = new StringConcatenation();
65 _builder_2.append("/"); 72 _builder_2.append("output/YakinduTest/");
66 String _plus_1 = (_plus + _builder_2); 73 String _plus = (_builder_2.toString() + formattedDate);
74 StringConcatenation _builder_3 = new StringConcatenation();
75 _builder_3.append("/");
76 String _plus_1 = (_plus + _builder_3);
67 final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, ""); 77 final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, "");
68 workspace.initAndClear(); 78 workspace.initAndClear();
69 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; 79 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;
@@ -75,117 +85,149 @@ public class YakinduTest {
75 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); 85 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi");
76 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); 86 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance());
77 InputOutput.<String>println("DSL loaded"); 87 InputOutput.<String>println("DSL loaded");
78 int SZ_TOP = 10; 88 int SZ_TOP = 30;
79 int SZ_BOT = 126; 89 int SZ_BOT = 5;
80 int INC = 1; 90 int INC = 5;
81 int REPS = 1; 91 int REPS = 1;
82 final int RANGE = 3; 92 final int RUNTIME = 20;
83 final int EXACT = 10; 93 final int EXACT = (-1);
84 if ((EXACT != (-1))) { 94 if ((EXACT != (-1))) {
85 SZ_TOP = EXACT; 95 SZ_TOP = EXACT;
86 SZ_BOT = EXACT; 96 SZ_BOT = EXACT;
87 INC = 1; 97 INC = 1;
88 REPS = 1; 98 REPS = 10;
89 } 99 }
90 URI _workspaceURI = workspace.getWorkspaceURI(); 100 final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList(
91 String _plus_2 = (_workspaceURI + "//_yakinduStats.csv"); 101 BackendSolver.IPROVER);
92 PrintWriter writer = new PrintWriter(_plus_2); 102 String str = "";
93 writer.append("size,"); 103 for (final BackendSolver solver : BACKENDSOLVERS) {
94 for (int x = 0; (x < REPS); x++) { 104 String _str = str;
95 writer.append(((((("tTransf" + Integer.valueOf(x)) + ",") + "tSolv") + Integer.valueOf(x)) + ",")); 105 String _substring = solver.name().substring(0, 1);
106 str = (_str + _substring);
96 } 107 }
97 writer.append("medSolv,medTransf\n"); 108 URI _workspaceURI = dataWorkspace.getWorkspaceURI();
98 ArrayList<Double> solverTimes = CollectionLiterals.<Double>newArrayList(); 109 String _plus_2 = (_workspaceURI + "//_stats");
99 ArrayList<Double> transformationTimes = CollectionLiterals.<Double>newArrayList(); 110 String _plus_3 = (_plus_2 + formattedDate);
100 boolean modelFound = true; 111 String _plus_4 = (_plus_3 + "-");
112 String _plus_5 = (_plus_4 + str);
113 String _plus_6 = (_plus_5 + Integer.valueOf(SZ_BOT));
114 String _plus_7 = (_plus_6 + "to");
115 String _plus_8 = (_plus_7 + Integer.valueOf(SZ_TOP));
116 String _plus_9 = (_plus_8 + "by");
117 String _plus_10 = (_plus_9 + Integer.valueOf(INC));
118 String _plus_11 = (_plus_10 +
119 "x");
120 String _plus_12 = (_plus_11 + Integer.valueOf(REPS));
121 String _plus_13 = (_plus_12 + ".csv");
122 PrintWriter writer = new PrintWriter(_plus_13);
123 writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n");
124 ArrayList<Object> solverTimes = CollectionLiterals.<Object>newArrayList();
125 ArrayList<Object> transformationTimes = CollectionLiterals.<Object>newArrayList();
101 LogicResult solution = null; 126 LogicResult solution = null;
102 { 127 for (final BackendSolver BESOLVER : BACKENDSOLVERS) {
103 int i = SZ_BOT; 128 {
104 boolean _while = (i <= SZ_TOP); 129 int i = SZ_BOT;
105 while (_while) { 130 boolean _while = (i <= SZ_TOP);
106 { 131 while (_while) {
107 final int num = ((i - SZ_BOT) / INC); 132 {
108 InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); 133 final int num = ((i - SZ_BOT) / INC);
109 String _plus_3 = (Integer.valueOf(i) + ","); 134 InputOutput.println();
110 writer.append(_plus_3); 135 String _name = BESOLVER.name();
111 solverTimes.clear(); 136 String _plus_14 = ("SOLVER: " + _name);
112 transformationTimes.clear(); 137 String _plus_15 = (_plus_14 + ", SIZE=");
113 modelFound = true; 138 String _plus_16 = (_plus_15 + Integer.valueOf(i));
114 for (int j = 0; (j < REPS); j++) { 139 InputOutput.<String>println(_plus_16);
115 { 140 InputOutput.println();
116 InputOutput.<Integer>print(Integer.valueOf(j)); 141 solverTimes.clear();
117 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); 142 transformationTimes.clear();
118 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); 143 for (int j = 0; (j < REPS); j++) {
119 TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); 144 {
120 Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); 145 InputOutput.<String>print((("<<Run number " + Integer.valueOf(j)) + ">> :"));
121 TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration); 146 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
122 LogicProblem problem = modelGenerationProblem.getOutput(); 147 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
123 workspace.writeModel(problem, "Yakindu.logicproblem"); 148 TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel);
124 long startTime = System.currentTimeMillis(); 149 Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration();
125 VampireSolver reasoner = null; 150 TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration);
126 VampireSolver _vampireSolver = new VampireSolver(); 151 LogicProblem problem = modelGenerationProblem.getOutput();
127 reasoner = _vampireSolver; 152 long startTime = System.currentTimeMillis();
128 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); 153 VampireSolver reasoner = null;
129 classMapMin.put(Region.class, Integer.valueOf(1)); 154 VampireSolver _vampireSolver = new VampireSolver();
130 classMapMin.put(Transition.class, Integer.valueOf(2)); 155 reasoner = _vampireSolver;
131 classMapMin.put(CompositeElement.class, Integer.valueOf(3)); 156 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
132 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 157 classMapMin.put(Region.class, Integer.valueOf(1));
133 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); 158 classMapMin.put(Transition.class, Integer.valueOf(2));
134 classMapMax.put(Region.class, Integer.valueOf(5)); 159 classMapMin.put(CompositeElement.class, Integer.valueOf(3));
135 classMapMax.put(Transition.class, Integer.valueOf(2)); 160 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic,
136 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 161 modelGenerationProblem.getTrace());
137 final int size = i; 162 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
138 final int inc = INC; 163 classMapMax.put(Region.class, Integer.valueOf(5));
139 final int iter = j; 164 classMapMax.put(Transition.class, Integer.valueOf(2));
140 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); 165 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic,
141 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { 166 modelGenerationProblem.getTrace());
142 it.documentationLevel = DocumentationLevel.FULL; 167 final int size = i;
143 it.iteration = iter; 168 final int inc = INC;
144 it.runtimeLimit = 60; 169 final int iter = j;
145 it.typeScopes.maxNewElements = (-1); 170 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
146 it.typeScopes.minNewElements = size; 171 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
147 it.genModel = false; 172 it.documentationLevel = DocumentationLevel.FULL;
148 int _size = typeMapMin.size(); 173 it.iteration = iter;
149 boolean _notEquals = (_size != 0); 174 it.runtimeLimit = RUNTIME;
150 if (_notEquals) { 175 it.typeScopes.minNewElements = size;
151 it.typeScopes.minNewElementsByType = typeMapMin; 176 it.genModel = true;
152 } 177 it.server = true;
153 int _size_1 = typeMapMin.size(); 178 it.solver = BESOLVER;
154 boolean _notEquals_1 = (_size_1 != 0); 179 it.contCycleLevel = 5;
155 if (_notEquals_1) { 180 it.uniquenessDuplicates = false;
156 it.typeScopes.maxNewElementsByType = typeMapMax; 181 };
157 } 182 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
158 it.contCycleLevel = 5; 183 solution = reasoner.solve(problem, vampireConfig, workspace);
159 it.uniquenessDuplicates = false; 184 String _name_1 = vampireConfig.solver.name();
160 }; 185 String _plus_17 = (_name_1 + ",");
161 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); 186 writer.append(_plus_17);
162 solution = reasoner.solve(problem, vampireConfig, workspace); 187 String _plus_18 = (Integer.valueOf(size) + ",");
163 int _transformationTime = solution.getStatistics().getTransformationTime(); 188 writer.append(_plus_18);
164 final double tTime = (_transformationTime / 1000.0); 189 int _transformationTime = solution.getStatistics().getTransformationTime();
165 int _solverTime = solution.getStatistics().getSolverTime(); 190 double _divide = (_transformationTime / 1000.0);
166 final double sTime = (_solverTime / 1000.0); 191 String _plus_19 = (Double.valueOf(_divide) + ",");
167 String _plus_4 = (Double.valueOf(tTime) + ","); 192 writer.append(_plus_19);
168 String _plus_5 = (_plus_4 + Double.valueOf(sTime)); 193 final Function1<StatisticEntry, Boolean> _function_1 = (StatisticEntry it) -> {
169 String _plus_6 = (_plus_5 + ","); 194 String _name_2 = it.getName();
170 writer.append(_plus_6); 195 return Boolean.valueOf(Objects.equal(_name_2, "satOut"));
171 InputOutput.<String>print((((("(" + Double.valueOf(tTime)) + "/") + Double.valueOf(sTime)) + "s)..")); 196 };
172 solverTimes.add(Double.valueOf(sTime)); 197 StatisticEntry _get = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_1), StatisticEntry.class))[0];
173 transformationTimes.add(Double.valueOf(tTime)); 198 final String satOut = ((StringStatisticEntry) _get).getValue();
199 final Function1<StatisticEntry, Boolean> _function_2 = (StatisticEntry it) -> {
200 String _name_2 = it.getName();
201 return Boolean.valueOf(Objects.equal(_name_2, "satTime"));
202 };
203 StatisticEntry _get_1 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_2), StatisticEntry.class))[0];
204 final double satTime = ((RealStatisticEntry) _get_1).getValue();
205 final Function1<StatisticEntry, Boolean> _function_3 = (StatisticEntry it) -> {
206 String _name_2 = it.getName();
207 return Boolean.valueOf(Objects.equal(_name_2, "modOut"));
208 };
209 StatisticEntry _get_2 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_3), StatisticEntry.class))[0];
210 final String modOut = ((StringStatisticEntry) _get_2).getValue();
211 final Function1<StatisticEntry, Boolean> _function_4 = (StatisticEntry it) -> {
212 String _name_2 = it.getName();
213 return Boolean.valueOf(Objects.equal(_name_2, "modTime"));
214 };
215 StatisticEntry _get_3 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_4), StatisticEntry.class))[0];
216 final double modTime = ((RealStatisticEntry) _get_3).getValue();
217 writer.append((satOut + ","));
218 String _plus_20 = (Double.valueOf(satTime) + ",");
219 writer.append(_plus_20);
220 writer.append((modOut + ","));
221 String _plus_21 = (Double.valueOf(modTime) + ",");
222 writer.append(_plus_21);
223 writer.append("\n");
224 }
174 } 225 }
175 } 226 }
176 InputOutput.println(); 227 int _i = i;
177 Double solverMed = IterableExtensions.<Double>sort(solverTimes).get((REPS / 2)); 228 i = (_i + INC);
178 Double transformationMed = IterableExtensions.<Double>sort(transformationTimes).get((REPS / 2)); 229 _while = (i <= SZ_TOP);
179 String _string = solverMed.toString();
180 String _plus_4 = (_string + ",");
181 String _string_1 = transformationMed.toString();
182 String _plus_5 = (_plus_4 + _string_1);
183 writer.append(_plus_5);
184 writer.append("\n");
185 } 230 }
186 int _i = i;
187 i = (_i + INC);
188 _while = (i <= SZ_TOP);
189 } 231 }
190 } 232 }
191 writer.close(); 233 writer.close();
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
index 96f343fa..b596dc1f 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
index 1ca8223d..e1434d74 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
Binary files differ
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
index 5d6a9ee2..50068d97 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
Binary files differ
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-26 14:27:18 +0000