From 7c3c6e8fbff3e51db09961ae8174841c75ba474f Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Fri, 6 Jul 2018 13:21:45 +0200
Subject: Get model if satisfiable

---
 Assignment2/src/DTMC.icl | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Assignment2')

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]
-- 
cgit v1.2.3