diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-10 22:25:07 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:14 -0400 |
commit | b97501f5f1cdce51ead750e806dc16013f59ec38 (patch) | |
tree | 4e8f60623112320eaece09b7854063d02ff93259 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src | |
parent | VAMPIRE: Further develop testing fo r Vampire solver (diff) | |
download | VIATRA-Generator-b97501f5f1cdce51ead750e806dc16013f59ec38.tar.gz VIATRA-Generator-b97501f5f1cdce51ead750e806dc16013f59ec38.tar.zst VIATRA-Generator-b97501f5f1cdce51ead750e806dc16013f59ec38.zip |
implement http requests for the TPTP server
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src')
3 files changed, 104 insertions, 35 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend index 2495ab77..5289371f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend | |||
@@ -86,7 +86,7 @@ class FileSystemTest { | |||
86 | it.uniquenessDuplicates = false | 86 | it.uniquenessDuplicates = false |
87 | ] | 87 | ] |
88 | 88 | ||
89 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS") | 89 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) |
90 | 90 | ||
91 | /*/ | 91 | /*/ |
92 | * | 92 | * |
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 89375801..5225fb89 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 | |||
@@ -9,6 +9,11 @@ import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | |||
9 | import java.util.HashMap | 9 | import java.util.HashMap |
10 | import java.util.List | 10 | import java.util.List |
11 | import java.util.Map | 11 | import java.util.Map |
12 | import okhttp3.MediaType | ||
13 | import okhttp3.OkHttpClient | ||
14 | import okhttp3.Request | ||
15 | import okhttp3.RequestBody | ||
16 | import okhttp3.Response | ||
12 | import org.eclipse.emf.ecore.EAttribute | 17 | import org.eclipse.emf.ecore.EAttribute |
13 | import org.eclipse.emf.ecore.EClass | 18 | import org.eclipse.emf.ecore.EClass |
14 | import org.eclipse.emf.ecore.EEnum | 19 | import org.eclipse.emf.ecore.EEnum |
@@ -20,15 +25,77 @@ import org.eclipse.emf.ecore.resource.Resource | |||
20 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 25 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
21 | import org.eclipse.viatra.query.runtime.api.IQueryGroup | 26 | import org.eclipse.viatra.query.runtime.api.IQueryGroup |
22 | 27 | ||
23 | class GeneralTest { | 28 | class GeneralTest { |
24 | def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) { | 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")) | ||
69 | return 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 | |||
89 | def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, | ||
90 | Ecore2Logic e2l, Ecore2Logic_Trace trace) { | ||
25 | val typeMap = new HashMap<Type, Integer> | 91 | val typeMap = new HashMap<Type, Integer> |
26 | val listMap = metamodel.classes.toMap[s|s.name] | 92 | val listMap = metamodel.classes.toMap[s|s.name] |
27 | 93 | ||
28 | for (Class elem : classMap.keySet) { | 94 | for (Class elem : classMap.keySet) { |
29 | typeMap.put(e2l.TypeofEClass( | 95 | typeMap.put(e2l.TypeofEClass( |
30 | trace, listMap.get(elem.simpleName) | 96 | trace, |
31 | ), classMap.get(elem)) | 97 | listMap.get(elem.simpleName) |
98 | ), classMap.get(elem)) | ||
32 | } | 99 | } |
33 | return typeMap | 100 | return typeMap |
34 | } | 101 | } |
@@ -43,7 +110,7 @@ class GeneralTest { | |||
43 | } | 110 | } |
44 | 111 | ||
45 | def static loadPartialModel(ReasonerWorkspace inputs, String path) { | 112 | def static loadPartialModel(ReasonerWorkspace inputs, String path) { |
46 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); | 113 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()) |
47 | inputs.readModel(EObject, path).eResource.contents | 114 | inputs.readModel(EObject, path).eResource.contents |
48 | // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList | 115 | // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList |
49 | } | 116 | } |
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 28e3e685..c35b200e 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 | |||
@@ -3,13 +3,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse | |||
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.VampireSolver | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 5 | 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.Region | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage | 9 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
13 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | 14 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore |
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | 15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic |
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | 16 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration |
@@ -17,8 +18,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.Insta | |||
17 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 18 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
18 | import java.io.PrintWriter | 19 | import java.io.PrintWriter |
19 | import java.text.SimpleDateFormat | 20 | import java.text.SimpleDateFormat |
20 | import java.time.LocalDate | ||
21 | import java.util.Date | 21 | import java.util.Date |
22 | import java.util.HashMap | ||
22 | import org.eclipse.emf.ecore.resource.Resource | 23 | import org.eclipse.emf.ecore.resource.Resource |
23 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 24 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
24 | 25 | ||
@@ -54,16 +55,18 @@ class YakinduTest { | |||
54 | // val queries = null | 55 | // val queries = null |
55 | println("DSL loaded") | 56 | println("DSL loaded") |
56 | 57 | ||
57 | var MAX = 80 | 58 | var SZ_TOP = 10 |
58 | var START = 79 | 59 | var SZ_BOT = 126 |
59 | var INC = 1 | 60 | var INC = 1 |
60 | var REPS = 3 | 61 | var REPS = 1 |
62 | |||
63 | val RANGE = 3 | ||
61 | 64 | ||
62 | val EXACT = 130 | 65 | val EXACT = 10 |
63 | if (EXACT != -1) { | 66 | if (EXACT != -1) { |
64 | MAX = EXACT | 67 | SZ_TOP = EXACT |
65 | START = EXACT | 68 | SZ_BOT = EXACT |
66 | INC = 5 | 69 | INC = 1 |
67 | REPS = 1 | 70 | REPS = 1 |
68 | } | 71 | } |
69 | 72 | ||
@@ -77,8 +80,8 @@ class YakinduTest { | |||
77 | var transformationTimes = newArrayList | 80 | var transformationTimes = newArrayList |
78 | var modelFound = true | 81 | var modelFound = true |
79 | var LogicResult solution = null | 82 | var LogicResult solution = null |
80 | for (var i = START; i <= MAX; i += INC) { | 83 | for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { |
81 | val num = (i - START) / INC | 84 | val num = (i - SZ_BOT) / INC |
82 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") | 85 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") |
83 | writer.append(i + ",") | 86 | writer.append(i + ",") |
84 | solverTimes.clear | 87 | solverTimes.clear |
@@ -106,17 +109,16 @@ class YakinduTest { | |||
106 | 109 | ||
107 | // ///////////////////////////////////////////////////// | 110 | // ///////////////////////////////////////////////////// |
108 | // Minimum Scope | 111 | // Minimum Scope |
109 | // val classMapMin = new HashMap<Class, Integer> | 112 | val classMapMin = new HashMap<Class, Integer> |
110 | // classMapMin.put(Region, 1) | 113 | classMapMin.put(Region, 1) |
111 | // classMapMin.put(Transition, 2) | 114 | classMapMin.put(Transition, 2) |
112 | // classMapMin.put(CompositeElement, 3) | 115 | classMapMin.put(CompositeElement, 3) |
113 | // val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) | 116 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) |
114 | // Maximum Scope | 117 | // Maximum Scope |
115 | // val classMapMax = new HashMap<Class, Integer> | 118 | val classMapMax = new HashMap<Class, Integer> |
116 | // classMapMax.put(Region, 5) | 119 | classMapMax.put(Region, 5) |
117 | // classMapMax.put(Transition, 2) | 120 | classMapMax.put(Transition, 2) |
118 | // classMapMax.put(Synchronization, 4) | 121 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) |
119 | // val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | ||
120 | // Define Config File | 122 | // Define Config File |
121 | val size = i | 123 | val size = i |
122 | val inc = INC | 124 | val inc = INC |
@@ -126,18 +128,18 @@ class YakinduTest { | |||
126 | it.documentationLevel = DocumentationLevel::FULL | 128 | it.documentationLevel = DocumentationLevel::FULL |
127 | it.iteration = iter | 129 | it.iteration = iter |
128 | it.runtimeLimit = 60 | 130 | it.runtimeLimit = 60 |
129 | it.typeScopes.maxNewElements = size | 131 | it.typeScopes.maxNewElements = -1 |
130 | it.typeScopes.minNewElements = size - 5 | 132 | it.typeScopes.minNewElements = size |
131 | 133 | it.genModel = false | |
132 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 134 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
133 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 135 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
134 | it.contCycleLevel = 5 | 136 | it.contCycleLevel = 5 |
135 | it.uniquenessDuplicates = false | 137 | it.uniquenessDuplicates = false |
136 | ] | 138 | ] |
137 | 139 | ||
138 | solution = reasoner.solve(problem, vampireConfig, workspace) | 140 | solution = reasoner.solve(problem, vampireConfig, workspace) |
139 | // print((solution as ModelResult).representation.get(0)) | 141 | // print((solution as ModelResult).representation.get(0)) |
140 | val soln = ((solution as ModelResult).representation.get(0) as VampireModel) | 142 | // val soln = ((solution as ModelResult).representation.get(0) as VampireModel) |
141 | // println(soln.confirmations) | 143 | // println(soln.confirmations) |
142 | // println((solution as ModelResult).representation) | 144 | // println((solution as ModelResult).representation) |
143 | // modelFound = !soln.confirmations.filter [ | 145 | // modelFound = !soln.confirmations.filter [ |