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, Journal on 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 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 and 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 to reduce the numbers of parameter samples or the number of iteration (note that the `data/` folder is shared with the host machine if you run the container with the command above). We also included a benchmark set with such reduced numbers in `run_experiments_fast.sh`.

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

Table 1 can be replicated by putting the CSV output files from running the drone experiment 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.

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 values (N).

## 5. List of possible arguments

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

| Argument     | Required? | Default          | Type                      | Description |
| ---          | ---       | ---              | ---                       | ---         |
| model        | Yes       | n/a              | string                    | Model file, e.g. `models/brp/brp.sm` |
| property     | Yes       | n/a              | string                    | File to load properties from |
| threshold    | Yes       | n/a              | float in [0,1]            | Threshold for the specification to compare against |
| comparator   | Yes       | n/a              | string                    | Is either `geq` or `leq`, or a list of strings, e.g. `'("geq","leq")'` |
| num_samples  | Yes       | n/a              | (list of) integers        | Number of parameter samples to use, e.g. `1000` or `'(1000,5000)'` |
| bisimulation | No        | `strong`         | string                    | Bisimulation mode. Can be `strong`, `weak`, or `none` |
| num_iter     | No        | 1                | integer                   | Number of iterations, given as integer |
| 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]. Can 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 .
```