From ba066dd83a61458cc61250d29ded3db6bd106ddd Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Fri, 6 Jul 2018 22:03:12 +0200
Subject: Trivial fixes

---
 Assignment2/report/discussion.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Assignment2/report/discussion.tex')

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.
-- 
cgit v1.2.3

