diff options
Diffstat (limited to 'Tests/MODELS2020-CaseStudies/case.study.pledge.run')
8 files changed, 443 insertions, 9 deletions
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/MODELS2020Plots-temp.ipynb b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/MODELS2020Plots-temp.ipynb new file mode 100644 index 00000000..3ced7f5b --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/MODELS2020Plots-temp.ipynb | |||
@@ -0,0 +1,364 @@ | |||
1 | { | ||
2 | "cells": [ | ||
3 | { | ||
4 | "cell_type": "markdown", | ||
5 | "metadata": {}, | ||
6 | "source": [ | ||
7 | "# Data analysis for the paper \"Automated Generation of Consistent Models with Structural and Attribute Constraints\"" | ||
8 | ] | ||
9 | }, | ||
10 | { | ||
11 | "cell_type": "markdown", | ||
12 | "metadata": {}, | ||
13 | "source": [ | ||
14 | "First, let's load some packages." | ||
15 | ] | ||
16 | }, | ||
17 | { | ||
18 | "cell_type": "code", | ||
19 | "execution_count": 7, | ||
20 | "metadata": { | ||
21 | "scrolled": true | ||
22 | }, | ||
23 | "outputs": [ | ||
24 | { | ||
25 | "name": "stderr", | ||
26 | "output_type": "stream", | ||
27 | "text": [ | ||
28 | "Warning message in dir.create(\"plots\"):\n", | ||
29 | "“'plots' already exists”\n" | ||
30 | ] | ||
31 | } | ||
32 | ], | ||
33 | "source": [ | ||
34 | "require(tidyverse)\n", | ||
35 | "dir.create('plots')" | ||
36 | ] | ||
37 | }, | ||
38 | { | ||
39 | "cell_type": "code", | ||
40 | "execution_count": 28, | ||
41 | "metadata": { | ||
42 | "scrolled": false | ||
43 | }, | ||
44 | "outputs": [], | ||
45 | "source": [ | ||
46 | "ProcessDetailedStatistics <- function(str) {\n", | ||
47 | " str <- sub('TransformationExecutionTime', 'TransformationExecutionTime:', str)\n", | ||
48 | " str <- sub('Backtrackingtime', 'BacktrackingTime', str)\n", | ||
49 | " str <- gsub('\\\\(|\\\\)', '', str)\n", | ||
50 | " str <- lapply(strsplit(str, '\\\\||:'), function (v) {\n", | ||
51 | " dim(v) <- c(2, 11)\n", | ||
52 | " values <- as.double(v[2,])\n", | ||
53 | " names(values) <- v[1,]\n", | ||
54 | " as.data.frame(t(values))\n", | ||
55 | " })\n", | ||
56 | " str\n", | ||
57 | "}\n", | ||
58 | "Load10Log <- function(filename, size) {\n", | ||
59 | " read_csv(filename, col_types = cols(\n", | ||
60 | " .default = col_double(),\n", | ||
61 | " Result = col_character(),\n", | ||
62 | " Solution1DetailedStatistics = col_character(),\n", | ||
63 | " Solution2DetailedStatistics = col_character(),\n", | ||
64 | " Solution3DetailedStatistics = col_character(),\n", | ||
65 | " Solution4DetailedStatistics = col_character(),\n", | ||
66 | " Solution5DetailedStatistics = col_character(),\n", | ||
67 | " Solution6DetailedStatistics = col_character(),\n", | ||
68 | " Solution7DetailedStatistics = col_character(),\n", | ||
69 | " Solution8DetailedStatistics = col_character(),\n", | ||
70 | " Solution9DetailedStatistics = col_character(),\n", | ||
71 | " Solution10DetailedStatistics = col_character()\n", | ||
72 | " )) %>% transmute(\n", | ||
73 | " n = size,\n", | ||
74 | " Run = Run,\n", | ||
75 | " preprocessingTime = get('Domain to logic transformation time') + get('Logic to solver transformation time') + ExplorationInitializationTime,\n", | ||
76 | " Solution0FoundAt = Solution0FoundAt,\n", | ||
77 | " additionalTime = Solution9FoundAt - Solution0FoundAt,\n", | ||
78 | " Solution1DetailedStatistics = ProcessDetailedStatistics(Solution1DetailedStatistics)\n", | ||
79 | " ) %>% unnest()\n", | ||
80 | "# %>% unnest() %>% mutate(\n", | ||
81 | "# # (Logical) constraint evluation should count as refinement.\n", | ||
82 | "# ForwardTime = ForwardTime + GlobalConstraintEvaluationTime + FitnessCalculationTime,\n", | ||
83 | "# preprocessingTime = preprocessingTime,\n", | ||
84 | "# BacktrackingTime = Solution0FoundAt - (StateCoderTime + ForwardTime + NumericalSolverSumTime)\n", | ||
85 | "# ) %>% select(n, Run, preprocessingTime, StateCoderTime, ForwardTime, BacktrackingTime, NumericalSolverSumTime, additionalTime)\n", | ||
86 | "}\n", | ||
87 | "Load1Log <- function(filename, size) {\n", | ||
88 | " read_csv(filename, col_types = cols(\n", | ||
89 | " .default = col_double(),\n", | ||
90 | " Result = col_character(),\n", | ||
91 | " Solution1DetailedStatistics = col_character()\n", | ||
92 | " )) %>% filter(Result == \"ModelResultImpl\") %>% transmute(\n", | ||
93 | " n = size,\n", | ||
94 | " Run = Run,\n", | ||
95 | " preprocessingTime = get('Domain to logic transformation time') + get('Logic to solver transformation time') + ExplorationInitializationTime,\n", | ||
96 | " Solution0FoundAt = Solution0FoundAt,\n", | ||
97 | " Solution1DetailedStatistics = ProcessDetailedStatistics(Solution1DetailedStatistics)\n", | ||
98 | " ) %>% unnest(cols = c(Solution1DetailedStatistics)) %>% mutate(\n", | ||
99 | " ForwardTime = ForwardTime + GlobalConstraintEvaluationTime + FitnessCalculationTime,\n", | ||
100 | " BacktrackingTime = Solution0FoundAt - (StateCoderTime + ForwardTime + NumericalSolverSumTime)\n", | ||
101 | " ) %>% select(n, Run, preprocessingTime, StateCoderTime, ForwardTime, BacktrackingTime, NumericalSolverSumTime)\n", | ||
102 | "}" | ||
103 | ] | ||
104 | }, | ||
105 | { | ||
106 | "cell_type": "code", | ||
107 | "execution_count": 13, | ||
108 | "metadata": {}, | ||
109 | "outputs": [], | ||
110 | "source": [ | ||
111 | "ProcessRQ1 <- function(df) {\n", | ||
112 | " df %>% group_by(n) %>% summarize(\n", | ||
113 | " .groups = 'drop',\n", | ||
114 | " time = median(preprocessingTime + StateCoderTime + ForwardTime + BacktrackingTime + NumericalSolverSumTime) / 1000.0\n", | ||
115 | " )\n", | ||
116 | "}\n", | ||
117 | "ProcessRQ2 <- function(df) {\n", | ||
118 | " df %>% group_by(n) %>% summarize(\n", | ||
119 | " .groups = 'drop',\n", | ||
120 | " preprocessingTime = median(preprocessingTime) / 1000.0,\n", | ||
121 | " StateCoderTime = median(StateCoderTime) / 1000.0,\n", | ||
122 | " ForwardTime = median(ForwardTime) / 1000.0,\n", | ||
123 | " BacktrackingTime = median(BacktrackingTime) / 1000.0,\n", | ||
124 | " NumericalSolverSumTime = median(NumericalSolverSumTime) / 1000.0,\n", | ||
125 | " additionalTime = median(additionalTime) / 1000.0\n", | ||
126 | " )\n", | ||
127 | "}\n", | ||
128 | "ProcessRQ3 <- ProcessRQ1" | ||
129 | ] | ||
130 | }, | ||
131 | { | ||
132 | "cell_type": "code", | ||
133 | "execution_count": 14, | ||
134 | "metadata": {}, | ||
135 | "outputs": [], | ||
136 | "source": [ | ||
137 | "RQ2Plot <- function(df, name) {\n", | ||
138 | " df <- df %>% gather(name, value, -n) %>% filter(name != \"preprocessingTime\")\n", | ||
139 | " df$name <- factor(df$name, levels=rev(c('ForwardTime', 'BacktrackingTime', 'StateCoderTime', 'NumericalSolverSumTime', 'additionalTime')))\n", | ||
140 | " plot <- df %>% ggplot(aes(x=n, y=value, fill=name)) +\n", | ||
141 | " geom_bar(stat='identity') +\n", | ||
142 | " scale_fill_brewer(palette='Set2',\n", | ||
143 | " labels=rev(c('Refinement', 'Backtracking', 'State Coding', 'SMT Solver Calls', 'Additional Model Generation')),\n", | ||
144 | " guide=FALSE) +\n", | ||
145 | " scale_x_continuous(breaks=c(20, 40, 60, 80, 100), name=\"Model Size (# nodes)\") +\n", | ||
146 | " scale_y_continuous(name=\"Runtime (s)\") +\n", | ||
147 | " theme_bw()\n", | ||
148 | " ggsave(plot=plot, filename=paste0('plots/plot_RQ2_', name, '.pdf'), width=3.5, height=2.5)\n", | ||
149 | " plot\n", | ||
150 | "}" | ||
151 | ] | ||
152 | }, | ||
153 | { | ||
154 | "cell_type": "markdown", | ||
155 | "metadata": {}, | ||
156 | "source": [ | ||
157 | "### Fam domain" | ||
158 | ] | ||
159 | }, | ||
160 | { | ||
161 | "cell_type": "code", | ||
162 | "execution_count": 29, | ||
163 | "metadata": {}, | ||
164 | "outputs": [ | ||
165 | { | ||
166 | "name": "stderr", | ||
167 | "output_type": "stream", | ||
168 | "text": [ | ||
169 | "Warning message:\n", | ||
170 | "“`cols` is now required when using unnest().\n", | ||
171 | "Please use `cols = c(Solution1DetailedStatistics)`”\n" | ||
172 | ] | ||
173 | }, | ||
174 | { | ||
175 | "data": { | ||
176 | "text/html": [ | ||
177 | "<table>\n", | ||
178 | "<caption>A tibble: 10 × 16</caption>\n", | ||
179 | "<thead>\n", | ||
180 | "\t<tr><th scope=col>n</th><th scope=col>Run</th><th scope=col>preprocessingTime</th><th scope=col>Solution0FoundAt</th><th scope=col>additionalTime</th><th scope=col>TransformationExecutionTime</th><th scope=col>ForwardTime</th><th scope=col>BacktrackingTime</th><th scope=col>GlobalConstraintEvaluationTime</th><th scope=col>FitnessCalculationTime</th><th scope=col>ActivationSelectionTime</th><th scope=col>SolutionCopyTime</th><th scope=col>NumericalSolverSumTime</th><th scope=col>NumericalSolverProblemFormingTime</th><th scope=col>NumericalSolverSolvingTime</th><th scope=col>NumericalSolverInterpretingSolution</th></tr>\n", | ||
181 | "\t<tr><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th><th scope=col><dbl></th></tr>\n", | ||
182 | "</thead>\n", | ||
183 | "<tbody>\n", | ||
184 | "\t<tr><td>20</td><td> 1</td><td>1038</td><td>5248</td><td>3980</td><td>31</td><td>225</td><td>108</td><td>10</td><td>1</td><td>0</td><td>1</td><td>4675</td><td>2239</td><td>2239</td><td>0</td></tr>\n", | ||
185 | "\t<tr><td>20</td><td> 2</td><td> 724</td><td>4132</td><td>3628</td><td>20</td><td>155</td><td> 76</td><td> 6</td><td>1</td><td>0</td><td>0</td><td>3780</td><td>2019</td><td>2019</td><td>0</td></tr>\n", | ||
186 | "\t<tr><td>20</td><td> 3</td><td> 735</td><td>5329</td><td>4437</td><td>20</td><td>195</td><td>106</td><td> 6</td><td>2</td><td>0</td><td>0</td><td>4876</td><td>2588</td><td>2588</td><td>0</td></tr>\n", | ||
187 | "\t<tr><td>20</td><td> 4</td><td> 694</td><td>4261</td><td>4920</td><td>16</td><td>150</td><td> 69</td><td> 5</td><td>1</td><td>0</td><td>0</td><td>3925</td><td>2085</td><td>2085</td><td>0</td></tr>\n", | ||
188 | "\t<tr><td>20</td><td> 5</td><td> 888</td><td>5959</td><td>5086</td><td>18</td><td>200</td><td> 93</td><td> 8</td><td>1</td><td>0</td><td>0</td><td>5490</td><td>2946</td><td>2946</td><td>0</td></tr>\n", | ||
189 | "\t<tr><td>20</td><td> 6</td><td> 665</td><td>6310</td><td>4320</td><td>17</td><td>195</td><td> 90</td><td> 6</td><td>1</td><td>0</td><td>0</td><td>5870</td><td>3167</td><td>3167</td><td>0</td></tr>\n", | ||
190 | "\t<tr><td>20</td><td> 7</td><td> 604</td><td>5024</td><td>5738</td><td>14</td><td>165</td><td> 74</td><td> 4</td><td>1</td><td>0</td><td>0</td><td>4662</td><td>2464</td><td>2464</td><td>0</td></tr>\n", | ||
191 | "\t<tr><td>20</td><td> 8</td><td> 589</td><td>5733</td><td>3917</td><td>15</td><td>181</td><td> 81</td><td> 4</td><td>1</td><td>0</td><td>0</td><td>5337</td><td>2827</td><td>2827</td><td>0</td></tr>\n", | ||
192 | "\t<tr><td>20</td><td> 9</td><td> 705</td><td>4719</td><td>4259</td><td>14</td><td>156</td><td> 71</td><td> 4</td><td>1</td><td>0</td><td>2</td><td>4367</td><td>2390</td><td>2390</td><td>0</td></tr>\n", | ||
193 | "\t<tr><td>20</td><td>10</td><td> 554</td><td>4061</td><td>3990</td><td>13</td><td>141</td><td> 68</td><td> 3</td><td>1</td><td>0</td><td>0</td><td>3741</td><td>1991</td><td>1991</td><td>0</td></tr>\n", | ||
194 | "</tbody>\n", | ||
195 | "</table>\n" | ||
196 | ], | ||
197 | "text/latex": [ | ||
198 | "A tibble: 10 × 16\n", | ||
199 | "\\begin{tabular}{llllllllllllllll}\n", | ||
200 | " n & Run & preprocessingTime & Solution0FoundAt & additionalTime & TransformationExecutionTime & ForwardTime & BacktrackingTime & GlobalConstraintEvaluationTime & FitnessCalculationTime & ActivationSelectionTime & SolutionCopyTime & NumericalSolverSumTime & NumericalSolverProblemFormingTime & NumericalSolverSolvingTime & NumericalSolverInterpretingSolution\\\\\n", | ||
201 | " <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl> & <dbl>\\\\\n", | ||
202 | "\\hline\n", | ||
203 | "\t 20 & 1 & 1038 & 5248 & 3980 & 31 & 225 & 108 & 10 & 1 & 0 & 1 & 4675 & 2239 & 2239 & 0\\\\\n", | ||
204 | "\t 20 & 2 & 724 & 4132 & 3628 & 20 & 155 & 76 & 6 & 1 & 0 & 0 & 3780 & 2019 & 2019 & 0\\\\\n", | ||
205 | "\t 20 & 3 & 735 & 5329 & 4437 & 20 & 195 & 106 & 6 & 2 & 0 & 0 & 4876 & 2588 & 2588 & 0\\\\\n", | ||
206 | "\t 20 & 4 & 694 & 4261 & 4920 & 16 & 150 & 69 & 5 & 1 & 0 & 0 & 3925 & 2085 & 2085 & 0\\\\\n", | ||
207 | "\t 20 & 5 & 888 & 5959 & 5086 & 18 & 200 & 93 & 8 & 1 & 0 & 0 & 5490 & 2946 & 2946 & 0\\\\\n", | ||
208 | "\t 20 & 6 & 665 & 6310 & 4320 & 17 & 195 & 90 & 6 & 1 & 0 & 0 & 5870 & 3167 & 3167 & 0\\\\\n", | ||
209 | "\t 20 & 7 & 604 & 5024 & 5738 & 14 & 165 & 74 & 4 & 1 & 0 & 0 & 4662 & 2464 & 2464 & 0\\\\\n", | ||
210 | "\t 20 & 8 & 589 & 5733 & 3917 & 15 & 181 & 81 & 4 & 1 & 0 & 0 & 5337 & 2827 & 2827 & 0\\\\\n", | ||
211 | "\t 20 & 9 & 705 & 4719 & 4259 & 14 & 156 & 71 & 4 & 1 & 0 & 2 & 4367 & 2390 & 2390 & 0\\\\\n", | ||
212 | "\t 20 & 10 & 554 & 4061 & 3990 & 13 & 141 & 68 & 3 & 1 & 0 & 0 & 3741 & 1991 & 1991 & 0\\\\\n", | ||
213 | "\\end{tabular}\n" | ||
214 | ], | ||
215 | "text/markdown": [ | ||
216 | "\n", | ||
217 | "A tibble: 10 × 16\n", | ||
218 | "\n", | ||
219 | "| n <dbl> | Run <dbl> | preprocessingTime <dbl> | Solution0FoundAt <dbl> | additionalTime <dbl> | TransformationExecutionTime <dbl> | ForwardTime <dbl> | BacktrackingTime <dbl> | GlobalConstraintEvaluationTime <dbl> | FitnessCalculationTime <dbl> | ActivationSelectionTime <dbl> | SolutionCopyTime <dbl> | NumericalSolverSumTime <dbl> | NumericalSolverProblemFormingTime <dbl> | NumericalSolverSolvingTime <dbl> | NumericalSolverInterpretingSolution <dbl> |\n", | ||
220 | "|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|\n", | ||
221 | "| 20 | 1 | 1038 | 5248 | 3980 | 31 | 225 | 108 | 10 | 1 | 0 | 1 | 4675 | 2239 | 2239 | 0 |\n", | ||
222 | "| 20 | 2 | 724 | 4132 | 3628 | 20 | 155 | 76 | 6 | 1 | 0 | 0 | 3780 | 2019 | 2019 | 0 |\n", | ||
223 | "| 20 | 3 | 735 | 5329 | 4437 | 20 | 195 | 106 | 6 | 2 | 0 | 0 | 4876 | 2588 | 2588 | 0 |\n", | ||
224 | "| 20 | 4 | 694 | 4261 | 4920 | 16 | 150 | 69 | 5 | 1 | 0 | 0 | 3925 | 2085 | 2085 | 0 |\n", | ||
225 | "| 20 | 5 | 888 | 5959 | 5086 | 18 | 200 | 93 | 8 | 1 | 0 | 0 | 5490 | 2946 | 2946 | 0 |\n", | ||
226 | "| 20 | 6 | 665 | 6310 | 4320 | 17 | 195 | 90 | 6 | 1 | 0 | 0 | 5870 | 3167 | 3167 | 0 |\n", | ||
227 | "| 20 | 7 | 604 | 5024 | 5738 | 14 | 165 | 74 | 4 | 1 | 0 | 0 | 4662 | 2464 | 2464 | 0 |\n", | ||
228 | "| 20 | 8 | 589 | 5733 | 3917 | 15 | 181 | 81 | 4 | 1 | 0 | 0 | 5337 | 2827 | 2827 | 0 |\n", | ||
229 | "| 20 | 9 | 705 | 4719 | 4259 | 14 | 156 | 71 | 4 | 1 | 0 | 2 | 4367 | 2390 | 2390 | 0 |\n", | ||
230 | "| 20 | 10 | 554 | 4061 | 3990 | 13 | 141 | 68 | 3 | 1 | 0 | 0 | 3741 | 1991 | 1991 | 0 |\n", | ||
231 | "\n" | ||
232 | ], | ||
233 | "text/plain": [ | ||
234 | " n Run preprocessingTime Solution0FoundAt additionalTime\n", | ||
235 | "1 20 1 1038 5248 3980 \n", | ||
236 | "2 20 2 724 4132 3628 \n", | ||
237 | "3 20 3 735 5329 4437 \n", | ||
238 | "4 20 4 694 4261 4920 \n", | ||
239 | "5 20 5 888 5959 5086 \n", | ||
240 | "6 20 6 665 6310 4320 \n", | ||
241 | "7 20 7 604 5024 5738 \n", | ||
242 | "8 20 8 589 5733 3917 \n", | ||
243 | "9 20 9 705 4719 4259 \n", | ||
244 | "10 20 10 554 4061 3990 \n", | ||
245 | " TransformationExecutionTime ForwardTime BacktrackingTime\n", | ||
246 | "1 31 225 108 \n", | ||
247 | "2 20 155 76 \n", | ||
248 | "3 20 195 106 \n", | ||
249 | "4 16 150 69 \n", | ||
250 | "5 18 200 93 \n", | ||
251 | "6 17 195 90 \n", | ||
252 | "7 14 165 74 \n", | ||
253 | "8 15 181 81 \n", | ||
254 | "9 14 156 71 \n", | ||
255 | "10 13 141 68 \n", | ||
256 | " GlobalConstraintEvaluationTime FitnessCalculationTime\n", | ||
257 | "1 10 1 \n", | ||
258 | "2 6 1 \n", | ||
259 | "3 6 2 \n", | ||
260 | "4 5 1 \n", | ||
261 | "5 8 1 \n", | ||
262 | "6 6 1 \n", | ||
263 | "7 4 1 \n", | ||
264 | "8 4 1 \n", | ||
265 | "9 4 1 \n", | ||
266 | "10 3 1 \n", | ||
267 | " ActivationSelectionTime SolutionCopyTime NumericalSolverSumTime\n", | ||
268 | "1 0 1 4675 \n", | ||
269 | "2 0 0 3780 \n", | ||
270 | "3 0 0 4876 \n", | ||
271 | "4 0 0 3925 \n", | ||
272 | "5 0 0 5490 \n", | ||
273 | "6 0 0 5870 \n", | ||
274 | "7 0 0 4662 \n", | ||
275 | "8 0 0 5337 \n", | ||
276 | "9 0 2 4367 \n", | ||
277 | "10 0 0 3741 \n", | ||
278 | " NumericalSolverProblemFormingTime NumericalSolverSolvingTime\n", | ||
279 | "1 2239 2239 \n", | ||
280 | "2 2019 2019 \n", | ||
281 | "3 2588 2588 \n", | ||
282 | "4 2085 2085 \n", | ||
283 | "5 2946 2946 \n", | ||
284 | "6 3167 3167 \n", | ||
285 | "7 2464 2464 \n", | ||
286 | "8 2827 2827 \n", | ||
287 | "9 2390 2390 \n", | ||
288 | "10 1991 1991 \n", | ||
289 | " NumericalSolverInterpretingSolution\n", | ||
290 | "1 0 \n", | ||
291 | "2 0 \n", | ||
292 | "3 0 \n", | ||
293 | "4 0 \n", | ||
294 | "5 0 \n", | ||
295 | "6 0 \n", | ||
296 | "7 0 \n", | ||
297 | "8 0 \n", | ||
298 | "9 0 \n", | ||
299 | "10 0 " | ||
300 | ] | ||
301 | }, | ||
302 | "metadata": {}, | ||
303 | "output_type": "display_data" | ||
304 | }, | ||
305 | { | ||
306 | "ename": "ERROR", | ||
307 | "evalue": "Error: Problem with `summarise()` input `StateCoderTime`.\n\u001b[31m✖\u001b[39m object 'StateCoderTime' not found\n\u001b[34mℹ\u001b[39m Input `StateCoderTime` is `median(StateCoderTime)/1000`.\n\u001b[34mℹ\u001b[39m The error occurred in group 1: n = 20.\n", | ||
308 | "output_type": "error", | ||
309 | "traceback": [ | ||
310 | "Error: Problem with `summarise()` input `StateCoderTime`.\n\u001b[31m✖\u001b[39m object 'StateCoderTime' not found\n\u001b[34mℹ\u001b[39m Input `StateCoderTime` is `median(StateCoderTime)/1000`.\n\u001b[34mℹ\u001b[39m The error occurred in group 1: n = 20.\nTraceback:\n", | ||
311 | "1. FamilyTreeRQ2Raw %>% ProcessRQ2", | ||
312 | "2. ProcessRQ2(.)", | ||
313 | "3. df %>% group_by(n) %>% summarize(.groups = \"drop\", preprocessingTime = median(preprocessingTime)/1000, \n . StateCoderTime = median(StateCoderTime)/1000, ForwardTime = median(ForwardTime)/1000, \n . BacktrackingTime = median(BacktrackingTime)/1000, NumericalSolverSumTime = median(NumericalSolverSumTime)/1000, \n . additionalTime = median(additionalTime)/1000) # at line 8-16 of file <text>", | ||
314 | "4. summarize(., .groups = \"drop\", preprocessingTime = median(preprocessingTime)/1000, \n . StateCoderTime = median(StateCoderTime)/1000, ForwardTime = median(ForwardTime)/1000, \n . BacktrackingTime = median(BacktrackingTime)/1000, NumericalSolverSumTime = median(NumericalSolverSumTime)/1000, \n . additionalTime = median(additionalTime)/1000)", | ||
315 | "5. summarise.grouped_df(., .groups = \"drop\", preprocessingTime = median(preprocessingTime)/1000, \n . StateCoderTime = median(StateCoderTime)/1000, ForwardTime = median(ForwardTime)/1000, \n . BacktrackingTime = median(BacktrackingTime)/1000, NumericalSolverSumTime = median(NumericalSolverSumTime)/1000, \n . additionalTime = median(additionalTime)/1000)", | ||
316 | "6. summarise_cols(.data, ...)", | ||
317 | "7. withCallingHandlers({\n . for (i in seq_along(dots)) {\n . quo <- dots[[i]]\n . chunks[[i]] <- mask$eval_all_summarise(quo)\n . mask$across_cache_reset()\n . result_type <- types[[i]] <- withCallingHandlers(vec_ptype_common(!!!chunks[[i]]), \n . vctrs_error_incompatible_type = function(cnd) {\n . abort(class = \"dplyr:::error_summarise_incompatible_combine\", \n . parent = cnd)\n . })\n . if ((is.null(dots_names) || dots_names[i] == \"\") && is.data.frame(result_type)) {\n . map2(seq_along(result_type), names(result_type), \n . function(j, nm) {\n . mask$add(nm, pluck(chunks[[i]], j))\n . })\n . }\n . else {\n . mask$add(auto_named_dots[i], chunks[[i]])\n . }\n . }\n . recycle_info <- .Call(dplyr_summarise_recycle_chunks, chunks, \n . mask$get_rows(), types)\n . chunks <- recycle_info$chunks\n . sizes <- recycle_info$sizes\n . for (i in seq_along(dots)) {\n . result <- vec_c(!!!chunks[[i]], .ptype = types[[i]])\n . if ((is.null(dots_names) || dots_names[i] == \"\") && is.data.frame(result)) {\n . cols[names(result)] <- result\n . }\n . else {\n . cols[[auto_named_dots[i]]] <- result\n . }\n . }\n . }, error = function(e) {\n . local_call_step(dots = dots, .index = i, .fn = \"summarise\", \n . .dot_data = inherits(e, \"rlang_error_data_pronoun_not_found\"))\n . call_step <- peek_call_step()\n . error_name <- call_step$error_name\n . if (inherits(e, \"dplyr:::error_summarise_incompatible_combine\")) {\n . bullets <- c(x = glue(\"Input `{error_name}` must return compatible vectors across groups\", \n . .envir = peek_call_step()), i = cnd_bullet_combine_details(e$parent$x, \n . e$parent$x_arg), i = cnd_bullet_combine_details(e$parent$y, \n . e$parent$y_arg))\n . }\n . else if (inherits(e, \"dplyr:::summarise_unsupported_type\")) {\n . bullets <- c(x = glue(\"Input `{error_name}` must be a vector, not {friendly_type_of(result)}.\", \n . result = e$result), i = cnd_bullet_rowwise_unlist())\n . }\n . else if (inherits(e, \"dplyr:::summarise_incompatible_size\")) {\n . peek_mask()$set_current_group(e$group)\n . bullets <- c(x = glue(\"Input `{error_name}` must be size {or_1(expected_size)}, not {size}.\", \n . expected_size = e$expected_size, size = e$size), \n . i = glue(\"An earlier column had size {expected_size}.\", \n . expected_size = e$expected_size))\n . }\n . else {\n . bullets <- c(x = conditionMessage(e))\n . }\n . bullets <- c(cnd_bullet_header(), bullets, i = cnd_bullet_input_info())\n . if (!inherits(e, \"dplyr:::error_summarise_incompatible_combine\")) {\n . bullets <- c(bullets, i = cnd_bullet_cur_group_label())\n . }\n . abort(bullets, class = \"dplyr_error\")\n . })", | ||
318 | "8. mask$eval_all_summarise(quo)", | ||
319 | "9. median(StateCoderTime)", | ||
320 | "10. .handleSimpleError(function (e) \n . {\n . local_call_step(dots = dots, .index = i, .fn = \"summarise\", \n . .dot_data = inherits(e, \"rlang_error_data_pronoun_not_found\"))\n . call_step <- peek_call_step()\n . error_name <- call_step$error_name\n . if (inherits(e, \"dplyr:::error_summarise_incompatible_combine\")) {\n . bullets <- c(x = glue(\"Input `{error_name}` must return compatible vectors across groups\", \n . .envir = peek_call_step()), i = cnd_bullet_combine_details(e$parent$x, \n . e$parent$x_arg), i = cnd_bullet_combine_details(e$parent$y, \n . e$parent$y_arg))\n . }\n . else if (inherits(e, \"dplyr:::summarise_unsupported_type\")) {\n . bullets <- c(x = glue(\"Input `{error_name}` must be a vector, not {friendly_type_of(result)}.\", \n . result = e$result), i = cnd_bullet_rowwise_unlist())\n . }\n . else if (inherits(e, \"dplyr:::summarise_incompatible_size\")) {\n . peek_mask()$set_current_group(e$group)\n . bullets <- c(x = glue(\"Input `{error_name}` must be size {or_1(expected_size)}, not {size}.\", \n . expected_size = e$expected_size, size = e$size), \n . i = glue(\"An earlier column had size {expected_size}.\", \n . expected_size = e$expected_size))\n . }\n . else {\n . bullets <- c(x = conditionMessage(e))\n . }\n . bullets <- c(cnd_bullet_header(), bullets, i = cnd_bullet_input_info())\n . if (!inherits(e, \"dplyr:::error_summarise_incompatible_combine\")) {\n . bullets <- c(bullets, i = cnd_bullet_cur_group_label())\n . }\n . abort(bullets, class = \"dplyr_error\")\n . }, \"object 'StateCoderTime' not found\", base::quote(median(StateCoderTime)))", | ||
321 | "11. h(simpleError(msg, call))", | ||
322 | "12. abort(bullets, class = \"dplyr_error\")", | ||
323 | "13. signal_abort(cnd)" | ||
324 | ] | ||
325 | } | ||
326 | ], | ||
327 | "source": [ | ||
328 | "FamilyTreeRQ2Raw <- rbind(\n", | ||
329 | "# Load10Log(\"measurements/stats/FamilyTree//size010to-1r10n10rt300nsdrealstats_06-0249.csv\", 10),\n", | ||
330 | " Load10Log(\"measurements/stats/FamilyTree//size020to-1r10n10rt3600nsz3stats_06-0205.csv\", 20)\n", | ||
331 | ")\n", | ||
332 | "FamilyTreeRQ2Raw\n", | ||
333 | "FamilyTreeRQ2 <- FamilyTreeRQ2Raw %>% ProcessRQ2\n", | ||
334 | "FamilyTreeRQ2\n", | ||
335 | "# median(FamilyTreeRQ2Raw$preprocessingTime) / 1000.0\n", | ||
336 | "# FamilyTreeRQ2 %>% RQ2Plot('FamilyTree')" | ||
337 | ] | ||
338 | }, | ||
339 | { | ||
340 | "cell_type": "code", | ||
341 | "execution_count": null, | ||
342 | "metadata": {}, | ||
343 | "outputs": [], | ||
344 | "source": [] | ||
345 | } | ||
346 | ], | ||
347 | "metadata": { | ||
348 | "kernelspec": { | ||
349 | "display_name": "R", | ||
350 | "language": "R", | ||
351 | "name": "ir" | ||
352 | }, | ||
353 | "language_info": { | ||
354 | "codemirror_mode": "r", | ||
355 | "file_extension": ".r", | ||
356 | "mimetype": "text/x-r-source", | ||
357 | "name": "R", | ||
358 | "pygments_lexer": "r", | ||
359 | "version": "4.0.3" | ||
360 | } | ||
361 | }, | ||
362 | "nbformat": 4, | ||
363 | "nbformat_minor": 2 | ||
364 | } | ||
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 a5fd3189..94295dd1 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig | |||
@@ -1,5 +1,5 @@ | |||
1 | import epackage "../case.study.familyTree.model/model/familytree.ecore" | 1 | import epackage "../case.study.familyTree.model/model/familytree.ecore" |
2 | import viatra "queries/familyTreeConstraints.vql" | 2 | import viatra "queries/familyTreeConstraintsNumUB.vql" |
3 | import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" | 3 | import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" |
4 | import viatra "queries/SatelliteQueries.vql" | 4 | import viatra "queries/SatelliteQueries.vql" |
5 | 5 | ||
@@ -14,7 +14,8 @@ generate { | |||
14 | 14 | ||
15 | config = { | 15 | config = { |
16 | runtime = 10000, | 16 | runtime = 10000, |
17 | log-level = normal | 17 | log-level = normal, |
18 | "scopePropagator" = "typeHierarchy" | ||
18 | } | 19 | } |
19 | 20 | ||
20 | runs = 1 | 21 | runs = 1 |
@@ -34,6 +35,7 @@ generate { | |||
34 | config = { | 35 | config = { |
35 | runtime = 10000, | 36 | runtime = 10000, |
36 | "numeric-solver" = "z3", | 37 | "numeric-solver" = "z3", |
38 | "scopePropagator" = "typeHierarchy", | ||
37 | log-level = normal, | 39 | log-level = normal, |
38 | "fitness-punishSize" = "false", | 40 | "fitness-punishSize" = "false", |
39 | "fitness-scope" = "3" | 41 | "fitness-scope" = "3" |
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 e833397f..fdb04161 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig | |||
@@ -14,7 +14,8 @@ generate { | |||
14 | 14 | ||
15 | config = { | 15 | config = { |
16 | runtime = 10000, | 16 | runtime = 10000, |
17 | log-level = normal | 17 | log-level = normal, |
18 | "scopePropagator" = "typeHierarchy" | ||
18 | } | 19 | } |
19 | 20 | ||
20 | runs = 1 | 21 | runs = 1 |
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 36df7eef..56dc86b5 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig | |||
@@ -14,7 +14,8 @@ generate { | |||
14 | 14 | ||
15 | config = { | 15 | config = { |
16 | runtime = 10000, | 16 | runtime = 10000, |
17 | log-level = normal | 17 | log-level = normal, |
18 | "scopePropagator" = "typeHierarchy" | ||
18 | } | 19 | } |
19 | 20 | ||
20 | runs = 1 | 21 | runs = 1 |
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 3ee164cd..4a0bd920 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig | |||
@@ -12,7 +12,8 @@ generate { | |||
12 | 12 | ||
13 | config = { | 13 | config = { |
14 | runtime = 10000, | 14 | runtime = 10000, |
15 | log-level = normal | 15 | log-level = normal, |
16 | "scopePropagator" = "typeHierarchy" | ||
16 | } | 17 | } |
17 | 18 | ||
18 | runs = 1 | 19 | 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 0f2657c1..c609bf33 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig | |||
@@ -14,7 +14,8 @@ generate { | |||
14 | 14 | ||
15 | config = { | 15 | config = { |
16 | runtime = 10000, | 16 | runtime = 10000, |
17 | log-level = normal | 17 | log-level = normal, |
18 | "scopePropagator" = "typeHierarchy" | ||
18 | } | 19 | } |
19 | 20 | ||
20 | runs = 1 | 21 | runs = 1 |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/familyTreeConstraintsNumUB.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/familyTreeConstraintsNumUB.vql new file mode 100644 index 00000000..f8650073 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/familyTreeConstraintsNumUB.vql | |||
@@ -0,0 +1,47 @@ | |||
1 | package queries | ||
2 | |||
3 | import "http://www.example.org/familytree" | ||
4 | |||
5 | @Constraint(message="memberIsItsOwnParent", severity="error", key={m}) | ||
6 | pattern memberIsItsOwnParent(m: Member) = { | ||
7 | FamilyTree.members(_, m); | ||
8 | Member.parents(m, p); | ||
9 | m == p; | ||
10 | } | ||
11 | |||
12 | @Constraint(message="twoMembersHaveNoParent", severity="error", key={m1, m2}) | ||
13 | pattern twoMembersHaveNoParent(m1:Member, m2:Member) = { | ||
14 | neg find memberHasParent(m1); | ||
15 | neg find memberHasParent(m2); | ||
16 | m1 != m2; | ||
17 | } | ||
18 | |||
19 | pattern memberHasParent(m: Member) = { | ||
20 | Member.parents(m, _); | ||
21 | } | ||
22 | |||
23 | @Constraint(message="negativeAge", severity="error",key={m}) | ||
24 | pattern negativeAge(m: Member) { | ||
25 | Member.age(m,mage); | ||
26 | check(mage<0); | ||
27 | } | ||
28 | |||
29 | @Constraint(message="realisticAge", severity="error",key={m}) | ||
30 | pattern realisticAge(m: Member) { | ||
31 | Member.age(m,mage); | ||
32 | check(mage>120); | ||
33 | } | ||
34 | |||
35 | @Constraint(message="parentTooYoung", severity="error", key={c, p}) | ||
36 | pattern parentTooYoung(c: Member, p: Member) = { | ||
37 | FamilyTree.members(_, c); | ||
38 | Member.parents(c, p); | ||
39 | Member.age(c, cAge); | ||
40 | Member.age(p, pAge); | ||
41 | check (pAge <= (cAge + 12)); | ||
42 | } | ||
43 | |||
44 | |||
45 | |||
46 | |||
47 | |||
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 e1d9b9d9..e1232040 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,6 +38,7 @@ 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 | 42 | ||
42 | static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation" | 43 | static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation" |
43 | static val QUERIES = true | 44 | static val QUERIES = true |
@@ -69,6 +70,9 @@ class RunGeneratorConfig { | |||
69 | 70 | ||
70 | val ns = new Option("ns", "numericSolver", true, "what numeric solver to use") | 71 | val ns = new Option("ns", "numericSolver", true, "what numeric solver to use") |
71 | options.addOption(ns) | 72 | options.addOption(ns) |
73 | |||
74 | val sp = new Option("sp", "scopePropagator", true, "scope Propagator") | ||
75 | options.addOption(sp) | ||
72 | 76 | ||
73 | val d = new Option("d", "domain", true, "domain") | 77 | val d = new Option("d", "domain", true, "domain") |
74 | options.addOption(d) | 78 | options.addOption(d) |
@@ -100,6 +104,8 @@ class RunGeneratorConfig { | |||
100 | if(rtIn !== null) RUNTIME = Integer.parseInt(rtIn) | 104 | if(rtIn !== null) RUNTIME = Integer.parseInt(rtIn) |
101 | val nsIn = cmd.getOptionValue("numericSolver") | 105 | val nsIn = cmd.getOptionValue("numericSolver") |
102 | if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal" | 106 | if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal" |
107 | val spIn = cmd.getOptionValue("scopePropagator") | ||
108 | if(spIn !== null ) SCOPE_PROPAGATOR = spIn | ||
103 | val dIn = cmd.getOptionValue("domain") | 109 | val dIn = cmd.getOptionValue("domain") |
104 | if(dIn !== null) DOMAIN = dIn | 110 | if(dIn !== null) DOMAIN = dIn |
105 | val hhIn = cmd.getOptionValue("household") | 111 | val hhIn = cmd.getOptionValue("household") |
@@ -118,11 +124,20 @@ class RunGeneratorConfig { | |||
118 | // ///////////////////////// | 124 | // ///////////////////////// |
119 | // BEGIN RUN | 125 | // BEGIN RUN |
120 | println( | 126 | println( |
121 | "<<DOMAIN: " + DOMAIN + ", NumSolver=" + NUM_SOLVER + ", SIZE=" + SIZE_LB + "to" + SIZE_UB + ", Runs=" + RUNS + ", ModelsPerRun=" + | 127 | "<<DOMAIN: " + DOMAIN + |
122 | MODELS + ", Runtime=" + RUNTIME + ">>") | 128 | ", NumSolver=" + NUM_SOLVER + |
129 | ", scopeProp=" + SCOPE_PROPAGATOR + | ||
130 | ", SIZE=" + SIZE_LB + "to" + SIZE_UB + | ||
131 | ", Runs=" + RUNS + | ||
132 | ", ModelsPerRun=" + MODELS + | ||
133 | ", Runtime=" + RUNTIME + ">>") | ||
123 | if (isTaxation) println("<<Households: " + HOUSEHOLD + ">>") | 134 | if (isTaxation) println("<<Households: " + HOUSEHOLD + ">>") |
124 | 135 | ||
125 | var naming = DOMAIN + "/size" + toStr(SIZE_LB) + "to" + toStr(SIZE_UB) + "r" + RUNS + "n" + MODELS + "rt" + RUNTIME | 136 | var naming = DOMAIN + "/size" + toStr(SIZE_LB) + "to" + toStr(SIZE_UB) + |
137 | "r" + RUNS + | ||
138 | "n" + MODELS + | ||
139 | "rt" + RUNTIME + | ||
140 | "ns" + NUM_SOLVER | ||
126 | if (isTaxation) naming = naming + "hh" + HOUSEHOLD | 141 | if (isTaxation) naming = naming + "hh" + HOUSEHOLD |
127 | val outputPath = "measurements/" + "models/" + naming + "_" + formattedDate | 142 | val outputPath = "measurements/" + "models/" + naming + "_" + formattedDate |
128 | val debugPath = "measurements/" + "debug/" + naming + "_" + formattedDate | 143 | val debugPath = "measurements/" + "debug/" + naming + "_" + formattedDate |
@@ -188,6 +203,8 @@ class RunGeneratorConfig { | |||
188 | runtimeEntry.millisecLimit = RUNTIME | 203 | runtimeEntry.millisecLimit = RUNTIME |
189 | val numSolverEntry = configScope.entries.get(1) as CustomEntry | 204 | val numSolverEntry = configScope.entries.get(1) as CustomEntry |
190 | numSolverEntry.value = NUM_SOLVER | 205 | numSolverEntry.value = NUM_SOLVER |
206 | val scopePropEntry = configScope.entries.get(2) as CustomEntry | ||
207 | scopePropEntry.value = SCOPE_PROPAGATOR | ||
191 | 208 | ||
192 | // Output locations | 209 | // Output locations |
193 | val debug = genTask.debugFolder as FileSpecification | 210 | val debug = genTask.debugFolder as FileSpecification |