diff options
| author | Erin van der Veen | 2018-07-06 22:03:12 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-07-06 22:03:12 +0200 |
| commit | ba066dd83a61458cc61250d29ded3db6bd106ddd (patch) | |
| tree | aedaac0fa717cb7f2dcf6428e3bfb13729555dbb /Assignment2/report | |
| parent | Tsk tsk (diff) | |
Trivial fixes
Diffstat (limited to 'Assignment2/report')
| -rw-r--r-- | Assignment2/report/discussion.tex | 4 | ||||
| -rw-r--r-- | Assignment2/report/implementation.tex | 2 |
2 files changed, 3 insertions, 3 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. diff --git a/Assignment2/report/implementation.tex b/Assignment2/report/implementation.tex index f39df5e..3acdea6 100644 --- a/Assignment2/report/implementation.tex +++ b/Assignment2/report/implementation.tex @@ -62,7 +62,7 @@ The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists 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 generated DTMC $\mathcal M$ is exported in DRN format using storm. 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 |