Lalala

4 files changed, 80 insertions, 71 deletions

diff --git a/Assignment2/report/assignment2.tex b/Assignment2/report/assignment2.tex
index c9a94f7..48e9328 100644
--- a/Assignment2/report/assignment2.tex
+++ b/Assignment2/report/assignment2.tex
@@ -29,13 +29,22 @@
 \maketitle
 
 \begin{abstract}
-	Model repair bladibla % TODO
+	We discuss an approach to the repair of parametric models using an SMT solver.
+	To repair a model $\mathcal M$ which does not satisfy a probabilistic CTL formula $\phi$,
+		we add an additional parameter to the probability of each transition in $\mathcal M$,
+		after which we eliminate all non-initial non-absorbing states.
+	The SMT solver gets constraints to ensure that the repaired model remains valid
+		and to satisfy $\phi$.
+	Cost functions for the model repair problem can be formulated as a minimisation goal for the SMT solver.
+	Unfortunately, some technical issues prevent us from using the tool in practice.
+	We provide pointers to future work to resolve these issues.
 \end{abstract}
 
 \input{intro}
 \input{method}
 \input{implementation}
 \input{discussion}
+\input{future}
 
 \bibliography{library}
 \bibliographystyle{splncs04}
diff --git a/Assignment2/report/discussion.tex b/Assignment2/report/discussion.tex
index 6928701..85e4d79 100644
--- a/Assignment2/report/discussion.tex
+++ b/Assignment2/report/discussion.tex
@@ -1,24 +1,29 @@
-zsection{Discussion}
-There were many things that we encountered during the creation of this tool.
-This section serves to provide an overview of these things.
+\section{Discussion}
+Our tool is fully capable of dealing with parameterized DRN files.
+The parameters of the model are then added as constants to the Z3 model, and model repair proceeds as usually.
+However, unfortunately, it turned out that Storm is not able to output (or parse) parameterized DRN files%
+	\footnote{Since the DRN files contain a \texttt{@parameters} key, it was a reasonable assumption that this key would be considered in at least one direction.}.
+Therefore, this was not tested extensively.
+For the same reason, we have not been able to extend our approach to MDPs.
 
-\paragraph{Storm}
-Our initial plan was to use stormpy for the conversion of the transition formulas to smt2.
-We would do this by creating exporting the model as DRN, and then parse this model using storm.
-The DRN files that storm outputs suggest that it is capable parsing DRN files of parameterized DTMCs~\footnote{The output file contains the @parameters keyword}.
-Unfortunately, we quickly realized that this is not the case.
-To overcome this problem we had to implement a formula parser and create a function that could convert infix notation to the prefix notation that is used in smt2.
+Another drawback of the lack of parameterization is that properties have to be specified on the generated DTMC rather than on the \PRISM\ program itself.
+This means one must have a look at the generated DRN file when writing properties.
+For each property that should be satisfied, we need to pass an assertion to Z3.
+However, this assertion depends on the parameterized DTMC after state elimination, which lives in a Clean data structure.
+Since Storm is not able to parse such a DTMC, we cannot let Storm parse properties and generate the Z3 assertions for us.
+Implementing this in Clean for all kinds of properties was beyond the scope of this project.
+Currently, we only support formulas of the forms $\mathbb P_{< p}s$, $\mathbb P_{= p}s$ and $\mathbb P_{> p}s$, where $s$ is a state in the DTMC.
+However, are tool \emph{can} satisfies conjunctions of these formulas.
 
-\paragraph{z3}
-We encountered slight performance issues with z3.
-When we include the cost-function (as described earlier in this paper) z3 is no longer able to create a model within reasonable time~\footnote{Where reasonable time is less than 5 seconds}.
-We tried to work around this issue by limiting the domain the of Real numbers to the integers \texttt{[0 .. 1000]}, but this had no effect.
+Because we could not let Storm generate the Z3 assertions, we also had to implement a function to convert prefix notation (of the probabilities in the DRN files) to infix notation (of Z3's default SMT2 format).
+This is done in Clean.
 
-\paragraph{Our tool}
-There are many thing that were not implemented in the tool described in this paper, either because of a time constraint, or constraints in the tools that were used.
-Our tool fully capable of dealing with parameterized DRN files, we can fully parse and output them.
-Due to limitations with storm however, this was not extensively tested.
-
-Right now, the interface to z3 that was created for our tool is very na\"ively implemented.
-Ideally, we would like to create a python-like api to z3.
-This does not mean that our interface is less powerful, in fact, we provide a reasonable subset of smt2 that can easily be extended to provide full support.
+Z3 is well able to repair the unfair Knuth-Yao die of \cref{fig:var-unfair-die}, when it is not given a minimization goal.
+As rules, we set $\mathbb P_{> 0.166666666}s_i$ for $i\in\{7,8,9,10,11,12\}$.
+The result approximates the Knuth-Yao die with $p=0.5$, as expected, within a negligible amount of time.
+Unfortunately, adding a minimization goal increases the complexity drastically.
+The NMT measure is in principle decidable, but takes too long (over 10 minutes on the unfair die example).
+The SSE measure is not decidable, and Z3 is not able to solve the system.
+However, the cost can be approximated by adding an upper bound on the cost as a Z3 assertion.
+When a satisfying model is found, the cost of that model can be used as a new upper bound.
+This can be repeated until the model cannot be satisfied.
diff --git a/Assignment2/report/implementation.tex b/Assignment2/report/implementation.tex
index 1137163..f39df5e 100644
--- a/Assignment2/report/implementation.tex
+++ b/Assignment2/report/implementation.tex
@@ -5,43 +5,6 @@ Due to a lack of documentation of the Storm ecosystem,
 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{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 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]$.
-		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 and produces a model.
-	\item
-		The generated model is the returned to the user.
-\end{enumerate}
-
 \begin{figure}
 	\begin{minted}{text}
 	state 0 init
@@ -53,13 +16,7 @@ The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists
 		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 with $p=0.4$.\label{fig:unfair-drn}}
 \end{figure}
@@ -72,7 +29,7 @@ The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists
 		\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_{0,3}$} ++ (s3);
+		\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);
@@ -97,7 +54,45 @@ The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists
 		\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~\cite{KnuthYao1976}.\label{fig:var-unfair-die}}
+	\caption{An unfair instance of the Knuth-Yao die model with fresh variables.\label{fig:var-unfair-die}}
 \end{figure}
 
-%TODO: Describe resulting model
+\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
+		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}
diff --git a/Assignment2/report/intro.tex b/Assignment2/report/intro.tex
index 9d9121c..90f8ff7 100644
--- a/Assignment2/report/intro.tex
+++ b/Assignment2/report/intro.tex
@@ -14,11 +14,11 @@ Properties of DTMCs and MDPs are typically described using Probabilistic Computa
 It adds state formulae $\mathbb P_J(\phi)$, where $J$ is an interval with rational bounds and $\phi$ a path formula.
 A state $s$ satisfies $\mathbb P_J(\phi)$ iff the probability of satisfying $\phi$ for a path starting in $s$ is in $J$.
 PCTL also adds the bounded-until path formula $\Phi_1 \Uop^{\le n} \Phi_2$, where $n\in \mathbb N$ and $\Phi_{1,2}$ are state formulae ---
-	the semantics are that $\Phi_2$ should be satisfied at most $n$ steps after $\Phi_1$.%
+	the semantics are that $\Phi_2$ should be satisfied at most $n$ steps after $\Phi_1$%
 	\footnote{%
-		Furthermore, to PCTL adds state formulae $\mathbb E_R(\phi)$ to accommodate Markov Reward Models (a Markov Chain with a reward function mapping states or transitions to natural numbers~\cite[817]{BK}).
+		Furthermore, PCTL adds state formulae $\mathbb E_R(\phi)$ to accommodate Markov Reward Models (a Markov Chain with a reward function mapping states or transitions to natural numbers~\cite[817]{BK}).
 		Here, $R$ is an interval with rational bounds, $\phi$ a path formula, and $\mathbb{E}$ a function that determines the cost of satisfying $\phi$ in $R$.
-		Since $\mathbb E$ is not relevant to the present discussion, we do not discuss it in further detail.}
+		Since $\mathbb E$ is not relevant to the present discussion, we do not discuss it in further detail.}.
 
 The Model Checking problem for a PCTL state formula $\Phi$ and a state $s$ in a DTMC is to verify whether $s \vDash \Phi$.
 Model checking proceeds as for the plain CTL case, by computing the satisfaction set of the subformulas of $\Phi$.