diff options
Diffstat (limited to 'Tests')
10 files changed, 34 insertions, 27 deletions
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 26b91525..f26a1c91 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 | |||
@@ -59,12 +59,12 @@ class YakinduTest { | |||
59 | // val queries = null | 59 | // val queries = null |
60 | println("DSL loaded") | 60 | println("DSL loaded") |
61 | 61 | ||
62 | var SZ_TOP = 150 | 62 | var SZ_TOP = 25 |
63 | var SZ_BOT = 150 | 63 | var SZ_BOT = 5 |
64 | var INC = 10 | 64 | var INC = 5 |
65 | var REPS = 10 | 65 | var REPS = 5 |
66 | 66 | ||
67 | val RUNTIME = 300 | 67 | val RUNTIME = 60 |
68 | 68 | ||
69 | val EXACT = -1 | 69 | val EXACT = -1 |
70 | if (EXACT != -1) { | 70 | if (EXACT != -1) { |
@@ -88,7 +88,9 @@ class YakinduTest { | |||
88 | // , | 88 | // , |
89 | // BackendSolver::VAMPIRE | 89 | // BackendSolver::VAMPIRE |
90 | // , | 90 | // , |
91 | BackendSolver::Z3 | 91 | // BackendSolver::Z3 |
92 | // , | ||
93 | BackendSolver::LOCVAMP | ||
92 | ) | 94 | ) |
93 | 95 | ||
94 | 96 | ||
@@ -163,12 +165,17 @@ class YakinduTest { | |||
163 | it.typeScopes.minNewElements = size | 165 | it.typeScopes.minNewElements = size |
164 | 166 | ||
165 | it.genModel = true | 167 | it.genModel = true |
166 | it.server = true | 168 | it.server = false |
167 | it.solver = BESOLVER | 169 | if(it.server){ |
170 | it.solver = BESOLVER | ||
171 | } else{ | ||
172 | it.solver = BackendSolver::LOCVAMP | ||
173 | } | ||
174 | |||
168 | 175 | ||
169 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 176 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
170 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 177 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
171 | it.contCycleLevel = 5 | 178 | // it.contCycleLevel = 5 |
172 | it.uniquenessDuplicates = false | 179 | it.uniquenessDuplicates = false |
173 | ] | 180 | ] |
174 | 181 | ||
@@ -187,11 +194,11 @@ class YakinduTest { | |||
187 | 194 | ||
188 | val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry). | 195 | val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry). |
189 | value | 196 | value |
190 | val satTime = (solution.statistics.entries.filter[name == "satTime"].get(0) as RealStatisticEntry). | 197 | val satTime = (solution.statistics.entries.filter[name == "satTime"].get(0) as StringStatisticEntry). |
191 | value | 198 | value |
192 | val modOut = (solution.statistics.entries.filter[name == "modOut"].get(0) as StringStatisticEntry). | 199 | val modOut = (solution.statistics.entries.filter[name == "modOut"].get(0) as StringStatisticEntry). |
193 | value | 200 | value |
194 | val modTime = (solution.statistics.entries.filter[name == "modTime"].get(0) as RealStatisticEntry). | 201 | val modTime = (solution.statistics.entries.filter[name == "modTime"].get(0) as StringStatisticEntry). |
195 | value | 202 | value |
196 | 203 | ||
197 | writer.append(satOut + ",") | 204 | writer.append(satOut + ",") |
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 5dc01040..1174c9aa 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 e96cf904..369ae25b 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 688908b9..d66e9ca0 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 0d18615c..19872b6a 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 b29e18b1..1e5c3981 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/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java index c2aaee03..c46f75d2 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 | |||
@@ -19,7 +19,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | |||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | 20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; |
21 | 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; | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry; |
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; | 23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry; |
25 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | 24 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; |
@@ -85,11 +84,11 @@ public class YakinduTest { | |||
85 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); | 84 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); |
86 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); | 85 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); |
87 | InputOutput.<String>println("DSL loaded"); | 86 | InputOutput.<String>println("DSL loaded"); |
88 | int SZ_TOP = 150; | 87 | int SZ_TOP = 25; |
89 | int SZ_BOT = 150; | 88 | int SZ_BOT = 5; |
90 | int INC = 10; | 89 | int INC = 5; |
91 | int REPS = 10; | 90 | int REPS = 5; |
92 | final int RUNTIME = 300; | 91 | final int RUNTIME = 60; |
93 | final int EXACT = (-1); | 92 | final int EXACT = (-1); |
94 | if ((EXACT != (-1))) { | 93 | if ((EXACT != (-1))) { |
95 | SZ_TOP = EXACT; | 94 | SZ_TOP = EXACT; |
@@ -98,7 +97,7 @@ public class YakinduTest { | |||
98 | REPS = 10; | 97 | REPS = 10; |
99 | } | 98 | } |
100 | final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList( | 99 | final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList( |
101 | BackendSolver.Z3); | 100 | BackendSolver.LOCVAMP); |
102 | String str = ""; | 101 | String str = ""; |
103 | for (final BackendSolver solver : BACKENDSOLVERS) { | 102 | for (final BackendSolver solver : BACKENDSOLVERS) { |
104 | String _str = str; | 103 | String _str = str; |
@@ -174,9 +173,12 @@ public class YakinduTest { | |||
174 | it.runtimeLimit = RUNTIME; | 173 | it.runtimeLimit = RUNTIME; |
175 | it.typeScopes.minNewElements = size; | 174 | it.typeScopes.minNewElements = size; |
176 | it.genModel = true; | 175 | it.genModel = true; |
177 | it.server = true; | 176 | it.server = false; |
178 | it.solver = BESOLVER; | 177 | if (it.server) { |
179 | it.contCycleLevel = 5; | 178 | it.solver = BESOLVER; |
179 | } else { | ||
180 | it.solver = BackendSolver.LOCVAMP; | ||
181 | } | ||
180 | it.uniquenessDuplicates = false; | 182 | it.uniquenessDuplicates = false; |
181 | }; | 183 | }; |
182 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | 184 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); |
@@ -201,7 +203,7 @@ public class YakinduTest { | |||
201 | return Boolean.valueOf(Objects.equal(_name_2, "satTime")); | 203 | return Boolean.valueOf(Objects.equal(_name_2, "satTime")); |
202 | }; | 204 | }; |
203 | StatisticEntry _get_1 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_2), StatisticEntry.class))[0]; | 205 | 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(); | 206 | final String satTime = ((StringStatisticEntry) _get_1).getValue(); |
205 | final Function1<StatisticEntry, Boolean> _function_3 = (StatisticEntry it) -> { | 207 | final Function1<StatisticEntry, Boolean> _function_3 = (StatisticEntry it) -> { |
206 | String _name_2 = it.getName(); | 208 | String _name_2 = it.getName(); |
207 | return Boolean.valueOf(Objects.equal(_name_2, "modOut")); | 209 | return Boolean.valueOf(Objects.equal(_name_2, "modOut")); |
@@ -213,13 +215,11 @@ public class YakinduTest { | |||
213 | return Boolean.valueOf(Objects.equal(_name_2, "modTime")); | 215 | return Boolean.valueOf(Objects.equal(_name_2, "modTime")); |
214 | }; | 216 | }; |
215 | StatisticEntry _get_3 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_4), StatisticEntry.class))[0]; | 217 | 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(); | 218 | final String modTime = ((StringStatisticEntry) _get_3).getValue(); |
217 | writer.append((satOut + ",")); | 219 | writer.append((satOut + ",")); |
218 | String _plus_20 = (Double.valueOf(satTime) + ","); | 220 | writer.append((satTime + ",")); |
219 | writer.append(_plus_20); | ||
220 | writer.append((modOut + ",")); | 221 | writer.append((modOut + ",")); |
221 | String _plus_21 = (Double.valueOf(modTime) + ""); | 222 | writer.append((modTime + "")); |
222 | writer.append(_plus_21); | ||
223 | writer.append("\n"); | 223 | writer.append("\n"); |
224 | } | 224 | } |
225 | } | 225 | } |
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 b596dc1f..41df0b2f 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 e1434d74..9bf38940 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 50068d97..54f2770d 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 | |||