diff options
Diffstat (limited to 'Assignment2/report')
| -rw-r--r-- | Assignment2/report/assignment2.tex | 11 | ||||
| -rw-r--r-- | Assignment2/report/discussion.tex | 47 | ||||
| -rw-r--r-- | Assignment2/report/implementation.tex | 87 | ||||
| -rw-r--r-- | Assignment2/report/intro.tex | 6 |
4 files changed, 80 insertions, 71 deletions
diff --git a/Assignment2/report/assignment2.tex b/Assignment2/report/assignment2.tex index c9a94f7..48e9328 100644 --- a/Assignment2/report/assignment2.tex +++ b/Assignment2/report/assignment2.tex @@ -29,13 +29,22 @@ \maketitle \begin{abstract} - Model repair bladibla % TODO + We discuss an approach to the repair of parametric models using an SMT solver. + To repair a model $\mathcal M$ which does not satisfy a probabilistic CTL formula $\phi$, + we add an additional parameter to the probability of each transition in $\mathcal M$, + after which we eliminate all non-initial non-absorbing states. + The SMT solver gets constraints to ensure that the repaired model remains valid + and to satisfy $\phi$. + Cost functions for the model repair problem can be formulated as a minimisation goal for the SMT solver. + Unfortunately, some technical issues prevent us from using the tool in practice. + We provide pointers to future work to resolve these issues. \end{abstract} \input{intro} \input{method} \input{implementation} \input{discussion} +\input{future} \bibliography{library} \bibliographystyle{splncs04} diff --git a/Assignment2/report/discussion.tex b/Assignment2/report/discussion.tex index 6928701..85e4d79 100644 --- a/Assignment2/report/discussion.tex +++ b/Assignment2/report/discussion.tex @@ -1,24 +1,29 @@ -zsection{Discussion} -There were many things that we encountered during the creation of this tool. -This section serves to provide an overview of these things. +\section{Discussion} +Our tool is fully capable of dealing with parameterized DRN files. +The parameters of the model are then added as constants to the Z3 model, and model repair proceeds as usually. +However, unfortunately, it turned out that Storm is not able to output (or parse) parameterized DRN files% + \footnote{Since the DRN files contain a \texttt{@parameters} key, it was a reasonable assumption that this key would be considered in at least one direction.}. +Therefore, this was not tested extensively. +For the same reason, we have not been able to extend our approach to MDPs. -\paragraph{Storm} -Our initial plan was to use stormpy for the conversion of the transition formulas to smt2. -We would do this by creating exporting the model as DRN, and then parse this model using storm. -The DRN files that storm outputs suggest that it is capable parsing DRN files of parameterized DTMCs~\footnote{The output file contains the @parameters keyword}. -Unfortunately, we quickly realized that this is not the case. -To overcome this problem we had to implement a formula parser and create a function that could convert infix notation to the prefix notation that is used in smt2. +Another drawback of the lack of parameterization is that properties have to be specified on the generated DTMC rather than on the \PRISM\ program itself. +This means one must have a look at the generated DRN file when writing properties. +For each property that should be satisfied, we need to pass an assertion to Z3. +However, this assertion depends on the parameterized DTMC after state elimination, which lives in a Clean data structure. +Since Storm is not able to parse such a DTMC, we cannot let Storm parse properties and generate the Z3 assertions for us. +Implementing this in Clean for all kinds of properties was beyond the scope of this project. +Currently, we only support formulas of the forms $\mathbb P_{< p}s$, $\mathbb P_{= p}s$ and $\mathbb P_{> p}s$, where $s$ is a state in the DTMC. +However, are tool \emph{can} satisfies conjunctions of these formulas. -\paragraph{z3} -We encountered slight performance issues with z3. -When we include the cost-function (as described earlier in this paper) z3 is no longer able to create a model within reasonable time~\footnote{Where reasonable time is less than 5 seconds}. -We tried to work around this issue by limiting the domain the of Real numbers to the integers \texttt{[0 .. 1000]}, but this had no effect. +Because we could not let Storm generate the Z3 assertions, we also had to implement a function to convert prefix notation (of the probabilities in the DRN files) to infix notation (of Z3's default SMT2 format). +This is done in Clean. -\paragraph{Our tool} -There are many thing that were not implemented in the tool described in this paper, either because of a time constraint, or constraints in the tools that were used. -Our tool fully capable of dealing with parameterized DRN files, we can fully parse and output them. -Due to limitations with storm however, this was not extensively tested. - -Right now, the interface to z3 that was created for our tool is very na\"ively implemented. -Ideally, we would like to create a python-like api to z3. -This does not mean that our interface is less powerful, in fact, we provide a reasonable subset of smt2 that can easily be extended to provide full support. +Z3 is well able to repair the unfair Knuth-Yao die of \cref{fig:var-unfair-die}, when it is not given a minimization goal. +As rules, we set $\mathbb P_{> 0.166666666}s_i$ for $i\in\{7,8,9,10,11,12\}$. +The result approximates the Knuth-Yao die with $p=0.5$, as expected, within a negligible amount of time. +Unfortunately, adding a minimization goal increases the complexity drastically. +The NMT measure is in principle decidable, but takes too long (over 10 minutes on the unfair die example). +The SSE measure is not decidable, and Z3 is not able to solve the system. +However, the cost can be approximated by adding an upper bound on the cost as a Z3 assertion. +When a satisfying model is found, the cost of that model can be used as a new upper bound. +This can be repeated until the model cannot be satisfied. 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} diff --git a/Assignment2/report/intro.tex b/Assignment2/report/intro.tex index 9d9121c..90f8ff7 100644 --- a/Assignment2/report/intro.tex +++ b/Assignment2/report/intro.tex @@ -14,11 +14,11 @@ Properties of DTMCs and MDPs are typically described using Probabilistic Computa It adds state formulae $\mathbb P_J(\phi)$, where $J$ is an interval with rational bounds and $\phi$ a path formula. A state $s$ satisfies $\mathbb P_J(\phi)$ iff the probability of satisfying $\phi$ for a path starting in $s$ is in $J$. PCTL also adds the bounded-until path formula $\Phi_1 \Uop^{\le n} \Phi_2$, where $n\in \mathbb N$ and $\Phi_{1,2}$ are state formulae --- - the semantics are that $\Phi_2$ should be satisfied at most $n$ steps after $\Phi_1$.% + the semantics are that $\Phi_2$ should be satisfied at most $n$ steps after $\Phi_1$% \footnote{% - Furthermore, to PCTL adds state formulae $\mathbb E_R(\phi)$ to accommodate Markov Reward Models (a Markov Chain with a reward function mapping states or transitions to natural numbers~\cite[817]{BK}). + Furthermore, PCTL adds state formulae $\mathbb E_R(\phi)$ to accommodate Markov Reward Models (a Markov Chain with a reward function mapping states or transitions to natural numbers~\cite[817]{BK}). Here, $R$ is an interval with rational bounds, $\phi$ a path formula, and $\mathbb{E}$ a function that determines the cost of satisfying $\phi$ in $R$. - Since $\mathbb E$ is not relevant to the present discussion, we do not discuss it in further detail.} + Since $\mathbb E$ is not relevant to the present discussion, we do not discuss it in further detail.}. The Model Checking problem for a PCTL state formula $\Phi$ and a state $s$ in a DTMC is to verify whether $s \vDash \Phi$. Model checking proceeds as for the plain CTL case, by computing the satisfaction set of the subformulas of $\Phi$. |