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 --- .../.classpath | 6 + .../META-INF/MANIFEST.MF | 78 ++++++------ .../dslreasoner/vampire/icse/FileSystemTest.xtend | 2 +- .../dslreasoner/vampire/icse/GeneralTest.xtend | 79 +++++++++++- .../dslreasoner/vampire/icse/YakinduTest.xtend | 58 ++++----- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 4545 -> 4552 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 6624 -> 6632 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 6204 -> 6207 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 6456 -> 10182 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 7958 -> 8484 bytes .../dslreasoner/vampire/icse/FileSystemTest.java | 135 +++++++++++---------- .../ecse/dslreasoner/vampire/icse/GeneralTest.java | 71 ++++++++++- .../ecse/dslreasoner/vampire/icse/YakinduTest.java | 56 ++++++--- .../vampire/test/.MedicalSystem.xtendbin | Bin 4997 -> 4997 bytes .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 687 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6500 -> 6500 bytes 16 files changed, 326 insertions(+), 159 deletions(-) (limited to 'Tests') diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath index 3f0838b6..7618afdf 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/.classpath @@ -5,5 +5,11 @@ + + + + + + diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF index 0af80e6c..dead7622 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF @@ -6,48 +6,44 @@ Bundle-Version: 1.0.0.qualifier Bundle-ClassPath: . Bundle-Vendor: %providerName Bundle-Localization: plugin -Export-Package: ca.mcgill.ecse.dslreasoner.vamipre.yakindumm, - ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.impl, - ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.util, - ca.mcgill.ecse.dslreasoner.vampire.queries, - ca.mcgill.ecse.dslreasoner.vampire.yakindumm, - ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl, - ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util, - yakindumm, - yakindumm.impl, - yakindumm.util, - yakindumm.yakindumm, - yakindumm.yakindumm.impl, - yakindumm.yakindumm.util +Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries, + ca.mcgill.ecse.dslreasoner.vampire.yakindumm, + ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl, + ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime, - org.eclipse.core.runtime, - org.eclipse.emf.ecore;visibility:=reexport, - org.eclipse.viatra.query.runtime.rete, - org.eclipse.viatra.query.runtime.localsearch, - com.google.guava, - org.eclipse.xtext.xbase.lib, - org.eclipse.xtend.lib, - org.eclipse.xtend.lib.macro, - ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", - ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", - org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", - hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0", - ModelGenExampleFAM_plugin;bundle-version="1.0.0", - ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1", - hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", - hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1", - org.eclipse.viatra.query.runtime;bundle-version="2.1.0", - org.eclipse.collections;bundle-version="9.2.0", - hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", - ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0" + org.eclipse.core.runtime, + org.eclipse.emf.ecore;visibility:=reexport, + org.eclipse.viatra.query.runtime.rete, + org.eclipse.viatra.query.runtime.localsearch, + com.google.guava, + org.eclipse.xtext.xbase.lib, + org.eclipse.xtend.lib, + org.eclipse.xtend.lib.macro, + ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", + ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", + org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", + hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0", + ModelGenExampleFAM_plugin;bundle-version="1.0.0", + ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1", + hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1", + org.eclipse.viatra.query.runtime;bundle-version="2.1.0", + org.eclipse.collections;bundle-version="9.2.0", + hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", + ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0", + org.apache.httpcomponents.httpcore;bundle-version="4.4.6", + org.apache.httpcomponents.httpclient;bundle-version="4.5.2", + org.apache.httpcomponents.httpclient.source;bundle-version="4.5.2", + org.apache.httpcomponents.httpclient.win;bundle-version="4.5.2", + org.apache.httpcomponents.httpcore.source;bundle-version="4.4.6" Import-Package: org.apache.log4j Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test Bundle-ActivationPolicy: lazy 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 [ 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 084503b5..93d27b4d 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin 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 2315cd50..bc2bae6f 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin 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 a3386941..5687258f 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin 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 dee6f742..de68a908 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin 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 f54cd3a0..16a3cd03 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin differ diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java index 7579bd98..8c7923be 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java @@ -25,6 +25,7 @@ import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.Exceptions; import org.eclipse.xtext.xbase.lib.InputOutput; import org.eclipse.xtext.xbase.lib.ObjectExtensions; import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @@ -32,70 +33,74 @@ import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @SuppressWarnings("all") public class FileSystemTest { public static void main(final String[] args) { - final Ecore2Logic ecore2Logic = new Ecore2Logic(); - final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); - final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); - StringConcatenation _builder = new StringConcatenation(); - _builder.append("initialModels/"); - final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("output/FileSystemTest/"); - final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); - workspace.initAndClear(); - final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; - final Map map = reg.getExtensionToFactoryMap(); - XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); - map.put("logicproblem", _xMIResourceFactoryImpl); - InputOutput.println("Input and output workspaces are created"); - final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); - final EList partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); - InputOutput.println("DSL loaded"); - Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); - final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); - LogicProblem problem = modelGenerationProblem.getOutput(); - problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); - workspace.writeModel(problem, "FileSystem.logicproblem"); - InputOutput.println("Problem created"); - long startTime = System.currentTimeMillis(); - VampireSolver reasoner = null; - VampireSolver _vampireSolver = new VampireSolver(); - reasoner = _vampireSolver; - final HashMap classMapMin = new HashMap(); - classMapMin.put(Dir.class, Integer.valueOf(10)); - classMapMin.put(File.class, Integer.valueOf(5)); - final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); - final HashMap classMapMax = new HashMap(); - classMapMax.put(File.class, Integer.valueOf(15)); - classMapMax.put(Dir.class, Integer.valueOf(15)); - final Map typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); - VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); - final Procedure1 _function = (VampireSolverConfiguration it) -> { - it.documentationLevel = DocumentationLevel.FULL; - it.typeScopes.minNewElements = 10; - it.typeScopes.maxNewElements = 25; - int _size = typeMapMin.size(); - boolean _notEquals = (_size != 0); - if (_notEquals) { - it.typeScopes.minNewElementsByType = typeMapMin; - } - int _size_1 = typeMapMin.size(); - boolean _notEquals_1 = (_size_1 != 0); - if (_notEquals_1) { - it.typeScopes.maxNewElementsByType = typeMapMax; - } - it.contCycleLevel = 5; - it.uniquenessDuplicates = false; - }; - final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); - LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS"); - long _currentTimeMillis = System.currentTimeMillis(); - long _minus = (_currentTimeMillis - startTime); - long totalTimeMin = (_minus / 60000); - long _currentTimeMillis_1 = System.currentTimeMillis(); - long _minus_1 = (_currentTimeMillis_1 - startTime); - long _divide = (_minus_1 / 1000); - long totalTimeSec = (_divide % 60); - InputOutput.println("Problem solved"); - InputOutput.println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); + try { + final Ecore2Logic ecore2Logic = new Ecore2Logic(); + final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); + final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("initialModels/"); + final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("output/FileSystemTest/"); + final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); + workspace.initAndClear(); + final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; + final Map map = reg.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); + map.put("logicproblem", _xMIResourceFactoryImpl); + InputOutput.println("Input and output workspaces are created"); + final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); + final EList partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); + InputOutput.println("DSL loaded"); + Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); + final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); + LogicProblem problem = modelGenerationProblem.getOutput(); + problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); + workspace.writeModel(problem, "FileSystem.logicproblem"); + InputOutput.println("Problem created"); + long startTime = System.currentTimeMillis(); + VampireSolver reasoner = null; + VampireSolver _vampireSolver = new VampireSolver(); + reasoner = _vampireSolver; + final HashMap classMapMin = new HashMap(); + classMapMin.put(Dir.class, Integer.valueOf(10)); + classMapMin.put(File.class, Integer.valueOf(5)); + final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + final HashMap classMapMax = new HashMap(); + classMapMax.put(File.class, Integer.valueOf(15)); + classMapMax.put(Dir.class, Integer.valueOf(15)); + final Map typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); + final Procedure1 _function = (VampireSolverConfiguration it) -> { + it.documentationLevel = DocumentationLevel.FULL; + it.typeScopes.minNewElements = 10; + it.typeScopes.maxNewElements = 25; + int _size = typeMapMin.size(); + boolean _notEquals = (_size != 0); + if (_notEquals) { + it.typeScopes.minNewElementsByType = typeMapMin; + } + int _size_1 = typeMapMin.size(); + boolean _notEquals_1 = (_size_1 != 0); + if (_notEquals_1) { + it.typeScopes.maxNewElementsByType = typeMapMax; + } + it.contCycleLevel = 5; + it.uniquenessDuplicates = false; + }; + final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); + LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); + long _currentTimeMillis = System.currentTimeMillis(); + long _minus = (_currentTimeMillis - startTime); + long totalTimeMin = (_minus / 60000); + long _currentTimeMillis_1 = System.currentTimeMillis(); + long _minus_1 = (_currentTimeMillis_1 - startTime); + long _divide = (_minus_1 / 1000); + long totalTimeSec = (_divide % 60); + InputOutput.println("Problem solved"); + InputOutput.println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); + } } } 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 0bb8f76e..ce057092 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,6 +13,11 @@ import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.Set; +import okhttp3.MediaType; +import okhttp3.OkHttpClient; +import okhttp3.Request; +import okhttp3.RequestBody; +import okhttp3.Response; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.ecore.EAttribute; import org.eclipse.emf.ecore.EClass; @@ -28,12 +33,75 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup; import org.eclipse.viatra.query.runtime.api.IQuerySpecification; import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; import org.eclipse.xtext.xbase.lib.CollectionLiterals; +import org.eclipse.xtext.xbase.lib.Exceptions; import org.eclipse.xtext.xbase.lib.Functions.Function1; +import org.eclipse.xtext.xbase.lib.InputOutput; import org.eclipse.xtext.xbase.lib.IterableExtensions; import org.eclipse.xtext.xbase.lib.ListExtensions; @SuppressWarnings("all") public class GeneralTest { + 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"; + + public static void main(final String[] args) { + try { + 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); + final String x = GeneralTest.sendPost(form); + InputOutput.print(x.toString()); + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); + } + } + + public static String makeForm(final String formula, final String solver, final String cmd, final int time) { + String _header = GeneralTest.getHeader(); + String _addSpec = GeneralTest.addSpec(formula); + String _plus = (_header + _addSpec); + String _addOptions = GeneralTest.addOptions(); + String _plus_1 = (_plus + _addOptions); + String _addSolver = GeneralTest.addSolver(solver, cmd.replace("%d", Integer.valueOf(time).toString())); + String _plus_2 = (_plus_1 + _addSolver); + String _addEnd = GeneralTest.addEnd(); + return (_plus_2 + _addEnd); + } + + public static String sendPost(final String formData) throws Exception { + final OkHttpClient client = new OkHttpClient(); + final MediaType mediaType = MediaType.parse( + "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); + final RequestBody body = RequestBody.create(mediaType, formData); + 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", + "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(); + final Response response = client.newCall(request).execute(); + return response.body().string(); + } + + public static String 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"; + } + + public static String addSpec(final String spec) { + return spec.replace("\n", "\r\n"); + } + + public static String 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"; + } + + public static String addSolver(final String ID, final 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"); + } + + public static String addEnd() { + return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"; + } + public static Map getTypeMap(final Map classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { final HashMap typeMap = new HashMap(); final Function1 _function = (EClass s) -> { @@ -43,7 +111,8 @@ public class GeneralTest { Set _keySet = classMap.keySet(); for (final Class elem : _keySet) { typeMap.put( - e2l.TypeofEClass(trace, listMap.get(elem.getSimpleName())), classMap.get(elem)); + e2l.TypeofEClass(trace, + listMap.get(elem.getSimpleName())), classMap.get(elem)); } return typeMap; } 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 b18ede4f..3a8f3fb4 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 @@ -4,17 +4,19 @@ import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; 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.ecore2logic.Ecore2Logic_Trace; import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; 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; @@ -26,6 +28,7 @@ import java.io.PrintWriter; import java.text.SimpleDateFormat; import java.util.ArrayList; import java.util.Date; +import java.util.HashMap; import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.common.util.URI; @@ -72,15 +75,16 @@ public class YakinduTest { final EList partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); InputOutput.println("DSL loaded"); - int MAX = 80; - int START = 79; + int SZ_TOP = 10; + int SZ_BOT = 126; int INC = 1; - int REPS = 3; - final int EXACT = 130; + int REPS = 1; + final int RANGE = 3; + final int EXACT = 10; if ((EXACT != (-1))) { - MAX = EXACT; - START = EXACT; - INC = 5; + SZ_TOP = EXACT; + SZ_BOT = EXACT; + INC = 1; REPS = 1; } URI _workspaceURI = workspace.getWorkspaceURI(); @@ -96,11 +100,11 @@ public class YakinduTest { boolean modelFound = true; LogicResult solution = null; { - int i = START; - boolean _while = (i <= MAX); + int i = SZ_BOT; + boolean _while = (i <= SZ_TOP); while (_while) { { - final int num = ((i - START) / INC); + final int num = ((i - SZ_BOT) / INC); InputOutput.print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); String _plus_3 = (Integer.valueOf(i) + ","); writer.append(_plus_3); @@ -121,6 +125,15 @@ public class YakinduTest { VampireSolver reasoner = null; VampireSolver _vampireSolver = new VampireSolver(); reasoner = _vampireSolver; + final HashMap classMapMin = new HashMap(); + classMapMin.put(Region.class, Integer.valueOf(1)); + classMapMin.put(Transition.class, Integer.valueOf(2)); + classMapMin.put(CompositeElement.class, Integer.valueOf(3)); + final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); + final HashMap classMapMax = new HashMap(); + classMapMax.put(Region.class, Integer.valueOf(5)); + classMapMax.put(Transition.class, Integer.valueOf(2)); + final Map typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); final int size = i; final int inc = INC; final int iter = j; @@ -129,15 +142,24 @@ public class YakinduTest { it.documentationLevel = DocumentationLevel.FULL; it.iteration = iter; it.runtimeLimit = 60; - it.typeScopes.maxNewElements = size; - it.typeScopes.minNewElements = (size - 5); + it.typeScopes.maxNewElements = (-1); + it.typeScopes.minNewElements = size; + it.genModel = false; + int _size = typeMapMin.size(); + boolean _notEquals = (_size != 0); + if (_notEquals) { + it.typeScopes.minNewElementsByType = typeMapMin; + } + int _size_1 = typeMapMin.size(); + boolean _notEquals_1 = (_size_1 != 0); + if (_notEquals_1) { + it.typeScopes.maxNewElementsByType = typeMapMax; + } it.contCycleLevel = 5; it.uniquenessDuplicates = false; }; final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); solution = reasoner.solve(problem, vampireConfig, workspace); - Object _get = ((ModelResult) solution).getRepresentation().get(0); - final VampireModel soln = ((VampireModel) _get); int _transformationTime = solution.getStatistics().getTransformationTime(); final double tTime = (_transformationTime / 1000.0); int _solverTime = solution.getStatistics().getSolverTime(); @@ -163,7 +185,7 @@ public class YakinduTest { } int _i = i; i = (_i + INC); - _while = (i <= MAX); + _while = (i <= SZ_TOP); } } 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 e77449e7..96f343fa 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin 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 97f29b0c..1ca8223d 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin 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 0e320f18..5d6a9ee2 100644 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin differ -- cgit v1.2.3-54-g00ecf