diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire')
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; | |||
25 | import org.eclipse.emf.ecore.resource.Resource; | 25 | import org.eclipse.emf.ecore.resource.Resource; |
26 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; | 26 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; |
27 | import org.eclipse.xtend2.lib.StringConcatenation; | 27 | import org.eclipse.xtend2.lib.StringConcatenation; |
28 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
28 | import org.eclipse.xtext.xbase.lib.InputOutput; | 29 | import org.eclipse.xtext.xbase.lib.InputOutput; |
29 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 30 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
30 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 31 | import 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") |
33 | public class FileSystemTest { | 34 | public 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; | |||
13 | import java.util.List; | 13 | import java.util.List; |
14 | import java.util.Map; | 14 | import java.util.Map; |
15 | import java.util.Set; | 15 | import java.util.Set; |
16 | import okhttp3.MediaType; | ||
17 | import okhttp3.OkHttpClient; | ||
18 | import okhttp3.Request; | ||
19 | import okhttp3.RequestBody; | ||
20 | import okhttp3.Response; | ||
16 | import org.eclipse.emf.common.util.EList; | 21 | import org.eclipse.emf.common.util.EList; |
17 | import org.eclipse.emf.ecore.EAttribute; | 22 | import org.eclipse.emf.ecore.EAttribute; |
18 | import org.eclipse.emf.ecore.EClass; | 23 | import org.eclipse.emf.ecore.EClass; |
@@ -28,12 +33,75 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup; | |||
28 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; | 33 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; |
29 | import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; | 34 | import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; |
30 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 35 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
36 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 37 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
38 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | 39 | import org.eclipse.xtext.xbase.lib.IterableExtensions; |
33 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 40 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
34 | 41 | ||
35 | @SuppressWarnings("all") | 42 | @SuppressWarnings("all") |
36 | public class GeneralTest { | 43 | public 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; | |||
4 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; | 11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; |
10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; | 12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; |
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; | 13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; |
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; | 14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | 20 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; |
19 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; | 21 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; |
20 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; | 22 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; |
@@ -26,6 +28,7 @@ import java.io.PrintWriter; | |||
26 | import java.text.SimpleDateFormat; | 28 | import java.text.SimpleDateFormat; |
27 | import java.util.ArrayList; | 29 | import java.util.ArrayList; |
28 | import java.util.Date; | 30 | import java.util.Date; |
31 | import java.util.HashMap; | ||
29 | import java.util.Map; | 32 | import java.util.Map; |
30 | import org.eclipse.emf.common.util.EList; | 33 | import org.eclipse.emf.common.util.EList; |
31 | import org.eclipse.emf.common.util.URI; | 34 | import 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 | |||