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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
\section{Implementation}
In this section we will look at the individual steps as described in the Methods section.
As an example, we will look at the unfair Knuth-Yao die model in \cref{fig:unfair-die}.
\begin{figure}
\centering
\begin{tikzpicture}[->,>=stealth,scale=0.9,every node/.style={scale=0.9,transform shape}]
\node[state,initial,initial text={}] (s0) {$s_0$};
\node[state,above right=of s0] (s1) {$s_1$};
\draw (s0) -- node[above left] {$0.4$} ++ (s1);
\node[state,above right=of s1] (s3) {$s_3$};
\draw (s1) -- node[below right] {$0.4$} ++ (s3);
\draw (s3) edge[bend right=45] node[above left] {$0.4$} (s1);
\node[state,right=of s3,label={right:\enquote{1}}] (s7) {$s_7$};
\draw (s3) -- node[above] {$0.6$} ++ (s7);
\node[state,below right=of s1,yshift=3em] (s4) {$s_4$};
\draw (s1) -- node[below,xshift=-.5em] {$0.6$} ++ (s4);
\node[state,right=of s4,yshift=2.7em,label={right:\enquote{2}}] (s8) {$s_8$};
\draw (s4) -- node[above] {$0.4$} ++ (s8);
\node[state,right=of s4,yshift=-1em,label={right:\enquote{3}}] (s9) {$s_9$};
\draw (s4) -- node[below] {$0.6$} ++ (s9);
\node[state,below right=of s0] (s2) {$s_2$};
\draw (s0) -- node[below left] {$0.6$} ++ (s2);
\node[state,above right=of s2,yshift=-3em] (s5) {$s_5$};
\draw (s2) -- node[above,xshift=-.5em] {$0.6$} ++ (s5);
\node[state,right=of s5,yshift=1em,label={right:\enquote{4}}] (s10) {$s_{10}$};
\draw (s5) -- node[above] {$0.4$} ++ (s10);
\node[state,right=of s5,yshift=-2.7em,label={right:\enquote{5}}] (s11) {$s_{11}$};
\draw (s5) -- node[below] {$0.6$} ++ (s11);
\node[state,below right=of s2] (s6) {$s_6$};
\draw (s2) -- node[above right] {$0.4$} ++ (s6);
\draw (s6) edge[bend left=45] node[below left] {$0.4$} (s2);
\node[state,right=of s6,label={right:\enquote{6}}] (s12) {$s_{12}$};
\draw (s6) -- node[above] {$0.6$} ++ (s12);
\end{tikzpicture}
\caption{An unfair instance of the Knuth-Yao die model~\cite{KnuthYao1976}.\label{fig:unfair-die}}
\end{figure}
\subsection{The \PRISM\ program is read and parsed by stormpy}
Stormpy reads the \PRISM\ program an converts it to its internal DTMC representation.
\subsection{The DTMC is exported in DRN format using stormpy}
In order to parse our model in Clean, stormpy outputs its internal representation to a DRN file.
The resulting DRN file looks like as shown in~\cref{fig:unfair-drn}.
\begin{figure}
\begin{minted}{text}
// Exported by storm
// Original model type: DTMC
@type: DTMC
@parameters
@reward_models
@nr_states
13
@model
state 0 init
action 0
1 : 0.4
2 : 0.6
...
state 6
action 0
2 : 0.4
12 : 0.6
state 7
action 0
7 : 1
...
state 12
action 0
12 : 1
\end{minted}
\caption{The DRN file representing the unfair Knuth-Yao die model.\label{fig:unfair-drn}}
\end{figure}
\subsection{The DRN format is parsed in a Clean}
A parser for DRN files was written for Clean.
This parser parses the DRN file into an internal presentation.
Note that, in state elimination, transitions are used in whole.
This meant that the internals of the formulas are not of concern.
For this reason, we chose to store the formulas as their string representation.
\subsection{Parameters are added to the transitions}
Given the Clean Datastructure, which makes use of uniqueness to improve performance, a simple algorithm was created to give every transition an additional fresh variable.
The resulting model is shown in \cref{fig:var-unfair-die}.
\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 + v0\_1$} ++ (s1);
\node[state,above right=of s1] (s3) {$s_3$};
\draw (s1) -- node[below right] {$0.4 + v0\_3$} ++ (s3);
\draw (s3) edge[bend right=45] node[above left] {$0.4 + v3\_1$} (s1);
\node[state,right=of s3,label={right:\enquote{1}}] (s7) {$s_7$};
\draw (s3) -- node[above] {$0.6 + v3\_7$} ++ (s7);
\node[state,below right=of s1,yshift=3em] (s4) {$s_4$};
\draw (s1) -- node[below,xshift=-.5em] {$0.6 + v1\_4$} ++ (s4);
\node[state,right=of s4,yshift=2.7em,label={right:\enquote{2}}] (s8) {$s_8$};
\draw (s4) -- node[above] {$0.4 + v4\_8$} ++ (s8);
\node[state,right=of s4,yshift=-1em,label={right:\enquote{3}}] (s9) {$s_9$};
\draw (s4) -- node[below] {$0.6 + v4\_9$} ++ (s9);
\node[state,below right=of s0] (s2) {$s_2$};
\draw (s0) -- node[below left] {$0.6 + v0\_2$} ++ (s2);
\node[state,above right=of s2,yshift=-3em] (s5) {$s_5$};
\draw (s2) -- node[above,xshift=-.5em] {$0.6 + v2\_5$} ++ (s5);
\node[state,right=of s5,yshift=1em,label={right:\enquote{4}}] (s10) {$s_{10}$};
\draw (s5) -- node[above] {$0.4 + v5\_10$} ++ (s10);
\node[state,right=of s5,yshift=-2.7em,label={right:\enquote{5}}] (s11) {$s_{11}$};
\draw (s5) -- node[below] {$0.6 + v5\_11$} ++ (s11);
\node[state,below right=of s2] (s6) {$s_6$};
\draw (s2) -- node[above right] {$0.4 + v2\_6$} ++ (s6);
\draw (s6) edge[bend left=45] node[below left] {$0.4 + v6\_2$} (s2);
\node[state,right=of s6,label={right:\enquote{6}}] (s12) {$s_{12}$};
\draw (s6) -- node[above] {$0.6 + v6\_12$} ++ (s12);
\end{tikzpicture}
\caption{An unfair instance of the Knuth-Yao die model with fresh variables~\cite{KnuthYao1976}.\label{fig:var-unfair-die}}
\end{figure}
\subsection{State elimination is performed in Clean}
%TODO: Camil, please write this section
\subsection{The DRN format is exported by Clean}
In order to convert our internal representation back to a DRN file, a Clean function was created: \mintinline{Clean}|printDTMC :: !*DTMC -> *(!String, !*DTMC)|.
This step is performed to pass our model back to stormpy.
We want to do this, to allow us to easily create Z3 formulas.
\subsection{The formulas are passed to z3 with additional constraints by stormpy}
The transition labels are passed to z3.
Additionally, we ensure that the sum of all outgoing transitions of a state equals 1.
Furthermore, z3 is required to minimize the sum of all fresh variables introduced in step 4.
The last assertion that is passed to z3 is, of course, the goal.
In our case, we want that eventually reaching an absorbing state is $\frac{1}{6}$.
%TODO: Describe resulting model
|
