diff options
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 |