diff options
| author | Erin van der Veen | 2018-07-06 13:12:10 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-07-06 13:12:10 +0200 |
| commit | 25ba6a68d7b5b9ce44b02a5236864a6df0c9b505 (patch) | |
| tree | f3153a730e3c6cf92e5d14bd17d3a4e08a2280f8 /Assignment2/src/DTMC.icl | |
| parent | Whoops v2 (diff) | |
Allow more powerfull properties by allowing operators
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 45abd4d..c89722b 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 <+ ") (" <+ parseInfix formula <+ "))" +# formula = "(" <+ op <+ " (" <+ prob <+ ") (" <+ parseInfix formula <+ "))" # w = addAssert z3 formula w = (dtmc, w) @@ -298,4 +304,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 |