blob: 5fa6f9a3766017c5c7dd9db400f4799aba5cb062 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
You can run this tool in Docker.
All you need to do is run:
./start.sh die.prism die.properties
Which repairs the model in die.prism for the properties in die.properties.
The first time, this will build the Docker image. This can take a while, and
may seem to freeze your system, and no progress is reported (unless you remove
the -q switch in start.sh). The next time will be faster.
The result is a Z3 model which contains instantiations for variables like v0x1.
These are the values that should be added to the probabilities of transitions
(here from state 0 to state 1) to make the model satisfy. Additionally, there
is a variable cost which is the cost of the reparation. By default, this is the
Sum of Squared Errors measure. To change to the Number of Modified Transitions
measure, change line 328 of DTMC.icl to:
# (config,dtmc) = repairConfig NumberModifiedTransitions dtmc
To run Z3 with a minimisation goal, uncomment line 339 in the same line.
Additionally, to approximate the cost as described in the discussion of the
paper, add a line like this under line 338:
# w = addAssert z3 "(> 0.3 cost)" w
|
