diff options
Diffstat (limited to 'Assignment2/src/DTMC.icl')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 12 |
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 |