Update README for docker

README.md

@@ -63,12 +63,72 @@ Only if `--overwrite` is given, the tool will overwrite existing files.
 ## Reproducing the Evaluation Results
 
 We provide a docker image to reproduce the results.
-[TODO]
 
-### How to Setup
+### Resource Requirements and Expected Run Time
 
-### How to Run
+This evaluation was originally conducted on a laptop with a 11th Gen Intel® Core™ i7-1165G7 2.80GHz with 32GB of RAM.
+However, the computation was not parallelized and the maximal RAM usage was less than 500MB.
+The run time was less than 6 minutes.
+[TODO: these numbers are not within docker but directly. ADAPT]
 
-### How to Inspect
 
-### Resource Requirements
+### How to Setup and Run
+
+We first load the docker image `docker-tool-cav` from the `tar`-files.
+
+```
+docker load < docker-tool-cav.tar
+```
+
+We run it in interactive mode and provide an absolute path `/absolute/path/to/local/result/folder`, 
+which will be mapped to the results folder in the docker container, and will, thus, later contain the results.
+(This might require `sudo`.)
+
+```
+docker run -v /absolute/path/to/local/result/folder:/tool-cav/evaluation_results -it docker-tool-cav bash
+```
+
+Then, we first change directory to the tool.
+
+```
+cd tool-cav/
+```
+
+Last, we run the evaluation script.
+
+```
+./evaluation_functionality/script_evaluation.sh 
+```
+
+While computing, it reports in which step it is:
+
+```
+1) Computing results for subset projection.
+2) Computing results for classical projection.
+3) Computing results for state space explosion analysis.
+```
+
+If each command was successful, it prints:
+```
+Computing requested results was successful.
+```
+
+### How to Inspect the Results
+
+The results of the evaluation can be found in `evaluation_results`.
+The file `table_projection_subset.txt` and `table_projection_classical.txt` contain the results of projecting various global types 
+using the respective projection operator.
+Combined, they provide the data as presented in Table 1.
+For both approaches, we provid the expected result of the projection (in `EvalSubsetProjection.py` and `EvalClassicalProjection.py`) 
+and check against this, as indicated by the last line in each table.
+If some projection was not defined, we report -1 as their sum.
+Note that the size for global types is computed slightly differently for both approaches.
+For the classical projection, the size is computed purely syntactically, accounting for identical subterms multiple times.
+For the subset projection, however, we consider the resulting finite state machine, i.e., the number of states as well as the number of transitions, 
+and, thus, do not account for identical subterms several times.
+The file `plot_state_space_explosion.pdf` provides a plot as in Figure 4 in which sizes are determined using finite state machines.
+The example comprises a family of global types G_n.
+While Figure 4 reports results for n < 20, the default configuration does only report for n < 17.
+This is considerably faster while showing the state space explosion.
+Still, the size of the global type can be changed in `evaluation_config.py`.
+The intermediate results of the evaluation can be found in `evaluation_data` for inspection.

evaluation_functionality/evaluation_config.py

@@ -3,7 +3,7 @@ MAX_NUM_RUNS = 1000
 
 DEFAULT_MAX_SIZE_OVERHEAD = 250
 DEFAULT_MAX_SIZE_STATE_EXP = 175
-TIMEOUT_SCALE = 1000*60*10      # 10 minutes
+TIMEOUT_SCALE = 1000*60*60      # 60 minutes
 
 PREFIX_TYPES = "global_types/projectability/"
 PREFIX_PARAMETRIC_TYPES = "global_types/parametric/"