diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse')
7 files changed, 146 insertions, 172 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 93d27b4d..5dc01040 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 bc2bae6f..e96cf904 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 5687258f..688908b9 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 de68a908..0d18615c 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 16a3cd03..cf52d6a6 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/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java index ce057092..bdea5746 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,11 +13,6 @@ 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; | ||
21 | import org.eclipse.emf.common.util.EList; | 16 | import org.eclipse.emf.common.util.EList; |
22 | import org.eclipse.emf.ecore.EAttribute; | 17 | import org.eclipse.emf.ecore.EAttribute; |
23 | import org.eclipse.emf.ecore.EClass; | 18 | import org.eclipse.emf.ecore.EClass; |
@@ -33,75 +28,12 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup; | |||
33 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; | 28 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification; |
34 | import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; | 29 | import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; |
35 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 30 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
36 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
37 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | 31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; |
38 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
39 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | 32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; |
40 | import org.eclipse.xtext.xbase.lib.ListExtensions; | 33 | import org.eclipse.xtext.xbase.lib.ListExtensions; |
41 | 34 | ||
42 | @SuppressWarnings("all") | 35 | @SuppressWarnings("all") |
43 | public class GeneralTest { | 36 | 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 | |||
105 | public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { | 37 | public static Map<Type, Integer> getTypeMap(final Map<Class, Integer> classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { |
106 | final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>(); | 38 | final HashMap<Type, Integer> typeMap = new HashMap<Type, Integer>(); |
107 | final Function1<EClass, String> _function = (EClass s) -> { | 39 | final Function1<EClass, String> _function = (EClass s) -> { |
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 3a8f3fb4..1837b768 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 | |||
@@ -2,12 +2,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; | |||
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; | 3 | 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.BackendSolver; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 7 | 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.CompositeElement; |
8 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region; | 9 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region; |
9 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition; | 10 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition; |
10 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; | 11 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; |
12 | import com.google.common.base.Objects; | ||
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; | 13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; |
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; | 14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; |
13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; | 15 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; |
@@ -17,6 +19,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | |||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | 25 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; |
21 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; | 26 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; |
22 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; | 27 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; |
@@ -37,7 +42,9 @@ import org.eclipse.emf.ecore.resource.Resource; | |||
37 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; | 42 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; |
38 | import org.eclipse.xtend2.lib.StringConcatenation; | 43 | import org.eclipse.xtend2.lib.StringConcatenation; |
39 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 44 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
45 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
40 | import org.eclipse.xtext.xbase.lib.Exceptions; | 46 | import org.eclipse.xtext.xbase.lib.Exceptions; |
47 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
41 | import org.eclipse.xtext.xbase.lib.InputOutput; | 48 | import org.eclipse.xtext.xbase.lib.InputOutput; |
42 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | 49 | import org.eclipse.xtext.xbase.lib.IterableExtensions; |
43 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 50 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
@@ -53,17 +60,20 @@ public class YakinduTest { | |||
53 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); | 60 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); |
54 | long _currentTimeMillis = System.currentTimeMillis(); | 61 | long _currentTimeMillis = System.currentTimeMillis(); |
55 | final Date date = new Date(_currentTimeMillis); | 62 | final Date date = new Date(_currentTimeMillis); |
56 | final SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss"); | 63 | final SimpleDateFormat format = new SimpleDateFormat("dd-HHmm"); |
57 | final String formattedDate = format.format(date); | 64 | final String formattedDate = format.format(date); |
58 | StringConcatenation _builder = new StringConcatenation(); | 65 | StringConcatenation _builder = new StringConcatenation(); |
59 | _builder.append("initialModels/"); | 66 | _builder.append("initialModels/"); |
60 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); | 67 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); |
61 | StringConcatenation _builder_1 = new StringConcatenation(); | 68 | StringConcatenation _builder_1 = new StringConcatenation(); |
62 | _builder_1.append("output/YakinduTest/"); | 69 | _builder_1.append("output/YakinduTest/"); |
63 | String _plus = (_builder_1.toString() + formattedDate); | 70 | final FileSystemWorkspace dataWorkspace = new FileSystemWorkspace(_builder_1.toString(), ""); |
64 | StringConcatenation _builder_2 = new StringConcatenation(); | 71 | StringConcatenation _builder_2 = new StringConcatenation(); |
65 | _builder_2.append("/"); | 72 | _builder_2.append("output/YakinduTest/"); |
66 | String _plus_1 = (_plus + _builder_2); | 73 | String _plus = (_builder_2.toString() + formattedDate); |
74 | StringConcatenation _builder_3 = new StringConcatenation(); | ||
75 | _builder_3.append("/"); | ||
76 | String _plus_1 = (_plus + _builder_3); | ||
67 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, ""); | 77 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, ""); |
68 | workspace.initAndClear(); | 78 | workspace.initAndClear(); |
69 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; | 79 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; |
@@ -75,117 +85,149 @@ public class YakinduTest { | |||
75 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); | 85 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); |
76 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); | 86 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); |
77 | InputOutput.<String>println("DSL loaded"); | 87 | InputOutput.<String>println("DSL loaded"); |
78 | int SZ_TOP = 10; | 88 | int SZ_TOP = 30; |
79 | int SZ_BOT = 126; | 89 | int SZ_BOT = 5; |
80 | int INC = 1; | 90 | int INC = 5; |
81 | int REPS = 1; | 91 | int REPS = 1; |
82 | final int RANGE = 3; | 92 | final int RUNTIME = 20; |
83 | final int EXACT = 10; | 93 | final int EXACT = (-1); |
84 | if ((EXACT != (-1))) { | 94 | if ((EXACT != (-1))) { |
85 | SZ_TOP = EXACT; | 95 | SZ_TOP = EXACT; |
86 | SZ_BOT = EXACT; | 96 | SZ_BOT = EXACT; |
87 | INC = 1; | 97 | INC = 1; |
88 | REPS = 1; | 98 | REPS = 10; |
89 | } | 99 | } |
90 | URI _workspaceURI = workspace.getWorkspaceURI(); | 100 | final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList( |
91 | String _plus_2 = (_workspaceURI + "//_yakinduStats.csv"); | 101 | BackendSolver.IPROVER); |
92 | PrintWriter writer = new PrintWriter(_plus_2); | 102 | String str = ""; |
93 | writer.append("size,"); | 103 | for (final BackendSolver solver : BACKENDSOLVERS) { |
94 | for (int x = 0; (x < REPS); x++) { | 104 | String _str = str; |
95 | writer.append(((((("tTransf" + Integer.valueOf(x)) + ",") + "tSolv") + Integer.valueOf(x)) + ",")); | 105 | String _substring = solver.name().substring(0, 1); |
106 | str = (_str + _substring); | ||
96 | } | 107 | } |
97 | writer.append("medSolv,medTransf\n"); | 108 | URI _workspaceURI = dataWorkspace.getWorkspaceURI(); |
98 | ArrayList<Double> solverTimes = CollectionLiterals.<Double>newArrayList(); | 109 | String _plus_2 = (_workspaceURI + "//_stats"); |
99 | ArrayList<Double> transformationTimes = CollectionLiterals.<Double>newArrayList(); | 110 | String _plus_3 = (_plus_2 + formattedDate); |
100 | boolean modelFound = true; | 111 | String _plus_4 = (_plus_3 + "-"); |
112 | String _plus_5 = (_plus_4 + str); | ||
113 | String _plus_6 = (_plus_5 + Integer.valueOf(SZ_BOT)); | ||
114 | String _plus_7 = (_plus_6 + "to"); | ||
115 | String _plus_8 = (_plus_7 + Integer.valueOf(SZ_TOP)); | ||
116 | String _plus_9 = (_plus_8 + "by"); | ||
117 | String _plus_10 = (_plus_9 + Integer.valueOf(INC)); | ||
118 | String _plus_11 = (_plus_10 + | ||
119 | "x"); | ||
120 | String _plus_12 = (_plus_11 + Integer.valueOf(REPS)); | ||
121 | String _plus_13 = (_plus_12 + ".csv"); | ||
122 | PrintWriter writer = new PrintWriter(_plus_13); | ||
123 | writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n"); | ||
124 | ArrayList<Object> solverTimes = CollectionLiterals.<Object>newArrayList(); | ||
125 | ArrayList<Object> transformationTimes = CollectionLiterals.<Object>newArrayList(); | ||
101 | LogicResult solution = null; | 126 | LogicResult solution = null; |
102 | { | 127 | for (final BackendSolver BESOLVER : BACKENDSOLVERS) { |
103 | int i = SZ_BOT; | 128 | { |
104 | boolean _while = (i <= SZ_TOP); | 129 | int i = SZ_BOT; |
105 | while (_while) { | 130 | boolean _while = (i <= SZ_TOP); |
106 | { | 131 | while (_while) { |
107 | final int num = ((i - SZ_BOT) / INC); | 132 | { |
108 | InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); | 133 | final int num = ((i - SZ_BOT) / INC); |
109 | String _plus_3 = (Integer.valueOf(i) + ","); | 134 | InputOutput.println(); |
110 | writer.append(_plus_3); | 135 | String _name = BESOLVER.name(); |
111 | solverTimes.clear(); | 136 | String _plus_14 = ("SOLVER: " + _name); |
112 | transformationTimes.clear(); | 137 | String _plus_15 = (_plus_14 + ", SIZE="); |
113 | modelFound = true; | 138 | String _plus_16 = (_plus_15 + Integer.valueOf(i)); |
114 | for (int j = 0; (j < REPS); j++) { | 139 | InputOutput.<String>println(_plus_16); |
115 | { | 140 | InputOutput.println(); |
116 | InputOutput.<Integer>print(Integer.valueOf(j)); | 141 | solverTimes.clear(); |
117 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); | 142 | transformationTimes.clear(); |
118 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); | 143 | for (int j = 0; (j < REPS); j++) { |
119 | TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); | 144 | { |
120 | Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); | 145 | InputOutput.<String>print((("<<Run number " + Integer.valueOf(j)) + ">> :")); |
121 | TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration); | 146 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); |
122 | LogicProblem problem = modelGenerationProblem.getOutput(); | 147 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); |
123 | workspace.writeModel(problem, "Yakindu.logicproblem"); | 148 | TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); |
124 | long startTime = System.currentTimeMillis(); | 149 | Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); |
125 | VampireSolver reasoner = null; | 150 | TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration); |
126 | VampireSolver _vampireSolver = new VampireSolver(); | 151 | LogicProblem problem = modelGenerationProblem.getOutput(); |
127 | reasoner = _vampireSolver; | 152 | long startTime = System.currentTimeMillis(); |
128 | final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); | 153 | VampireSolver reasoner = null; |
129 | classMapMin.put(Region.class, Integer.valueOf(1)); | 154 | VampireSolver _vampireSolver = new VampireSolver(); |
130 | classMapMin.put(Transition.class, Integer.valueOf(2)); | 155 | reasoner = _vampireSolver; |
131 | classMapMin.put(CompositeElement.class, Integer.valueOf(3)); | 156 | final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); |
132 | final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); | 157 | classMapMin.put(Region.class, Integer.valueOf(1)); |
133 | final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); | 158 | classMapMin.put(Transition.class, Integer.valueOf(2)); |
134 | classMapMax.put(Region.class, Integer.valueOf(5)); | 159 | classMapMin.put(CompositeElement.class, Integer.valueOf(3)); |
135 | classMapMax.put(Transition.class, Integer.valueOf(2)); | 160 | final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, |
136 | final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); | 161 | modelGenerationProblem.getTrace()); |
137 | final int size = i; | 162 | final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); |
138 | final int inc = INC; | 163 | classMapMax.put(Region.class, Integer.valueOf(5)); |
139 | final int iter = j; | 164 | classMapMax.put(Transition.class, Integer.valueOf(2)); |
140 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); | 165 | final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, |
141 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { | 166 | modelGenerationProblem.getTrace()); |
142 | it.documentationLevel = DocumentationLevel.FULL; | 167 | final int size = i; |
143 | it.iteration = iter; | 168 | final int inc = INC; |
144 | it.runtimeLimit = 60; | 169 | final int iter = j; |
145 | it.typeScopes.maxNewElements = (-1); | 170 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); |
146 | it.typeScopes.minNewElements = size; | 171 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { |
147 | it.genModel = false; | 172 | it.documentationLevel = DocumentationLevel.FULL; |
148 | int _size = typeMapMin.size(); | 173 | it.iteration = iter; |
149 | boolean _notEquals = (_size != 0); | 174 | it.runtimeLimit = RUNTIME; |
150 | if (_notEquals) { | 175 | it.typeScopes.minNewElements = size; |
151 | it.typeScopes.minNewElementsByType = typeMapMin; | 176 | it.genModel = true; |
152 | } | 177 | it.server = true; |
153 | int _size_1 = typeMapMin.size(); | 178 | it.solver = BESOLVER; |
154 | boolean _notEquals_1 = (_size_1 != 0); | 179 | it.contCycleLevel = 5; |
155 | if (_notEquals_1) { | 180 | it.uniquenessDuplicates = false; |
156 | it.typeScopes.maxNewElementsByType = typeMapMax; | 181 | }; |
157 | } | 182 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); |
158 | it.contCycleLevel = 5; | 183 | solution = reasoner.solve(problem, vampireConfig, workspace); |
159 | it.uniquenessDuplicates = false; | 184 | String _name_1 = vampireConfig.solver.name(); |
160 | }; | 185 | String _plus_17 = (_name_1 + ","); |
161 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | 186 | writer.append(_plus_17); |
162 | solution = reasoner.solve(problem, vampireConfig, workspace); | 187 | String _plus_18 = (Integer.valueOf(size) + ","); |
163 | int _transformationTime = solution.getStatistics().getTransformationTime(); | 188 | writer.append(_plus_18); |
164 | final double tTime = (_transformationTime / 1000.0); | 189 | int _transformationTime = solution.getStatistics().getTransformationTime(); |
165 | int _solverTime = solution.getStatistics().getSolverTime(); | 190 | double _divide = (_transformationTime / 1000.0); |
166 | final double sTime = (_solverTime / 1000.0); | 191 | String _plus_19 = (Double.valueOf(_divide) + ","); |
167 | String _plus_4 = (Double.valueOf(tTime) + ","); | 192 | writer.append(_plus_19); |
168 | String _plus_5 = (_plus_4 + Double.valueOf(sTime)); | 193 | final Function1<StatisticEntry, Boolean> _function_1 = (StatisticEntry it) -> { |
169 | String _plus_6 = (_plus_5 + ","); | 194 | String _name_2 = it.getName(); |
170 | writer.append(_plus_6); | 195 | return Boolean.valueOf(Objects.equal(_name_2, "satOut")); |
171 | InputOutput.<String>print((((("(" + Double.valueOf(tTime)) + "/") + Double.valueOf(sTime)) + "s)..")); | 196 | }; |
172 | solverTimes.add(Double.valueOf(sTime)); | 197 | StatisticEntry _get = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_1), StatisticEntry.class))[0]; |
173 | transformationTimes.add(Double.valueOf(tTime)); | 198 | final String satOut = ((StringStatisticEntry) _get).getValue(); |
199 | final Function1<StatisticEntry, Boolean> _function_2 = (StatisticEntry it) -> { | ||
200 | String _name_2 = it.getName(); | ||
201 | return Boolean.valueOf(Objects.equal(_name_2, "satTime")); | ||
202 | }; | ||
203 | StatisticEntry _get_1 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_2), StatisticEntry.class))[0]; | ||
204 | final double satTime = ((RealStatisticEntry) _get_1).getValue(); | ||
205 | final Function1<StatisticEntry, Boolean> _function_3 = (StatisticEntry it) -> { | ||
206 | String _name_2 = it.getName(); | ||
207 | return Boolean.valueOf(Objects.equal(_name_2, "modOut")); | ||
208 | }; | ||
209 | StatisticEntry _get_2 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_3), StatisticEntry.class))[0]; | ||
210 | final String modOut = ((StringStatisticEntry) _get_2).getValue(); | ||
211 | final Function1<StatisticEntry, Boolean> _function_4 = (StatisticEntry it) -> { | ||
212 | String _name_2 = it.getName(); | ||
213 | return Boolean.valueOf(Objects.equal(_name_2, "modTime")); | ||
214 | }; | ||
215 | StatisticEntry _get_3 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_4), StatisticEntry.class))[0]; | ||
216 | final double modTime = ((RealStatisticEntry) _get_3).getValue(); | ||
217 | writer.append((satOut + ",")); | ||
218 | String _plus_20 = (Double.valueOf(satTime) + ","); | ||
219 | writer.append(_plus_20); | ||
220 | writer.append((modOut + ",")); | ||
221 | String _plus_21 = (Double.valueOf(modTime) + ","); | ||
222 | writer.append(_plus_21); | ||
223 | writer.append("\n"); | ||
224 | } | ||
174 | } | 225 | } |
175 | } | 226 | } |
176 | InputOutput.println(); | 227 | int _i = i; |
177 | Double solverMed = IterableExtensions.<Double>sort(solverTimes).get((REPS / 2)); | 228 | i = (_i + INC); |
178 | Double transformationMed = IterableExtensions.<Double>sort(transformationTimes).get((REPS / 2)); | 229 | _while = (i <= SZ_TOP); |
179 | String _string = solverMed.toString(); | ||
180 | String _plus_4 = (_string + ","); | ||
181 | String _string_1 = transformationMed.toString(); | ||
182 | String _plus_5 = (_plus_4 + _string_1); | ||
183 | writer.append(_plus_5); | ||
184 | writer.append("\n"); | ||
185 | } | 230 | } |
186 | int _i = i; | ||
187 | i = (_i + INC); | ||
188 | _while = (i <= SZ_TOP); | ||
189 | } | 231 | } |
190 | } | 232 | } |
191 | writer.close(); | 233 | writer.close(); |