diff options
Diffstat (limited to 'Assignment2')
| -rw-r--r-- | Assignment2/report/assignment2.tex | 2 | ||||
| -rw-r--r-- | Assignment2/report/implementation.tex | 138 |
2 files changed, 140 insertions, 0 deletions
diff --git a/Assignment2/report/assignment2.tex b/Assignment2/report/assignment2.tex index 8e9b5a7..4e0424b 100644 --- a/Assignment2/report/assignment2.tex +++ b/Assignment2/report/assignment2.tex @@ -4,6 +4,7 @@ \usepackage{amssymb} \usepackage{cleveref} \usepackage{csquotes} +\usepackage{minted} \usepackage{tikz} \usetikzlibrary{automata,positioning} @@ -33,6 +34,7 @@ \input{intro} \input{method} +\input{implementation} \bibliography{library} \bibliographystyle{splncs04} diff --git a/Assignment2/report/implementation.tex b/Assignment2/report/implementation.tex new file mode 100644 index 0000000..ba70220 --- /dev/null +++ b/Assignment2/report/implementation.tex @@ -0,0 +1,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 |