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

Update README.md

parent a2aec831
......@@ -11,7 +11,7 @@ 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.
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.
......@@ -69,35 +69,35 @@ The results for individual experiments are saved in the `data/` folder. Dependin
## 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).
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 such reduced numbers in `run_experiments_fast.sh` (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.
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 replicated as follows:
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 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 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.
- 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 values (N).
- 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 command for running SLURF. Arguments are given as `--<argument name> <value>`.
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 | 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)'` |
| 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]. Can be `uniform`, `y-pos-bias`, or `x-neg-bias` |
| 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
......
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