diff options
| author | Erin van der Veen | 2018-07-06 12:43:54 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-07-06 12:43:54 +0200 |
| commit | 44d31e5248ccf58bc107da54e5af7231a3e65d34 (patch) | |
| tree | dea5554dfabeabed8bbd2dd4ed83c83090dc107d /Assignment2 | |
| parent | Let z3 know that we have parameters (diff) | |
Change var naming, change order of commands to Z3
Diffstat (limited to 'Assignment2')
| -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 |