summaryrefslogtreecommitdiff
path: root/Assignment2/src/DTMC.icl
diff options
context:
space:
mode:
Diffstat (limited to 'Assignment2/src/DTMC.icl')
-rw-r--r--Assignment2/src/DTMC.icl12
1 files changed, 9 insertions, 3 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 4bb6c18..53d1297 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -259,13 +259,19 @@ where
| isJust state && (fromJust state).init = (fromJust state, states)
| otherwise = findInitial` (i - 1) states
+instance toString Op
+where
+ toString LT = "<"
+ toString EQ = "="
+ toString GT = ">"
+
assertProperty :: !Property !*DTMC !Z3 !*World -> (*DTMC, *World)
-assertProperty (prob, target) dtmc z3 w
+assertProperty (op, prob, target) dtmc z3 w
# (init, dtmc) = findInitial dtmc
# formula = 'M'.get target init.transitions
| isNothing formula = abort "Cannot reach property target from initial state"
# formula = fromJust formula
-# formula = "(= " <+ prob <+ " " <+ parenthesise (parseInfix formula) <+ ")"
+# formula = "( " <+ op <+ " " <+ prob <+ " " <+ parenthesise (parseInfix formula) <+ ")"
# w = addAssert z3 formula w
= (dtmc, w)
@@ -301,4 +307,4 @@ Start w
= w
where
prop :: Property
- prop = (0.5, 7) // Chance to reach state 7 is 0.5
+ prop = (EQ, 0.5, 7) // Chance to reach state 7 is 0.5