diff options
Diffstat (limited to 'Assignment2/report/discussion.tex')
| -rw-r--r-- | Assignment2/report/discussion.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Assignment2/report/discussion.tex b/Assignment2/report/discussion.tex index 85e4d79..51c88c5 100644 --- a/Assignment2/report/discussion.tex +++ b/Assignment2/report/discussion.tex @@ -13,9 +13,9 @@ However, this assertion depends on the parameterized DTMC after state eliminatio 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. +However, our tool \emph{can} satisfies conjunctions of these formulas. -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). +Because we could not let Storm generate the Z3 assertions, we also had to implement a function to convert infix notation (of the probabilities in the DRN files) to prefix notation (of Z3's default SMT2 format). This is done in Clean. 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. |