diff options
| author | Camil Staps | 2018-07-06 15:30:13 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-07-06 15:30:13 +0200 |
| commit | d9011b5b2b5163228de4dd33edd3903ff09d8434 (patch) | |
| tree | 3d741e6e4cb71381e49a0ee80449078f91df423b /Assignment2/src/DTMC.icl | |
| parent | Add minimization goals (not supported by Z3) (diff) | |
Try to let Z3 minimize stuff
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 |