diff options
Diffstat (limited to 'Assignment2/report/discussion.tex')
| -rw-r--r-- | Assignment2/report/discussion.tex | 47 |
1 files changed, 26 insertions, 21 deletions
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. |