Experiments from the paper "Monitoring Hyperproperties With Prefix Transducers" accepted at RV'23

The CSV files that were generated by our experiments are in the folder csv_from_paper. In the rest of this README, we describe how to generate the CSV files.

You can build the docker image with the artifact using docker build

# run from the top-level directory
docker build . -t rv23-experiments

If you are on a new enough Linux system, you may use the BuildKit to get faster builds:

DOCKER_BUILDKIT=1 docker build . -t rv23-experiments

To run the built image, use:

docker run -ti -v "$(pwd)/results":/opt/rv23-experiments/results rv23-experiments

This command starts a docker container with experiments ready to run and gives you a shell in this container. It also binds a folder results/ in the current directory to the same directory in the container, so you can see access the results of the experiments in the host system. Feel free to change $(pwd)/results to a directory of your choice.

These are requirements for Ubuntu, on other systems, the packages will be named similarly:

sudo apt-get install python3 g++ gcc make time cmake

For plotting the results, we use Python packages matplotlib, seaborn, and pandas. On Ubuntu, these can be installed with

sudo apt-get install python3-matplotlib python3-seaborn python3-pandas

Or you can install them via pip:

pip install matplotlib seaborn pandas

# clone the repo
git checkout https://github.com/ista-vamos/rv23-experiments
cd rv23-experiments

# initialize and build vamos-buffers
git submodule update --init -- vamos-buffers
cd vamos-buffers
cmake . -DCMAKE_BUILD_TYPE=Release
make -j4
cd -

# configure and build the project
cmake . -DCMAKE_BUILD_TYPE=Release
make -j4

In the top level directory is the script run.sh that takes as an argument either rand to run experiments on random traces, or 1t to run experiments on multiple instances of the same trace. So run the experiments as follows:

./run.sh rand
./run.sh 1t

By default, the script repeats the experiments 10 times (can be modified by changing the REP variable in the script). If you run the script multiple times, it will prompt the user if the old results should be overwritten or not.

The result of the experiments will be printed to the standard output and also saved into files results_rand.csv and results_1t.csv in the directory results.

As stated above, the number of repetitions of the experiments can be set by the REP variable in the script run.sh. There is also the variable NPROC that controls how many processes should be run in parallel. By default, it is empty which means that the script should detect the number of cores and use a suitable number of processes. You can set this variable to a number of processes that you want to use.

There is a script plot.sh that takes the generated CSV files and generates plots to plot-rand.pdf and plot-1t.pdf into the results directory. Simply run it as

./plot.sh

You can use it also to re-generate the plots from the paper on the data in csv_from_paper:

./plot.sh paper