From 67e25c8c580fe1e17a628ec0cf5a87adfdca7469 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Fri, 6 Jul 2018 22:31:29 +0200
Subject: Add text about PRISM repair

---
 Assignment2/report/future.tex         |  9 +++++++++
 Assignment2/report/implementation.tex | 19 +------------------
 2 files changed, 10 insertions(+), 18 deletions(-)

(limited to 'Assignment2')

diff --git a/Assignment2/report/future.tex b/Assignment2/report/future.tex
index 5adb602..4bdc071 100644
--- a/Assignment2/report/future.tex
+++ b/Assignment2/report/future.tex
@@ -7,3 +7,12 @@ Either of these options seem to be possible straightforwardly given more knowled
 To implement the cost functions properly, there are different options.
 The simplest would be implementing the approximation method described in the previous section.
 Another option is to find different kinds of cost functions which can be minimised efficiently.
+
+The present implementation works on DTMCs directly.
+It would be more useful to be able to perform model repair on \PRISM\ files directly.
+A straightforward way to work on \PRISM\ files directly would be to add parameters on the transitions in the \PRISM\ file rather than in the DRN file.
+Then the instantiations found by Z3 can be used directly to modify the transition probabilities in the \PRISM\ program.
+
+This does not resolve all faults, because one transition in a \PRISM\ program may describe several transitions in the DTMC.
+To fix such transitions independent from each other, one could add annotations to the DRN format to be able to reconstruct the \PRISM\ program.
+Then the DRN can be fixed with the solution found by Z3, and the \PRISM\ program can be reconstructed from there.
diff --git a/Assignment2/report/implementation.tex b/Assignment2/report/implementation.tex
index 1df4217..1db8497 100644
--- a/Assignment2/report/implementation.tex
+++ b/Assignment2/report/implementation.tex
@@ -5,30 +5,13 @@ 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{figure}
-	\begin{minted}{text}
-	state 0 init
-		action 0
-			1 : 0.4
-			2 : 0.6
-	...
-	state 6
-		action 0
-			2 : 0.4
-			12 : 0.6
-	...
-	\end{minted}
-	\caption{The DRN file representing the unfair Knuth-Yao die model with $p=0.4$.\label{fig:unfair-drn}}
-\end{figure}
-
 \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 storm.
-		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}.
+		The DRN format is an explicit textual representation of a DTMC.
 	\item
 		The DRN format is parsed in Clean.
 		The transition probabilities are stored as strings for simplicity.
-- 
cgit v1.2.3