diff options
Diffstat (limited to 'Assignment2/report/implementation.tex')
| -rw-r--r-- | Assignment2/report/implementation.tex | 87 |
1 files changed, 41 insertions, 46 deletions
diff --git a/Assignment2/report/implementation.tex b/Assignment2/report/implementation.tex index 1137163..f39df5e 100644 --- a/Assignment2/report/implementation.tex +++ b/Assignment2/report/implementation.tex @@ -5,43 +5,6 @@ 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{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 stormpy. - 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}. - \item - The DRN format is parsed in Clean. - The transition probabilities are stored as strings for simplicity. - This is enough for state elimination, as the internals of formulas are irrelevant. - \item - Parameters are added to transitions to generate $\mathcal M'$ as described above. - This is done by a simple graph traversal of the data structure in Clean, using uniqueness~\cite{DeVries2007} for performance reasons. - The result on the Knuth-Yao die with $p=0.4$ is shown in \cref{fig:var-unfair-die}. - \item - All non-initial non-absorbing states are eliminated, in Clean. - The algorithm is a straightforward implementation of \cite[220]{Dehnert2015}.% - \footnote{% - The given algorithm is non-deterministic and requires a sensible choice for the next state to be eliminated. - Our implementation only eliminates states with a transition to an absorbing state. - Since this is always possible and the number of transitions strictly decreases, - the algorithm always terminates, although it may not be the most efficient implementation.} - \item - We generate properties to ensure that the repaired model will still be a valid model. - For all states $s$ in $\mathcal M$, we ensure that totality holds, i.e. $\sum_{s'\in\textsl{succ}(s)}P(s,s') + v_{s,s'}=1$. - Also, for all transitions $s\to s'$ in $\mathcal M$, we ensure that $P(s,s') + v_{s,s'} \in [0,1]$. - Additionally, we generate a property to ensure that the repaired model satisfies $\phi$. - \item - We generate a minimalisation goal depending on the cost function used. - \item - The properties and the minimalisation goal are passed to Z3 which satisfies the properties and produces a model. - \item - The generated model is the returned to the user. -\end{enumerate} - \begin{figure} \begin{minted}{text} state 0 init @@ -53,13 +16,7 @@ The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists action 0 2 : 0.4 12 : 0.6 - state 7 - action 0 - 7 : 1 ... - state 12 - action 0 - 12 : 1 \end{minted} \caption{The DRN file representing the unfair Knuth-Yao die model with $p=0.4$.\label{fig:unfair-drn}} \end{figure} @@ -72,7 +29,7 @@ The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists \node[state,above right=of s0] (s1) {$s_1$}; \draw (s0) -- node[above left] {$0.4 + v_{0,1}$} ++ (s1); \node[state,above right=of s1] (s3) {$s_3$}; - \draw (s1) -- node[below right] {$0.4 + v_{0,3}$} ++ (s3); + \draw (s1) -- node[below right] {$0.4 + v_{1,3}$} ++ (s3); \draw (s3) edge[bend right=45] node[above left] {$0.4 + v_{3,1}$} (s1); \node[state,right=of s3,label={right:\enquote{1}}] (s7) {$s_7$}; \draw (s3) -- node[above] {$0.6 + v_{3,7}$} ++ (s7); @@ -97,7 +54,45 @@ The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists \node[state,right=of s6,label={right:\enquote{6}}] (s12) {$s_{12}$}; \draw (s6) -- node[above] {$0.6 + v_{6,12}$} ++ (s12); \end{tikzpicture} - \caption{An unfair instance of the Knuth-Yao die model with fresh variables~\cite{KnuthYao1976}.\label{fig:var-unfair-die}} + \caption{An unfair instance of the Knuth-Yao die model with fresh variables.\label{fig:var-unfair-die}} \end{figure} -%TODO: Describe resulting model +\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 stormpy. + 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}. + \item + The DRN format is parsed in Clean. + The transition probabilities are stored as strings for simplicity. + This is enough for state elimination, as the internals of formulas are irrelevant. + \item + Parameters are added to transitions to generate $\mathcal M'$ as described above. + This is done by a simple graph traversal of the data structure in Clean, using uniqueness~\cite{DeVries2007} for performance reasons. + The result on the Knuth-Yao die with $p=0.4$ is shown in \cref{fig:var-unfair-die}. + \item + We generate properties to ensure that the repaired model will still be a valid model. + For all states $s$ in $\mathcal M$, we ensure that totality holds, i.e.: + $$\sum_{s'\in\textsl{succ}(s)}P(s,s') + v_{s,s'}=1$$ + Also, for all transitions $s\to s'$ in $\mathcal M$, we ensure that $P(s,s') + v_{s,s'} \in [0,1]$. + Since Z3 does not prevent division by zero, we also add properties to prevent this ourselves. + Additionally, we generate a property to ensure that the repaired model satisfies $\phi$. + \item + All non-initial non-absorbing states are eliminated, in Clean. + The algorithm is a straightforward implementation of \cite[220]{Dehnert2015}% + \footnote{% + The given algorithm is non-deterministic and requires a sensible choice for the next state to be eliminated. + Our implementation only eliminates states with a transition to an absorbing state. + Since this is always possible and the number of transitions strictly decreases, + the algorithm always terminates, although it may not be the most efficient implementation.}. + \item + We generate a minimisation goal depending on the cost function used. + \item + The properties and the minimisation goal are passed to Z3 which satisfies the properties and produces a model. + \item + The generated Z3 model is returned to the user. + It contains the instantiations of the variables $v_{s,s'}$, with which $\mathcal M$ can be adapted to satisfy $\phi$. +\end{enumerate} |