aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-10 22:25:07 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-10-10 22:25:07 -0400
commit16f9cd46474a4934c1afd733d687f3c382fbdf56 (patch)
tree465a7cc53a489ae81d80f54d45642d84185d5e43 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse
parentVAMPIRE: Further develop testing fo r Vampire solver (diff)
downloadVIATRA-Generator-16f9cd46474a4934c1afd733d687f3c382fbdf56.tar.gz
VIATRA-Generator-16f9cd46474a4934c1afd733d687f3c382fbdf56.tar.zst
VIATRA-Generator-16f9cd46474a4934c1afd733d687f3c382fbdf56.zip
implement http requests for the TPTP server
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse')
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbinbin4545 -> 4552 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbinbin6624 -> 6632 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbinbin6204 -> 6207 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbinbin6456 -> 10182 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbinbin7958 -> 8484 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java135
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java71
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java56
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbinbin4997 -> 4997 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbinbin687 -> 687 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbinbin6500 -> 6500 bytes
11 files changed, 179 insertions, 83 deletions
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
--- 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
Binary files 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
--- 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
Binary files 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
--- 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
Binary files 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
--- 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
Binary files 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
--- 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
Binary files 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;
25import org.eclipse.emf.ecore.resource.Resource; 25import org.eclipse.emf.ecore.resource.Resource;
26import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; 26import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
27import org.eclipse.xtend2.lib.StringConcatenation; 27import org.eclipse.xtend2.lib.StringConcatenation;
28import org.eclipse.xtext.xbase.lib.Exceptions;
28import org.eclipse.xtext.xbase.lib.InputOutput; 29import org.eclipse.xtext.xbase.lib.InputOutput;
29import org.eclipse.xtext.xbase.lib.ObjectExtensions; 30import org.eclipse.xtext.xbase.lib.ObjectExtensions;
30import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; 31import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
@@ -32,70 +33,74 @@ import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
32@SuppressWarnings("all") 33@SuppressWarnings("all")
33public class FileSystemTest { 34public class FileSystemTest {
34 public static void main(final String[] args) { 35 public static void main(final String[] args) {
35 final Ecore2Logic ecore2Logic = new Ecore2Logic(); 36 try {
36 final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); 37 final Ecore2Logic ecore2Logic = new Ecore2Logic();
37 final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); 38 final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);
38 StringConcatenation _builder = new StringConcatenation(); 39 final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();
39 _builder.append("initialModels/"); 40 StringConcatenation _builder = new StringConcatenation();
40 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); 41 _builder.append("initialModels/");
41 StringConcatenation _builder_1 = new StringConcatenation(); 42 final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");
42 _builder_1.append("output/FileSystemTest/"); 43 StringConcatenation _builder_1 = new StringConcatenation();
43 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); 44 _builder_1.append("output/FileSystemTest/");
44 workspace.initAndClear(); 45 final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), "");
45 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; 46 workspace.initAndClear();
46 final Map<String, Object> map = reg.getExtensionToFactoryMap(); 47 final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;
47 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); 48 final Map<String, Object> map = reg.getExtensionToFactoryMap();
48 map.put("logicproblem", _xMIResourceFactoryImpl); 49 XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
49 InputOutput.<String>println("Input and output workspaces are created"); 50 map.put("logicproblem", _xMIResourceFactoryImpl);
50 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); 51 InputOutput.<String>println("Input and output workspaces are created");
51 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); 52 final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE);
52 InputOutput.<String>println("DSL loaded"); 53 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi");
53 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); 54 InputOutput.<String>println("DSL loaded");
54 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); 55 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
55 LogicProblem problem = modelGenerationProblem.getOutput(); 56 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
56 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); 57 LogicProblem problem = modelGenerationProblem.getOutput();
57 workspace.writeModel(problem, "FileSystem.logicproblem"); 58 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput();
58 InputOutput.<String>println("Problem created"); 59 workspace.writeModel(problem, "FileSystem.logicproblem");
59 long startTime = System.currentTimeMillis(); 60 InputOutput.<String>println("Problem created");
60 VampireSolver reasoner = null; 61 long startTime = System.currentTimeMillis();
61 VampireSolver _vampireSolver = new VampireSolver(); 62 VampireSolver reasoner = null;
62 reasoner = _vampireSolver; 63 VampireSolver _vampireSolver = new VampireSolver();
63 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); 64 reasoner = _vampireSolver;
64 classMapMin.put(Dir.class, Integer.valueOf(10)); 65 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
65 classMapMin.put(File.class, Integer.valueOf(5)); 66 classMapMin.put(Dir.class, Integer.valueOf(10));
66 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 67 classMapMin.put(File.class, Integer.valueOf(5));
67 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); 68 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
68 classMapMax.put(File.class, Integer.valueOf(15)); 69 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
69 classMapMax.put(Dir.class, Integer.valueOf(15)); 70 classMapMax.put(File.class, Integer.valueOf(15));
70 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 71 classMapMax.put(Dir.class, Integer.valueOf(15));
71 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); 72 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
72 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { 73 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
73 it.documentationLevel = DocumentationLevel.FULL; 74 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
74 it.typeScopes.minNewElements = 10; 75 it.documentationLevel = DocumentationLevel.FULL;
75 it.typeScopes.maxNewElements = 25; 76 it.typeScopes.minNewElements = 10;
76 int _size = typeMapMin.size(); 77 it.typeScopes.maxNewElements = 25;
77 boolean _notEquals = (_size != 0); 78 int _size = typeMapMin.size();
78 if (_notEquals) { 79 boolean _notEquals = (_size != 0);
79 it.typeScopes.minNewElementsByType = typeMapMin; 80 if (_notEquals) {
80 } 81 it.typeScopes.minNewElementsByType = typeMapMin;
81 int _size_1 = typeMapMin.size(); 82 }
82 boolean _notEquals_1 = (_size_1 != 0); 83 int _size_1 = typeMapMin.size();
83 if (_notEquals_1) { 84 boolean _notEquals_1 = (_size_1 != 0);
84 it.typeScopes.maxNewElementsByType = typeMapMax; 85 if (_notEquals_1) {
85 } 86 it.typeScopes.maxNewElementsByType = typeMapMax;
86 it.contCycleLevel = 5; 87 }
87 it.uniquenessDuplicates = false; 88 it.contCycleLevel = 5;
88 }; 89 it.uniquenessDuplicates = false;
89 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); 90 };
90 LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS"); 91 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
91 long _currentTimeMillis = System.currentTimeMillis(); 92 LogicResult solution = reasoner.solve(problem, vampireConfig, workspace);
92 long _minus = (_currentTimeMillis - startTime); 93 long _currentTimeMillis = System.currentTimeMillis();
93 long totalTimeMin = (_minus / 60000); 94 long _minus = (_currentTimeMillis - startTime);
94 long _currentTimeMillis_1 = System.currentTimeMillis(); 95 long totalTimeMin = (_minus / 60000);
95 long _minus_1 = (_currentTimeMillis_1 - startTime); 96 long _currentTimeMillis_1 = System.currentTimeMillis();
96 long _divide = (_minus_1 / 1000); 97 long _minus_1 = (_currentTimeMillis_1 - startTime);
97 long totalTimeSec = (_divide % 60); 98 long _divide = (_minus_1 / 1000);
98 InputOutput.<String>println("Problem solved"); 99 long totalTimeSec = (_divide % 60);
99 InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); 100 InputOutput.<String>println("Problem solved");
101 InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec)));
102 } catch (Throwable _e) {
103 throw Exceptions.sneakyThrow(_e);
104 }
100 } 105 }
101} 106}
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;
13import java.util.List; 13import java.util.List;
14import java.util.Map; 14import java.util.Map;
15import java.util.Set; 15import java.util.Set;
16import okhttp3.MediaType;
17import okhttp3.OkHttpClient;
18import okhttp3.Request;
19import okhttp3.RequestBody;
20import okhttp3.Response;
16import org.eclipse.emf.common.util.EList; 21import org.eclipse.emf.common.util.EList;
17import org.eclipse.emf.ecore.EAttribute; 22import org.eclipse.emf.ecore.EAttribute;
18import org.eclipse.emf.ecore.EClass; 23import org.eclipse.emf.ecore.EClass;
@@ -28,12 +33,75 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup;
28import org.eclipse.viatra.query.runtime.api.IQuerySpecification; 33import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
29import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; 34import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation;
30import org.eclipse.xtext.xbase.lib.CollectionLiterals; 35import org.eclipse.xtext.xbase.lib.CollectionLiterals;
36import org.eclipse.xtext.xbase.lib.Exceptions;
31import org.eclipse.xtext.xbase.lib.Functions.Function1; 37import org.eclipse.xtext.xbase.lib.Functions.Function1;
38import org.eclipse.xtext.xbase.lib.InputOutput;
32import org.eclipse.xtext.xbase.lib.IterableExtensions; 39import org.eclipse.xtext.xbase.lib.IterableExtensions;
33import org.eclipse.xtext.xbase.lib.ListExtensions; 40import org.eclipse.xtext.xbase.lib.ListExtensions;
34 41
35@SuppressWarnings("all") 42@SuppressWarnings("all")
36public class GeneralTest { 43public class GeneralTest {
44 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";
45
46 public static void main(final String[] args) {
47 try {
48 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);
49 final String x = GeneralTest.sendPost(form);
50 InputOutput.<String>print(x.toString());
51 } catch (Throwable _e) {
52 throw Exceptions.sneakyThrow(_e);
53 }
54 }
55
56 public static String makeForm(final String formula, final String solver, final String cmd, final int time) {
57 String _header = GeneralTest.getHeader();
58 String _addSpec = GeneralTest.addSpec(formula);
59 String _plus = (_header + _addSpec);
60 String _addOptions = GeneralTest.addOptions();
61 String _plus_1 = (_plus + _addOptions);
62 String _addSolver = GeneralTest.addSolver(solver, cmd.replace("%d", Integer.valueOf(time).toString()));
63 String _plus_2 = (_plus_1 + _addSolver);
64 String _addEnd = GeneralTest.addEnd();
65 return (_plus_2 + _addEnd);
66 }
67
68 public static String sendPost(final String formData) throws Exception {
69 final OkHttpClient client = new OkHttpClient();
70 final MediaType mediaType = MediaType.parse(
71 "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA");
72 final RequestBody body = RequestBody.create(mediaType, formData);
73 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",
74 "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type",
75 "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent",
76 "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",
77 "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",
78 "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token",
79 "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host",
80 "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build();
81 final Response response = client.newCall(request).execute();
82 return response.body().string();
83 }
84
85 public static String getHeader() {
86 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";
87 }
88
89 public static String addSpec(final String spec) {
90 return spec.replace("\n", "\r\n");
91 }
92
93 public static String addOptions() {
94 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";
95 }
96
97 public static String addSolver(final String ID, final String cmd) {
98 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");
99 }
100
101 public static String addEnd() {
102 return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--";
103 }
104
37 public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { 105 public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) {
38 final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>(); 106 final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>();
39 final Function1<EClass, String> _function = (EClass s) -> { 107 final Function1<EClass, String> _function = (EClass s) -> {
@@ -43,7 +111,8 @@ public class GeneralTest {
43 Set<Class> _keySet = classMap.keySet(); 111 Set<Class> _keySet = classMap.keySet();
44 for (final Class elem : _keySet) { 112 for (final Class elem : _keySet) {
45 typeMap.put( 113 typeMap.put(
46 e2l.TypeofEClass(trace, listMap.get(elem.getSimpleName())), classMap.get(elem)); 114 e2l.TypeofEClass(trace,
115 listMap.get(elem.getSimpleName())), classMap.get(elem));
47 } 116 }
48 return typeMap; 117 return typeMap;
49 } 118 }
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;
4import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns; 4import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; 5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; 6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
7import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement;
8import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region;
9import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition;
7import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; 10import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage;
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; 11import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
10import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; 12import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;
11import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; 13import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;
12import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; 14import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
13import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; 15import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
14import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; 16import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
15import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; 18import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
16import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; 19import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
17import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
18import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; 20import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;
19import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; 21import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;
20import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; 22import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration;
@@ -26,6 +28,7 @@ import java.io.PrintWriter;
26import java.text.SimpleDateFormat; 28import java.text.SimpleDateFormat;
27import java.util.ArrayList; 29import java.util.ArrayList;
28import java.util.Date; 30import java.util.Date;
31import java.util.HashMap;
29import java.util.Map; 32import java.util.Map;
30import org.eclipse.emf.common.util.EList; 33import org.eclipse.emf.common.util.EList;
31import org.eclipse.emf.common.util.URI; 34import org.eclipse.emf.common.util.URI;
@@ -72,15 +75,16 @@ public class YakinduTest {
72 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); 75 final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi");
73 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); 76 final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance());
74 InputOutput.<String>println("DSL loaded"); 77 InputOutput.<String>println("DSL loaded");
75 int MAX = 80; 78 int SZ_TOP = 10;
76 int START = 79; 79 int SZ_BOT = 126;
77 int INC = 1; 80 int INC = 1;
78 int REPS = 3; 81 int REPS = 1;
79 final int EXACT = 130; 82 final int RANGE = 3;
83 final int EXACT = 10;
80 if ((EXACT != (-1))) { 84 if ((EXACT != (-1))) {
81 MAX = EXACT; 85 SZ_TOP = EXACT;
82 START = EXACT; 86 SZ_BOT = EXACT;
83 INC = 5; 87 INC = 1;
84 REPS = 1; 88 REPS = 1;
85 } 89 }
86 URI _workspaceURI = workspace.getWorkspaceURI(); 90 URI _workspaceURI = workspace.getWorkspaceURI();
@@ -96,11 +100,11 @@ public class YakinduTest {
96 boolean modelFound = true; 100 boolean modelFound = true;
97 LogicResult solution = null; 101 LogicResult solution = null;
98 { 102 {
99 int i = START; 103 int i = SZ_BOT;
100 boolean _while = (i <= MAX); 104 boolean _while = (i <= SZ_TOP);
101 while (_while) { 105 while (_while) {
102 { 106 {
103 final int num = ((i - START) / INC); 107 final int num = ((i - SZ_BOT) / INC);
104 InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); 108 InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: "));
105 String _plus_3 = (Integer.valueOf(i) + ","); 109 String _plus_3 = (Integer.valueOf(i) + ",");
106 writer.append(_plus_3); 110 writer.append(_plus_3);
@@ -121,6 +125,15 @@ public class YakinduTest {
121 VampireSolver reasoner = null; 125 VampireSolver reasoner = null;
122 VampireSolver _vampireSolver = new VampireSolver(); 126 VampireSolver _vampireSolver = new VampireSolver();
123 reasoner = _vampireSolver; 127 reasoner = _vampireSolver;
128 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
129 classMapMin.put(Region.class, Integer.valueOf(1));
130 classMapMin.put(Transition.class, Integer.valueOf(2));
131 classMapMin.put(CompositeElement.class, Integer.valueOf(3));
132 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
133 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
134 classMapMax.put(Region.class, Integer.valueOf(5));
135 classMapMax.put(Transition.class, Integer.valueOf(2));
136 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
124 final int size = i; 137 final int size = i;
125 final int inc = INC; 138 final int inc = INC;
126 final int iter = j; 139 final int iter = j;
@@ -129,15 +142,24 @@ public class YakinduTest {
129 it.documentationLevel = DocumentationLevel.FULL; 142 it.documentationLevel = DocumentationLevel.FULL;
130 it.iteration = iter; 143 it.iteration = iter;
131 it.runtimeLimit = 60; 144 it.runtimeLimit = 60;
132 it.typeScopes.maxNewElements = size; 145 it.typeScopes.maxNewElements = (-1);
133 it.typeScopes.minNewElements = (size - 5); 146 it.typeScopes.minNewElements = size;
147 it.genModel = false;
148 int _size = typeMapMin.size();
149 boolean _notEquals = (_size != 0);
150 if (_notEquals) {
151 it.typeScopes.minNewElementsByType = typeMapMin;
152 }
153 int _size_1 = typeMapMin.size();
154 boolean _notEquals_1 = (_size_1 != 0);
155 if (_notEquals_1) {
156 it.typeScopes.maxNewElementsByType = typeMapMax;
157 }
134 it.contCycleLevel = 5; 158 it.contCycleLevel = 5;
135 it.uniquenessDuplicates = false; 159 it.uniquenessDuplicates = false;
136 }; 160 };
137 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); 161 final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
138 solution = reasoner.solve(problem, vampireConfig, workspace); 162 solution = reasoner.solve(problem, vampireConfig, workspace);
139 Object _get = ((ModelResult) solution).getRepresentation().get(0);
140 final VampireModel soln = ((VampireModel) _get);
141 int _transformationTime = solution.getStatistics().getTransformationTime(); 163 int _transformationTime = solution.getStatistics().getTransformationTime();
142 final double tTime = (_transformationTime / 1000.0); 164 final double tTime = (_transformationTime / 1000.0);
143 int _solverTime = solution.getStatistics().getSolverTime(); 165 int _solverTime = solution.getStatistics().getSolverTime();
@@ -163,7 +185,7 @@ public class YakinduTest {
163 } 185 }
164 int _i = i; 186 int _i = i;
165 i = (_i + INC); 187 i = (_i + INC);
166 _while = (i <= MAX); 188 _while = (i <= SZ_TOP);
167 } 189 }
168 } 190 }
169 writer.close(); 191 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
--- 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
Binary files 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
--- 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
Binary files 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
--- 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
Binary files differ