diff options
| -rw-r--r-- | Assignment2/report/assignment2.tex | 1 | ||||
| -rw-r--r-- | Assignment2/report/method.tex | 16 |
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.}. |