Get model if satisfiable

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]