diff options
| -rw-r--r-- | Assignment2/src/DTMC.icl | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index d3010e9..45abd4d 100644 --- a/Assignment2/src/DTMC.icl +++ b/Assignment2/src/DTMC.icl @@ -221,7 +221,7 @@ where # dtmc & parameters = [var:parameters] = dtmc where - var = "v" <+ f <+ "_" <+ t + var = "v" <+ f <+ "x" <+ t repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC) repairConfig dtmc=:{nr_states,states} @@ -287,10 +287,12 @@ Start w # dtmc = addVars dtmc # dtmc = stateElimination dtmc # (z3,w) = startZ3 w +# (dtmc,w) = z3AddVars dtmc z3 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 +# (sat,w) = checkSat z3 w +| sat = abort "test" # (dtmcs,dtmc) = printDTMC dtmc # (_,w) = writeFile drn_out dtmcs w = w |