Add small section on our method

2 files changed, 17 insertions, 0 deletions

diff --git a/Assignment2/report/assignment2.tex b/Assignment2/report/assignment2.tex
index f8edcaf..8e9b5a7 100644
--- a/Assignment2/report/assignment2.tex
+++ b/Assignment2/report/assignment2.tex
@@ -32,6 +32,7 @@
 \end{abstract}
 
 \input{intro}
+\input{method}
 
 \bibliography{library}
 \bibliographystyle{splncs04}
diff --git a/Assignment2/report/method.tex b/Assignment2/report/method.tex
new file mode 100644
index 0000000..2bb9525
--- /dev/null
+++ b/Assignment2/report/method.tex
@@ -0,0 +1,16 @@
+\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.}.