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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
\section{Implementation}
We will now discuss the implementation of the method described above.
Due to a lack of documentation of the Storm ecosystem,
we chose to implement most functionality in Clean.
However, we use Storm for parsing \PRISM\ programs.
The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists of the following steps:
\begin{figure}
\begin{minted}{text}
state 0 init
action 0
1 : 0.4
2 : 0.6
...
state 6
action 0
2 : 0.4
12 : 0.6
...
\end{minted}
\caption{The DRN file representing the unfair Knuth-Yao die model with $p=0.4$.\label{fig:unfair-drn}}
\end{figure}
\begin{figure}
\centering
\begin{tikzpicture}[->,>=stealth,scale=0.9,every node/.style={scale=0.9,transform shape}, node distance=2cm]
\node[state,initial,initial text={}] (s0) {$s_0$};
\node[state,above right=of s0] (s1) {$s_1$};
\draw (s0) -- node[above left] {$0.4 + v_{0,1}$} ++ (s1);
\node[state,above right=of s1] (s3) {$s_3$};
\draw (s1) -- node[below right] {$0.4 + v_{1,3}$} ++ (s3);
\draw (s3) edge[bend right=45] node[above left] {$0.4 + v_{3,1}$} (s1);
\node[state,right=of s3,label={right:\enquote{1}}] (s7) {$s_7$};
\draw (s3) -- node[above] {$0.6 + v_{3,7}$} ++ (s7);
\node[state,below right=of s1,yshift=3em] (s4) {$s_4$};
\draw (s1) -- node[below,xshift=-.5em] {$0.6 + v_{1,4}$} ++ (s4);
\node[state,right=of s4,yshift=2.7em,label={right:\enquote{2}}] (s8) {$s_8$};
\draw (s4) -- node[above] {$0.4 + v_{4,8}$} ++ (s8);
\node[state,right=of s4,yshift=-1em,label={right:\enquote{3}}] (s9) {$s_9$};
\draw (s4) -- node[below] {$0.6 + v_{4,9}$} ++ (s9);
\node[state,below right=of s0] (s2) {$s_2$};
\draw (s0) -- node[below left] {$0.6 + v_{0,2}$} ++ (s2);
\node[state,above right=of s2,yshift=-3em] (s5) {$s_5$};
\draw (s2) -- node[above,xshift=-.5em] {$0.6 + v_{2,5}$} ++ (s5);
\node[state,right=of s5,yshift=1em,label={right:\enquote{4}}] (s10) {$s_{10}$};
\draw (s5) -- node[above] {$0.4 + v_{5,10}$} ++ (s10);
\node[state,right=of s5,yshift=-2.7em,label={right:\enquote{5}}] (s11) {$s_{11}$};
\draw (s5) -- node[below] {$0.6 + v_{5,11}$} ++ (s11);
\node[state,below right=of s2] (s6) {$s_6$};
\draw (s2) -- node[above right] {$0.4 + v_{2,6}$} ++ (s6);
\draw (s6) edge[bend left=45] node[below left] {$0.4 + v_{6,2}$} (s2);
\node[state,right=of s6,label={right:\enquote{6}}] (s12) {$s_{12}$};
\draw (s6) -- node[above] {$0.6 + v_{6,12}$} ++ (s12);
\end{tikzpicture}
\caption{An unfair instance of the Knuth-Yao die model with fresh variables.\label{fig:var-unfair-die}}
\end{figure}
\begin{enumerate}
\item
The \PRISM\ program is read and parsed by stormpy.
Storm generates a DTMC in its internal representation.
\item
The generated DTMC $\mathcal M$ is exported in DRN format using storm.
The DRN format is an explicit textual representation of DTMCs.
Some representative parts of the DRN of the Knuth-Yao die with $p=0.4$ are shown in \cref{fig:unfair-drn}.
\item
The DRN format is parsed in Clean.
The transition probabilities are stored as strings for simplicity.
This is enough for state elimination, as the internals of formulas are irrelevant.
\item
Parameters are added to transitions to generate $\mathcal M'$ as described above.
This is done by a simple graph traversal of the data structure in Clean, using uniqueness~\cite{DeVries2007} for performance reasons.
The result on the Knuth-Yao die with $p=0.4$ is shown in \cref{fig:var-unfair-die}.
\item
We generate properties to ensure that the repaired model will still be a valid model.
For all states $s$ in $\mathcal M$, we ensure that totality holds, i.e.:
$$\sum_{s'\in\textsl{succ}(s)}P(s,s') + v_{s,s'}=1$$
Also, for all transitions $s\to s'$ in $\mathcal M$, we ensure that $P(s,s') + v_{s,s'} \in [0,1]$.
Since Z3 does not prevent division by zero, we also add properties to prevent this ourselves.
Additionally, we generate a property to ensure that the repaired model satisfies $\phi$.
\item
All non-initial non-absorbing states are eliminated, in Clean.
The algorithm is a straightforward implementation of \cite[220]{Dehnert2015}%
\footnote{%
The given algorithm is non-deterministic and requires a sensible choice for the next state to be eliminated.
Our implementation only eliminates states with a transition to an absorbing state.
Since this is always possible and the number of transitions strictly decreases,
the algorithm always terminates, although it may not be the most efficient implementation.}.
\item
We generate a minimisation goal depending on the cost function used.
\item
The properties and the minimisation goal are passed to Z3 which satisfies the properties and produces a model.
\item
The generated Z3 model is returned to the user.
It contains the instantiations of the variables $v_{s,s'}$, with which $\mathcal M$ can be adapted to satisfy $\phi$.
\end{enumerate}
|
