diff options
Diffstat (limited to 'Assignment2/src/DTMC.icl')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index c89722b..b1a12ce 100644 --- a/Assignment2/src/DTMC.icl +++ b/Assignment2/src/DTMC.icl @@ -265,6 +265,12 @@ where toString EQ = "=" toString GT = ">" +assertProperties :: !Properties !*DTMC !Z3 !*World -> (*DTMC, *World) +assertProperties [] dtmc _ w = (dtmc,w) +assertProperties [prop:props] dtmc z3 w +# (dtmc, w) = assertProperty prop dtmc z3 w += assertProperties props dtmc z3 w + assertProperty :: !Property !*DTMC !Z3 !*World -> (*DTMC, *World) assertProperty (op, prob, target) dtmc z3 w # (init, dtmc) = findInitial dtmc @@ -294,7 +300,7 @@ Start w # dtmc = stateElimination dtmc # (z3,w) = startZ3 w # (dtmc,w) = z3AddVars dtmc z3 w -# (dtmc,w) = assertProperty prop dtmc z3 w +# (dtmc,w) = assertProperties properties dtmc z3 w # (rC,dtmc) = repairConfig dtmc # w = seqSt (addAssert z3) rC.totality_restrictions w # (sat,w) = checkSat z3 w @@ -303,5 +309,8 @@ Start w # (_,w) = writeFile drn_out dtmcs w = w where + properties :: Properties + properties = [prop] + prop :: Property prop = (EQ, 0.5, 7) // Chance to reach state 7 is 0.5 |