diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-11 15:51:49 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:17 -0400 |
commit | 606f6965f3ccec837aa216cbb3f56fdcf943a59b (patch) | |
tree | e9d1283f60b335de331b5e8abd93f040636f871b /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend | |
parent | implement http requests for the TPTP server (diff) | |
download | VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.tar.gz VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.tar.zst VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.zip |
VAMPIRE: complete testing setup
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend')
-rw-r--r-- | Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend | 59 |
1 files changed, 0 insertions, 59 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 | |||
26 | import org.eclipse.viatra.query.runtime.api.IQueryGroup | 26 | import org.eclipse.viatra.query.runtime.api.IQueryGroup |
27 | 27 | ||
28 | class GeneralTest { | 28 | class 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")) | ||
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 | 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) { |