diff options
| -rw-r--r-- | Assignment2/src/DTMC.icl | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index 0c71420..29b505c 100644 --- a/Assignment2/src/DTMC.icl +++ b/Assignment2/src/DTMC.icl @@ -296,7 +296,7 @@ Start w # (io,w) = stdio w # io = io <<< "Usage: " <<< prog <<< " DRN_IN DRN_OUT\n" # (_,w) = fclose io w - = w + = ("", w) # [drn_in,drn_out:_] = args # (dtmc,w) = parseDTMC drn_in w # dtmc = addVars dtmc @@ -306,11 +306,11 @@ Start 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 -| sat = abort "test" # (dtmcs,dtmc) = printDTMC dtmc # (_,w) = writeFile drn_out dtmcs w -= w +# (sat,w) = checkSat z3 w +| sat = getModel z3 w +| otherwise = ("Could not satisfy the property", w) where properties :: Properties properties = [prop] |