diff options
Diffstat (limited to 'Assignment2/src/DTMC.icl')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index c9696cf..bd6f9e1 100644 --- a/Assignment2/src/DTMC.icl +++ b/Assignment2/src/DTMC.icl @@ -300,8 +300,8 @@ assertProperty (op, prob, target) dtmc z3 w z3AddVars :: !*DTMC !Z3 !*World -> (!*DTMC, !*World) z3AddVars dtmc z3 w -# (param,dtmc) = dtmc!parameters -# w = seqSt (addVariable z3) param w +# (params,dtmc) = dtmc!parameters +# w = seqSt (addVariable z3 "Real") params w = (dtmc,w) parenthesise :: !a -> String | toString a @@ -330,7 +330,9 @@ Start w # (dtmc,w) = assertProperties props dtmc z3 w # w = seqSt (addAssert z3) config.totality_restrictions w # w = seqSt (addAssert z3) config.transition_restrictions w -//# w = addMinimize z3 config.minimalisation_goal w // TODO: not supported by Z3! +# w = addVariable z3 "Real" "cost" w +# w = addAssert z3 ("(= cost " +++ config.minimalisation_goal +++ ")") w +//# w = addMinimize z3 "cost" w // TODO: not supported by Z3! # (sat,w) = checkSat z3 w | sat |