summaryrefslogtreecommitdiff
path: root/Assignment2
diff options
context:
space:
mode:
Diffstat (limited to 'Assignment2')
-rw-r--r--Assignment2/src/DTMC.icl5
1 files changed, 2 insertions, 3 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index c4e49c4..c532dfb 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -236,9 +236,8 @@ assertProperty (prob, target) dtmc z3 w
# formula = 'M'.get target init.transitions
| isNothing formula = abort "Cannot reach property target from initial state"
# formula = fromJust formula
-# formula = "((" <+ formula <+ ") = " <+ prob <+ ")"
-# formula = parseInfix formula
-# w = addAssert z3 (toString formula) w
+# formula = "(= (" <+ prob <+ ") (" <+ parseInfix formula <+ "))"
+# w = addAssert z3 formula w
= (dtmc, w)
Start w