diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-12 23:10:19 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-12 23:10:19 -0400 |
commit | e0fc38cb9a22bf0c21053361a22b8fa167f30625 (patch) | |
tree | 35b063b75bc970594ca496297fb57de2b9776776 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test | |
parent | VAMPIRE: complete testing setup (diff) | |
download | VIATRA-Generator-e0fc38cb9a22bf0c21053361a22b8fa167f30625.tar.gz VIATRA-Generator-e0fc38cb9a22bf0c21053361a22b8fa167f30625.tar.zst VIATRA-Generator-e0fc38cb9a22bf0c21053361a22b8fa167f30625.zip |
VAMPIRE: complete data collection and code setup
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test')
3 files changed, 15 insertions, 15 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 9121367b..26b91525 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 = 30 | 62 | var SZ_TOP = 150 |
63 | var SZ_BOT = 5 | 63 | var SZ_BOT = 150 |
64 | var INC = 5 | 64 | var INC = 10 |
65 | var REPS = 1 | 65 | var REPS = 10 |
66 | 66 | ||
67 | val RUNTIME = 20 | 67 | val RUNTIME = 300 |
68 | 68 | ||
69 | val EXACT = -1 | 69 | val EXACT = -1 |
70 | if (EXACT != -1) { | 70 | if (EXACT != -1) { |
@@ -82,13 +82,13 @@ class YakinduTest { | |||
82 | // , | 82 | // , |
83 | // BackendSolver::GEOIII | 83 | // BackendSolver::GEOIII |
84 | // , | 84 | // , |
85 | BackendSolver::IPROVER | 85 | // BackendSolver::IPROVER |
86 | // , | 86 | // , |
87 | // BackendSolver::PARADOX | 87 | // BackendSolver::PARADOX |
88 | // , | 88 | // , |
89 | // BackendSolver::VAMPIRE | 89 | // BackendSolver::VAMPIRE |
90 | // , | 90 | // , |
91 | // BackendSolver::Z3 | 91 | BackendSolver::Z3 |
92 | ) | 92 | ) |
93 | 93 | ||
94 | 94 | ||
@@ -197,7 +197,7 @@ class YakinduTest { | |||
197 | writer.append(satOut + ",") | 197 | writer.append(satOut + ",") |
198 | writer.append(satTime + ",") | 198 | writer.append(satTime + ",") |
199 | writer.append(modOut + ",") | 199 | writer.append(modOut + ",") |
200 | writer.append(modTime + ",") | 200 | writer.append(modTime + "") |
201 | writer.append("\n") | 201 | writer.append("\n") |
202 | 202 | ||
203 | // print("(" + tTime + "/" + sTime + "s)..") | 203 | // print("(" + tTime + "/" + sTime + "s)..") |
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 cf52d6a6..b29e18b1 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 1837b768..c2aaee03 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 | |||
@@ -85,11 +85,11 @@ public class YakinduTest { | |||
85 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); | 85 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); |
86 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); | 86 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); |
87 | InputOutput.<String>println("DSL loaded"); | 87 | InputOutput.<String>println("DSL loaded"); |
88 | int SZ_TOP = 30; | 88 | int SZ_TOP = 150; |
89 | int SZ_BOT = 5; | 89 | int SZ_BOT = 150; |
90 | int INC = 5; | 90 | int INC = 10; |
91 | int REPS = 1; | 91 | int REPS = 10; |
92 | final int RUNTIME = 20; | 92 | final int RUNTIME = 300; |
93 | final int EXACT = (-1); | 93 | final int EXACT = (-1); |
94 | if ((EXACT != (-1))) { | 94 | if ((EXACT != (-1))) { |
95 | SZ_TOP = EXACT; | 95 | SZ_TOP = EXACT; |
@@ -98,7 +98,7 @@ public class YakinduTest { | |||
98 | REPS = 10; | 98 | REPS = 10; |
99 | } | 99 | } |
100 | final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList( | 100 | final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList( |
101 | BackendSolver.IPROVER); | 101 | BackendSolver.Z3); |
102 | String str = ""; | 102 | String str = ""; |
103 | for (final BackendSolver solver : BACKENDSOLVERS) { | 103 | for (final BackendSolver solver : BACKENDSOLVERS) { |
104 | String _str = str; | 104 | String _str = str; |
@@ -218,7 +218,7 @@ public class YakinduTest { | |||
218 | String _plus_20 = (Double.valueOf(satTime) + ","); | 218 | String _plus_20 = (Double.valueOf(satTime) + ","); |
219 | writer.append(_plus_20); | 219 | writer.append(_plus_20); |
220 | writer.append((modOut + ",")); | 220 | writer.append((modOut + ",")); |
221 | String _plus_21 = (Double.valueOf(modTime) + ","); | 221 | String _plus_21 = (Double.valueOf(modTime) + ""); |
222 | writer.append(_plus_21); | 222 | writer.append(_plus_21); |
223 | writer.append("\n"); | 223 | writer.append("\n"); |
224 | } | 224 | } |