aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-07 04:54:42 +0100
committerLibravatar Aren Babikian <aren.babikian@mail.mcgill.ca>2021-02-07 04:54:42 +0100
commit9f02e7e2fe8b3e347f3d05e8d0751dec016842cd (patch)
tree6d0c34c617ed51c9c9715f3ec18552425656b3a5
parentRemove dreal (diff)
downloadVIATRA-Generator-9f02e7e2fe8b3e347f3d05e8d0751dec016842cd.tar.gz
VIATRA-Generator-9f02e7e2fe8b3e347f3d05e8d0751dec016842cd.tar.zst
VIATRA-Generator-9f02e7e2fe8b3e347f3d05e8d0751dec016842cd.zip
measurement setup is ready for server
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java35
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java7
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend1
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend2
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend12
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/.gitignore1
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/MODELS2020Plots-temp.ipynb143
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jarbin0 -> 78139397 bytes
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig13
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig101
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig107
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig10
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig107
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/plots/plot_RQ2_FamilyTree.pdfbin4775 -> 4527 bytes
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/plugin.xml2
-rwxr-xr-xTests/MODELS2020-CaseStudies/case.study.pledge.run/run.sh2
-rwxr-xr-xTests/MODELS2020-CaseStudies/case.study.pledge.run/runFamilyTree.sh15
-rwxr-xr-xTests/MODELS2020-CaseStudies/case.study.pledge.run/runSatellite.sh15
-rwxr-xr-xTests/MODELS2020-CaseStudies/case.study.pledge.run/runTaxation.sh15
-rwxr-xr-xTests/MODELS2020-CaseStudies/case.study.pledge.run/runTest.sh6
-rw-r--r--Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend28
21 files changed, 340 insertions, 282 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
index 4fef6448..e0ebcb6b 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
@@ -43,7 +43,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
43 private Map<String, String> curVar2Decl; 43 private Map<String, String> curVar2Decl;
44 44
45 private final int TIMEOUT_DOCKER = 5000; 45 private final int TIMEOUT_DOCKER = 5000;
46 private final int TIMEOUT_LOCAL = 20000; 46 private final int TIMEOUT_LOCAL = 10000;
47 private final boolean DEBUG_PRINT = false;
47 48
48 public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException { 49 public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath) throws IOException, InterruptedException {
49 this.useDocker = useDocker; 50 this.useDocker = useDocker;
@@ -86,8 +87,10 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
86 } 87 }
87 return null; 88 return null;
88 } 89 }
89 double duration = (double) (System.nanoTime() - startTime) / 1000000000; 90 if (DEBUG_PRINT) {
90 System.out.println("Dur = " + duration + " : "); 91 double duration = (double) (System.nanoTime() - startTime) / 1000000000;
92 System.out.println("Dur = " + duration + " : ");
93 }
91 return p; 94 return p;
92 } 95 }
93 96
@@ -397,17 +400,15 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
397 } 400 }
398 endSolvingProblem = System.nanoTime()-startSolvingProblem; 401 endSolvingProblem = System.nanoTime()-startSolvingProblem;
399 402
400 //DEBUG - Print things 403 if (outputProcess == null) {
401 if (outputProcess == null) {
402
403 System.err.println("TIMEOUT"); 404 System.err.println("TIMEOUT");
404// printOutput(numProbContent); 405// printOutput(numProbContent);
405 } 406 }
406 407 if (DEBUG_PRINT) {
407// printOutput(numProbContent); 408 // printOutput(numProbContent);
408// if (outputs != null) printOutput(outputs.get(0)); 409 // if (outputs != null) printOutput(outputs.get(0));
409 System.out.println(result); 410 System.out.println(result);
410// END DEBUG 411 }
411 412
412 return result; 413 return result;
413 } 414 }
@@ -459,12 +460,12 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
459 boolean result = getDrealResult(outputProcess.exitValue(), outputs); 460 boolean result = getDrealResult(outputProcess.exitValue(), outputs);
460 endSolvingProblem = System.nanoTime()-startSolvingProblem; 461 endSolvingProblem = System.nanoTime()-startSolvingProblem;
461 462
462 //DEBUG - Print things 463 if (DEBUG_PRINT) {
463 System.out.println("Getting Solution!"); 464 System.out.println("Getting Solution!");
464// printOutput(numProbContent); 465 // printOutput(numProbContent);
465// printOutput(outputs.get(0)); 466 // printOutput(outputs.get(0));
466// System.out.println(result); 467 // System.out.println(result);
467 //END DEBUG 468 }
468 469
469 //GET SOLUTION 470 //GET SOLUTION
470 if (result) { 471 if (result) {
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
index 0e47e820..612e93a6 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java
@@ -39,9 +39,10 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
39 public NumericZ3ProblemSolver() { 39 public NumericZ3ProblemSolver() {
40 //FOR LINUX VM 40 //FOR LINUX VM
41 //Not Elegant, but this is working for now 41 //Not Elegant, but this is working for now
42 String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); 42// String root = "/home/models/VIATRA-Generator";
43 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); 43// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
44 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); 44// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
45// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
45 //End non-elegance 46 //End non-elegance
46 47
47 HashMap<String, String> cfg = new HashMap<String, String>(); 48 HashMap<String, String> cfg = new HashMap<String, String>();
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
index 1e2bbe6d..381823b3 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
@@ -195,6 +195,7 @@ class InstanceModel2PartialInterpretation {
195 EAttribute attribute, 195 EAttribute attribute,
196 Map<String, Map<String, String>> ignoredAttribs 196 Map<String, Map<String, String>> ignoredAttribs
197 ) { 197 ) {
198 if (ignoredAttribs === null || ignoredAttribs.isEmpty) return false;
198 val classInIgnored = ignoredAttribs.get(object.eClass.name) 199 val classInIgnored = ignoredAttribs.get(object.eClass.name)
199 val mayIgnored = ( 200 val mayIgnored = (
200 classInIgnored !== null && classInIgnored.containsKey("*") 201 classInIgnored !== null && classInIgnored.containsKey("*")
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
index fbcd6e1d..61a2ac41 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend
@@ -77,7 +77,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
77 public var nonContainmentWeight = 1 77 public var nonContainmentWeight = 1
78 public var unfinishedWFWeight = 1 78 public var unfinishedWFWeight = 1
79 public var calculateObjectCreationCosts = false 79 public var calculateObjectCreationCosts = false
80 public NumericSolverSelection numericSolverSelection = NumericSolverSelection.DREAL_DOCKER //currently defaulted to DREAL 80 public NumericSolverSelection numericSolverSelection = NumericSolverSelection.Z3 //currently defaulted to Z3
81 public var drealLocalPath = "<path-to-dreal>"; 81 public var drealLocalPath = "<path-to-dreal>";
82 public var Map<String, Map<String, String>> ignoredAttributesMap = null; 82 public var Map<String, Map<String, String>> ignoredAttributesMap = null;
83 83
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
index fc1a616b..b8ea25e5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend
@@ -53,7 +53,17 @@ class NumericSolver {
53 return new NumericDrealProblemSolver(true, null) 53 return new NumericDrealProblemSolver(true, null)
54 if (solverSelection == NumericSolverSelection.DREAL_LOCAL) 54 if (solverSelection == NumericSolverSelection.DREAL_LOCAL)
55 return new NumericDrealProblemSolver(false, drealLocalPath) 55 return new NumericDrealProblemSolver(false, drealLocalPath)
56 if (solverSelection == NumericSolverSelection.Z3) return new NumericZ3ProblemSolver 56 if (solverSelection == NumericSolverSelection.Z3) {
57 //TODO THIS IS HARD-CODED for now
58 val root = "/data/viatra/VIATRA-Generator";
59 //END HARD-CODED
60// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent();
61 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so");
62 System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so");
63// System.load("libz3.so");
64// System.load("libz3java.so");
65 return new NumericZ3ProblemSolver
66 }
57 } 67 }
58 68
59 def init(ThreadContext context) { 69 def init(ThreadContext context) {
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/.gitignore b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/.gitignore
index 18e1ed03..c2abd3d1 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/.gitignore
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/.gitignore
@@ -6,4 +6,5 @@
6/x/ 6/x/
7/.ipynb_checkpoints/ 7/.ipynb_checkpoints/
8/measurements1/ 8/measurements1/
9/measurements2/
9/archives/ 10/archives/
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/MODELS2020Plots-temp.ipynb b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/MODELS2020Plots-temp.ipynb
index cc342a87..dac7e324 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/MODELS2020Plots-temp.ipynb
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/MODELS2020Plots-temp.ipynb
@@ -146,7 +146,7 @@
146 }, 146 },
147 { 147 {
148 "cell_type": "code", 148 "cell_type": "code",
149 "execution_count": 6, 149 "execution_count": 4,
150 "metadata": {}, 150 "metadata": {},
151 "outputs": [], 151 "outputs": [],
152 "source": [ 152 "source": [
@@ -175,7 +175,7 @@
175 }, 175 },
176 { 176 {
177 "cell_type": "code", 177 "cell_type": "code",
178 "execution_count": 7, 178 "execution_count": 8,
179 "metadata": {}, 179 "metadata": {},
180 "outputs": [ 180 "outputs": [
181 { 181 {
@@ -184,15 +184,6 @@
184 "text": [ 184 "text": [
185 "Warning message:\n", 185 "Warning message:\n",
186 "“`cols` is now required when using unnest().\n", 186 "“`cols` is now required when using unnest().\n",
187 "Please use `cols = c(Solution1DetailedStatistics)`”\n",
188 "Warning message:\n",
189 "“`cols` is now required when using unnest().\n",
190 "Please use `cols = c(Solution1DetailedStatistics)`”\n",
191 "Warning message:\n",
192 "“`cols` is now required when using unnest().\n",
193 "Please use `cols = c(Solution1DetailedStatistics)`”\n",
194 "Warning message:\n",
195 "“`cols` is now required when using unnest().\n",
196 "Please use `cols = c(Solution1DetailedStatistics)`”\n" 187 "Please use `cols = c(Solution1DetailedStatistics)`”\n"
197 ] 188 ]
198 }, 189 },
@@ -200,54 +191,84 @@
200 "data": { 191 "data": {
201 "text/html": [ 192 "text/html": [
202 "<table>\n", 193 "<table>\n",
203 "<caption>A tibble: 4 × 8</caption>\n", 194 "<caption>A tibble: 10 × 8</caption>\n",
204 "<thead>\n", 195 "<thead>\n",
205 "\t<tr><th scope=col>n</th><th scope=col>Run</th><th scope=col>preprocessingTime</th><th scope=col>StateCoderTime</th><th scope=col>ForwardTime</th><th scope=col>BacktrackingTime</th><th scope=col>NumericalSolverSumTime</th><th scope=col>additionalTime</th></tr>\n", 196 "\t<tr><th scope=col>n</th><th scope=col>Run</th><th scope=col>preprocessingTime</th><th scope=col>StateCoderTime</th><th scope=col>ForwardTime</th><th scope=col>BacktrackingTime</th><th scope=col>NumericalSolverSumTime</th><th scope=col>additionalTime</th></tr>\n",
206 "\t<tr><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th></tr>\n", 197 "\t<tr><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th></tr>\n",
207 "</thead>\n", 198 "</thead>\n",
208 "<tbody>\n", 199 "<tbody>\n",
209 "\t<tr><td>20</td><td>1</td><td>33339</td><td> 878</td><td> 2654</td><td>1610</td><td> 7655</td><td> 39044</td></tr>\n", 200 "\t<tr><td>20</td><td> 1</td><td>2526</td><td>502</td><td>1125</td><td>904</td><td>7754</td><td> 9384</td></tr>\n",
210 "\t<tr><td>30</td><td>1</td><td>36670</td><td>2016</td><td> 5187</td><td>2687</td><td> 33695</td><td>103508</td></tr>\n", 201 "\t<tr><td>20</td><td> 2</td><td>2091</td><td>408</td><td> 745</td><td>645</td><td>7068</td><td> 7242</td></tr>\n",
211 "\t<tr><td>40</td><td>1</td><td>48868</td><td>3907</td><td> 9219</td><td>4814</td><td> 99075</td><td>309361</td></tr>\n", 202 "\t<tr><td>20</td><td> 3</td><td>2981</td><td>353</td><td> 884</td><td>724</td><td>8865</td><td> 9243</td></tr>\n",
212 "\t<tr><td>50</td><td>1</td><td>62541</td><td>5581</td><td>12720</td><td>5863</td><td>268490</td><td>552214</td></tr>\n", 203 "\t<tr><td>20</td><td> 4</td><td>1772</td><td>307</td><td> 595</td><td>510</td><td>7406</td><td> 6593</td></tr>\n",
204 "\t<tr><td>20</td><td> 5</td><td>2123</td><td>349</td><td> 786</td><td>580</td><td>8281</td><td> 9641</td></tr>\n",
205 "\t<tr><td>20</td><td> 6</td><td>1554</td><td>308</td><td> 670</td><td>690</td><td>7610</td><td> 7545</td></tr>\n",
206 "\t<tr><td>20</td><td> 7</td><td>1405</td><td>245</td><td> 612</td><td>547</td><td>7967</td><td>15679</td></tr>\n",
207 "\t<tr><td>20</td><td> 8</td><td>1764</td><td>232</td><td> 588</td><td>409</td><td>5559</td><td>15092</td></tr>\n",
208 "\t<tr><td>20</td><td> 9</td><td>1091</td><td>151</td><td> 269</td><td>228</td><td>3226</td><td> 5018</td></tr>\n",
209 "\t<tr><td>20</td><td>10</td><td>1974</td><td>319</td><td> 821</td><td>687</td><td>7977</td><td> 6758</td></tr>\n",
213 "</tbody>\n", 210 "</tbody>\n",
214 "</table>\n" 211 "</table>\n"
215 ], 212 ],
216 "text/latex": [ 213 "text/latex": [
217 "A tibble: 4 × 8\n", 214 "A tibble: 10 × 8\n",
218 "\\begin{tabular}{llllllll}\n", 215 "\\begin{tabular}{llllllll}\n",
219 " n & Run & preprocessingTime & StateCoderTime & ForwardTime & BacktrackingTime & NumericalSolverSumTime & additionalTime\\\\\n", 216 " n & Run & preprocessingTime & StateCoderTime & ForwardTime & BacktrackingTime & NumericalSolverSumTime & additionalTime\\\\\n",
220 " <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl>\\\\\n", 217 " <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl>\\\\\n",
221 "\\hline\n", 218 "\\hline\n",
222 "\t 20 & 1 & 33339 & 878 & 2654 & 1610 & 7655 & 39044\\\\\n", 219 "\t 20 & 1 & 2526 & 502 & 1125 & 904 & 7754 & 9384\\\\\n",
223 "\t 30 & 1 & 36670 & 2016 & 5187 & 2687 & 33695 & 103508\\\\\n", 220 "\t 20 & 2 & 2091 & 408 & 745 & 645 & 7068 & 7242\\\\\n",
224 "\t 40 & 1 & 48868 & 3907 & 9219 & 4814 & 99075 & 309361\\\\\n", 221 "\t 20 & 3 & 2981 & 353 & 884 & 724 & 8865 & 9243\\\\\n",
225 "\t 50 & 1 & 62541 & 5581 & 12720 & 5863 & 268490 & 552214\\\\\n", 222 "\t 20 & 4 & 1772 & 307 & 595 & 510 & 7406 & 6593\\\\\n",
223 "\t 20 & 5 & 2123 & 349 & 786 & 580 & 8281 & 9641\\\\\n",
224 "\t 20 & 6 & 1554 & 308 & 670 & 690 & 7610 & 7545\\\\\n",
225 "\t 20 & 7 & 1405 & 245 & 612 & 547 & 7967 & 15679\\\\\n",
226 "\t 20 & 8 & 1764 & 232 & 588 & 409 & 5559 & 15092\\\\\n",
227 "\t 20 & 9 & 1091 & 151 & 269 & 228 & 3226 & 5018\\\\\n",
228 "\t 20 & 10 & 1974 & 319 & 821 & 687 & 7977 & 6758\\\\\n",
226 "\\end{tabular}\n" 229 "\\end{tabular}\n"
227 ], 230 ],
228 "text/markdown": [ 231 "text/markdown": [
229 "\n", 232 "\n",
230 "A tibble: 4 × 8\n", 233 "A tibble: 10 × 8\n",
231 "\n", 234 "\n",
232 "| n &lt;dbl&gt; | Run &lt;dbl&gt; | preprocessingTime &lt;dbl&gt; | StateCoderTime &lt;dbl&gt; | ForwardTime &lt;dbl&gt; | BacktrackingTime &lt;dbl&gt; | NumericalSolverSumTime &lt;dbl&gt; | additionalTime &lt;dbl&gt; |\n", 235 "| n &lt;dbl&gt; | Run &lt;dbl&gt; | preprocessingTime &lt;dbl&gt; | StateCoderTime &lt;dbl&gt; | ForwardTime &lt;dbl&gt; | BacktrackingTime &lt;dbl&gt; | NumericalSolverSumTime &lt;dbl&gt; | additionalTime &lt;dbl&gt; |\n",
233 "|---|---|---|---|---|---|---|---|\n", 236 "|---|---|---|---|---|---|---|---|\n",
234 "| 20 | 1 | 33339 | 878 | 2654 | 1610 | 7655 | 39044 |\n", 237 "| 20 | 1 | 2526 | 502 | 1125 | 904 | 7754 | 9384 |\n",
235 "| 30 | 1 | 36670 | 2016 | 5187 | 2687 | 33695 | 103508 |\n", 238 "| 20 | 2 | 2091 | 408 | 745 | 645 | 7068 | 7242 |\n",
236 "| 40 | 1 | 48868 | 3907 | 9219 | 4814 | 99075 | 309361 |\n", 239 "| 20 | 3 | 2981 | 353 | 884 | 724 | 8865 | 9243 |\n",
237 "| 50 | 1 | 62541 | 5581 | 12720 | 5863 | 268490 | 552214 |\n", 240 "| 20 | 4 | 1772 | 307 | 595 | 510 | 7406 | 6593 |\n",
241 "| 20 | 5 | 2123 | 349 | 786 | 580 | 8281 | 9641 |\n",
242 "| 20 | 6 | 1554 | 308 | 670 | 690 | 7610 | 7545 |\n",
243 "| 20 | 7 | 1405 | 245 | 612 | 547 | 7967 | 15679 |\n",
244 "| 20 | 8 | 1764 | 232 | 588 | 409 | 5559 | 15092 |\n",
245 "| 20 | 9 | 1091 | 151 | 269 | 228 | 3226 | 5018 |\n",
246 "| 20 | 10 | 1974 | 319 | 821 | 687 | 7977 | 6758 |\n",
238 "\n" 247 "\n"
239 ], 248 ],
240 "text/plain": [ 249 "text/plain": [
241 " n Run preprocessingTime StateCoderTime ForwardTime BacktrackingTime\n", 250 " n Run preprocessingTime StateCoderTime ForwardTime BacktrackingTime\n",
242 "1 20 1 33339 878 2654 1610 \n", 251 "1 20 1 2526 502 1125 904 \n",
243 "2 30 1 36670 2016 5187 2687 \n", 252 "2 20 2 2091 408 745 645 \n",
244 "3 40 1 48868 3907 9219 4814 \n", 253 "3 20 3 2981 353 884 724 \n",
245 "4 50 1 62541 5581 12720 5863 \n", 254 "4 20 4 1772 307 595 510 \n",
246 " NumericalSolverSumTime additionalTime\n", 255 "5 20 5 2123 349 786 580 \n",
247 "1 7655 39044 \n", 256 "6 20 6 1554 308 670 690 \n",
248 "2 33695 103508 \n", 257 "7 20 7 1405 245 612 547 \n",
249 "3 99075 309361 \n", 258 "8 20 8 1764 232 588 409 \n",
250 "4 268490 552214 " 259 "9 20 9 1091 151 269 228 \n",
260 "10 20 10 1974 319 821 687 \n",
261 " NumericalSolverSumTime additionalTime\n",
262 "1 7754 9384 \n",
263 "2 7068 7242 \n",
264 "3 8865 9243 \n",
265 "4 7406 6593 \n",
266 "5 8281 9641 \n",
267 "6 7610 7545 \n",
268 "7 7967 15679 \n",
269 "8 5559 15092 \n",
270 "9 3226 5018 \n",
271 "10 7977 6758 "
251 ] 272 ]
252 }, 273 },
253 "metadata": {}, 274 "metadata": {},
@@ -257,54 +278,39 @@
257 "data": { 278 "data": {
258 "text/html": [ 279 "text/html": [
259 "<table>\n", 280 "<table>\n",
260 "<caption>A tibble: 4 × 7</caption>\n", 281 "<caption>A tibble: 1 × 7</caption>\n",
261 "<thead>\n", 282 "<thead>\n",
262 "\t<tr><th scope=col>n</th><th scope=col>preprocessingTime</th><th scope=col>StateCoderTime</th><th scope=col>ForwardTime</th><th scope=col>BacktrackingTime</th><th scope=col>NumericalSolverSumTime</th><th scope=col>additionalTime</th></tr>\n", 283 "\t<tr><th scope=col>n</th><th scope=col>preprocessingTime</th><th scope=col>StateCoderTime</th><th scope=col>ForwardTime</th><th scope=col>BacktrackingTime</th><th scope=col>NumericalSolverSumTime</th><th scope=col>additionalTime</th></tr>\n",
263 "\t<tr><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th></tr>\n", 284 "\t<tr><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th><th scope=col>&lt;dbl&gt;</th></tr>\n",
264 "</thead>\n", 285 "</thead>\n",
265 "<tbody>\n", 286 "<tbody>\n",
266 "\t<tr><td>20</td><td>33.339</td><td>0.878</td><td> 2.654</td><td>1.610</td><td> 7.655</td><td> 39.044</td></tr>\n", 287 "\t<tr><td>20</td><td>1.873</td><td>0.3135</td><td>0.7075</td><td>0.6125</td><td>7.682</td><td>8.394</td></tr>\n",
267 "\t<tr><td>30</td><td>36.670</td><td>2.016</td><td> 5.187</td><td>2.687</td><td> 33.695</td><td>103.508</td></tr>\n",
268 "\t<tr><td>40</td><td>48.868</td><td>3.907</td><td> 9.219</td><td>4.814</td><td> 99.075</td><td>309.361</td></tr>\n",
269 "\t<tr><td>50</td><td>62.541</td><td>5.581</td><td>12.720</td><td>5.863</td><td>268.490</td><td>552.214</td></tr>\n",
270 "</tbody>\n", 288 "</tbody>\n",
271 "</table>\n" 289 "</table>\n"
272 ], 290 ],
273 "text/latex": [ 291 "text/latex": [
274 "A tibble: 4 × 7\n", 292 "A tibble: 1 × 7\n",
275 "\\begin{tabular}{lllllll}\n", 293 "\\begin{tabular}{lllllll}\n",
276 " n & preprocessingTime & StateCoderTime & ForwardTime & BacktrackingTime & NumericalSolverSumTime & additionalTime\\\\\n", 294 " n & preprocessingTime & StateCoderTime & ForwardTime & BacktrackingTime & NumericalSolverSumTime & additionalTime\\\\\n",
277 " <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl>\\\\\n", 295 " <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl>\\\\\n",
278 "\\hline\n", 296 "\\hline\n",
279 "\t 20 & 33.339 & 0.878 & 2.654 & 1.610 & 7.655 & 39.044\\\\\n", 297 "\t 20 & 1.873 & 0.3135 & 0.7075 & 0.6125 & 7.682 & 8.394\\\\\n",
280 "\t 30 & 36.670 & 2.016 & 5.187 & 2.687 & 33.695 & 103.508\\\\\n",
281 "\t 40 & 48.868 & 3.907 & 9.219 & 4.814 & 99.075 & 309.361\\\\\n",
282 "\t 50 & 62.541 & 5.581 & 12.720 & 5.863 & 268.490 & 552.214\\\\\n",
283 "\\end{tabular}\n" 298 "\\end{tabular}\n"
284 ], 299 ],
285 "text/markdown": [ 300 "text/markdown": [
286 "\n", 301 "\n",
287 "A tibble: 4 × 7\n", 302 "A tibble: 1 × 7\n",
288 "\n", 303 "\n",
289 "| n &lt;dbl&gt; | preprocessingTime &lt;dbl&gt; | StateCoderTime &lt;dbl&gt; | ForwardTime &lt;dbl&gt; | BacktrackingTime &lt;dbl&gt; | NumericalSolverSumTime &lt;dbl&gt; | additionalTime &lt;dbl&gt; |\n", 304 "| n &lt;dbl&gt; | preprocessingTime &lt;dbl&gt; | StateCoderTime &lt;dbl&gt; | ForwardTime &lt;dbl&gt; | BacktrackingTime &lt;dbl&gt; | NumericalSolverSumTime &lt;dbl&gt; | additionalTime &lt;dbl&gt; |\n",
290 "|---|---|---|---|---|---|---|\n", 305 "|---|---|---|---|---|---|---|\n",
291 "| 20 | 33.339 | 0.878 | 2.654 | 1.610 | 7.655 | 39.044 |\n", 306 "| 20 | 1.873 | 0.3135 | 0.7075 | 0.6125 | 7.682 | 8.394 |\n",
292 "| 30 | 36.670 | 2.016 | 5.187 | 2.687 | 33.695 | 103.508 |\n",
293 "| 40 | 48.868 | 3.907 | 9.219 | 4.814 | 99.075 | 309.361 |\n",
294 "| 50 | 62.541 | 5.581 | 12.720 | 5.863 | 268.490 | 552.214 |\n",
295 "\n" 307 "\n"
296 ], 308 ],
297 "text/plain": [ 309 "text/plain": [
298 " n preprocessingTime StateCoderTime ForwardTime BacktrackingTime\n", 310 " n preprocessingTime StateCoderTime ForwardTime BacktrackingTime\n",
299 "1 20 33.339 0.878 2.654 1.610 \n", 311 "1 20 1.873 0.3135 0.7075 0.6125 \n",
300 "2 30 36.670 2.016 5.187 2.687 \n",
301 "3 40 48.868 3.907 9.219 4.814 \n",
302 "4 50 62.541 5.581 12.720 5.863 \n",
303 " NumericalSolverSumTime additionalTime\n", 312 " NumericalSolverSumTime additionalTime\n",
304 "1 7.655 39.044 \n", 313 "1 7.682 8.394 "
305 "2 33.695 103.508 \n",
306 "3 99.075 309.361 \n",
307 "4 268.490 552.214 "
308 ] 314 ]
309 }, 315 },
310 "metadata": {}, 316 "metadata": {},
@@ -313,16 +319,16 @@
313 { 319 {
314 "data": { 320 "data": {
315 "text/html": [ 321 "text/html": [
316 "42.769" 322 "1.873"
317 ], 323 ],
318 "text/latex": [ 324 "text/latex": [
319 "42.769" 325 "1.873"
320 ], 326 ],
321 "text/markdown": [ 327 "text/markdown": [
322 "42.769" 328 "1.873"
323 ], 329 ],
324 "text/plain": [ 330 "text/plain": [
325 "[1] 42.769" 331 "[1] 1.873"
326 ] 332 ]
327 }, 333 },
328 "metadata": {}, 334 "metadata": {},
@@ -330,7 +336,7 @@
330 }, 336 },
331 { 337 {
332 "data": { 338 "data": {
333 "image/png": "iVBORw0KGgoAAAANSUhEUgAAA0gAAANICAIAAAByhViMAAAACXBIWXMAABJ0AAASdAHeZh94\nAAAgAElEQVR4nOzdfZyVdZ34/+ucM8MwA3MDciOEN4gIeBOGWpi3FZlppZaW6QbrTTLWfll0\nzdVyg7BNXddA0xapxQdboWxurrubuuJ9lrakqGTqGt58ASUcB+Yw9+fu+8f5dX7zQGYYmDke\n5jPP5x8+5lzncJ23n7k48+I6NxPL5XIRAAADX7zUAwAA0D+EHQBAIIQdAEAghB0AQCCEHQBA\nIIQdAEAghB0AQCCEHQBAIMpKPcCe+9a3vvX73/++X3aVy+VyuVw8LnOjKIqy2WwURVYjL5vN\nWoo8B0ZXDowCB0ZXDowCP1i7yv8yiFgs1i97Gzt27LJly7q7dgCHXUNDw6233rrffvv1fVfp\ndLqtra26urrvuxrostlsY2PjkCFDampqSj1L6eVyuW3bto0YMaLUg+wVGhsbY7GY1chrbGwc\nOXJkqafYKzQ1NaVSqX322ae/fmgNaMlkctiwYYlEotSDlF5zc3N7e3tdXV1Z2QAujf7S0tJS\nVlZWUVHR912lUqmzzz67hxtIaQCAQAg7AIBACDsAgEAIOwCAQAg7AIBACDsAgEAIOwCAQAg7\nAIBACDsAgEAIOwCAQAg7AIBACDsAgEAIOwCAQAg7AIBACDsAgEAIOwCAQAg7AIBACDsAgEAI\nOwCAQAg7AIBACDsAgEAIOwCAQAg7AIBACDsAgEAIOwCAQAg7AIBACDsAgEAIOwCAQAg7AIBA\nCDsAgEAIOwCAQAg7AIBACDsAgEAIOwCAQJSVegAAGBTm/mplqUeguG4/4bxSj+CMHQBAKIQd\nAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCE\nHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAg\nhB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIMqKuveNGzfecccdr7zy\nSjqdnjhx4le+8pVDDz00iqLm5uZly5a98MILqVRqypQp9fX1Y8aM6WE7AAC7VMQzdrlcbtGi\nRSNGjFi2bNmKFSsOP/zwhQsXbt++PYqiJUuWbNmyZcGCBTfeeGNVVdWiRYuy2WwP2wEA2KUi\nhl0ymdy8efOsWbOqqqoqKipOO+209vb2t99+u6GhYc2aNZdccsnEiRPHjx9fX1+/adOmdevW\ndbe9eBMCAISkiGFXW1s7derUBx54YPv27e3t7Q888MDYsWMPPPDAV199tby8fOLEifmbDR8+\nfMKECa+88kp324s3IQBASIr7Grurrrrq29/+9vnnnx9F0YgRI7797W8PGTIkmUxWV1fHYrHC\nzWpra5uammpra3e6vXDx+eefv/322wsXm5ubt2/f3vUGeyyXy2Wz2X7Z1UCXy+WiKEqn01Yj\nL5PJWIq8XC6Xy+WsRp5HjIJ0Oh1FUVNTU9dH70ErnU5v377dUgxa3T0sZDKZzs7O9vb2vt9F\nKpXq+VVqRQy7dDq9aNGiqVOn/v3f/315efl99923YMGCH/zgB1EUdXfQ9/yXobGx8X/+538K\nFydNmpROp1OpVH8N7PV8Bdls1moU9OMxFgCrUWApusrnHZGlGNx6fljIZDLFvouoqGG3bt26\n119//frrrx86dGgURWefffb999//5JNPjhkzJplM5nK5QsY1NTWNGDGirq5up9sLOzzhhBMe\neeSRwsUrrriirq5un3326fuo6XS6vb19+PDhfd/VQJfNZrdu3TpkyJDq6upSz1J6+RNUdXV1\npR5kr7B169ZYLGY18rZu3dr10WkwSyaTqVRq5MiRTlNFUbR9+/aqqqpEIlHqQSiN7pqktbU1\nkUhUVFT0/S5SqVQ83tPr6IoYdvknbrqe+Mn/O2by5MmpVGr9+vUHH3xwFEXJZHLDhg3Tpk0b\nN27cTrf//7OWldXU1BQuxv6s76Pmd+JRKeqyCFajwFJ0ZTUKLEVX/fVoHABLMZj18K3v32Lp\nQRHfPDF16tQRI0YsX768ubm5s7PzF7/4RUtLy9FHHz1y5Mhjjz32tttue/311zdt2rR48eJJ\nkyYdeuih3W0v3oQAACEp4hm7/AfRrVixor6+PpPJ7L///gsWLBg3blwURfPmzVu2bNnChQsz\nmcxhhx12zTXX5Au0u+0AAOxScd8Ve8ABB3z7299+7/aqqqr58+f3fjsAALvkd8UCAARC2AEA\nBELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgB\nAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELY\nAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC\n2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAE\nQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEA\nBELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgB\nAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABKKs\n1APsuWw229HR0d7e3i+7ymQy/bKrgS6Xy0VRlM1mrUYURblcLpfLWYq8/LFhNfIcGAXZbDaK\novb29lgsVupZSi//gyked9JkkOruYSGdTud/oPT9LlKpVM/7GcBhF/35526/7Kfw30GusBRW\nI3Jg7IzVKLAUXVmNPA8ag1wP3/r+LZYeDOCwi8fjQ4cOrays7Puu0ul0Npvtl10NdNlstrW1\nNZFIWI0oinK5XEdHh6XIa2tri8ViViOvra3NUuR1dnZmMpnKykpn7KIoSqVSFRUViUSi1INQ\nGt09LGSz2bKysoqKir7fRVlZWc9/15wuBgAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISw\nAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiE\nsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAI\nhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMA\nCISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLAD\nAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISw\nAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiE\nsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAhEWbHv4L777rvnnnvefffdD3zgA7Nnzz7m\nmGOiKGpubl62bNkLL7yQSqWmTJlSX18/ZsyYHrYDALBLxT1j9/DDD69atWru3LlLly6dNWvW\nj370o9bW1iiKlixZsmXLlgULFtx4441VVVWLFi3KZrM9bAcAYJeKG3arVq2aM2fO0UcfPWbM\nmDPOOGPZsmVVVVUNDQ1r1qy55JJLJk6cOH78+Pr6+k2bNq1bt6677UWdEAAgGEV8Kvbdd9/d\nvHlzFEXz5s17++23DzjggIsvvnjq1KmvvvpqeXn5xIkT8zcbPnz4hAkTXnnlldbW1p1unz59\nevGGBAAIRnHDLoqihx566Morr6ytrb3rrru+853vLF26NJlMVldXx2Kxwi1ra2ubmppqa2t3\nur1w8dFHH/3GN75RuDhp0qStW7dWVlb218AdHR39tauBrrOzs6GhodRT7C0sRVdWo8BSdJV/\nwCeKos7OzlKPQMn0/LCwffv2vt9FKpXq+VVqRX/zxJe+9KUJEyZEUXThhRc++uijv/vd76Io\n6lpvXXW3Pa+6unratGmFi5lMJpFIlJX1w/9CLpfLZrOJRKLvuxrocrlcJpOJxWJWIy9/mJV6\nir1CJpOJoshq5KXT6X558AlAJpPJ5XKJRKLnB/BBIpPJxONxSzFodfewkM1mY7FYvxwYuVxu\nFzP0/T66M3LkyCiKhg0blr+YSCRGjhy5devW/fbbL5lM5nK5wv9hU1PTiBEj6urqdrq9sMOj\njz76Jz/5SeHi3Llza2pq6urq+j5qOp1ua2urrq7u+64Gumw229jYWF5eXlNTU+pZSi+Xy23b\ntq1fjrEANDY2xmIxq5HX2NhoKfKamppSqVRdXZ2aiaIomUwOGzbMv38Gre4eFlpaWsrKyioq\nKvp+F6lUKh7v6Q0SRXzzxMiRI0eMGPHyyy/nL3Z2dr7zzjtjx46dPHlyKpVav359fnsymdyw\nYcO0adO62168CQEAQlLEsIvH45/97Gfvuuuu5557rqGh4fbbbx86dOgxxxwzcuTIY4899rbb\nbnv99dc3bdq0ePHiSZMmHXrood1tL96EAAAhKe5rRD7/+c+3trZ+//vfb25unjJlyne/+92h\nQ4dGUTRv3rxly5YtXLgwk8kcdthh11xzTf4cfnfbAQDYpeKGXTwenz179uzZs3fYXlVVNX/+\n/PfevrvtAADskt8VCwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcA\nEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEH\nABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhh\nBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAI\nYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQ\nCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcA\nEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEH\nABAIYQcAEAhhBwAQCGEHABCIslIPsOcymcz27dubmpr6vqtcLpfNZvtlVwNdLpeLoiidTluN\nPAdGQS6Xy+VyViPPgVGQTqejKGpqaorFYqWepfQymUxzc3Opp6BkuntYyGQynZ2d7e3tfb+L\nVCqVzWZ7uMEADrt4PF5VVTVs2LC+7yqTyXR0dFRVVfV9VwNdNptNJpOJRKJfFnagy+Vy27dv\ntxR5yWQyiiKrkZdMJi1FXnNzczqdHjZsmLCLoqilpaWysjIe92zYINXdw0JbW1sikRgyZEjf\n7yKVSvV8gA3gsIvFYolEoqysf/4XYrFYf+1qQMv/O8Bq5OVyOUvRldXoylLk5XuurKxM2EV/\n/sGUSCRKPQil0d3DQjwe769iyT+x1gP/qgAACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiE\nsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAIhLADAAiEsAMACISwAwAI\nRFlvbtTS0vJf//VfDz744LPPPtvQ0LBt27ba2trRo0fPmDHjlFNO+cxnPjNs2LBiDwoAQM92\nccauo6Pjpptumjhx4rnnnvvTn/40m80ecsghp5xyypQpU7LZ7E9/+tNzzz134sSJN910U0dH\nx/szMQAAO9XTGbs33njj7LPPXrt27dlnnz1nzpyTTz65qqqq6w1aW1sfe+yxFStWXHnllXfe\neefdd9994IEHFndeAAC60dMZuxkzZtTU1Pz+979ftWrVaaedtkPVRVFUVVV12mmnrVq16ve/\n/31NTc1RRx1VzFEBAOhJT2H39a9/ffXq1dOmTdvlXqZNm7Z69epLL720/wYDAGD39PRU7LXX\nXlv4urW1tampady4cVEUtbW1rVq16t133z3rrLMOOuig/A0SicR3v/vdos4KAEAPevVxJy+/\n/PLEiRNXrFgRRVE6nT7xxBMvuOCCK664YsaMGWvXri3yhAAA9Eqvwu5b3/rW2LFjzznnnCiK\n7rrrrt/97nc//OEP//jHPx522GHf+973ijwhAAC90quwe/LJJ6+66qpJkyZFUfSLX/zi8MMP\nv/TSSydNmvT1r3/9t7/9bZEnBACgV3oVdtu2bcu/ui6TyTz22GOnnXZafvvo0aP/9Kc/FXE6\nAAB6rVdhN3bs2Ndeey2KokceeWTr1q2nnnpqfvuGDRv22WefIk4HAECv9epXip1yyinXXHPN\nH//4xzvvvHPSpEknnnhiFEVbtmy5+eabjzvuuCJPCABAr/Qq7K699toXX3zx+uuvHzVq1H/+\n538mEokoiubNm/fmm2/+5Cc/KfKEAAD0Sq/Cbty4cU899VQymaysrCwvL89vvOKKK26++eax\nY8cWczwAAHqrp9fYXXjhhW1tbYWLNTU1haqLoujoo4/uWnVtbW0XXXRRMUYEAKA3egq7Rx55\nZObMmY8//vgu9/L444/PnDnz4Ycf7r/BAADYPT2F3TPPPLPvvvuefPLJJ5100h133LFp06Yd\nbrBp06Y77rjjpJNOOvnkk/fdd99nnnmmmKMCANCTnl5jt88++9x///0rV678zne+c+GFF0ZR\nNHbs2FGjRtXW1jY1NTU0NOQ/xG7y5Mk/+clPzjvvvHi8Vx+eAgBAMezizRPxePwv/uIvvvzl\nLz/55JMPPfTQ2rVr33nnncbGxpqamgMPPPBDH/rQrFmzjj/++Pz7ZAEAKKFevSs2kUicdNJJ\nJ510UrGnAQBgj3nyFAAgEMIOACAQwg4AIBDCDgAgEMIOACAQuxF27e3ta9asueeeexoaGqIo\nSqfTRZsKAIDd1tuwu+mmm8aMGfPhD3/485///B//+McoihYsWHDBBRfIOwCAvUSvwu5HP/rR\nFVdc8bGPfWzp0qWFjVOmTPnpT3+6ePHios0GAMBu6FXY3XrrrfX19ffee++cOXMKG2fPnv2N\nb3zjxz/+cdFmAwBgN/Qq7P73f//3C1/4wnu3n3zyya+//np/jwQAwJ7oVdjV1NS0t7e/d3tT\nU1NlZWV/jwQAwJ7oVdh98IMf/Md//Me2trauGxsbGxctWjRz5sziDAYAwO4p682NvvWtb82a\nNeuDH/zg6aefHkXRj370o6VLl95zzz1tbW1d304BAEAJ9eqM3cknn/zf//3f1dXVN998cxRF\ny5cvX7FixdSpU1evXn3ccccVeUIAAHqlV2fsoij6xCc+8eyzz27ZsuWtt96KouiAAw4YMWJE\nMQcDAGD39Dbs8iorKw888MD819u2bct/UVdX178zAQCwB3oVdq+99tq8efMee+yxlpaW916b\ny+X6eyoAAHZbr8LuoosuWrt27Zlnnjlu3LhEIlHsmQAA2AO9Crs1a9Y8+OCDH/3oR4s9DQAA\ne6xX74odNmxY4aV1AADsnXoVdl/5yleWL19e7FEAAOiLXj0V+73vfe/0009/4IEHjj322H32\n2WeHa6+66qoiDAYAwO7pVdh9//vff+ihh6Io+vWvf/3ea4UdQFdzf7Wy1CNQXLefcF6pR4Cd\n61XY3XLLLV/4whcuu+yyfffd17tiAQD2Tr0Ku8bGxltuuWX8+PHFngYAgD3WqzdPHHrooe+8\n806xRwEAoC96FXZLliy5/PLLX3jhhWJPAwDAHuvVU7Hf/OY333zzzenTpw8fPvy974p94403\n+n8uAAB2U6/CLh6PT5kyZcqUKcWeBgCAPdarsHviiSeKPQcAAH3Uq9fYAQCw9+vpjN3UqVPn\nzJlz9dVXT506tYebvfzyy/09FQAAu62nsKurq6usrMx/8X7NAwDAHuop7J5++ukdvgAAYK/V\nq9fYHX300S+99NJ7t//bv/3boYce2t8jAQCwJ3oVds8880xLS8sOG9Pp9Isvvrh+/foiTAUA\nwG7bxcedxGKx/BfHHHPMTm8wY8aMfp4IAIA9souwe+655x5//PG//uu/PuOMM0aNGtX1qlgs\nNn78+K9+9avFHA8AgN7aRdhNnz59+vTp991334033jh58uT3ZyYAAPZAr37zxAMPPFDsOQAA\n6KNehd2WLVuuvPLK1atXb968OZvN7nBtLpfb5R4efvjhm2+++Zvf/ObMmTOjKGpubl62bNkL\nL7yQSqWmTJlSX18/ZsyYHrYDALBLvQq7v/qrv7rnnntOOumkT37yk2VlvfojXW3btm3FihVD\nhgwpbFmyZElzc/OCBQsqKipWrly5aNGiW265JR6Pd7d9d+8RAGAQ6lWlPfLII3ffffcZZ5yx\nZ/exdOnSk08++bHHHstfbGhoWLNmzeLFiydOnBhFUX19/Ve+8pV169Z94AMf2On26dOn79n9\nAgAMKr0Ku7a2to9+9KN7dgdPPfXU+vXr58+fXwi7V199tby8PF9vURQNHz58woQJr7zySmtr\n6063F8Juy5YtL7zwQmHPqVSqs7Ozo6NjzwbrKpPJZDKZftnVQJd/Yj2bzVqNKIpyuVwul7MU\nefljw2rkOTAGue6++9lstrOz0xNNg1Z3B0Ymk+nN69Z6I5VK9byrXoXdUUcd9eKLL5588sm7\ne/fNzc1Lly697LLLhg4dWtiYTCarq6sLn5AXRVFtbW1TU1Ntbe1Otxcuvvjii1dddVXh4qRJ\nk1paWrZv3767U3WnH3c10KXTaatRYCkKcrmc1SiwFINZD9/9dDr9fk7CXqXnh4X29va+30X/\nhN3ixYu/9rWvLVmy5Nhjj92tu//nf/7nGTNmHHnkkTts71pvvdmeN2nSpP/zf/5P4eIjjzxS\nWVk5bNiw3Rppp7LZbCqVqqio6PuuBrpcLtfa2ppIJLq2+KCVy+Xa29srKytLPcheobW1NRaL\nWY281tbWqqqqUk9ByXT3o6ejo6O8vNwZu0GruwMjfx53D96l8F6pVKrnWOrVffz1X//122+/\n/dGPfrSqqmr06NE7XPvGG2/s9E8999xzzz777K233rrD9rq6umQymcvlCpM1NTWNGDGiu+2F\nP7j//vvPmTOncPE3v/nN0KFD++XHTDqdzmazfmJFUZTNZvNhZzWiPz/dZiny2trahF1BW1ub\npRjMuvvup1KpoUOHJhKJ93ke9hLdHRjZbLasrKxfzh+VlZX1Q9jF4/FDDjnkkEMO2a37Xr16\ndUtLS319ff5ic3Pz4sWLjzzyyLlz56ZSqfXr1x988MFRFCWTyQ0bNkybNm3cuHE73b5bdwoA\nMGj1KuyeeOKJPdh1fX39BRdcULh42WWXzZ49+yMf+UhNTc2xxx572223zZs3b8iQIT/+8Y8n\nTZp06KGHxmKxnW7fg7sGABiE+uHp3u5UV1dXV1cXLsZiserq6pqamiiK5s2bt2zZsoULF2Yy\nmcMOO+yaa67Jn1fsbjsAALvUq7AbNWpUd1d1dnYmk8ne7ORf/uVfCl9XVVXNnz//vbfpbjsA\nALvUq7A7/vjjd9jy9ttvr1u3btKkSSeddFIRpgIAYLf1Kuz+/d///b0bN2/e/KUvfenTn/50\nf48EAMCe2PPP2tl3331vuummBQsW9OM0AADssT59iOKECRP+8Ic/9NcoAAD0xZ6HXS6XW758\n+T777NOP0wAAsMd69Rq79/5OsEwms3nz5oaGhiuuuKIIUwEAsNv28HPsysvLP/jBD55xxhmF\nXywBAEBp9SrsnnvuuWLPAQBAH/XpzRNRFL3xxhv9MQYAAH21i7B74oknPvWpT02ePPlTn/rU\n/fff3/Wqjo6Ov//7v/e7XAEA9hI9hd3TTz89a9as1atXd3Z2Pvroo6effvrPf/7z/FUPPvjg\nEUcccc011+y///7vy5wAAOxCT2F3/fXXV1VVrV279s0339y4ceNRRx21YMGCjRs3nnPOOZ/6\n1KfeeeedxYsXr1u37n2bFQCAHvT05onnn3/+L//yL6dPnx5F0ZgxY6699tpPf/rTkydPTqVS\nl1566aJFi0aNGvV+zQkAwC70FHYbN2485JBDChenTZsWRdFHPvKRW2+99fDDDy/6aAAA7I6e\nnopNp9NDhgwpXKyoqIii6KqrrlJ1AAB7ob5+3AkAAHsJYQcAEIhd/OaJ11577emnn85/3djY\nGEXRyy+/XFdX1/U2M2fOLNJwAAD03i7C7rrrrrvuuuu6brnssst2uE0ul+vnoQAA2H09hd2C\nBQvetzkAAOijnsJu4cKF79cYAAD0lTdPAAAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELY\nAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC\n2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAE\nQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEA\nBELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgB\nAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAASirNQD7LlMJtPU1DR8+PB+2Vs2m926\ndWu/7GpAy+VyURSlUimrkZfJZCxFXi6Xy+VyViPPI8Yg1913P5vNJpPJ93kY9h49HBixWKy1\ntbXvd5FKpbLZbA83GMBhl0gkamtrR4wY0fddpdPptra26urqvu9qoMtms42NjZpwVW8AAB7E\nSURBVOXl5TU1NaWepfRyudy2bdv65RgLQGNjYywWsxp5jY2NlmIw6+67n0wmhw0blkgk3ud5\n2Et0d2C0tLSUlZVVVFT0/S5SqVQ83tPTrZ6KBQAIhLADAAiEsAMACISwAwAIhLADAAjEAH5X\nLAAMID9c83CpR6DITjiv1BM4YwcAEAphBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhh\nBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAI\nYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQ\nCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcA\nEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEH\nABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhh\nBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQiLKi7r2x\nsXH58uXPP/98Z2fnQQcddMEFFxxyyCFRFDU3Ny9btuyFF15IpVJTpkypr68fM2ZMD9sBANil\n4p6x++53v9vQ0PCd73xnyZIlo0aNWrRoUXt7exRFS5Ys2bJly4IFC2688caqqqpFixZls9ke\ntgMAsEtFDLvt27ePHj3661//+kEHHTRu3LjZs2cnk8kNGzY0NDSsWbPmkksumThx4vjx4+vr\n6zdt2rRu3bruthdvQgCAkBTxqdjq6uqrr766cPHdd9+Nx+OjRo16+eWXy8vLJ06cmN8+fPjw\nCRMmvPLKK62trTvdPn369OINCQAQjOK+xq5g+/btP/jBD84888wRI0Ykk8nq6upYLFa4tra2\ntqmpqba2dqfbCxf/93//9+677y5cbGtra21tbW5u7vt42Ww2k8n0y64GulwuF0VROp22GnnZ\nbNZS5OVyuVwuZzXyLMUg1913P51Ot7a2dv1B1lVlMUdib9DDgZFOp1OpVN/vIpVK5X9Sd+f9\nCLuNGzdee+21Rx555Jw5c/Jbujvou9uet2nTpl/84heFi5MmTero6Mi/aK9fZDKZ/trVQJfN\nZvtxYQc6S9GV1SiwFINZD9/9jo6O7q4SdsHr+WEhkLB7/vnn/+Ef/uHLX/7yZz7zmfyWurq6\nZDKZy+UKGdfU1DRixIjuthd2dfTRR//kJz8pXLzppptqamrq6ur6PmQmk+no6Kiqqur7rga6\nbDabTCbLy8uHDRtW6llKL5fLbd++vaamptSD7BWSyWQURVYjL5lMWorBrLsfPS0tLZWVlfG4\njxIbpLo7MNra2hKJxJAhQ/p+F6lUqucDrLhh94c//OGGG274m7/5m6OOOqqwcfLkyalUav36\n9QcffHAURfl3VEybNm3cuHE73V74g9XV1V0vJhKJRCJRVtY//wuxWKy/djWg5d+GbDXy8v/M\nsBQFVqMrSzGYdffdj8Vi+Z9NO73Ws0LB6+7AiMfj/VUsPZ+ui4r6rtjOzs4lS5Z87nOfO+CA\nAxr+rL29feTIkccee+xtt932+uuvb9q0afHixZMmTTr00EO72168CQEAQlLEf3G+9NJLmzdv\nXrly5cqVKwsb586de/rpp8+bN2/ZsmULFy7MZDKHHXbYNddck3/6tbvtAADsUhHDbvr06f/x\nH/+x06uqqqrmz5/f++0AAOySF3gCAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC\n2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAE\nQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEA\nBELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELYAQAEoqzU\nA8BANfdXK0s9AkV3+wnnlXoEgN3gjB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0A\nQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQd\nAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAgyko9AEBofrjm4VKPQJGdcF6pJ4Cd\nc8YOACAQwg4AIBDCDgAgEMIOACAQwg4AIBDCDgAgEMIOACAQwg4AIBDCDgAgEMIOACAQwg4A\nIBDCDgAgEGWlHmDP5XK5zs7Ojo6Ovu8qm81ms9l+2dVAl8vloiiyGnm5XC6Xy1mKway7737P\nB8YAfmCld7r77mez2c7Oznh85ydNHBjB6+7AyGQy+R+vfZdKpXre1QA+zHK5XDqdTqVS/bKr\nbDbbL7sa6AphZzXycrmcpRjMevju93DVAH5gpXe6++7nfzDFYrGdXuvACF53B0Y2m+3HsOv5\nBgP4MIvH41VVVcOHD+/7rtLpdFtbW7/saqDLn6srKyuzGtGfq85SDGbdffc7Ozt7ODAyRZuH\nvUR33/1kMllVVZVIJHZ6rQMjeN0dGC0tLWVlZRUVFX2/i1Qq1d2/HPK8xg4AIBDCDgAgEMIO\nACAQwg4AIBDCDgAgEMIOACAQwg4AIBDCDgAgEMIOACAQwg4AIBDCDgAgEMIOACAQwg4AIBDC\nDgAgEMIOACAQwg4AIBDCDgAgEMIOACAQwg4AIBDCDgAgEMIOACAQwg4AIBDCDgAgEMIOACAQ\nwg4AIBDCDgAgEMIOACAQwg4AIBDCDgAgEMIOACAQwg4AIBDCDgAgEMIOACAQwg4AIBDCDgAg\nEMIOACAQwg4AIBDCDgAgEMIOACAQZaUeYACY+6uVpR6B4rr9hPNKPQIA9ANn7AAAAiHsAAAC\nIewAAAIh7AAAAiHsAAAC4V2xsId+uObhUo9A8XnHNDCgOGMHABAIYQcAEAhhBwAQCGEHABAI\nYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQCGEHABAIYQcAEAhhBwAQ\nCGEHABCIslIPAACDws37XFrqESiuy0s9QOSMHQBAMIQdAEAghB0AQCC8xg4A3g/nbWkv9QiE\nT9gB9DOvkQ/e3vAaedgpT8UCAARC2AEABMJTsQD9zEupgFIRdrv2wzUPl3oEiuyE80o9ARC+\nRz93c6lHoLi+HB1f6hE8FQsAEAphBwAQCE/Fwh7ykRaDwZ59qoVn3IK3NzzjBjsl7GAPeYE8\nAHsbT8UCAARi7zpj19zcvGzZshdeeCGVSk2ZMqW+vn7MmDGlHgoAYGDYu8JuyZIlzc3NCxYs\nqKioWLly5aJFi2655ZZ4vMSnFd/JXFDaASi2fffoT3kd1WDgpVTAwLIXPRXb0NCwZs2aSy65\nZOLEiePHj6+vr9+0adO6detKPRcAwMCwF52xe/XVV8vLyydOnJi/OHz48AkTJrzyyivTp08v\n7WBOzATPWRkAwrAXhV0ymayuro7FYoUttbW1TU1NhYtPP/30ddddV7g4bNiwpqam4cOH9/2u\nc7lcLpfbunVr33fFQNTDtz6bzTowBrPuvvseMQa57r772Ww2mUy+z8Ow9+jhEaOjo6O1tbXv\nd5FKpbLZbA832IvCLoqirlW39zh1zLJSj/D+yeVy2Ww2FouV/KWNe79BdWBEUZR/KHFg9Mag\nOjay2Wwul0skEqUeZAAYhAdGPB7fO3+yB2wvCru6urpkMpnL5QoHQVNT04gRIwo3mDlz5r33\n3lu4OHfu3Nra2q432GPpdLqtra26urrvuxrostlsY2NjeXl5TU1NqWcpvVwut23btn45xgLQ\n2NgYi8WsRl5jY6OlyGtqakqlUnV1dX5+R1GUTCaHDRsmc6Moam5ubm9vr6mpKSvbi0qjVFpa\nWsrKyioqKvq+q1Qq1fM/sPeif3xPnjw5lUqtX78+fzGZTG7YsGHatGmlnQoAYKDYi8Ju5MiR\nxx577G233fb6669v2rRp8eLFkyZNOvTQQ0s9FwDAwLB3nSCdN2/esmXLFi5cmMlkDjvssGuu\nuca5fQCAXtq7wq6qqmr+/PmlngIAYEDai56KBQCgL4QdAEAghB0AQCCEHQBAIIQdAEAghB0A\nQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQd\nAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCEHQBAIIQdAEAghB0AQCCE\nHQBAIMpKPUCf3HPPPbW1tX3fTzabTaVSFRUVfd/VQJfL5VpbW8vKyqxGFEW5XK69vb2ysrLU\ng+wVWltbY7GY1chrbW2tqqoq9RR7hfb29kwmU1VVFYvFSj1L6XV0dJSXl8fjTppEnZ2dqVSq\nsrLSakRR1NnZGY/Hy8r6IboymUzPN4jlcrm+301JPPHEEw0NDf2yq1wul81mE4lEv+xtQOvo\n6HjooYdGjx794Q9/uNSz7BXS6XS//FUMwOrVq8vKyj72sY+VepC9ggOj4KmnnmpsbPz0pz/t\n53cURel0OpFIaNwoitatW/d//+//Pf744/vl/MtAl81moyjqr78jw4cPP+WUU7q7dgCHHcWw\nbdu2WbNmnXDCCYsXLy71LOxdTjnllMrKynvvvbfUg7B3mTt37jPPPPOb3/xmyJAhpZ6FvcgN\nN9zw85///Kc//enUqVNLPcvg4h9YAACBEHYAAIEQdgAAgfAaOwCAQDhjBwAQCGEHABAIYQcA\nEAgfsDnYNTY2Ll++/Pnnn+/s7DzooIMuuOCCQw45JIqi5ubmZcuWvfDCC6lUasqUKfX19WPG\njCn1sLx/NmzYsGLFipdeeimXy02cOPErX/lK/sOoHBjkPfzwwzfffPM3v/nNmTNnRg6MQW/e\nvHlvvPFG4eLQoUP/9V//NXJglII3Twx2l19++ZAhQy655JLKysqVK1euXbv2xz/+8dChQ7/7\n3e82NzfPnTu3oqJi5cqVb7zxxi233OKT5QeJdDp98cUXT58+/Ytf/GI8Hl+1atVvf/vb5cuX\nV1ZWOjCIomjbtm3z5s1rbW294oor8mHnwBjkLrzwws9//vP5gyGKong8PnLkyMiBUQoWd1Db\nvn376NGjv/71rx900EHjxo2bPXt2MpncsGFDQ0PDmjVrLrnkkokTJ44fP76+vn7Tpk3r1q0r\n9by8T1paWs4444z6+voPfOAD48aNO+ecc1paWt5++20HBnlLly49+eSTC78t14HB9u3b9913\n31F/lq86B0ZJCLtBrbq6+uqrr95vv/3yF9999914PD5q1KhXX321vLx84sSJ+e3Dhw+fMGHC\nK6+8UrpJeV/V1taeddZZlZWVURRt3779P/7jPyZMmLDffvs5MIii6Kmnnlq/fv15551X2OLA\nGORSqVRHR8dTTz01f/78iy666Lrrrtu0aVPkwCgRr7Hj/7N9+/Yf/OAHZ5555ogRI5LJZHV1\nddffY11bW9vU1FTC8Xj/ZbPZc845J5VKHX744ddee215ebkDg+bm5qVLl1522WVDhw4tbHRg\nDHKtra11dXXpdPprX/taFEV33nnn1Vdf/U//9E8OjJIQdkRRFG3cuPHaa6898sgj58yZk9/S\n9a8ig1M8Hr/55pu3bt36y1/+8pvf/OZNN90UOTAGvX/+53+eMWPGkUceucN2B8ZgVltb+y//\n8i+Fi1deeeWcOXN+85vfRA6MUvBULNHzzz//t3/7t5/97GcvvfTS/F/Curq6ZDLZ9Y01TU1N\nI0aMKN2MlMaECROOOOKIK6+8sqmp6fHHH3dgDHLPPffcs88+e+GFF+6w3YFBV5WVlaNHj25o\naHBglISwG+z+8Ic/3HDDDZdffvlnPvOZwsbJkyenUqn169fnL+bfUTFt2rQSzcj7be3atZdc\ncklHR0f+YiwWKysrixwYg97q1atbWlrq6+vPP//8888/v6mpafHixdddd50DY5B78803b731\n1nQ6nb/Y3t7+zjvv7Lvvvg6MkkgsXLiw1DNQMp2dnd/+9rdPPfXUGTNmtP5ZPB6vrq5+8803\nH3300SlTprS2tv7whz8cNmzY+eef76T6IFFdXX3vvfe+9tprBxxwQFtb21133fXKK69cfPHF\no0ePdmAMZh/84Ac/3cVjjz12wQUXnHXWWXV1dQ6MwSyRSCxdunTTpk0HHnhgU1PT7bff3tzc\nfOmll/pRUhI+x25Qe/755//u7/5uh41z5849/fTTW1tbly1btnbt2kwmc9hhh9XX1zt/Pqi8\n+eabd9xxxx/+8IdYLLb//vv/xV/8xfTp06MocmBQMHv27K997Wv5jy5zYAxyr7322h133JF/\nG+yUKVO++tWvjh07NnJglIKwAwAIhNfYAQAEQtgBAARC2AEABELYAQAEQtgBAARC2AEABELY\nAQAEQtgBe27hwoWxWGzMmDGpVOq911588cWxWOz444/fs52fe+65w4cP780tjz/++KlTp3Z3\nbUNDw/e+972jjjpq1KhR5eXlY8aMOfXUU//7v/+7cIOZM2f28Mf74t133z3wwAMvuuiiwpZf\n/OIXX/ziF/Nfv/POO+PHjy/G/e6g9yvZnWuuuWafffZ54403+mkioFjKSj0AMLDF4/HGxsZf\n/vKXZ555ZtftbW1tP//5z8vLy0s1WF5jY+MxxxyzZcuWCy+88PLLL08kEuvXr1++fPlpp532\ns5/97Nxzz42i6Nxzz21ra+v3u85ms+edd15tbe2tt95a2Pjss89+6EMfeu/Xe7nvfOc7v/nN\nb84+++xf//rXFRUVpR4H6JawA/okHo9/+MMfvuOOO3YIu3vuuaetrS3/i8hKaMWKFW+88cZd\nd931pS99qbDxa1/72hFHHHHVVVd98YtfjMfj8+fPL8Zdr1y58sEHH3zssccqKysLG5955pnC\n3T377LMzZswoxl33u0Qicdtttx1++OG33nrr3/zN35R6HKBbnooF+iSdTn/mM5+57777/vSn\nP3XdvmLFio997GM7nN25//77TzzxxOrq6srKysMPP/z73/9+4bca5nK5RYsW7bfffkOHDj3i\niCPuvvvuHe7o8ccf/+QnP1lTU1NVVTVjxozly5f3Zry33347iqKjjjqq68YRI0Y8/fTTL730\nUjwej7o8Ffu73/0utjO///3vd3eGTCZz7bXXnnjiiSeddFLX7V1jroewO/HEE0844YS1a9d+\n4hOfqKmpGTNmzJe//OUtW7YUblCklXz77be/+tWvHnDAAUOHDt13332/8IUvvPzyy/mrpk2b\ndvbZZ//DP/xDS0tLd//XQOnlAPbUggULoih69dVX4/H4P/7jPxa2b9y4MR6PL1++fObMmccd\nd1x+4z333BOLxU499dR///d/f+ihhy6//PIoir7xjW/kr73hhhuiKDr//PNXr169atWqww8/\nfMqUKcOGDctf+9BDDyUSiRNPPPE///M/H3zwwfr6+iiKCvd43HHHTZkyZacT3nnnnVEUnXXW\nWVu3bu3u/+IjH/lI/o8nk8nVXfzXf/3X6NGjJ0yYsG3btl3OsIPHH388iqLly5fnL954440V\nFRX5zK34s1gslv9i48aNO/zxT3ziE/vtt98xxxyzevXqP/3pT3fffXcikZgzZ06xV3LmzJn7\n7rvvj3/840ceeeRnP/vZEUccMWbMmJaWlvy1v/zlL6MoWrVqVXcrCZScsAP2XD7s2traZs2a\nddhhhxW2X3/99ZWVlclk8iMf+Ugh7KZOnbr//vt3dHQUbnbmmWeWl5c3NDRks9nx48cffvjh\nhaveeuut8vLyQo586EMfOvjggwuFkcvlPve5z1VXV7e1teV6DLtMJpN/s0JFRcVpp512ww03\nPP3005lMputtCmG3gwsuuKCiouK3v/1tb2bYwd/93d9FUbRDsd19992f//zn819v3rx5/Pjx\nO505l8t94hOfiKLoySef7LqlcPsirWRTU1MURVdddVXhqj/+8Y/f+973Nm3alL/Y0tIyZMiQ\niy66qLuxgZLzVCzQD/7yL//yxRdfXLNmTf7iihUrzjzzzOrq6sIN3nrrrZdffvm0004bMmRI\nYeNnP/vZVCr19NNPb9iw4a233vr4xz9euGrcuHFHH310/ustW7asXbv29NNPj8fj7X922mmn\nbd++fd26dT0PFo/HV61a9cADD3zhC1947rnn/vZv/3bmzJljx469+uqrW1tbe/iD//RP/3TH\nHXfceuutH/7wh/dghmeffXbs2LEf+MAHum789a9/XXiP8K9//euPfvSjPQxQVVV13HHHFS5O\nmDBh8+bNUTFXsrKycp999rnzzjsffvjhbDYbRdGkSZOuvvrqwlt3q6qqpk6d+swzz/QwNlBa\nwg7oB2eddVZ1dfUdd9wRRdGaNWteeuml2bNnd73Bpk2boijaIXTGjRsXRdFbb72VT5bRo0d3\nvbbQE2+99VYURTfffHNlF/nnEDdu3Nib8T71qU/97Gc/27Rp0/r163/0ox9Nmzbt+uuvnzVr\nVj5f3uupp56aP3/+JZdccvHFF+/ZDO+8886oUaN22Pjkk08WWu3JJ5/sOex2WI2ysrL8tMVb\nyfLy8nvvvTcej8+aNWvMmDFnn332ypUr0+l0112NGjWqoaGhh7GB0vKuWKAfVFVVnXPOOXfe\neef3v//9FStWjBs37pOf/GTXG8RisSiKdgipXC4XRVE8Hs/9+YX/XWUyma4XL7zwwq9+9as7\n3Obggw/erTkPOuiggw466KKLLrr44ouXL1/+5JNPnnjiiTvcZvPmzWefffaHPvShH/zgBztc\n1fsZksnkyJEjCxcnTJjQ0NDQ0dFRuLvOzs7y8vKrr776vPPO6+UbQfKKupLHHXfcq6+++vjj\nj99///333Xff+eefv3jx4ieeeKLwxt66urpt27b1flrgfSbsgP4xZ86c5cuXP/jgg6tWrZoz\nZ04ikeh67YQJE6I/n20qyF+cMGFC/gxT/mxTQeHjcPfff/8oijKZzMyZM3drpI6OjrvvvnvY\nsGE7fBRLLBY76aSTli9fvmHDhh3+SCqV+uIXv5jJZP7t3/6t63OduztDTU1N/iVreRs3bnzq\nqaeuvPLKX/3qV1EUpdPpESNGNDQ07MFnwhV7JROJxMc//vGPf/zjN974/9q7v1Dm/jgO4Oes\n7ZA/U/JnkYiSC+NwoRS50I5c6SjFzZS0MrRyIRfmT7uyJzcoUqjdLAcjrbXWilJ2M2MXhDJX\nipxwNWJ2notT67Sf/PKwZ5zn/bo6++6c9tn3Yn36fHY+59f8/LzRaOQ4rru7W3z34eEhKyvr\nozEDwF+DViwAfI3GxsbS0lKLxcLzfFwfliAIjUZTWVnpdDqfnp5iiw6HIy0trb6+vqSkJCcn\nx+12xwpR5+fnwWBQPM7Ozq6rq9va2pLWimw22+joaFyjMA5FUZOTkwaDIRQKSddfX1/X1tYI\ngqiqqoq7ZGhoyOfzcRwX1+v8aAy5ublxLcujoyOapsXjk5OTsrKyP5v0m7idPDg46OzslA5V\nYRiGIIjb29vYCs/zcX1eAPhWkNgBwNcgSVKv1/v9/urq6v8mTARBTE1NXV9ft7W1bW9vu91u\no9HodrvNZrNarVYoFH19fRcXFx0dHQ6HY2FhgWEY6Yw3q9UaDoebmppsNpvH4zGbzb29vVdX\nV0rle20HkiQXFxcfHx9pmjYYDDMzM0tLSxaLpba21ul0Dg4OarVa6fkcx83NzbW3tz8/P3sl\nxLzwQzHQNH1zcyOtq0kTu8PDw8+MJk7QThYWFrpcLp1Ot7y87PV6V1dX9Xq9Wq1mWVa8NhwO\nn52d/ZSnZQD8o5J7Uy4A/GixcSfiy1AoRJLk9PR07ATpuBNBEDweT0NDQ3p6ekpKSk1NTWzM\nmyAIkUhkZGREo9FQFKXVajc3NwcGBiiKip2wt7en0+kyMzNVKlV5ebnVan15eRHfemfciSAI\nx8fHPT09YoVMqVTm5+e3traur69LgxQvN5lMb/5Ojo+P/28McXZ2dgiCWFlZkX6K3+8Xj00m\n0+zs7Dsb29zcXFxcLF0RHzib6J0MBoMsy+bl5alUqoKCApZlA4FA7EKXy0UQhN1ufydyAEgu\nUnjrn7YAAPAZkUikoqKiqKhIzPDkoaury+v1Xl5eZmRkJDsWAHgbWrEAAF9PqVSOjY3t7u6K\nd0vIwOnpKcdxw8PDyOoAvjNU7AAAEiIajba0tPA87/P5UlNTkx3Op0SjUYZh7u7u9vf3f/p3\nAZA3VOwAABJCoVDY7fb7+/v+/v5kx/JZExMTgUBgY2MDWR3AN4eKHQAAAIBMoGIHAAAAIBNI\n7AAAAABkAokdAAAAgEwgsQMAAACQCSR2AAAAADKBxA4AAABAJpDYAQAAAMjEb/85njrbF1HE\nAAAAAElFTkSuQmCC", 339 "image/png": "iVBORw0KGgoAAAANSUhEUgAAA0gAAANICAMAAADKOT/pAAAC91BMVEUAAAABAQECAgIDAwME\nBAQFBQUGBgYHBwcICAgJCQkKCgoLCwsMDAwNDQ0ODg4PDw8QEBARERESEhITExMUFBQVFRUW\nFhYXFxcYGBgZGRkaGhobGxscHBwdHR0eHh4fHx8gICAhISEiIiIjIyMkJCQlJSUmJiYnJyco\nKCgpKSkqKiorKyssLCwtLS0uLi4vLy8wMDAxMTEyMjIzMzM0NDQ1NTU2NjY3Nzc4ODg5OTk6\nOjo7Ozs8PDw9PT0+Pj4/Pz9AQEBBQUFCQkJDQ0NERERFRUVGRkZHR0dISEhJSUlKSkpLS0tM\nTExNTU1OTk5PT09QUFBRUVFSUlJTU1NUVFRVVVVWVlZXV1dYWFhZWVlaWlpbW1tcXFxdXV1e\nXl5fX19gYGBhYWFiYmJjY2NkZGRlZWVmZmZmwqVoaGhpaWlqampra2tsbGxtbW1ubm5vb29w\ncHBxcXFycnJzc3N0dHR1dXV2dnZ3d3d4eHh5eXl6enp7e3t8fHx9fX1+fn5/f3+AgICBgYGC\ngoKDg4OEhISFhYWGhoaHh4eIiIiJiYmKioqLi4uMjIyNjY2NoMuOjo6Pj4+RkZGSkpKTk5OV\nlZWWlpaXl5eYmJiampqbm5ucnJydnZ2enp6fn5+goKChoaGjo6OkpKSlpaWmpqam2FSnp6eo\nqKipqamqqqqrq6usrKytra2urq6vr6+wsLCxsbGzs7O0tLS1tbW2tra3t7e4uLi5ubm6urq7\nu7u8vLy9vb2+vr6/v7/AwMDBwcHCwsLDw8PExMTFxcXGxsbHx8fIyMjJycnKysrLy8vMzMzO\nzs7Pz8/Q0NDR0dHS0tLT09PU1NTV1dXW1tbX19fZ2dna2trb29vc3Nzd3d3e3t7f39/g4ODh\n4eHi4uLj4+Pk5OTl5eXm5ubnisPn5+fo6Ojp6enq6urr6+vs7Ozt7e3u7u7v7+/w8PDx8fHy\n8vLz8/P09PT19fX29vb39/f4+Pj5+fn6+vr7+/v8jWL8/Pz9/f3+/v7////wEBAMAAAACXBI\nWXMAABJ0AAASdAHeZh94AAAWwElEQVR4nO3dfZwddWHv8SGQRIFILU+KaHrrA3rBFAoFC0LL\nw01tJQnyWEAJCWhV8GLVXmihBS5tuBWosZYWAQVpkfpUEUVQBPUSFBXFKoSgrYEbwpJoIslG\ncpPMHz3nLLssip5kznd32Dnv9x8zc87OOTPM6/fhzMzmvLYogZ4Vde8ANIGQIEBIECAkCBAS\nBAgJAoQEAUKCgIoh/cVsajbryFl17wJv7jWkt/xntdcRs25gbd270PeemD2yKKSJSkj1E1ID\nCKl+QmoAIdVPSA0gpPoJqQGEVD8hNYCQ6iekBhBS/YTUAEKqn5AaQEj1E1IDCKl+QmoAIdVP\nSA0gpPoJqQGEVD8hNYCQ6iekBhBS/YTUAEKqn5AaQEj1E1IDCKl+QmoAIdVPSA0gpPoJqQGE\nVD8hNYCQ6iekBhBS/YTUAEKqn5AaQEj1E1IDCKl+QmoAIdVPSA0gpPoJqQGEVD8hNYCQ6iek\nBhBS/YTUAEKqn5AaQEj1E1IDCKl+4xPSn8CEJiQIEBIECAkChAQBQoIAIUHAOIR0+n2Pd1X3\nYYDedB3iP57Vc0iLB7uq+zBAb7oO8dU9h+TUjubrOsRdI0F3QoIAIUGAkCBASBAgJAgQEgQI\nCQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIA\nIUGAkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQ\nICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJ\nAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKEBAFCggAh\nQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQEA1p6bvntGfvmNVynJDoI8mQvnzKwk5I\n824cGBhYIST6SDKkLz66qBPSsXc/7Wkh0XzJkMqyE9ITs/7+rPkLlgqJPjIGIf3kTe+7774L\n3vR4a/Erh7ac8J3Huqr7MEBvug7xZUduaUgda4+7pf14dsuJ967squ7DAL3pOsSXVwupfPs/\nDy85taP5ug7xLT+1++EH1pfl4HG3CYn+kQxp5cAtcwYGBleftHDZ0gXz1gmJ/pEM6bT2L2Jn\nfbpcct4Jb7zokZGnhUTzJUP6JYRE8wkJAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIA\nIUGAkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQ\nICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJ\nAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKEBAFCggAh\nQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCBASBAg\nJAgQEgQICQKEBAFCggAhQYCQIGAcQjr9/rVd1X0YoDddh/iqWT2HtHiwq7oPA/Sm6xBf3XNI\nTu1ovq5D3DUSdCckCBASBAgJAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCBA\nSBAgJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQICQIEBIE\nCAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKC\nACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBI\nECAkCBASBAgJAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQI\nCQKEBAHRkJa+e0579tPL5p504XIh0UeSIX35lIWdkC46+8GHLjljo5DoH8mQvvjoonZIA7OX\ntD6VjrpHSPSPZEhl2QnpzmM2taZn3iAk+scYhHTzqe3Fc69oTb5yaMsJ33msq7oPA/Sm6xBf\nduQzh/T4R+fvvfv2L9p7/kcf//mQ5o2EtGh2y4n3ruyq7sMAvek6xJc/Y0jrLt25mDLjsKMP\nmzGl2PnSdU8L6a6hU7uPDT/p1I7m6zrEn/HU7gf7Tjr+pjWdxTU3HT9p3x+MDmnF7MVluWrO\nd4VE/6gW0vMP/d6oVb536K935isHbpkzMDBYXvzOB5de8K5NQqJ/VAvpvA1PW2fDuZ3ZabPa\nPl2uWXjKyQtWjvxUSDRftZDa1jxclms/dOmSru8gJJqvckjf3+Xicv1+RbHDN4UElUM6+tUP\nlNcWlz9w4LFCgsoh7XJdWb5hr7K87sVCgsohTbmt3PD8/1WWt0wRElQO6cVXlrcUt5XlVS8U\nElQO6bQXnDP9pRvK5TNcI0H1kB5+TbHTorI8YYdvCwkqh1SWq55oTe5+pOs7CInmqxbSvLVP\nW2ftfCHR36qFNH3G7aNWuX3GdCHR36qF9NjM4pCrl3YWl159SDHzMSHR36qFVG689mVFseue\nB+65a1G8/NqNz/A6IdFPKoZUlhtuP+/1+79y/9efd/uGX3iNkOg3lUPafEKi+YQEAUKCACFB\ngJAgQEgQ0ENIg1//5EC5XkjQS0iXTiuKReVfnNo1JSHRfJVDuqKY/U+tkK7Z5r2JkP4/TGiV\nQ5rx1nKwFVL5568QElQO6Tm3DoX0+clCgsoh7XLjUEj/+jwhQeWQjvi9te2QVuw1U0hQOaQv\nbf2ys4r5c583+atCgsohlV/Yp2jZ//aff4GQ6EPVQyrL5d/61sqyOyHRfL2EtPrHHUKCyiEt\nef12xRAhQeWQfn+Hk99zdoeQoHJI2/3f7nkIiX5ROaRdHhISDKsc0rsvEhIMqxzSz4446D0X\ndwgJKod0cVG4awdPqhzSC4/56gM/6BASVA5pqpsNMKJySPvcIyQYVjmkOw7r+qf6hETfqBzS\nQbsX20/vEBJUDungw4cJCSqHtPmERPMJCQKqhbTHgnKPEUKCaiEdsLA8YISQoFpIW0RINF/l\nkPb93tD8468SElQOqbi7M1t/4RQhQcWQiqf8tpCgYkj3vL+Yc1rb6X/1IyFBxZDK8g/u756H\nkOgXlUPafEKi+SqHtHzubpN8QxaGVA7puG0On9u5SjpNSFA5pB3/rXseQqJfVA5p20eFBMMq\nh3Twl4QEwyqH9I397xQSPKlySAe9uNjWV81hSOWQfNUcnlI5pM0nJJpPSBBQOaQdh00TElQO\naU7H/s/d6wwhQeWQnrTskM8ICXoNqbx7XyFBzyEte66QoNeQNv3N7kKCyiH9VsdeOxXvERL0\nGNI+h73/Z0KCyiFtPiHRfL2H5G/IQtWQ7pj5spmfbS+s+2t37aBiSIsmb/WSyVv9a1l+/uWF\nv0YBFUOas8M95fL9XvWjY4tfW/iEkKBaSL9xVmvyueI5W79toHskQqL5qoW0zT+0Jj8sfu/e\n7okIiX5QLaTig63JsuJzm9ORkOgDQoIAIUFAxZD+fNGiRTcVCxe1CQkqhjSakKBaSOePJiSo\nFtIWERLNJyQIEBIECAkChAQBQoIAIUGAkCBgHEI6/f61XdV9GKA3XYf4qlk9h7R4sKu6DwP0\npusQX91zSE7taL6uQ9w1EnQnJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKC\nACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBI\nECAkCBASBAgJAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQI\nCQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIA\nIUGAkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQ\nICQIEBIECAkChAQBYxHSO2a1HCck+shYhDTvxoGBgRVCoo+MRUjH3v20h0Ki+cYgpCdm/f1Z\n8xcsFRJ9ZAxC+smb3nfffRe86fHW4lcObTnhO491VfdhgN50HeLLjtzSkDrWHndLa7podsuJ\n967squ7DAL3pOsSXVwupfPs/Dy85taP5ug7xLT+1++EH1pfl4HG3CYn+MQYhrT5p4bKlC+at\nExL9YwxCKpecd8IbL3pk5KGQaL6xCOnnCInmExIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQI\nCQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIA\nIUGAkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQ\nICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJ\nAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKEBAFCggAh\nQYCQIEBIECAkCBASBAgJAoQEAUKCACFBwDiEdPr9a7uq+zBAb7oO8VWzeg5p8WBXdR8G6E3X\nIb6655Cc2tF8XYe4ayToTkgQICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKEBAFC\nggAhQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCDg\nWRLS38GEJiQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQICQKeJSH9P5jQhAQBQoIAIUGA\nkCBASBAgJAgQEgQICQKEBAFCggAhQYCQIEBIECAkCBASBAgJAoQEAUKCACFBgJAgQEgQICQI\nEBIECAkCniUh/QtMaEKCACFBgJAgQEgQICQIEBIECAkChAQBQoIAIUGAkCBASBAgJAgQEgQI\nCQKEBAFCggAhQYCQIEBIECAkCBASBIxFSD+9bO5JFy4XEn1kLEK66OwHH7rkjI1Con+MQUgD\ns5e0PpWOukdI9I8xCOnOYza1pmfeICT6xxiEdPOp7em5V7Qmi2a3nHjvyq7qPgzQm65DfPmR\nWxzSvC0PiTG1YmBF3bvQ97Y8pLuGTu0+Nvx4c07tGFPrBtbWvQt9b8tP7VbMXlyWq+Z8d/ix\nkGonpPpVuP198TsfXHrBuzYNPxRS7YRUvwohrVl4yskLVo48FFLthFS/8fknQowpIdVPSA0g\npPoJqQGEVD8hNYCQ6iekBhBS/YTUAEKqn5AaQEj1E1IDCKl+QmoAIdVPSA0gpPoJqQGEVD8h\nNYCQ6iekBhBS/YTUAEKqn5AaQEj1E1IDCKl+QmoAIdVPSA0gpPoJqQGEVD8hNYCQ6iekBhBS\n/YTUAEKqn5AaQEj1E1IDCKl+QmoAIdVPSA0gpPoJqQGEVD8hNYCQ6iekBhBS/QIhvf/D1OvK\nf/hg3bvQ967qOaQ7PkHNPjD/krp3gc/3GhK1u3Xfa+veBZ4ipIlKSM8qQpqohPSsIqSJSkjP\nKkKCACFBgJAgQEgQIKQJaMUlbzz+nPvK8qeXzT3pwuV17w1tQpqA/vTsJQ9fevJgedHZDz50\nyRkb694dSiFNRKsX/GdZPjrr/oHZS1qfSkfdU/f+UAppwvr+nJV3HrOptXDmDXXvCqWQJqrV\nb/9QefOp7aVzr6h7XyiFNEH96C2XbypvntdeFNKzgpAmontOurE1vWvo1O5jde8NpZAmpH8/\n8Rvt2YrZi8ty1Zzv1r07lEKaiH725usHWgbLi9/54NIL3rWp7v2hFNJEdM+sjs+UaxaecvKC\nlXXvDm1CggAhQYCQIEBIECAkCBASBAgJAoQEAUIaH+cXOz8xtHRacdAv/viE7UY/OmiP4aWB\nv/ntHbfZ+Q9ubi0esMcvvGqUx6bPb00/cVxZPvrCrjvz9K0NO/fXf9D1lfwyQhof50/a+lOd\nhbXPm7z5Ia34jW3P/Mj1f/2bk64vy4ULfsXbb5w5o/23Kc5trXPzH3XdmWcOacOh+67r+lJ+\nCSGNj/O3OXDoLxdcN3m/zQ/pfcVH27OVL5re5fvk1xa3t2eva310LTiv6848c0jl9yZd2vWl\n/BJCGh/nFwu2eaS9MHPmQe2QPnvw9s/Z87JNZbnpwt2n7vWxztC+/Yhpz93nqnJUSH9WLO7M\nf7S2c2p3dzHk3lHrdmx4xSGd+S6PluWxn3zyyYNf+83Dpu38x8u7be3h018yddejv99aOn6X\nx8fhUDSTkMbH+cXizv/vl066+jWtkD611ev+7QvvKv6sLP+2OPnWG/baozW0v7D1ITfe8tbi\n0lEhXV+84cfD79AKafWtLZ/ZefefjFq3447i6rK8ZOrUYurUqVtNnbq08+ThL/6dW5d/fOu5\n3bb2mhdcedt1r95lTVneVPjaelVCGh/nF4NH7Nma/5/nrj6gFdIrX/Kz1oOjJj+2abe9WgsP\nT24N7X1e1hrL5expg0+FtPH4Yuof/e1dnfO64ZsN86Z+bfS6HX9ZdNr5+NFl+chuw5s8vPhq\ne7pbl62tKs5pLTyw4KGyXDPltDE/EE0lpPHRCukjxdfL8lUnlq2QHire2n7yquIz/1H8z/bS\n725XLi/OGmz5p9ZaT921K28+abei2OmcNSMhXV58sBy9bsfrd+3M/vR9ZfmJY4dfevi27enc\nSV229sSO078wfAU2Y++xPAaNJqTx0QppzbS3lV8vPtcO6evFRe0nP1tc8bWhpWO2K7/15AVQ\n8cnRIbUs+eDBxe9ufDKkO6e8pTUdtW7H/nt2Zr/ztaGYhhw+vT09rei2ta/+t2LHY65b3/7B\nYbuP4SFoNiGNj1ZI5fxfGzzjhRvaId1dXNh+8qbiyruGhvZR7aE9f1HHwM+FVJab5hd3DIW0\nbLcD2mdpo9bteOWBrcmLhi6RpkydN/TkSEhdtlZu+OJ7/nuxX/v2+dHbj/VxaCwhjY92SHcU\nn97p3WU7pGVF+3OlvKK4eUlxRntp7+3KFcXc4ZWHQ1r3kaHfPZXXFB/phPTEwbt2LoZGrdsx\n9Il052vLcv32I78LGgmpy9Y6Li8+3Joe9qLUf2/fEdL4aIe06Tf3K77dCanca7f2bYLXbbtq\n404vbV2g3LdV6/J//x3ad+iuOXf9SEibXr7zkvZ8w5HFdzohnbnNHUM/eWrdjqFrpMvPLMtv\n/9bIJkdC+tVb+8YJ7RvkDxSXlK6ReiCk8dEOqbygaA/zdkg3TZr56c+9rbi4fcPt6E/84/R9\nW0P79skzrvn8eZNPHXX7+0vbT3vz+6/83zOKd3RuNtxQHN++AX7rklHrdpzbuWv3livL8sPz\nRjb5VEi/cmvLps246taPHvi8B8pyzdR5JdUIaXx0Qnpwq8vKoZDKW1673dR9rm4tbDjnBVNe\n/akzp7QWv/I/pk1+xXvXj/63dv8+/6VTt9n1Dz9edkI668kbBOePWrfjS8WH2mt8oyzP+sDI\nJp8K6Vdv7dtv2GXybm/4Ztm+HXH92B+JhhJSE6x/6e8n3uaPd/pp4m36kpAa4Zriy72/yfcn\nvbf3N+lXQmqEjUfsPdjzexy+T8/v0b+E1AwDne8j9eQvn/9gYk/6lJAgQEgQICQIEBIECAkC\nhAQBQoIAIUHAfwG0KGlJcWymTQAAAABJRU5ErkJggg==",
334 "text/plain": [ 340 "text/plain": [
335 "plot without title" 341 "plot without title"
336 ] 342 ]
@@ -351,10 +357,11 @@
351 "source": [ 357 "source": [
352 "FamilyTreeRQ2Raw <- rbind(\n", 358 "FamilyTreeRQ2Raw <- rbind(\n",
353 "# Load10Log(\"measurements/stats/FamilyTree//size010to-1r10n10rt300nsdrealstats_06-0249.csv\", 10),\n", 359 "# Load10Log(\"measurements/stats/FamilyTree//size010to-1r10n10rt300nsdrealstats_06-0249.csv\", 10),\n",
354 " Load10Log(\"measurements1/stats1010.csv\", 20),\n", 360 " Load10Log(\"measurements2/stats/FamilyTree/size020to-1r10n10rt3600nsdreal-localstats_06-1949.csv\", 20)\n",
355 " Load10Log(\"measurements1/stats1515.csv\", 30),\n", 361 "# Load10Log(\"measurements1/stats1010.csv\", 20),\n",
356 " Load10Log(\"measurements1/stats2020.csv\", 40),\n", 362 "# Load10Log(\"measurements1/stats1515.csv\", 30),\n",
357 " Load10Log(\"measurements1/stats2525.csv\", 50)\n", 363 "# Load10Log(\"measurements1/stats2020.csv\", 40),\n",
364 "# Load10Log(\"measurements1/stats2525.csv\", 50)\n",
358 ")\n", 365 ")\n",
359 "FamilyTreeRQ2Raw\n", 366 "FamilyTreeRQ2Raw\n",
360 "FamilyTreeRQ2 <- FamilyTreeRQ2Raw %>% ProcessRQ2\n", 367 "FamilyTreeRQ2 <- FamilyTreeRQ2Raw %>% ProcessRQ2\n",
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar
new file mode 100644
index 00000000..8d981fde
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar
Binary files differ
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig
index 94295dd1..0aa82872 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig
@@ -14,8 +14,8 @@ generate {
14 14
15 config = { 15 config = {
16 runtime = 10000, 16 runtime = 10000,
17 log-level = normal, 17 "numeric-solver" = "z3",
18 "scopePropagator" = "typeHierarchy" 18 log-level = none
19 } 19 }
20 20
21 runs = 1 21 runs = 1
@@ -35,10 +35,13 @@ generate {
35 config = { 35 config = {
36 runtime = 10000, 36 runtime = 10000,
37 "numeric-solver" = "z3", 37 "numeric-solver" = "z3",
38 "scopePropagator" = "typeHierarchy", 38 "dreal-local-path" = "enterPathHere",
39 log-level = normal, 39 log-level = none,
40 "fitness-punishSize" = "false", 40 "fitness-punishSize" = "false",
41 "fitness-scope" = "3" 41 "fitness-scope" = "3",
42 "fitness-objectCreationCosts" = "true",
43 "scopePropagator" = "typeHierarchy",
44 "fitness-missing-containment" = "2"
42 } 45 }
43 46
44 runs = 1 47 runs = 1
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig
index fdb04161..691b0e58 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig
@@ -1,51 +1,52 @@
1import epackage "../case.study.familyTree.model/model/familytree.ecore" 1import epackage "../case.study.familyTree.model/model/familytree.ecore"
2import viatra "queries/familyTreeConstraints.vql" 2import viatra "queries/familyTreeConstraints.vql"
3import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" 3import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"
4import viatra "queries/SatelliteQueries.vql" 4import viatra "queries/SatelliteQueries.vql"
5 5
6generate { 6generate {
7 metamodel = { package satellite } 7 metamodel = { package satellite }
8 constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } 8 constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries }
9 partial-model = { "inputs/SatelliteInstance.xmi"} 9 partial-model = { "inputs/SatelliteInstance.xmi"}
10 solver = ViatraSolver 10 solver = ViatraSolver
11 scope = { 11 scope = {
12 #node += 10..* 12 #node += 10..*
13 } 13 }
14 14
15 config = { 15 config = {
16 runtime = 10000, 16 runtime = 10000,
17 log-level = normal, 17 "numeric-solver" = "z3",
18 "scopePropagator" = "typeHierarchy" 18 log-level = none
19 } 19 }
20 20
21 runs = 1 21 runs = 1
22 22
23 output = "measurements/debug/warmup" 23 output = "measurements/debug/warmup"
24} 24}
25 25
26generate { 26generate {
27 metamodel = { package familytree } 27 metamodel = { package familytree }
28 constraints = { package queries} 28 constraints = { package queries}
29 partial-model = { "inputs/FamilyTree.xmi" } 29 partial-model = { "inputs/FamilyTree.xmi" }
30 solver = ViatraSolver 30 solver = ViatraSolver
31 scope = { 31 scope = {
32 #node += 6..* 32 #node += 6..*
33 } 33 }
34 34
35 config = { 35 config = {
36 runtime = 10000, 36 runtime = 10000,
37 "numeric-solver" = "z3", 37 "numeric-solver" = "z3",
38 log-level = normal, 38 "dreal-local-path" = "enterPathHere",
39 "fitness-punishSize" = "false", 39 log-level = none,
40 "fitness-scope" = "3", 40 "fitness-punishSize" = "false",
41 "numeric-solver-at-end" = "true" 41 "fitness-scope" = "3",
42 } 42 "numeric-solver-at-end" = "true"
43 43 }
44 runs = 1 44
45 number = 10 45 runs = 1
46 46 number = 10
47 debug = "outputs/debug" 47
48 log = "outputs/log.txt" 48 debug = "outputs/debug"
49 output = "outputs/models" 49 log = "outputs/log.txt"
50 statistics = "output/debug/statistics.csv" 50 output = "outputs/models"
51 statistics = "output/debug/statistics.csv"
51} \ No newline at end of file 52} \ No newline at end of file
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig
index 56dc86b5..e252d13c 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig
@@ -1,54 +1,55 @@
1import epackage "../case.study.familyTree.model/model/familytree.ecore" 1import epackage "../case.study.familyTree.model/model/familytree.ecore"
2import viatra "queries/familyTreeConstraintsQual.vql" 2import viatra "queries/familyTreeConstraintsQual.vql"
3import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" 3import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"
4import viatra "queries/SatelliteQueries.vql" 4import viatra "queries/SatelliteQueries.vql"
5 5
6generate { 6generate {
7 metamodel = { package satellite } 7 metamodel = { package satellite }
8 constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } 8 constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries }
9 partial-model = { "inputs/SatelliteInstance.xmi"} 9 partial-model = { "inputs/SatelliteInstance.xmi"}
10 solver = ViatraSolver 10 solver = ViatraSolver
11 scope = { 11 scope = {
12 #node += 10..* 12 #node += 10..*
13 } 13 }
14 14
15 config = { 15 config = {
16 runtime = 10000, 16 runtime = 10000,
17 log-level = normal, 17 "numeric-solver" = "z3",
18 "scopePropagator" = "typeHierarchy" 18 log-level = none
19 } 19 }
20 20
21 runs = 1 21 runs = 1
22 22
23 output = "measurements/debug/warmup" 23 output = "measurements/debug/warmup"
24} 24}
25 25
26generate { 26generate {
27 metamodel = { package familytree } 27 metamodel = { package familytree }
28 constraints = { package queries} 28 constraints = { package queries}
29 partial-model = { "inputs/FamilyTree.xmi" } 29 partial-model = { "inputs/FamilyTree.xmi" }
30 solver = ViatraSolver 30 solver = ViatraSolver
31 scope = { 31 scope = {
32 #node += 6..* 32 #node += 6..*
33 } 33 }
34 34
35 config = { 35 config = {
36 runtime = 10000, 36 runtime = 10000,
37 "numeric-solver" = "z3", 37 "numeric-solver" = "z3",
38 log-level = normal, 38 "dreal-local-path" = "enterPathHere",
39 "fitness-punishSize" = "false", 39 log-level = none,
40 "fitness-scope" = "3", 40 "fitness-punishSize" = "false",
41 "fitness-objectCreationCosts" = "true", 41 "fitness-scope" = "3",
42 "scopePropagator" = "typeHierarchy", 42 "fitness-objectCreationCosts" = "true",
43 "fitness-missing-containment" = "2", 43 "scopePropagator" = "typeHierarchy",
44 "numeric-solver-at-end" = "true" 44 "fitness-missing-containment" = "2",
45 } 45 "numeric-solver-at-end" = "true"
46 46 }
47 runs = 1 47
48 number = 10 48 runs = 1
49 49 number = 10
50 debug = "outputs/debug" 50
51 log = "outputs/log.txt" 51 debug = "outputs/debug"
52 output = "outputs/models" 52 log = "outputs/log.txt"
53 statistics = "output/debug/statistics.csv" 53 output = "outputs/models"
54 statistics = "output/debug/statistics.csv"
54} \ No newline at end of file 55} \ No newline at end of file
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig
index 4a0bd920..2be8cb2e 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig
@@ -12,8 +12,8 @@ generate {
12 12
13 config = { 13 config = {
14 runtime = 10000, 14 runtime = 10000,
15 log-level = normal, 15 "numeric-solver" = "z3",
16 "scopePropagator" = "typeHierarchy" 16 log-level = none
17 } 17 }
18 18
19 runs = 1 19 runs = 1
@@ -33,10 +33,12 @@ generate {
33 config = { 33 config = {
34 runtime = 10000, 34 runtime = 10000,
35 "numeric-solver" = "z3", 35 "numeric-solver" = "z3",
36 log-level = normal, 36 "dreal-local-path" = "enterPathHere",
37 log-level = none,
37 "fitness-scope" = "3", 38 "fitness-scope" = "3",
38 "fitness-punishSize" = "true", 39 "fitness-punishSize" = "true",
39 "scopePropagator" = "polyhedral" 40 "scopePropagator" = "polyhedral",
41 "fitness-missing-containment" = "1"
40 } 42 }
41 43
42 runs = 1 44 runs = 1
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig
index c609bf33..9d576660 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig
@@ -1,54 +1,55 @@
1import epackage "../case.study.pledge.model/model/TaxationWithRoot.ecore" 1import epackage "../case.study.pledge.model/model/TaxationWithRoot.ecore"
2import viatra "queries/case_study_A_withRoot.vql" 2import viatra "queries/case_study_A_withRoot.vql"
3import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" 3import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore"
4import viatra "queries/SatelliteQueries.vql" 4import viatra "queries/SatelliteQueries.vql"
5 5
6generate { 6generate {
7 metamodel = { package satellite } 7 metamodel = { package satellite }
8 constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } 8 constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries }
9 partial-model = { "inputs/SatelliteInstance.xmi"} 9 partial-model = { "inputs/SatelliteInstance.xmi"}
10 solver = ViatraSolver 10 solver = ViatraSolver
11 scope = { 11 scope = {
12 #node += 10..* 12 #node += 10..*
13 } 13 }
14 14
15 config = { 15 config = {
16 runtime = 10000, 16 runtime = 10000,
17 log-level = normal, 17 "numeric-solver" = "z3",
18 "scopePropagator" = "typeHierarchy" 18 log-level = none
19 } 19 }
20 20
21 runs = 1 21 runs = 1
22 22
23 output = "measurements/debug/warmup" 23 output = "measurements/debug/warmup"
24} 24}
25 25
26generate { 26generate {
27 metamodel = { package TaxationWithRoot } 27 metamodel = { package TaxationWithRoot }
28 constraints = { package queries} 28 constraints = { package queries}
29 partial-model = { "inputs/Resource.xmi" } 29 partial-model = { "inputs/Resource.xmi" }
30 solver = ViatraSolver 30 solver = ViatraSolver
31 scope = { 31 scope = {
32 #node += 70..*, 32 #node += 70..*,
33 #<Household> += 0 33 #<Household> += 0
34 } 34 }
35 35
36 config = { 36 config = {
37 runtime = 10000, 37 runtime = 10000,
38 "numeric-solver" = "z3", 38 "numeric-solver" = "z3",
39 log-level = normal, 39 "dreal-local-path" = "enterPathHere",
40 "fitness-scope" = "1", 40 log-level = none,
41 "fitness-punishSize" = "inverse", 41 "fitness-scope" = "1",
42 "fitness-objectCreationCosts" = "true", 42 "fitness-punishSize" = "inverse",
43 "scopePropagator" = "typeHierarchy", 43 "fitness-objectCreationCosts" = "true",
44 "fitness-missing-containment" = "2" 44 "scopePropagator" = "typeHierarchy",
45 } 45 "fitness-missing-containment" = "2"
46 46 }
47 runs = 1 47
48 number = 10 48 runs = 1
49 49 number = 10
50 debug = "output/debug/" 50
51 log = "output/debug/log.txt" 51 debug = "output/debug/"
52 output = "output/models" 52 log = "output/debug/log.txt"
53 statistics = "output/debug/statistics.csv" 53 output = "output/models"
54 statistics = "output/debug/statistics.csv"
54} \ No newline at end of file 55} \ No newline at end of file
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/plots/plot_RQ2_FamilyTree.pdf b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/plots/plot_RQ2_FamilyTree.pdf
index c6cda90a..c424f393 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/plots/plot_RQ2_FamilyTree.pdf
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/plots/plot_RQ2_FamilyTree.pdf
Binary files differ
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/plugin.xml b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/plugin.xml
index 2f4febdb..c760d4ef 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/plugin.xml
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/plugin.xml
@@ -1 +1 @@
<?xml version="1.0" encoding="UTF-8"?><plugin/> <?xml version="1.0" encoding="UTF-8"?><plugin/>
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/run.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/run.sh
index 0b0c560e..1800971d 100755
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/run.sh
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/run.sh
@@ -2,4 +2,4 @@
2NODE="$1" 2NODE="$1"
3shift 3shift
4CPUS="$((NODE*3))-$((NODE*3+2))" 4CPUS="$((NODE*3))-$((NODE*3+2))"
5taskset -c "${CPUS}" env LD_LIBRARY_PATH=/home/models/VIATRA-Generator/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/lib:/home/models/VIATRA-Generator/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib java -Xmx2g -Xms2g -XX:+UseG1GC -XX:ParallelGCThreads=3 -XX:ConcGCThreads=1 -XX:G1ConcRefinementThreads=3 -jar RunGeneratorConfig.jar "$@" 5taskset -c "${CPUS}" env LD_LIBRARY_PATH=/home/models/VIATRA-Generator/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/lib:/home/models/VIATRA-Generator/olvers/SMT-Solver/com.microsoft.z3/lib:/home/models/VIATRA-Generator/Solvers/ILP-Solver/hu.bme.mit.inf.dslreasoner.ilp.cbc/lib java -Xmx6g -Xms6g -XX:+UseG1GC -XX:ParallelGCThreads=3 -XX:ConcGCThreads=1 -XX:G1ConcRefinementThreads=3 -jar RunGeneratorConfig.jar "$@"
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runFamilyTree.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runFamilyTree.sh
index 5895ff6a..18724a1c 100755
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runFamilyTree.sh
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runFamilyTree.sh
@@ -1,7 +1,12 @@
1#!/usr/bin/bash 1#!/usr/bin/bash
2NODE="$1" 2NODE="$1"
3./run.sh "${NODE}" -d FamilyTree -lb 20 -nm 10 -rt 3600 3./run.sh "${NODE}" -d FamilyTree -lb 20 -nm 10 -rt 3600 -ns z3
4./run.sh "${NODE}" -d FamilyTree -lb 40 -nm 10 -rt 3600 4./run.sh "${NODE}" -d FamilyTree -lb 40 -nm 10 -rt 3600 -ns z3
5./run.sh "${NODE}" -d FamilyTree -lb 60 -nm 10 -rt 3600 5./run.sh "${NODE}" -d FamilyTree -lb 60 -nm 10 -rt 3600 -ns z3
6./run.sh "${NODE}" -d FamilyTree -lb 80 -nm 10 -rt 3600 6./run.sh "${NODE}" -d FamilyTree -lb 80 -nm 10 -rt 3600 -ns z3
7./run.sh "${NODE}" -d FamilyTree -lb 100 -nm 10 -rt 3600 7./run.sh "${NODE}" -d FamilyTree -lb 100 -nm 10 -rt 3600 -ns z3
8./run.sh "${NODE}" -d FamilyTree -lb 20 -nm 10 -rt 3600 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
9./run.sh "${NODE}" -d FamilyTree -lb 40 -nm 10 -rt 3600 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
10./run.sh "${NODE}" -d FamilyTree -lb 60 -nm 10 -rt 3600 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
11./run.sh "${NODE}" -d FamilyTree -lb 80 -nm 10 -rt 3600 -ns dreal -drp /home/modelsdreal4/bazel-bin/dreal/dreal
12./run.sh "${NODE}" -d FamilyTree -lb 100 -nm 10 -rt 3600 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runSatellite.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runSatellite.sh
index f5eee8a3..b6c41716 100755
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runSatellite.sh
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runSatellite.sh
@@ -1,7 +1,12 @@
1#!/usr/bin/bash 1#!/usr/bin/bash
2NODE="$1" 2NODE="$1"
3./run.sh "${NODE}" -d Satellite -lb 20 -nm 10 -rt 3600 3./run.sh "${NODE}" -d Satellite -lb 20 -nm 10 -rt 3600 -ns z3
4./run.sh "${NODE}" -d Satellite -lb 40 -nm 10 -rt 3600 4./run.sh "${NODE}" -d Satellite -lb 40 -nm 10 -rt 3600 -ns z3
5./run.sh "${NODE}" -d Satellite -lb 60 -nm 10 -rt 3600 5./run.sh "${NODE}" -d Satellite -lb 60 -nm 10 -rt 3600 -ns z3
6./run.sh "${NODE}" -d Satellite -lb 80 -nm 10 -rt 3600 6./run.sh "${NODE}" -d Satellite -lb 80 -nm 10 -rt 3600 -ns z3
7./run.sh "${NODE}" -d Satellite -lb 100 -nm 10 -rt 3600 7./run.sh "${NODE}" -d Satellite -lb 100 -nm 10 -rt 3600 -ns z3
8./run.sh "${NODE}" -d Satellite -lb 20 -nm 10 -rt 3600 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
9./run.sh "${NODE}" -d Satellite -lb 40 -nm 10 -rt 3600 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
10./run.sh "${NODE}" -d Satellite -lb 60 -nm 10 -rt 3600 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
11./run.sh "${NODE}" -d Satellite -lb 80 -nm 10 -rt 3600 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
12./run.sh "${NODE}" -d Satellite -lb 100 -nm 10 -rt 3600 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal \ No newline at end of file
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTaxation.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTaxation.sh
index 75080359..b77d4366 100755
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTaxation.sh
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTaxation.sh
@@ -1,7 +1,12 @@
1#!/usr/bin/bash 1#!/usr/bin/bash
2NODE="$1" 2NODE="$1"
3./run.sh "${NODE}" -d Taxation -lb 20 -nm 10 -rt 3600 -hh 1 3./run.sh "${NODE}" -d Taxation -lb 20 -nm 10 -rt 3600 -hh 1 -ns z3
4./run.sh "${NODE}" -d Taxation -lb 40 -nm 10 -rt 3600 -hh 2 4./run.sh "${NODE}" -d Taxation -lb 40 -nm 10 -rt 3600 -hh 2 -ns z3
5./run.sh "${NODE}" -d Taxation -lb 60 -nm 10 -rt 3600 -hh 3 5./run.sh "${NODE}" -d Taxation -lb 60 -nm 10 -rt 3600 -hh 3 -ns z3
6./run.sh "${NODE}" -d Taxation -lb 80 -nm 10 -rt 3600 -hh 4 6./run.sh "${NODE}" -d Taxation -lb 80 -nm 10 -rt 3600 -hh 4 -ns z3
7./run.sh "${NODE}" -d Taxation -lb 100 -nm 10 -rt 3600 -hh 5 7./run.sh "${NODE}" -d Taxation -lb 100 -nm 10 -rt 3600 -hh 5 -ns z3
8./run.sh "${NODE}" -d Taxation -lb 20 -nm 10 -rt 3600 -hh 1 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
9./run.sh "${NODE}" -d Taxation -lb 40 -nm 10 -rt 3600 -hh 2 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
10./run.sh "${NODE}" -d Taxation -lb 60 -nm 10 -rt 3600 -hh 3 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
11./run.sh "${NODE}" -d Taxation -lb 80 -nm 10 -rt 3600 -hh 4 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
12./run.sh "${NODE}" -d Taxation -lb 100 -nm 10 -rt 3600 -hh 5 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTest.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTest.sh
new file mode 100755
index 00000000..1b3f124c
--- /dev/null
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTest.sh
@@ -0,0 +1,6 @@
1#!/usr/bin/bash
2NODE="$1"
3./run.sh "${NODE}" -d FamilyTree -lb 10 -nr 3 -nm 2 -rt 3600 -hh 1 -ns z3
4./run.sh "${NODE}" -d Satellite -lb 10 -nr 3 -nm 2 -rt 3600 -hh 1 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal
5./run.sh "${NODE}" -d Taxation -lb 10 -nr 1 -nm 2 -rt 3600 -hh 1 -ns z3
6
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
index e1232040..eddb8bb5 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
@@ -38,7 +38,8 @@ class RunGeneratorConfig {
38 static var MODELS = 10 38 static var MODELS = 10
39 static var RUNTIME = 1500 39 static var RUNTIME = 1500
40 static var NUM_SOLVER = "z3" 40 static var NUM_SOLVER = "z3"
41 static var SCOPE_PROPAGATOR = "typeHierarchy" 41 static var DREAL_PATH = ""
42// static var SCOPE_PROPAGATOR = "typeHierarchy"
42 43
43 static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation" 44 static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation"
44 static val QUERIES = true 45 static val QUERIES = true
@@ -71,9 +72,12 @@ class RunGeneratorConfig {
71 val ns = new Option("ns", "numericSolver", true, "what numeric solver to use") 72 val ns = new Option("ns", "numericSolver", true, "what numeric solver to use")
72 options.addOption(ns) 73 options.addOption(ns)
73 74
74 val sp = new Option("sp", "scopePropagator", true, "scope Propagator") 75 val drp = new Option("drp", "drealPath", true, "path to dreal executeable")
75 options.addOption(sp) 76 options.addOption(drp)
76 77
78// val sp = new Option("sp", "scopePropagator", true, "scope Propagator")
79// options.addOption(sp)
80//
77 val d = new Option("d", "domain", true, "domain") 81 val d = new Option("d", "domain", true, "domain")
78 options.addOption(d) 82 options.addOption(d)
79 83
@@ -103,9 +107,11 @@ class RunGeneratorConfig {
103 val rtIn = cmd.getOptionValue("runtime") 107 val rtIn = cmd.getOptionValue("runtime")
104 if(rtIn !== null) RUNTIME = Integer.parseInt(rtIn) 108 if(rtIn !== null) RUNTIME = Integer.parseInt(rtIn)
105 val nsIn = cmd.getOptionValue("numericSolver") 109 val nsIn = cmd.getOptionValue("numericSolver")
106 if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal" 110 if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal-local"
107 val spIn = cmd.getOptionValue("scopePropagator") 111 val drpIn = cmd.getOptionValue("drealPath")
108 if(spIn !== null ) SCOPE_PROPAGATOR = spIn 112 if(drpIn !== null) DREAL_PATH = drpIn
113// val spIn = cmd.getOptionValue("scopePropagator")
114// if(spIn !== null ) SCOPE_PROPAGATOR = spIn
109 val dIn = cmd.getOptionValue("domain") 115 val dIn = cmd.getOptionValue("domain")
110 if(dIn !== null) DOMAIN = dIn 116 if(dIn !== null) DOMAIN = dIn
111 val hhIn = cmd.getOptionValue("household") 117 val hhIn = cmd.getOptionValue("household")
@@ -126,7 +132,7 @@ class RunGeneratorConfig {
126 println( 132 println(
127 "<<DOMAIN: " + DOMAIN + 133 "<<DOMAIN: " + DOMAIN +
128 ", NumSolver=" + NUM_SOLVER + 134 ", NumSolver=" + NUM_SOLVER +
129 ", scopeProp=" + SCOPE_PROPAGATOR + 135// ", scopeProp=" + SCOPE_PROPAGATOR +
130 ", SIZE=" + SIZE_LB + "to" + SIZE_UB + 136 ", SIZE=" + SIZE_LB + "to" + SIZE_UB +
131 ", Runs=" + RUNS + 137 ", Runs=" + RUNS +
132 ", ModelsPerRun=" + MODELS + 138 ", ModelsPerRun=" + MODELS +
@@ -203,8 +209,10 @@ class RunGeneratorConfig {
203 runtimeEntry.millisecLimit = RUNTIME 209 runtimeEntry.millisecLimit = RUNTIME
204 val numSolverEntry = configScope.entries.get(1) as CustomEntry 210 val numSolverEntry = configScope.entries.get(1) as CustomEntry
205 numSolverEntry.value = NUM_SOLVER 211 numSolverEntry.value = NUM_SOLVER
206 val scopePropEntry = configScope.entries.get(2) as CustomEntry 212 val drealPathEntry = configScope.entries.get(2) as CustomEntry
207 scopePropEntry.value = SCOPE_PROPAGATOR 213 drealPathEntry.value = DREAL_PATH
214// val scopePropEntry = configScope.entries.get(3) as CustomEntry
215// scopePropEntry.value = SCOPE_PROPAGATOR
208 216
209 // Output locations 217 // Output locations
210 val debug = genTask.debugFolder as FileSpecification 218 val debug = genTask.debugFolder as FileSpecification