diff options
| -rw-r--r-- | Assignment2/report/implementation.tex | 6 |
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} |