diff options
| author | Erin van der Veen | 2018-07-06 13:15:59 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-07-06 13:15:59 +0200 |
| commit | 9159f498443877a337dcba3c135b82c1537c8031 (patch) | |
| tree | ffd3269ca13cd189eaad7cba7e6b5ea1db47a4f8 /Assignment2 | |
| parent | Allow more powerfull properties by allowing operators (diff) | |
Allow multiple properties
Diffstat (limited to 'Assignment2')
| -rw-r--r-- | Assignment2/src/DTMC.dcl | 2 | ||||
| -rw-r--r-- | Assignment2/src/DTMC.icl | 11 |
2 files changed, 12 insertions, 1 deletions
diff --git a/Assignment2/src/DTMC.dcl b/Assignment2/src/DTMC.dcl index e7d0a78..233739b 100644 --- a/Assignment2/src/DTMC.dcl +++ b/Assignment2/src/DTMC.dcl @@ -25,6 +25,8 @@ instance toString Op // (Operator, Probability, state_id) :: Property :== (Op, Real, Int) +:: Properties :== [Property] + stateElimination :: !*DTMC -> *DTMC parseDTMC :: !FilePath !*World -> *(!*DTMC, !*World) printDTMC :: !*DTMC -> *(!String, !*DTMC) 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 |