Lalala

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.