Reword totality constraint, add producing model to enumeration

1 files changed, 4 insertions, 2 deletions

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}