README.md 15.1 KB
Newer Older
Thom Badings's avatar
Thom Badings committed
1
# Sampling-Based Verification of CTMCs with Uncertain Rates (SLURF)
2

3
4
5
6
This is an implementation of the approach proposed in the paper:

- [1] "Sampling-Based Verification of CTMCs with Uncertain Rates" by Thom Badings, Sebastian Junges, Nils Jansen, Marielle Stoelinga, and Matthias Volk, CAV 2022

Thom Badings's avatar
Thom Badings committed
7
Our implementation is called SLURF, named after the resemblance between a typical result figure and the trunk of an elephant, which is called a *slurf* in Dutch (Photo by [Rachel Claire](https://www.pexels.com/nl-nl/@rachel-claire/) via [Pexels](https://www.pexels.com/nl-nl/foto/voedsel-natuur-zonnig-veld-4577802/?utm_content=attributionCopyText&utm_medium=referral&utm_source=pexels)):
8
9
10

![img/slurf-intro.png](./img/slurf-intro.png)

Thom Badings's avatar
Thom Badings committed
11
## 1. Installation from source
12

Thom Badings's avatar
Thom Badings committed
13
14
While for users, we recommend to use SLURF via the Docker container, you can also build SLURF from source as follows:

15
- 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 stormpy documentation.
Thom Badings's avatar
Thom Badings committed
16

17
  Note that one must use at least version 1.7.
Matthias Volk's avatar
Matthias Volk committed
18
  Preferably, install pycarl and stormpy in a virtual environment.
Matthias Volk's avatar
Matthias Volk committed
19

20
21
22
23
24
- 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
25
- Install SLURF using
Matthias Volk's avatar
Matthias Volk committed
26
27
28

  `python setup.py install`

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

Thom Badings's avatar
Thom Badings committed
31
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
32
33

```
Thom Badings's avatar
Thom Badings committed
34
docker pull thombadings/slurf:cav22
Thom Badings's avatar
Thom Badings committed
35
36
37
38
39
```

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

```
Thom Badings's avatar
Thom Badings committed
40
docker load -i slurf_cav22_docker.tar
Thom Badings's avatar
Thom Badings committed
41
42
43
44
```

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

Matthias Volk's avatar
Matthias Volk committed
45
To use the docker container, open a terminal and navigate to the folder where you want to save the results in. 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
46
47

```
48
docker run --mount type=bind,source="$(pwd)",target=/opt/slurf/output -w /opt/slurf --rm -it --name slurf thombadings/slurf:cav22
Thom Badings's avatar
Thom Badings committed
49
50
```

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

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

55
A miminal command to run a single CTMC or fault tree is as follows:
56

57
```
Thom Badings's avatar
Thom Badings committed
58
python runfile.py --N <number of samples> --beta <confidence level> --model <path to model file>
59
```
60

Thom Badings's avatar
Thom Badings committed
61
The `model` argument should contain the path to the model file, rooted in the `model` folder. For defining parametric CTMCs, we support [the PRISM format](https://prismmodelchecker.org/manual/ThePRISMLanguage/Introduction), while for parametric fault trees, we support [the Galileo format](https://www.cse.msu.edu/~cse870/Materials/FaultTolerant/manual-galileo.htm#Editing%20in%20the%20Textual%20View). See Section 6 for how the parameters in these models are defined.
Thom Badings's avatar
Thom Badings committed
62
63

To run for 100 samples of the SIR epidemic model with a population of 20 and a confidence probability of 0.99 (i.e., the obtained results via scenario optimization are correct with at least 99% probability), the following command may be executed:
64

65
```
Thom Badings's avatar
Thom Badings committed
66
python runfile.py --N 100 --beta 0.99 --model ctmc/epidemic/sir20.sm
67
```
68

Thom Badings's avatar
Thom Badings committed
69
The `model` argument is mandatory, while the number of samples `N` is 100 by default, and the default confidence probability `beta` is 0.99. For details on all possible arguments and their default values, see below.
Thom Badings's avatar
Thom Badings committed
70

71
### Parameter distribution and property files
Thom Badings's avatar
Thom Badings committed
72

73
Besides the model specification file, SLURF requires two additional Excel or CSV (semi-colon separated) input files. In this ReadMe, we use Excel input files, but CSV input files work in an equivalent way (make sure that the CSV file is semi-colon separated). The input files must be located in the same folder as the model:
Thom Badings's avatar
Thom Badings committed
74

75
76
- A parameter probability distribution file: `parameters.xlsx` by default, but a manual file can be passed as follows: `--param_file filename`
- A property definition file: `properties.xlsx` by default, but a manual file can be passed as follows: `--prop_file filename`
Thom Badings's avatar
Thom Badings committed
77

78
The parameter distribution file defines the probability distributions of the parameters. For example, the `parameters.xlsx` for the SIR20 CTMC model looks as follows:
Thom Badings's avatar
Thom Badings committed
79

Thom Badings's avatar
Thom Badings committed
80
81
82
83
| name  | type     | mean | std   |
| ---   | ---      | ---  | ---   |
| ki    | gaussian | 0.05 | 0.002 |
| kr    | gaussian | 0.04 | 0.002 |
84

85
86
87
88
Here, `ki` and `kr` are the parameter names, `type` can either be `gaussian`, in which case we pass a `mean` and `std`, or it can be `interval` in which case we definee a `lb` and `ub` column for the lower and upper bounds (see the `parameters.xlsx` file for the Kanban CTMC for an example with interval distributions).

The properties file defines the properties that are verified by Storm. We can either pass a list of properties with only varying timebounds, or a list of independent properties. For the SIR20 CTMC, only the timebounds vary, so the `properties.xlsx` file looks as follows:

Matthias Volk's avatar
Matthias Volk committed
89
90
91
92
93
| label     | property                             | time | enabled |
|-----------|--------------------------------------|------| ---     |
| Rel T=104 | P=? [ (popI>0) U[100,104] (popI=0) ] | 104  | TRUE    |
| Rel T=108 | P=? [ (popI>0) U[100,108] (popI=0) ] | 108  | TRUE    |
| ...       | ...                                  | ...  | ...     |
94

Thom Badings's avatar
Thom Badings committed
95
By contrast, for the Kanban CTMC, we pass multiple independent properties, yielding the `properties.xlsx` file:
96

Thom Badings's avatar
Thom Badings committed
97
98
99
100
101
102
| label                 | property                      | enabled |
| ---                   | ---                           | ---     |
| Exp. tokens cell 1    | R{"tokens_cell1"}=? [ S ]     | TRUE    |
| Exp. tokens cell 2    | R{"tokens_cell2"}=? [ S ]     | TRUE    |
| Exp. tokens cell 3    | R{"tokens_cell3"}=? [ S ]     | TRUE    |
| Exp. tokens cell 4    | R{"tokens_cell4"}=? [ S ]     | TRUE    |
103
104

Note that in both cases, the `enabled` column should be set to `TRUE` in order for the property to be verified by Storm.
Thom Badings's avatar
Thom Badings committed
105
106

### Multiple expected reward measures
107

Thom Badings's avatar
Thom Badings committed
108
- For models with multiple reward structures, bisimulation should be disabled. You can do this by providing the optional argument `--no-bisim`.
109

Thom Badings's avatar
Thom Badings committed
110
### Constructing Pareto-curves
111

112
113
114
115
Besides computing rectangular confidence regions (which is the default), SLURF can also construct a Pareto-front or -curve on the computed solution vectors. To do so, set the option `--pareto_pieces n`, where `n` is an integer that describes the number of linear elements in the Pareto-front. For `n=0`, a default rectangular confidence region is computed.

### Inspecting results

Thom Badings's avatar
Thom Badings committed
116
The results for individual experiments are saved in the `output/` folder, where a folder is created for each run of the script. In this experiment folder, you will find all related figures, and several csv files (or a single Excel file, if this extension was specified) with the raw export data.
117

Thom Badings's avatar
Thom Badings committed
118
## 4. How to run experiments?
119

Thom Badings's avatar
Thom Badings committed
120
The figures and tables in the experimental section of [1] can be reproduced by running one the shell scripts in the `experiments` folder:
121

Thom Badings's avatar
Thom Badings committed
122
- `cd experiments; bash run_experiments.sh` runs the full experiments as presented in [1]. Expected run time: multiple days.
Thom Badings's avatar
Thom Badings committed
123
- `cd experiments; bash run_experiments_partial.sh` runs a partial set of experiments. Expected run time: 3 hours.
124

Thom Badings's avatar
Thom Badings committed
125
126
127
128
129
Before running the experiments, we recommend to remove any existing files/folders in the `output/` folder (except the `.keep` file). 

Note that warnings may pop up (related to the model checker Storm), but these can safely be ignored.

### Run times
Thom Badings's avatar
Thom Badings committed
130
131

- With the expected run times in mind, we recommend running the partial set. The partial set of experiments uses reduced numbers of solution vectors and less repetitions for each experiment.
Thom Badings's avatar
Thom Badings committed
132
- If you want to run the full experiment set anyways, you can reduce the number of repetitions per experiment to reduce the run time. To do this, open one of the respective shell scripts in the `experiments` folder, and reduce the value of variable `reps`, e.g. to `reps=2`.
Thom Badings's avatar
Thom Badings committed
133
- The default timeout of one hour (set in `table4_statistics.sh` / `table4_statistics_partial.sh`) may not be enough to run some benchmarks (e.g., Kanban 5; see Table 1 in [1]) in the full experiment set. If desired, you can increase the timeout for these experiments to finish.
134

Thom Badings's avatar
Thom Badings committed
135
### Inspecting experiment results
Thom Badings's avatar
Thom Badings committed
136
Both scripts run 5 experiments, which we now discuss one by one. All tables are stored in CSV format in the folder `output/` (which is the shared Docker folder, when using SLURF via the run command above). Partial tables are stored with the suffix `_partial` in the filename.
137

Thom Badings's avatar
Thom Badings committed
138
1. Creating all figures presented in [1]. The figures are saved in the `output/` folder, where a subfolder is created for each experiment, e.g. `sir60_N=400_date=2022-05-05_14-17-30`. Within these subfolders, you will find the experiment figures, saved as .pdf files.
Thom Badings's avatar
Thom Badings committed
139
140
141
142
2. Benchmark statistics. The table (corresponding with Tables 1 and 4 in [1]) is saved as `benchmark_statistics.csv`.
3. Tightness of obtained lower bounds. The tables (corresponding with Table 2 in [1]) are saved as `table2_kanban.csv` and `table2_rc.csv`.
4. Scenario optimization run times. The tables (corresponding with Table 3 in [1]) are saved as `table3_kanban.csv` and `table2_rc.csv`.
5. Comparison to naive Monte Carlo baseline. The table (corresponding with Table 5 in [1]) is saved as `naive_baseline.csv`.
Thom Badings's avatar
Thom Badings committed
143

Thom Badings's avatar
Thom Badings committed
144
## 5. List of possible arguments
145

Thom Badings's avatar
Thom Badings committed
146
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
147
148
149
150
151

| Argument    | Required? | Default          | Type                     | Description |
| ---         | ---       | ---              | ---                      | ---         |
| N           | No        | 100              | int. or list of integers | Number of solution vectors. A list can be passed as e.g., `[100,200]` |
| beta        | No        | [0.9,0.99,0.999] | float or list of floats  | Confidence level. A list can be passed as e.g., `[0.9,0.99]` |
Thom Badings's avatar
Thom Badings committed
152
| rho_list    | No        | --depends--      | float of floats          | Lists of the costs or relaxation to use, e.g. `[0.2,0.5,0.75,1.5]` |
Thom Badings's avatar
Thom Badings committed
153
154
155
156
157
158
159
160
161
162
| model       | Yes       | n/a              | string                   | Model file, e.g. `ctmc/epidemic/sir20.sm` |
| param_file  | No        | parameters.xlsx  | string                   | File to load parameter distributions from |
| prop_file   | No        | properties.xlsx  | string                   | File to load properties from |
| no-bisim    | No        | False            | bool                     | If this argument is added, bisimulation is disabled |
| seed        | No        | 1                | int                      | Random seed |
| Nvalidate   | No        | 0                | int                      | Number of solution vectors to use in computing empirical containment probabilities (as in Table 2 in [1]) |
| dft_checker | No        | concrete         | string                   | Type of DFT model checker to use (either `concrete` or `parametric`) |
| precision   | No        | 0                | float >= 0               | If specified (and if bigger than zero), approximate model checker is used |
| naive_baseline   | No   | False            | bool                     | If this argument is added, comparison with a naive Monte Carlo baseline is performed |
| export_stats| No        | None             | string                   | If this argument is added, benchmark statistics are exported to the specified file |
Thom Badings's avatar
Thom Badings committed
163
| export_filetype| No     | csv              | string                   | Extension of files to export results to (can be `csv` or `xlsx`) |
Thom Badings's avatar
Thom Badings committed
164
165
| refine      | No        | False            | bool                     | If this argument is added, the iterative refinement scheme is enabled |
| refine_precision | No   | 0                | float                    | Refinement precision to be used for refining solutions (0 means refining to exact solution vectors) |
166
| plot_timebounds | No    | None             | str                      | List of two timebounds to create 2D plot for (note: these should be present in the properties Excel or CSV file!) |
Thom Badings's avatar
Thom Badings committed
167
168
| curve_plot_mode | No    | conservative     | str                      | If `conservative`, overapproximation of curves are plotted over time; if `optimistic`, underapproximations are plotted |
| pareto_pieces | No      | 0                | int                      | If nonzero, a pareto front is plotted, with a front consisting of the specified number of linear pieces |
Thom Badings's avatar
Thom Badings committed
169
170
171

## 6. Defining parametric models

Thom Badings's avatar
Thom Badings committed
172
SLURF supports uncertain parametric CTMCs (defined in PRISM format) and fault trees (defined in Galileo format). For example, the SIR epidemic model CTMC is defined as follows:
Thom Badings's avatar
Thom Badings committed
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199

```
ctmc

const double ki;
const double kr;

const int maxPop = 20;
const int initS = maxPop-5;
const int initI = 5;
const int initR = 0;

module SIR

popS: [0..maxPop] init initS;
popI: [0..maxPop] init initI;
popR: [0..maxPop] init initR;

<>popS > 0 & popI > 0 & popI < maxPop  ->    ki*popS*popI  : (popS'= popS-1) & (popI'= popI+1);
<>popI > 0 & popR < maxPop ->    kr*popI  : (popR'= popR+1) & (popI'= popI-1);
<>popI=0 -> 1 : true;

endmodule

label "done" = popI=0;
```

200
There are two parameters, `ki` and `kr`. As described in Section 3, the parameter distributions are defined in a separate Excel or CSV file. 
Thom Badings's avatar
Thom Badings committed
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238

Similarly, the following is the DCAS dynamic fault tree, in Galileo format:

```
param P;
param B;
param CS;
param SS;
param MS;
param MA;
param MB;
param PA;
param PB;
param PS;
toplevel "System";
"System" or "FDEP" "CPU" "MOTOR" "PUMPS";
"FDEP" fdep "TRIGGER" "P" "B";
"TRIGGER" or "CS" "SS";
"CPU" wsp "P" "B";
"MOTOR" or "SWITCH" "MOTORS";
"SWITCH" pand "MS" "MA";
"MOTORS" csp "MA" "MB";
"PUMPS" and "PUMP1" "PUMP2";
"PUMP1" csp "PA" "PS";
"PUMP2" csp "PB" "PS";
"P" lambda=P dorm=0;
"B" lambda=B dorm=0.5;
"CS" lambda=CS dorm=0;
"SS" lambda=SS dorm=0;
"MS" lambda=MS dorm=0;
"MA" lambda=MA dorm=0;
"MB" lambda=MB dorm=0;
"PA" lambda=PA dorm=0;
"PB" lambda=PB dorm=0;
"PS" lambda=PS dorm=0;
```

The original non-parametric fault tree which we adapted can be found in the [FFORT benchmark suite](https://dftbenchmarks.utwente.nl/ffort.php). Other benchmarks from this suite can be converted to a parametric model in a similar way.
Thom Badings's avatar
Thom Badings committed
239

Thom Badings's avatar
Thom Badings committed
240
241
242
243
244
245
246
## 6. Rebuilding the Docker container

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

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