blob: 2bb9525e5d1e1d9d8b4fe152dcc014c6d8608a7f (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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.}.
|
