From c2a955b782561504d22c63cd41d62a001d17a477 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Fri, 6 Jul 2018 13:39:47 +0200
Subject: Reword totality constraint, add producing model to enumeration

---
 Assignment2/report/implementation.tex | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'Assignment2')

diff --git a/Assignment2/report/implementation.tex b/Assignment2/report/implementation.tex
index 903025a..1137163 100644
--- a/Assignment2/report/implementation.tex
+++ b/Assignment2/report/implementation.tex
@@ -31,13 +31,15 @@ The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists
 					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.
+		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.
+		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}
-- 
cgit v1.2.3