Commit cb688002 authored by Thom Badings's avatar Thom Badings
Browse files

Update README.md

parent b76d7691
......@@ -10,15 +10,9 @@ While for users, we recommend to use this artifact via the Docker container, you
- 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`
......@@ -56,13 +50,17 @@ We need two input files: (1) a parametric MDP in [the PRISM format](https://pris
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';
python3 sampler.py --model models/brp/brp_rewards4_16_5.pm --property models/brp/brp_rewards4.prctl --threshold 0.5 --comparator 'leq' --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).
The `model` and `property` arguments refer to the PRISM model and the property file, respectively. Moreover, the `threshold` is the probability for the property that we check against. The number of parameters samples is 1000 by default (not given in this minimal code), `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.
### Using variable vs. fixed thresholds
The two main theorems in [1] deal with the cases with either a variable or a fixed threshold on the specification of interest (we refer to the main reference for details). To run for a variable threshold (Theorem 1 in [1]), omit the `threshold` argument from the run command. On the other hand, to run for a fixed threshold (Theorem 2 in [1]), specify the `threshold` argument.
### 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].
......@@ -81,6 +79,8 @@ All results are stored in the `data/` folder, and the tables in [1] can be put t
- 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).
Finally, the histograms in [1] demonstrating the computation of variable thresholds can be reproduced by running the shell script `run_histogram_thm1.sh`. Running this script creates two figures with the histograms also presented in the main paper.
## 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>`.
......@@ -91,7 +91,7 @@ Below, we list all arguments that can be passed to the run command. Arguments ar
| 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)'`. |
| num_samples | No | 1000 | (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)'`. |
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment