From 262010e64b4f3748330a24f1e1cdb087b929fc2b Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Fri, 6 Jul 2018 08:25:00 +0200
Subject: Add small section on our method

---
 Assignment2/report/assignment2.tex |  1 +
 Assignment2/report/method.tex      | 16 ++++++++++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 Assignment2/report/method.tex

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.}.
-- 
cgit v1.2.3