diff options
Diffstat (limited to 'Assignment2/report/implementation.tex')
| -rw-r--r-- | Assignment2/report/implementation.tex | 19 |
1 files changed, 1 insertions, 18 deletions
diff --git a/Assignment2/report/implementation.tex b/Assignment2/report/implementation.tex index 1df4217..1db8497 100644 --- a/Assignment2/report/implementation.tex +++ b/Assignment2/report/implementation.tex @@ -5,30 +5,13 @@ Due to a lack of documentation of the Storm ecosystem, However, we use Storm for parsing \PRISM\ programs. The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists of the following steps: -\begin{figure} - \begin{minted}{text} - state 0 init - action 0 - 1 : 0.4 - 2 : 0.6 - ... - state 6 - action 0 - 2 : 0.4 - 12 : 0.6 - ... - \end{minted} - \caption{The DRN file representing the unfair Knuth-Yao die model with $p=0.4$.\label{fig:unfair-drn}} -\end{figure} - \begin{enumerate} \item The \PRISM\ program is read and parsed by stormpy. Storm generates a DTMC in its internal representation. \item The generated DTMC $\mathcal M$ is exported in DRN format using storm. - The DRN format is an explicit textual representation of DTMCs. - Some representative parts of the DRN of the Knuth-Yao die with $p=0.4$ are shown in \cref{fig:unfair-drn}. + The DRN format is an explicit textual representation of a DTMC. \item The DRN format is parsed in Clean. The transition probabilities are stored as strings for simplicity. |