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/.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 11 files changed, 179 insertions(+), 83 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner') 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