diff options
| author | Erin van der Veen | 2018-07-06 12:22:21 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-07-06 12:22:21 +0200 |
| commit | 0782d98f8f55e0f33eac5dc7ae51ddc25b2bc786 (patch) | |
| tree | 7a9fe5a2d575688473405b6bed30745610457351 /Assignment2/src/DTMC.icl | |
| parent | Remove a little bit of ugliness (diff) | |
Let z3 know that we have parameters
Diffstat (limited to 'Assignment2/src/DTMC.icl')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index 0adfa1f..d3010e9 100644 --- a/Assignment2/src/DTMC.icl +++ b/Assignment2/src/DTMC.icl @@ -269,6 +269,12 @@ assertProperty (prob, target) dtmc z3 w # w = addAssert z3 formula w = (dtmc, w) +z3AddVars :: !*DTMC !Z3 !*World -> (!*DTMC, !*World) +z3AddVars dtmc z3 w +# (param,dtmc) = dtmc!parameters +# w = seqSt (addVariable z3) param w += (dtmc,w) + Start w # ([prog:args],w) = getCommandLine w | length args <> 2 @@ -284,6 +290,7 @@ Start w # (dtmc,w) = assertProperty prop dtmc z3 w # (rC,dtmc) = repairConfig dtmc # w = seqSt (addAssert z3) rC.totality_restrictions w +# (dtmc,w) = z3AddVars dtmc z3 w # (dtmcs,dtmc) = printDTMC dtmc # (_,w) = writeFile drn_out dtmcs w = w |