README.md 8.01 KB
Newer Older
Thom Badings's avatar
Thom Badings committed
1
# Scenario-Based Verification of Uncertain Parametric MDPs
Thom Badings's avatar
Thom Badings committed
2

Thom Badings's avatar
Thom Badings committed
3
4
This is an implementation of the approach proposed in the paper:

Thom Badings's avatar
Thom Badings committed
5
- [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.
Thom Badings's avatar
Thom Badings committed
6
7
8

## 1. Installation from source

Thom Badings's avatar
Thom Badings committed
9
While for users, we recommend to use this artifact via the Docker container, you can also build it from source as follows:
Thom Badings's avatar
Thom Badings committed
10
11
12
13
14

- 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.
Thom Badings's avatar
Thom Badings committed
15
  We have tested the artifact using Storm version 1.6.4.
Thom Badings's avatar
Thom Badings committed
16
17
18
19
20
21

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

  `brew install python-tk`

Thom Badings's avatar
Thom Badings committed
22
- Install the artifact using
Thom Badings's avatar
Thom Badings committed
23
24
25

  `python setup.py install`

Thom Badings's avatar
Thom Badings committed
26
## 2. Run using a Docker container
Thom Badings's avatar
Thom Badings committed
27
28
29
30

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:

```
Thom Badings's avatar
Thom Badings committed
31
docker pull thombadings/upmdps:sttt
Thom Badings's avatar
Thom Badings committed
32
33
34
35
36
```

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

```
Thom Badings's avatar
Thom Badings committed
37
docker load -i upMDPs_STTT.tar
Thom Badings's avatar
Thom Badings committed
38
39
40
41
```

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).

Thom Badings's avatar
Thom Badings committed
42
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)):
Thom Badings's avatar
Thom Badings committed
43
44

```
Thom Badings's avatar
Thom Badings committed
45
docker run --mount type=bind,source="$(pwd)",target=/opt/upmdps/data -w /opt/upmdps --rm -it --name upmdps thombadings/upmdps:sttt
Thom Badings's avatar
Thom Badings committed
46
47
```

Thom Badings's avatar
Thom Badings committed
48
49
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).

Thom Badings's avatar
Thom Badings committed
50
51
52
53
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?

Thom Badings's avatar
Thom Badings committed
54
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.
Thom Badings's avatar
Thom Badings committed
55

Thom Badings's avatar
Thom Badings committed
56
A minimal code to run the BRP (256,5) benchmark is then as follows:
Thom Badings's avatar
Thom Badings committed
57
58

```
Thom Badings's avatar
Thom Badings committed
59
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';
Thom Badings's avatar
Thom Badings committed
60
61
```

Thom Badings's avatar
Thom Badings committed
62
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).
Thom Badings's avatar
Thom Badings committed
63

Thom Badings's avatar
Thom Badings committed
64
For details on all possible arguments and their default values, see below.
Thom Badings's avatar
Thom Badings committed
65
66
67

### Inspecting results

Thom Badings's avatar
Thom Badings committed
68
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].
Thom Badings's avatar
Thom Badings committed
69
70
71

## 4. How to run experiments?

Thom Badings's avatar
Thom Badings committed
72
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`.
Thom Badings's avatar
Thom Badings committed
73
74

All results are stored in the `data/` folder, and the tables in [1] can be replicated as follows:
Thom Badings's avatar
Thom Badings committed
75

Thom Badings's avatar
Thom Badings committed
76
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.
Thom Badings's avatar
Thom Badings committed
77

Thom Badings's avatar
Thom Badings committed
78
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.
Thom Badings's avatar
Thom Badings committed
79

Thom Badings's avatar
Thom Badings committed
80
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).
Thom Badings's avatar
Thom Badings committed
81
82
83
84
85

## 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>`.

Thom Badings's avatar
Thom Badings committed
86
87
88
89
90
91
92
93
94
95
96
97
98
| 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`  |
Thom Badings's avatar
Thom Badings committed
99
100
101

## 6. Rebuilding the Docker container

Thom Badings's avatar
Thom Badings committed
102
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):
Thom Badings's avatar
Thom Badings committed
103
104

``` 
Thom Badings's avatar
Thom Badings committed
105
docker build -f Dockerfile --tag upmdps:1.0 .
Thom Badings's avatar
Thom Badings committed
106
```