Report: abstract method, cut in text & figures to save space, bring implementation details more up-to-date

1 files changed, 54 insertions, 91 deletions

diff --git a/Assignment2/report/implementation.tex b/Assignment2/report/implementation.tex
index ba70220..903025a 100644
--- a/Assignment2/report/implementation.tex
+++ b/Assignment2/report/implementation.tex
@@ -1,58 +1,47 @@
 \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}
+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:
 
-\subsection{The \PRISM\ program is read and parsed by stormpy}
-Stormpy reads the \PRISM\ program an converts it to its internal DTMC representation.
+\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 stormpy.
+		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
+		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 properties to ensure that the repaired model will still be a valid model.
+		For all states $s$ in $\mathcal M$, we ensure that $\sum_{s'\in\textsl{succ}(s)}P(s,s') + v_{s,s'}=1$ for totality.
+		Also, for all transitions $s\to s'$ in $\mathcal M$, we ensure that $P(s,s') + v_{s,s'} \in [0,1]$.
+		Additionally, we generate a property to ensure that the repaired model satisfies $\phi$.
+	\item
+		We generate a minimalisation goal depending on the cost function used.
+	\item
+		The properties and the minimalisation goal are passed to Z3 which satisfies the properties.
+\end{enumerate}
 
-\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
@@ -70,69 +59,43 @@ The resulting DRN file looks like as shown in~\cref{fig:unfair-drn}.
 		action 0
 			12 : 1
 	\end{minted}
-	\caption{The DRN file representing the unfair Knuth-Yao die model.\label{fig:unfair-drn}}
+	\caption{The DRN file representing the unfair Knuth-Yao die model with $p=0.4$.\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);
+		\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 + v0\_3$} ++ (s3);
-		\draw (s3) edge[bend right=45] node[above left] {$0.4 + v3\_1$} (s1);
+		\draw (s1) -- node[below right] {$0.4 + v_{0,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 + v3\_7$} ++ (s7);
+		\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 + v1\_4$} ++ (s4);
+		\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 + v4\_8$} ++ (s8);
+		\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 + v4\_9$} ++ (s9);
+		\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 + v0\_2$} ++ (s2);
+		\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 + v2\_5$} ++ (s5);
+		\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 + v5\_10$} ++ (s10);
+		\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 + v5\_11$} ++ (s11);
+		\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 + v2\_6$} ++ (s6);
-		\draw (s6) edge[bend left=45] node[below left] {$0.4 + v6\_2$} (s2);
+		\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 + v6\_12$} ++ (s12);
+		\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~\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