1 files changed, 19 insertions, 16 deletions
diff --git a/Assignment2/report/method.tex b/Assignment2/report/method.tex
index 2bb9525..4f098fa 100644
--- a/Assignment2/report/method.tex
+++ b/Assignment2/report/method.tex
@@ -1,16 +1,19 @@
-\section{Methods}
-Due to a lack of experience and documentation (in/of the language and libraries used),
-	we chose to implement the state elimination procedure in Clean.
-In order to achieve this, the following steps are performed during Model Repair:
-\begin{enumerate}
-	\item The \PRISM\ program is read and parsed by stormpy
-	\item The DTMC is exported in DRN format using stormpy
-	\item The DRN format is parsed in a Clean
-	\item Parameters are added to the transitions
-	\item State elimination is performed in Clean
-	\item The DRN format is exported by Clean
-	\item The formulas are passed to z3 with additional constraints by stormpy
-\end{enumerate}
-The final step is performed only to convert infix notation.
-Ideally, this step would also be performed in Clean.
-In fact, in early versions of the project, legacy of this can still be found~\footnote{For example, a Z3 interface for Clean was made.}.
+\section{Method}
+To repair a DTMC $\mathcal M$ for a property $\phi$,
+	we generate a parametric DTMC $\mathcal M'$ which is like $\mathcal M$ but adds a unique parameter to each transition.
+For instance, if $s\to s'$ in $\mathcal M$ with probability $p$,
+	in $\mathcal M'$, this transition has probability $p+v_{s,s'}$,
+	where $v_{s,s'}$ is not a parameter in $\mathcal M$.
+We let $\mathcal V$ denote the set of all parameters $v_{s,s'}$ with $s\to s'$ in $\mathcal M$.
+
+Cost functions can be specified as minimalisation goals on $\mathcal V$.
+For the examples in the previous section, we can define:
+\begin{equation}
+	\textsl{SSE}(\mathcal V) \stackrel{\text{def}}{=} \sum_{v\in\mathcal V} v
+\end{equation}
+\begin{equation}
+	\textsl{MSE}(\mathcal V) \stackrel{\text{def}}{=} \frac{\textsl{SSE}(\mathcal V)}{|\mathcal V|}
+\end{equation}
+\begin{equation}
+	\textsl{NMT}(\mathcal V) \stackrel{\text{def}}{=} \sum_{v\in\mathcal V, v\ne 0} 1
+\end{equation}