This prototype implements the sound and complete subset projection operator for asynchronous Multiparty Session Types.
Notably, it uses a global message causality analysis to ensure correctness of projections.
In addition, the functionality of the incomplete generalised projection operator, also called classical projection operator, is implemented.
In addition, the functionality of the incomplete generalized projection operator, also called classical projection operator, is implemented.
## Corresponding Publication
This work will be published at CAV 2023 and will be available soon.
To use the same version for reproducing results, please refer to the corresponding tag.
This work is part of the paper "Complete Multiparty Session Type Projection with Automata", published at CAV 2023.
To use the same version of the tool that was used for producing the results reported in the paper, please refer to the CAV_23 tag.
## Contact
...
...
@@ -17,7 +17,7 @@ To use the same version for reproducing results, please refer to the correspondi
This repository contains (among others) the following folders:
-`main.py` is the entry point to our tool and provides a command line interface with several options (see Section "Command Line Interace")
-`main.py` is the entry point to our tool and provides a command line interface with several options (see Section "Command Line Interface")
-`datatypes` with basic data types for global and local types as well as finite state machine representations of those;
these contain the main functionality of both approaches
-`evaluation_data` stores the raw data for the evaluation
...
...
@@ -53,70 +53,64 @@ optional arguments:
--num_runs N specifies the number of runs for all but state_explosion (for which it is 1);
range: 1-1000; default of 10 applied if out of range or not given;
does not apply to 'state_explosion' (no times reported)
--size S specifies the size up to which the parametrised experiments should run
--size S specifies the size up to which the parameterized experiments should run
--save_to FILE store output in file or files with this prefix if multiple
(relative to where the script is called from)
--overwrite overwrites file if provided
```
The option `--option` specifies which experiment shall be run:
The option `--option` specifies which experiment will be run:
1) `subset_project`: a global type (given via `--global_type`) is projected using subset projection and the local specifications are output if they exist
2) `classical_project`: a global type (given via `--global_type`) is projected using classical projection and the local specifications are output if they exist
3) `projectability_subset`: this produces runs the subset projection on a number of examples and produces a table as results
4) `projecatablity_classical`: this produces runs the classical projection on a number of examples and produces a table as results
4) `projectability_classical`: this produces runs the classical projection on a number of examples and produces a table as results
5) `state_explosion`: this option generates the subset projections to show-case the exponential blow-up in state space when generating an implementation
6) `overhead`: this is a remainder of the past (TODO: remove for artifact)
Note that, in general, the tool outputs its result on `stdout`, but it can be disabled using `--no_output`.
Only if `--overwrite` is given, the tool will overwrite existing files.
Note that, in general, the tool outputs its result on `stdout`, which can be suppressed using `--no_output`.
To allow overwriting existing results files, use the option `--overwrite`.
## Reproducing the Evaluation Results
We provide a docker image to reproduce the results.
We provide a docker image to facilitate easy reproducability of the results reported in the paper.
### Resource Requirements and Expected Run Time
Using the provided docker image, 4GB RAM should be sufficient to run the evaluation
and we expect it to take at most 15 minutes to complete.
Not using a docker container, we conducted the evaluation on a laptop with a 11th Gen Intel® Core™ i7-1165G7 2.80GHz and 32GB RAM.
However, the computation was not parallelized and the maximal RAM usage was less than 500MB.
The run time was less than 6 minutes.
### How to Setup and Run
### How to Setup and Run the Docker Image
We first load the docker image `docker-tool-cav` from the `tar`-files.
First load the docker image `docker-tool-cav` from the `tar`-files:
```
```bash
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`.)
Create a directory on your machine that should be used to hold the outputs of the experiments.
This directory will be mapped to the results directory in the docker container.
In the following, we refer to the absolute path to this directory as `/absolute/path/to/local/result/directory`.
```
docker run -v /absolute/path/to/local/result/folder:/tool-cav/evaluation_results
Run the docker image in interactive mode, providing the absolute path to the local results directory.
(This may require `sudo`.)
```bash
docker run -v /absolute/path/to/local/result/directory:/tool-cav/evaluation_results
-it docker-tool-cav bash
```
This also allows to inspect the code.
In order to modify the code or configuration, we suggest to use a similar mapping using `-v` but for the folder `tool-cav`.
This opens a shell that allows you to run the experiments and inspect the code.
In order to modify the code or configuration, we suggest to use a similar mapping of a local directory via
the `-v` flag, but for the directory `tool-cav` in the docker container.
To run the evaluation, we first change directory to the tool.
To run the experiments, first change to the directory of the tool:
```
```bash
cd tool-cav/
```
Last, we run the evaluation script.
Finally, run the evaluation script:
```
```bash
./evaluation_functionality/script_evaluation.sh
```
While computing, it reports in which step it is:
The script will run three experiments. The script will indicate which experiment is currently running:
```
1) Computing results for subset projection.
...
...
@@ -124,28 +118,43 @@ While computing, it reports in which step it is:
3) Computing results for state space explosion analysis.
```
If each command was successful, it prints:
If all experiments were run successfully, the script will print:
```
Computing requested results was successful.
```
### Resource Requirements and Expected Run Time
Using the provided docker image, 4GB RAM should be sufficient to run the evaluation.
We expect that the experiments take at most 15 minutes to complete.
For the results reported in the paper, we ran the experiments without using a docker container
on a laptop with a 11th Gen Intel® Core™ i7-1165G7 2.80GHz and 32GB RAM.
The computation was not parallelized and the maximal RAM usage was less than 500MB.
The run time was less than 6 minutes.
### How to Inspect the Results
The results of the evaluation can be found in `evaluation_results`.
The results of the experiments can be found in `evaluation_results`. This directory is mapped to the local results directory outside the docker image as indicated earlier.
(The intermediate results of the evaluation can be found in `evaluation_data` for inspection.)
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 provide the expected result of the projection (in `EvalSubsetProjection.py` and `EvalClassicalProjection.py`)
The files `table_projection_subset.txt` and `table_projection_classical.txt` contain the results of the first two experiments, which project various global types using the respective projection operator.
Combined, these files provide the data for Table 1 in the paper.
For both projection operators, we provide 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.
If the projection operator is not defined for a given global type, then this is indicated by reporting the value -1 in the "Size Proj's" column.
Note that reported sizes of the global types may differ between the tables for the two projection operators.
This is because the size is computed slightly differently for each projection operator.
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 still showing the state space explosion.
Still, the size of the global type can be changed in `evaluation_config.py`.
For the subset projection, however, we consider the size of the resulting global finite state machine (i.e., the sum of the number of states and the number of transitions). This measure does not repeatedly count identical subterms.
The file `plot_state_space_explosion.pdf` provides the output of the third experiment. It consists of a plot as shown in Figure 4 of the paper.
The sizes reported in the plot are determined using the finite state machines obtained by projecting a family of global types G_n.
While Figure 4 in the paper reports results for all n < 20, the default configuration only considers values n < 17.
This is to speed up the run time of Experiment 3, while still showing the state space explosion.
The maximal value of n for this experiment can be configured in `evaluation_config.py`.
