Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking

4 files changed, 101 insertions, 109 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
diff --git a/Assignment2/report/intro.tex b/Assignment2/report/intro.tex
index 7e41932..9d9121c 100644
--- a/Assignment2/report/intro.tex
+++ b/Assignment2/report/intro.tex
@@ -46,7 +46,7 @@ The MSE is well-established in statistics.
 Of course, in the usual case where we only need to consider one model with different reparations,
 	the size of $M$ is fixed and we may use the sum of squared errors (SSE) as well.
 
-Another reasonable cost function is the number of modified transitions.
+Another reasonable cost function is the number of modified transitions (NMT).
 This measure counts the pairs of states $s_1,s_2$ for which the probability of $s_1\to s_2$ differs between $M$ and $M'$.
 The intuition is that the model is almost correct but may contain human errors, such as off-by-one errors or typos.
 
diff --git a/Assignment2/report/library.bib b/Assignment2/report/library.bib
index db8f78c..a310e1e 100644
--- a/Assignment2/report/library.bib
+++ b/Assignment2/report/library.bib
@@ -42,7 +42,7 @@
 
 @inproceedings{Z3,
 	title={Z3: An Efficient SMT Solver},
-	author={{de Moura}, Leonardo and Bj{\o}rner, Nikolaj},
+	author={{De Moura}, Leonardo and Bj{\o}rner, Nikolaj},
 	booktitle={Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008},
 	editor={Ramakrishnan, C. R. and Rehof, J.},
 	pages={337--340},
@@ -52,3 +52,29 @@
 	address={Berlin, Heidelberg},
 	year=2008
 }
+
+@inproceedings{DeVries2007,
+	title={Uniqueness Typing Redefined},
+	author={{De Vries}, Edsko and Plasmeijer, Rinus and Abrahamson, David R.},
+	booktitle={Proceedings of the 18th International Symposium on Implementation and Application of Functional Languages, IFL '06},
+	editor={Horv\'{a}th, Z. and Zs\'{o}k, V.},
+	pages={181--198},
+	series={Lecture Notes in Computer Science},
+	number=4449,
+	publisher={Springer},
+	address={Berlin, Heidelberg},
+	year=2007
+}
+
+@inproceedings{Dehnert2015,
+	title={\texttt{PROPhESY}: A PRObabilistic ParamEter SYnthesis Tool},
+	author={Dehnert, Christian and Junges, Sebastian and Jansen, Nils and Corzilius, Florian and Volk, Matthias and Bruintjes, Harold and Katoen, Joost-Pieter and \'{A}brah\'{a}m, Erika},
+	booktitle={Computer Aided Verification. CAV 2015},
+	editor={Kroening, D. and P\v{a}s\v{a}reanu, C.},
+	pages={181--198},
+	series={Lecture Notes in Computer Science},
+	number=9206,
+	publisher={Springer},
+	address={Cham},
+	year=2015
+}
diff --git a/Assignment2/report/method.tex b/Assignment2/report/method.tex
index 2bb9525..4f098fa 100644
--- a/Assignment2/report/method.tex
+++ b/Assignment2/report/method.tex
@@ -1,16 +1,19 @@
-\section{Methods}
-Due to a lack of experience and documentation (in/of the language and libraries used),
-	we chose to implement the state elimination procedure in Clean.
-In order to achieve this, the following steps are performed during Model Repair:
-\begin{enumerate}
-	\item The \PRISM\ program is read and parsed by stormpy
-	\item The DTMC is exported in DRN format using stormpy
-	\item The DRN format is parsed in a Clean
-	\item Parameters are added to the transitions
-	\item State elimination is performed in Clean
-	\item The DRN format is exported by Clean
-	\item The formulas are passed to z3 with additional constraints by stormpy
-\end{enumerate}
-The final step is performed only to convert infix notation.
-Ideally, this step would also be performed in Clean.
-In fact, in early versions of the project, legacy of this can still be found~\footnote{For example, a Z3 interface for Clean was made.}.
+\section{Method}
+To repair a DTMC $\mathcal M$ for a property $\phi$,
+	we generate a parametric DTMC $\mathcal M'$ which is like $\mathcal M$ but adds a unique parameter to each transition.
+For instance, if $s\to s'$ in $\mathcal M$ with probability $p$,
+	in $\mathcal M'$, this transition has probability $p+v_{s,s'}$,
+	where $v_{s,s'}$ is not a parameter in $\mathcal M$.
+We let $\mathcal V$ denote the set of all parameters $v_{s,s'}$ with $s\to s'$ in $\mathcal M$.
+
+Cost functions can be specified as minimalisation goals on $\mathcal V$.
+For the examples in the previous section, we can define:
+\begin{equation}
+	\textsl{SSE}(\mathcal V) \stackrel{\text{def}}{=} \sum_{v\in\mathcal V} v
+\end{equation}
+\begin{equation}
+	\textsl{MSE}(\mathcal V) \stackrel{\text{def}}{=} \frac{\textsl{SSE}(\mathcal V)}{|\mathcal V|}
+\end{equation}
+\begin{equation}
+	\textsl{NMT}(\mathcal V) \stackrel{\text{def}}{=} \sum_{v\in\mathcal V, v\ne 0} 1
+\end{equation}