README.md

# Scenario-Based Verification of Uncertain Parametric MDPs

This is an implementation of the approach proposed in the paper:

- [1] "Scenario-Based Verification of Uncertain Parametric MDPs" by Thom Badings, Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu. To appear in STTT (2022).

## 1. Installation from source

While for users, we recommend to use this artifact via the Docker container, you can also build it from source as follows:

- Install [Storm](https://www.stormchecker.org/documentation/obtain-storm/build.html), [pycarl](https://moves-rwth.github.io/pycarl/installation.html#installation-steps) and [stormpy](https://moves-rwth.github.io/stormpy/installation.html#installation-steps) using the instructions in the documentation.

  Note that one must use the master branches of all three tools.
  Preferably, install PyCarl and Stormpy in a virtual environment.
  We have tested the artifact using Storm and Stormpy version 1.6.4.

- Install dependencies: on macOS, tkinter needs to be available.
  It can be installed via [Homebrew](https://brew.sh/):

  `brew install python-tk`

- Install the artifact using

  `python setup.py install`

## 2. Run using a Docker container

We provide a docker container. We assume you have Docker installed (if not, see the [Docker installation guide](https://docs.docker.com/get-docker/)). Then, run:

```
docker pull thombadings/upmdps:sttt
```

or in case you downloaded this container from an (unpacked) archive:

```
docker load -i upMDPs_STTT.tar
```

Our Docker container is built upon a container for the probabilistic model checker Storm (see [this documentation](https://www.stormchecker.org/documentation/obtain-storm/docker.html) for details).

To use the docker container, open a terminal and navigate to the folder where you want to save the results in on your host machine. Then, run the following command (for Windows platforms, please see the [documentation on the Storm website](https://www.stormchecker.org/documentation/obtain-storm/docker.html#run-the-docker-image-windows)):

```
docker run --mount type=bind,source="$(pwd)",target=/opt/upmdps/data -w /opt/upmdps --rm -it --name upmdps thombadings/upmdps:sttt
```

Note that this command uses a shared folder between the host machine (in the directory where you run the command) and the Docker container (in the `/opt/upmdps/data` folder).

You will see a prompt inside the docker container. The README in this folder is what you are reading. Now you are ready to run the code for a single model (Section 3) or to replicate the experiments presented in [1] (Section 4).

## 3. How to run for a single model?

We need two input files: (1) a parametric MDP in [the PRISM format](https://prismmodelchecker.org/manual/ThePRISMLanguage/Introduction), and (2) a file that describes the property to verify against. The current implementation assumes a uniform distribution over the parameters of the parametric MDP.

A minimal code to run the BRP (256,5) benchmark is then as follows:

```
python3 sampler.py --model models/brp/brp_256_5.pm --property models/brp/brp.prctl --threshold 0.5 --bisimulation weak --comparator 'leq' --num_samples 10000 --beta 0.999 --outfile 'brp_256_5_output';
```

The `model` and `property` arguments refer to the PRISM model and the property file, respectively, and the `bisimulation` can either be strong, weak, or none. Moreover, the `threshold` is the probability for the property that we check against. Finally, `num_samples` is the number of parameter samples that is used, `beta` is the confidence level (for which we compute the lower bound on the satisfaction probability), and `outfile` is the file (prefix) in which we store the results (note that this is relative to the `data/` folder already).

For details on all possible arguments and their default values, see below.

### Inspecting results

The results for individual experiments are saved in the `data/` folder. Depending on the arguments provided to the script, at most three output files are created here: one .txt file with some logs, and two .csv files with results that are also shown in the tables in the main paper, [1].

## 4. How to run experiments?

The tables in the experimental section of [1] can be reproduced by running the shell script `run_experiments.sh` in the `opt/upmdps/` folder. To speed up run times, consider reducing the numbers of parameter samples or the numbers of iterations. 

We also included a benchmark set with reduced numbers of samples and iterations in `run_experiments_fast.sh` (the expected run time on a laptop with 16 GB of RAM is approximately 3 hours). Note that the results of these faster experiments will be different than in the paper, due to these reduced sample sizes and iterations.

All results are stored in the `data/` folder, and the tables in [1] can be put together as follows:

- Table 1 can be replicated by running the drone benchmarks and putting together the CSV output files that end with `_satprob.csv`. Note that three of such CSV files are created, for the different wind conditions in the experiment. Every of each files represents a row in Table 1.

- Table 3 can be replicated by collecting all CSV output files that end with `_confprob.csv` (except for the drone results, which are presented in Table 1). For every benchmark instance, such a file is created, which represents one row in Table 3 for the respective instance.

- Table 4 can be replicated by collecting all CSV output files that end with `_satprob.csv` (except for the drone results, which are presented in Table 1). For every benchmark instance, such a file is created. Table 4 can be produced by putting together the rows from the CSV files for the correct number of parameter samples (N).

## 5. List of possible arguments

Below, we list all arguments that can be passed to the run command. Arguments are given as `--<argument name> <value>`.

| Argument     | Required? | Default          | Type                      | Description |
| ---          | ---       | ---              | ---                       | ---         |
| model        | Yes       | --               | string                    | Model file, e.g., `models/brp/brp.sm`. |
| property     | Yes       | --               | string                    | File to load the property from, e.g., `models/brp/brp.prctl`. |
| threshold    | Yes       | --               | float in [0,1]            | Threshold for the specification to compare against, e.g. `0.8`. |
| comparator   | Yes       | --               | string                    | Is either `geq` or `leq`, or a list of strings, e.g., `'("geq","leq")'`. |
| num_samples  | Yes       | --               | (list of) integers        | Number of parameter samples to use, e.g., `1000` or `'(1000,5000)'`. |
| bisimulation | No        | `strong`         | string                    | Bisimulation mode. Must be `strong`, `weak`, or `none`. |
| num_iter     | No        | 1                | integer                   | Number of iterations, given as integerm, e.g., `10`. |
| eta          | No        | None             | (list if) floats in [0,1] | Fix the satisfaction probability (and compute the probability level). Either a float, e.g., `0.8` or a list of floats, e.g., `'(0.8, 0.9)'`. |
| beta         | No        | None             | (list if) floats in [0,1] | Fix the confidence probability (and compute the satisfaction level). Either a float, e.g., `0.99` or a list of floats, e.g., `'(0.99, 0.999)'`. |
| outfile      | No        | `outfile`        | string                    | Prefix of the output file for storing results, without extension (the extension, `.csv` or `.txt`, is automatically added).  |
| weather      | No        | 0                | string                    | Dedicated argument for the drone benchmark in [1]. If given, must be `uniform`, `y-pos-bias`, or `x-neg-bias`.  |

## 6. Rebuilding the Docker container

The included Docker image is based on the Stormpy 1.6.4 image (by the storm developers, see [this documentation](https://www.stormchecker.org/documentation/obtain-storm/docker.html) for details). If, one makes changes to our source code, the docker container must be built again, using the included Dockerfile. Rebuilding the image for this implementation can be done by executing the following command in the root directory (here, 1.0 indicates the version):

``` 
docker build -f Dockerfile --tag upmdps:1.0 .
```