diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test')
16 files changed, 326 insertions, 159 deletions
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 @@ | |||
5 | <classpathentry kind="src" path="src"/> | 5 | <classpathentry kind="src" path="src"/> |
6 | <classpathentry kind="src" path="src-gen"/> | 6 | <classpathentry kind="src" path="src-gen"/> |
7 | <classpathentry kind="src" path="xtend-gen"/> | 7 | <classpathentry kind="src" path="xtend-gen"/> |
8 | <classpathentry kind="lib" path="InputLPs/unirest-java-1.4.9.jar"/> | ||
9 | <classpathentry kind="lib" path="InputLPs/annotations-13.0.jar"/> | ||
10 | <classpathentry kind="lib" path="InputLPs/kotlin-stdlib-1.3.50.jar"/> | ||
11 | <classpathentry kind="lib" path="InputLPs/kotlin-stdlib-common-1.3.50.jar"/> | ||
12 | <classpathentry kind="lib" path="InputLPs/okhttp-4.2.0.jar"/> | ||
13 | <classpathentry kind="lib" path="InputLPs/okio-2.2.2.jar"/> | ||
8 | <classpathentry kind="output" path="bin"/> | 14 | <classpathentry kind="output" path="bin"/> |
9 | </classpath> | 15 | </classpath> |
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 | |||
6 | Bundle-ClassPath: . | 6 | Bundle-ClassPath: . |
7 | Bundle-Vendor: %providerName | 7 | Bundle-Vendor: %providerName |
8 | Bundle-Localization: plugin | 8 | Bundle-Localization: plugin |
9 | Export-Package: ca.mcgill.ecse.dslreasoner.vamipre.yakindumm, | 9 | Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries, |
10 | ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.impl, | 10 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm, |
11 | ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.util, | 11 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl, |
12 | ca.mcgill.ecse.dslreasoner.vampire.queries, | 12 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util |
13 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm, | ||
14 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl, | ||
15 | ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util, | ||
16 | yakindumm, | ||
17 | yakindumm.impl, | ||
18 | yakindumm.util, | ||
19 | yakindumm.yakindumm, | ||
20 | yakindumm.yakindumm.impl, | ||
21 | yakindumm.yakindumm.util | ||
22 | Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime, | 13 | Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime, |
23 | org.eclipse.core.runtime, | 14 | org.eclipse.core.runtime, |
24 | org.eclipse.emf.ecore;visibility:=reexport, | 15 | org.eclipse.emf.ecore;visibility:=reexport, |
25 | org.eclipse.viatra.query.runtime.rete, | 16 | org.eclipse.viatra.query.runtime.rete, |
26 | org.eclipse.viatra.query.runtime.localsearch, | 17 | org.eclipse.viatra.query.runtime.localsearch, |
27 | com.google.guava, | 18 | com.google.guava, |
28 | org.eclipse.xtext.xbase.lib, | 19 | org.eclipse.xtext.xbase.lib, |
29 | org.eclipse.xtend.lib, | 20 | org.eclipse.xtend.lib, |
30 | org.eclipse.xtend.lib.macro, | 21 | org.eclipse.xtend.lib.macro, |
31 | ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", | 22 | ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", |
32 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | 23 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", |
33 | ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", | 24 | ca.mcgill.ecse.dslreasoner.vampire.reasoner;bundle-version="1.0.0", |
34 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | 25 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", |
35 | hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", | 26 | hu.bme.mit.inf.dslreasoner.viatra2logic;bundle-version="1.0.0", |
36 | org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", | 27 | org.eclipse.emf.ecore.xmi;bundle-version="2.13.0", |
37 | hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", | 28 | hu.bme.mit.inf.dlsreasoner.alloy.reasoner;bundle-version="1.0.0", |
38 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", | 29 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", |
39 | hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", | 30 | hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner;bundle-version="1.0.0", |
40 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", | 31 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatraquery;bundle-version="1.0.0", |
41 | hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0", | 32 | hu.bme.mit.inf.dslreasoner.logic2ecore;bundle-version="1.0.0", |
42 | hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0", | 33 | hu.bme.mit.inf.dslreasoner.visualisation;bundle-version="1.0.0", |
43 | ModelGenExampleFAM_plugin;bundle-version="1.0.0", | 34 | ModelGenExampleFAM_plugin;bundle-version="1.0.0", |
44 | ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1", | 35 | ModelGenExampleFAM_plugin.validation;bundle-version="0.0.1", |
45 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", | 36 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph;bundle-version="1.0.0", |
46 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1", | 37 | hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.validation;bundle-version="0.0.1", |
47 | org.eclipse.viatra.query.runtime;bundle-version="2.1.0", | 38 | org.eclipse.viatra.query.runtime;bundle-version="2.1.0", |
48 | org.eclipse.collections;bundle-version="9.2.0", | 39 | org.eclipse.collections;bundle-version="9.2.0", |
49 | hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", | 40 | hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", |
50 | ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0" | 41 | ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0", |
42 | org.apache.httpcomponents.httpcore;bundle-version="4.4.6", | ||
43 | org.apache.httpcomponents.httpclient;bundle-version="4.5.2", | ||
44 | org.apache.httpcomponents.httpclient.source;bundle-version="4.5.2", | ||
45 | org.apache.httpcomponents.httpclient.win;bundle-version="4.5.2", | ||
46 | org.apache.httpcomponents.httpcore.source;bundle-version="4.4.6" | ||
51 | Import-Package: org.apache.log4j | 47 | Import-Package: org.apache.log4j |
52 | Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test | 48 | Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test |
53 | Bundle-ActivationPolicy: lazy | 49 | 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 { | |||
86 | it.uniquenessDuplicates = false | 86 | it.uniquenessDuplicates = false |
87 | ] | 87 | ] |
88 | 88 | ||
89 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "FS") | 89 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) |
90 | 90 | ||
91 | /*/ | 91 | /*/ |
92 | * | 92 | * |
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 | |||
9 | import java.util.HashMap | 9 | import java.util.HashMap |
10 | import java.util.List | 10 | import java.util.List |
11 | import java.util.Map | 11 | import java.util.Map |
12 | import okhttp3.MediaType | ||
13 | import okhttp3.OkHttpClient | ||
14 | import okhttp3.Request | ||
15 | import okhttp3.RequestBody | ||
16 | import okhttp3.Response | ||
12 | import org.eclipse.emf.ecore.EAttribute | 17 | import org.eclipse.emf.ecore.EAttribute |
13 | import org.eclipse.emf.ecore.EClass | 18 | import org.eclipse.emf.ecore.EClass |
14 | import org.eclipse.emf.ecore.EEnum | 19 | import org.eclipse.emf.ecore.EEnum |
@@ -20,15 +25,77 @@ import org.eclipse.emf.ecore.resource.Resource | |||
20 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 25 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
21 | import org.eclipse.viatra.query.runtime.api.IQueryGroup | 26 | import org.eclipse.viatra.query.runtime.api.IQueryGroup |
22 | 27 | ||
23 | class GeneralTest { | 28 | class GeneralTest { |
24 | def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) { | 29 | 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" |
30 | |||
31 | def static void main(String[] args) { | ||
32 | val form = makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300) | ||
33 | |||
34 | // 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 | ||
35 | // | ||
36 | //\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 | ||
37 | // | ||
38 | //------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--") | ||
39 | val x = sendPost(form) | ||
40 | print(x.toString) | ||
41 | } | ||
42 | |||
43 | def static makeForm(String formula, String solver, String cmd, int time) { | ||
44 | return header + addSpec(formula) + addOptions + addSolver(solver, cmd.replace("%d", time.toString)) + addEnd | ||
45 | } | ||
46 | |||
47 | def static sendPost(String formData ) throws Exception { | ||
48 | |||
49 | val OkHttpClient client = new OkHttpClient() | ||
50 | |||
51 | val MediaType mediaType = MediaType.parse( | ||
52 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") | ||
53 | val RequestBody body = RequestBody.create(mediaType, formData) | ||
54 | val Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body). | ||
55 | addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", | ||
56 | "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", | ||
57 | "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", | ||
58 | "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36"). | ||
59 | addHeader("Accept", | ||
60 | "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3"). | ||
61 | addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", | ||
62 | "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", | ||
63 | "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", | ||
64 | "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build() | ||
65 | |||
66 | val Response response = client.newCall(request).execute() | ||
67 | // TimeUnit.SECONDS.sleep(5) | ||
68 | // return newArrayList( response.body.string.split("\n")) | ||
69 | return response.body.string | ||
70 | |||
71 | // case 1: | ||
72 | } | ||
73 | def static getHeader() { | ||
74 | 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" | ||
75 | } | ||
76 | def static addSpec(String spec) { | ||
77 | return spec.replace("\n", "\r\n") | ||
78 | } | ||
79 | def static addOptions() { | ||
80 | 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" | ||
81 | } | ||
82 | def static addSolver(String ID, String cmd) { | ||
83 | 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" | ||
84 | } | ||
85 | def static addEnd() { | ||
86 | return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--" | ||
87 | } | ||
88 | |||
89 | def static Map<Type, Integer> getTypeMap(Map<Class, Integer> classMap, EcoreMetamodelDescriptor metamodel, | ||
90 | Ecore2Logic e2l, Ecore2Logic_Trace trace) { | ||
25 | val typeMap = new HashMap<Type, Integer> | 91 | val typeMap = new HashMap<Type, Integer> |
26 | val listMap = metamodel.classes.toMap[s|s.name] | 92 | val listMap = metamodel.classes.toMap[s|s.name] |
27 | 93 | ||
28 | for (Class elem : classMap.keySet) { | 94 | for (Class elem : classMap.keySet) { |
29 | typeMap.put(e2l.TypeofEClass( | 95 | typeMap.put(e2l.TypeofEClass( |
30 | trace, listMap.get(elem.simpleName) | 96 | trace, |
31 | ), classMap.get(elem)) | 97 | listMap.get(elem.simpleName) |
98 | ), classMap.get(elem)) | ||
32 | } | 99 | } |
33 | return typeMap | 100 | return typeMap |
34 | } | 101 | } |
@@ -43,7 +110,7 @@ class GeneralTest { | |||
43 | } | 110 | } |
44 | 111 | ||
45 | def static loadPartialModel(ReasonerWorkspace inputs, String path) { | 112 | def static loadPartialModel(ReasonerWorkspace inputs, String path) { |
46 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); | 113 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()) |
47 | inputs.readModel(EObject, path).eResource.contents | 114 | inputs.readModel(EObject, path).eResource.contents |
48 | // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList | 115 | // inputs.readModel(EObject,"FamInstance.xmi").eResource.allContents.toList |
49 | } | 116 | } |
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 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns | 3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
6 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage | 9 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
13 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | 14 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore |
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | 15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic |
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | 16 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration |
@@ -17,8 +18,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.Insta | |||
17 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 18 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
18 | import java.io.PrintWriter | 19 | import java.io.PrintWriter |
19 | import java.text.SimpleDateFormat | 20 | import java.text.SimpleDateFormat |
20 | import java.time.LocalDate | ||
21 | import java.util.Date | 21 | import java.util.Date |
22 | import java.util.HashMap | ||
22 | import org.eclipse.emf.ecore.resource.Resource | 23 | import org.eclipse.emf.ecore.resource.Resource |
23 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 24 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
24 | 25 | ||
@@ -54,16 +55,18 @@ class YakinduTest { | |||
54 | // val queries = null | 55 | // val queries = null |
55 | println("DSL loaded") | 56 | println("DSL loaded") |
56 | 57 | ||
57 | var MAX = 80 | 58 | var SZ_TOP = 10 |
58 | var START = 79 | 59 | var SZ_BOT = 126 |
59 | var INC = 1 | 60 | var INC = 1 |
60 | var REPS = 3 | 61 | var REPS = 1 |
62 | |||
63 | val RANGE = 3 | ||
61 | 64 | ||
62 | val EXACT = 130 | 65 | val EXACT = 10 |
63 | if (EXACT != -1) { | 66 | if (EXACT != -1) { |
64 | MAX = EXACT | 67 | SZ_TOP = EXACT |
65 | START = EXACT | 68 | SZ_BOT = EXACT |
66 | INC = 5 | 69 | INC = 1 |
67 | REPS = 1 | 70 | REPS = 1 |
68 | } | 71 | } |
69 | 72 | ||
@@ -77,8 +80,8 @@ class YakinduTest { | |||
77 | var transformationTimes = newArrayList | 80 | var transformationTimes = newArrayList |
78 | var modelFound = true | 81 | var modelFound = true |
79 | var LogicResult solution = null | 82 | var LogicResult solution = null |
80 | for (var i = START; i <= MAX; i += INC) { | 83 | for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { |
81 | val num = (i - START) / INC | 84 | val num = (i - SZ_BOT) / INC |
82 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") | 85 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") |
83 | writer.append(i + ",") | 86 | writer.append(i + ",") |
84 | solverTimes.clear | 87 | solverTimes.clear |
@@ -106,17 +109,16 @@ class YakinduTest { | |||
106 | 109 | ||
107 | // ///////////////////////////////////////////////////// | 110 | // ///////////////////////////////////////////////////// |
108 | // Minimum Scope | 111 | // Minimum Scope |
109 | // val classMapMin = new HashMap<Class, Integer> | 112 | val classMapMin = new HashMap<Class, Integer> |
110 | // classMapMin.put(Region, 1) | 113 | classMapMin.put(Region, 1) |
111 | // classMapMin.put(Transition, 2) | 114 | classMapMin.put(Transition, 2) |
112 | // classMapMin.put(CompositeElement, 3) | 115 | classMapMin.put(CompositeElement, 3) |
113 | // val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) | 116 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) |
114 | // Maximum Scope | 117 | // Maximum Scope |
115 | // val classMapMax = new HashMap<Class, Integer> | 118 | val classMapMax = new HashMap<Class, Integer> |
116 | // classMapMax.put(Region, 5) | 119 | classMapMax.put(Region, 5) |
117 | // classMapMax.put(Transition, 2) | 120 | classMapMax.put(Transition, 2) |
118 | // classMapMax.put(Synchronization, 4) | 121 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) |
119 | // val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | ||
120 | // Define Config File | 122 | // Define Config File |
121 | val size = i | 123 | val size = i |
122 | val inc = INC | 124 | val inc = INC |
@@ -126,18 +128,18 @@ class YakinduTest { | |||
126 | it.documentationLevel = DocumentationLevel::FULL | 128 | it.documentationLevel = DocumentationLevel::FULL |
127 | it.iteration = iter | 129 | it.iteration = iter |
128 | it.runtimeLimit = 60 | 130 | it.runtimeLimit = 60 |
129 | it.typeScopes.maxNewElements = size | 131 | it.typeScopes.maxNewElements = -1 |
130 | it.typeScopes.minNewElements = size - 5 | 132 | it.typeScopes.minNewElements = size |
131 | 133 | it.genModel = false | |
132 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 134 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
133 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 135 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
134 | it.contCycleLevel = 5 | 136 | it.contCycleLevel = 5 |
135 | it.uniquenessDuplicates = false | 137 | it.uniquenessDuplicates = false |
136 | ] | 138 | ] |
137 | 139 | ||
138 | solution = reasoner.solve(problem, vampireConfig, workspace) | 140 | solution = reasoner.solve(problem, vampireConfig, workspace) |
139 | // print((solution as ModelResult).representation.get(0)) | 141 | // print((solution as ModelResult).representation.get(0)) |
140 | val soln = ((solution as ModelResult).representation.get(0) as VampireModel) | 142 | // val soln = ((solution as ModelResult).representation.get(0) as VampireModel) |
141 | // println(soln.confirmations) | 143 | // println(soln.confirmations) |
142 | // println((solution as ModelResult).representation) | 144 | // println((solution as ModelResult).representation) |
143 | // modelFound = !soln.confirmations.filter [ | 145 | // 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 --- 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 | |||