{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# Data analysis for the paper \"Automated Generation of Consistent Models with Structural and Attribute Constraints\"" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "First, let's load some packages." ] }, { "cell_type": "code", "execution_count": 7, "metadata": { "scrolled": true }, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "Warning message in dir.create(\"plots\"):\n", "“'plots' already exists”\n" ] } ], "source": [ "require(tidyverse)\n", "dir.create('plots')" ] }, { "cell_type": "code", "execution_count": 28, "metadata": { "scrolled": false }, "outputs": [], "source": [ "ProcessDetailedStatistics <- function(str) {\n", " str <- sub('TransformationExecutionTime', 'TransformationExecutionTime:', str)\n", " str <- sub('Backtrackingtime', 'BacktrackingTime', str)\n", " str <- gsub('\\\\(|\\\\)', '', str)\n", " str <- lapply(strsplit(str, '\\\\||:'), function (v) {\n", " dim(v) <- c(2, 11)\n", " values <- as.double(v[2,])\n", " names(values) <- v[1,]\n", " as.data.frame(t(values))\n", " })\n", " str\n", "}\n", "Load10Log <- function(filename, size) {\n", " read_csv(filename, col_types = cols(\n", " .default = col_double(),\n", " Result = col_character(),\n", " Solution1DetailedStatistics = col_character(),\n", " Solution2DetailedStatistics = col_character(),\n", " Solution3DetailedStatistics = col_character(),\n", " Solution4DetailedStatistics = col_character(),\n", " Solution5DetailedStatistics = col_character(),\n", " Solution6DetailedStatistics = col_character(),\n", " Solution7DetailedStatistics = col_character(),\n", " Solution8DetailedStatistics = col_character(),\n", " Solution9DetailedStatistics = col_character(),\n", " Solution10DetailedStatistics = col_character()\n", " )) %>% transmute(\n", " n = size,\n", " Run = Run,\n", " preprocessingTime = get('Domain to logic transformation time') + get('Logic to solver transformation time') + ExplorationInitializationTime,\n", " Solution0FoundAt = Solution0FoundAt,\n", " additionalTime = Solution9FoundAt - Solution0FoundAt,\n", " Solution1DetailedStatistics = ProcessDetailedStatistics(Solution1DetailedStatistics)\n", " ) %>% unnest()\n", "# %>% unnest() %>% mutate(\n", "# # (Logical) constraint evluation should count as refinement.\n", "# ForwardTime = ForwardTime + GlobalConstraintEvaluationTime + FitnessCalculationTime,\n", "# preprocessingTime = preprocessingTime,\n", "# BacktrackingTime = Solution0FoundAt - (StateCoderTime + ForwardTime + NumericalSolverSumTime)\n", "# ) %>% select(n, Run, preprocessingTime, StateCoderTime, ForwardTime, BacktrackingTime, NumericalSolverSumTime, additionalTime)\n", "}\n", "Load1Log <- function(filename, size) {\n", " read_csv(filename, col_types = cols(\n", " .default = col_double(),\n", " Result = col_character(),\n", " Solution1DetailedStatistics = col_character()\n", " )) %>% filter(Result == \"ModelResultImpl\") %>% transmute(\n", " n = size,\n", " Run = Run,\n", " preprocessingTime = get('Domain to logic transformation time') + get('Logic to solver transformation time') + ExplorationInitializationTime,\n", " Solution0FoundAt = Solution0FoundAt,\n", " Solution1DetailedStatistics = ProcessDetailedStatistics(Solution1DetailedStatistics)\n", " ) %>% unnest(cols = c(Solution1DetailedStatistics)) %>% mutate(\n", " ForwardTime = ForwardTime + GlobalConstraintEvaluationTime + FitnessCalculationTime,\n", " BacktrackingTime = Solution0FoundAt - (StateCoderTime + ForwardTime + NumericalSolverSumTime)\n", " ) %>% select(n, Run, preprocessingTime, StateCoderTime, ForwardTime, BacktrackingTime, NumericalSolverSumTime)\n", "}" ] }, { "cell_type": "code", "execution_count": 13, "metadata": {}, "outputs": [], "source": [ "ProcessRQ1 <- function(df) {\n", " df %>% group_by(n) %>% summarize(\n", " .groups = 'drop',\n", " time = median(preprocessingTime + StateCoderTime + ForwardTime + BacktrackingTime + NumericalSolverSumTime) / 1000.0\n", " )\n", "}\n", "ProcessRQ2 <- function(df) {\n", " df %>% group_by(n) %>% summarize(\n", " .groups = 'drop',\n", " preprocessingTime = median(preprocessingTime) / 1000.0,\n", " StateCoderTime = median(StateCoderTime) / 1000.0,\n", " ForwardTime = median(ForwardTime) / 1000.0,\n", " BacktrackingTime = median(BacktrackingTime) / 1000.0,\n", " NumericalSolverSumTime = median(NumericalSolverSumTime) / 1000.0,\n", " additionalTime = median(additionalTime) / 1000.0\n", " )\n", "}\n", "ProcessRQ3 <- ProcessRQ1" ] }, { "cell_type": "code", "execution_count": 14, "metadata": {}, "outputs": [], "source": [ "RQ2Plot <- function(df, name) {\n", " df <- df %>% gather(name, value, -n) %>% filter(name != \"preprocessingTime\")\n", " df$name <- factor(df$name, levels=rev(c('ForwardTime', 'BacktrackingTime', 'StateCoderTime', 'NumericalSolverSumTime', 'additionalTime')))\n", " plot <- df %>% ggplot(aes(x=n, y=value, fill=name)) +\n", " geom_bar(stat='identity') +\n", " scale_fill_brewer(palette='Set2',\n", " labels=rev(c('Refinement', 'Backtracking', 'State Coding', 'SMT Solver Calls', 'Additional Model Generation')),\n", " guide=FALSE) +\n", " scale_x_continuous(breaks=c(20, 40, 60, 80, 100), name=\"Model Size (# nodes)\") +\n", " scale_y_continuous(name=\"Runtime (s)\") +\n", " theme_bw()\n", " ggsave(plot=plot, filename=paste0('plots/plot_RQ2_', name, '.pdf'), width=3.5, height=2.5)\n", " plot\n", "}" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Fam domain" ] }, { "cell_type": "code", "execution_count": 29, "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "Warning message:\n", "“`cols` is now required when using unnest().\n", "Please use `cols = c(Solution1DetailedStatistics)`”\n" ] }, { "data": { "text/html": [ "
n | Run | preprocessingTime | Solution0FoundAt | additionalTime | TransformationExecutionTime | ForwardTime | BacktrackingTime | GlobalConstraintEvaluationTime | FitnessCalculationTime | ActivationSelectionTime | SolutionCopyTime | NumericalSolverSumTime | NumericalSolverProblemFormingTime | NumericalSolverSolvingTime | NumericalSolverInterpretingSolution |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
<dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> | <dbl> |
20 | 1 | 1038 | 5248 | 3980 | 31 | 225 | 108 | 10 | 1 | 0 | 1 | 4675 | 2239 | 2239 | 0 |
20 | 2 | 724 | 4132 | 3628 | 20 | 155 | 76 | 6 | 1 | 0 | 0 | 3780 | 2019 | 2019 | 0 |
20 | 3 | 735 | 5329 | 4437 | 20 | 195 | 106 | 6 | 2 | 0 | 0 | 4876 | 2588 | 2588 | 0 |
20 | 4 | 694 | 4261 | 4920 | 16 | 150 | 69 | 5 | 1 | 0 | 0 | 3925 | 2085 | 2085 | 0 |
20 | 5 | 888 | 5959 | 5086 | 18 | 200 | 93 | 8 | 1 | 0 | 0 | 5490 | 2946 | 2946 | 0 |
20 | 6 | 665 | 6310 | 4320 | 17 | 195 | 90 | 6 | 1 | 0 | 0 | 5870 | 3167 | 3167 | 0 |
20 | 7 | 604 | 5024 | 5738 | 14 | 165 | 74 | 4 | 1 | 0 | 0 | 4662 | 2464 | 2464 | 0 |
20 | 8 | 589 | 5733 | 3917 | 15 | 181 | 81 | 4 | 1 | 0 | 0 | 5337 | 2827 | 2827 | 0 |
20 | 9 | 705 | 4719 | 4259 | 14 | 156 | 71 | 4 | 1 | 0 | 2 | 4367 | 2390 | 2390 | 0 |
20 | 10 | 554 | 4061 | 3990 | 13 | 141 | 68 | 3 | 1 | 0 | 0 | 3741 | 1991 | 1991 | 0 |