implement http requests for the TPTP server

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 {
                         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<Type, Integer> getTypeMap(Map<Class, Integer> 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<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel,

+                Ecore2Logic e2l, Ecore2Logic_Trace trace) {

                 val typeMap = new HashMap<Type, Integer>

                 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<Class, Integer>

-//                      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<Class, Integer>

+                        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<Class, Integer>

-//                      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<Class, Integer>

+                        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 [