From b97501f5f1cdce51ead750e806dc16013f59ec38 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 10 Oct 2019 22:25:07 -0400 Subject: implement http requests for the TPTP server --- .../dslreasoner/vampire/icse/FileSystemTest.xtend | 2 +- .../dslreasoner/vampire/icse/GeneralTest.xtend | 79 ++++++++++++++++++++-- .../dslreasoner/vampire/icse/YakinduTest.xtend | 58 ++++++++-------- 3 files changed, 104 insertions(+), 35 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse') 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 { it.uniquenessDuplicates = false ] - var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS") + var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) /*/ * 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 import java.util.HashMap import java.util.List import java.util.Map +import okhttp3.MediaType +import okhttp3.OkHttpClient +import okhttp3.Request +import okhttp3.RequestBody +import okhttp3.Response import org.eclipse.emf.ecore.EAttribute import org.eclipse.emf.ecore.EClass import org.eclipse.emf.ecore.EEnum @@ -20,15 +25,77 @@ import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl import org.eclipse.viatra.query.runtime.api.IQueryGroup -class GeneralTest { - def static Map getTypeMap(Map classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) { +class GeneralTest { + 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" + + def static void main(String[] args) { + val form = makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300) + +// 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 +// +//\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 +// +//------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--") + val x = sendPost(form) + print(x.toString) + } + + def static makeForm(String formula, String solver, String cmd, int time) { + return header + addSpec(formula) + addOptions + addSolver(solver, cmd.replace("%d", time.toString)) + addEnd + } + + def static sendPost(String formData ) throws Exception { + + val OkHttpClient client = new OkHttpClient() + + val MediaType mediaType = MediaType.parse( + "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") + val RequestBody body = RequestBody.create(mediaType, formData) + val 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", + "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", + "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("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"). + addHeader("Accept", + "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", + "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", + "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", + "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build() + + val Response response = client.newCall(request).execute() +// TimeUnit.SECONDS.sleep(5) +// return newArrayList( response.body.string.split("\n")) +return response.body.string + + // case 1: + } + def static getHeader() { + 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" + } + def static addSpec(String spec) { + return spec.replace("\n", "\r\n") + } + def static addOptions() { + 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" + } + def static addSolver(String ID, String cmd) { + 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" + } + def static addEnd() { + return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--" + } + + def static Map getTypeMap(Map classMap, EcoreMetamodelDescriptor metamodel, + Ecore2Logic e2l, Ecore2Logic_Trace trace) { val typeMap = new HashMap val listMap = metamodel.classes.toMap[s|s.name] - + for (Class elem : classMap.keySet) { typeMap.put(e2l.TypeofEClass( - trace, listMap.get(elem.simpleName) - ), classMap.get(elem)) + trace, + listMap.get(elem.simpleName) + ), classMap.get(elem)) } return typeMap } @@ -43,7 +110,7 @@ class GeneralTest { } def static loadPartialModel(ReasonerWorkspace inputs, String path) { - Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); + Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()) inputs.readModel(EObject, path).eResource.contents // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList } 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 import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement +import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region +import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult -import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration @@ -17,8 +18,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.Insta import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace import java.io.PrintWriter import java.text.SimpleDateFormat -import java.time.LocalDate import java.util.Date +import java.util.HashMap import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl @@ -54,16 +55,18 @@ class YakinduTest { // val queries = null println("DSL loaded") - var MAX = 80 - var START = 79 + var SZ_TOP = 10 + var SZ_BOT = 126 var INC = 1 - var REPS = 3 + var REPS = 1 + + val RANGE = 3 - val EXACT = 130 + val EXACT = 10 if (EXACT != -1) { - MAX = EXACT - START = EXACT - INC = 5 + SZ_TOP = EXACT + SZ_BOT = EXACT + INC = 1 REPS = 1 } @@ -77,8 +80,8 @@ class YakinduTest { var transformationTimes = newArrayList var modelFound = true var LogicResult solution = null - for (var i = START; i <= MAX; i += INC) { - val num = (i - START) / INC + for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { + val num = (i - SZ_BOT) / INC print("Generation " + num + ": SIZE=" + i + " Attempt: ") writer.append(i + ",") solverTimes.clear @@ -106,17 +109,16 @@ class YakinduTest { // ///////////////////////////////////////////////////// // Minimum Scope -// val classMapMin = new HashMap -// classMapMin.put(Region, 1) -// classMapMin.put(Transition, 2) -// classMapMin.put(CompositeElement, 3) -// val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) + val classMapMin = new HashMap + classMapMin.put(Region, 1) + classMapMin.put(Transition, 2) + classMapMin.put(CompositeElement, 3) + val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) // Maximum Scope -// val classMapMax = new HashMap -// classMapMax.put(Region, 5) -// classMapMax.put(Transition, 2) -// classMapMax.put(Synchronization, 4) -// val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) + val classMapMax = new HashMap + classMapMax.put(Region, 5) + classMapMax.put(Transition, 2) + val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) // Define Config File val size = i val inc = INC @@ -126,18 +128,18 @@ class YakinduTest { it.documentationLevel = DocumentationLevel::FULL it.iteration = iter it.runtimeLimit = 60 - it.typeScopes.maxNewElements = size - it.typeScopes.minNewElements = size - 5 - -// if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin -// if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax + it.typeScopes.maxNewElements = -1 + it.typeScopes.minNewElements = size + it.genModel = false + if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin + if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax it.contCycleLevel = 5 it.uniquenessDuplicates = false ] solution = reasoner.solve(problem, vampireConfig, workspace) // print((solution as ModelResult).representation.get(0)) - val soln = ((solution as ModelResult).representation.get(0) as VampireModel) +// val soln = ((solution as ModelResult).representation.get(0) as VampireModel) // println(soln.confirmations) // println((solution as ModelResult).representation) // modelFound = !soln.confirmations.filter [ -- cgit v1.2.3-70-g09d2