3 files changed, 28 insertions, 31 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 29b505c..83c5ac1 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -21,10 +21,13 @@ import System.CommandLine
 import System.File
 import System.FilePath
 import Text
+import Text.GenParse
 
 import Expression
 import Z3
 
+derive gParse Op, (,,)
+
 paths :: !*DTMC -> *([[Int]], !*DTMC)
 paths dtmc=:{nr_states,states}
 # (inits,states) = getInitStates (nr_states-1) states
@@ -275,7 +278,7 @@ assertProperty :: !Property !*DTMC !Z3 !*World -> (*DTMC, *World)
 assertProperty (op, prob, target) dtmc z3 w
 # (init, dtmc) = findInitial dtmc
 # formula = 'M'.get target init.transitions
-| isNothing formula = abort "Cannot reach property target from initial state"
+| isNothing formula = abort "Cannot reach property target from initial state\n"
 # formula = fromJust formula
 # formula = "( " <+ op <+ " " <+ prob <+ " " <+ parenthesise (parseInfix formula) <+ ")"
 # w = addAssert z3 formula w
@@ -290,30 +293,29 @@ z3AddVars dtmc z3 w
 parenthesise :: !a -> String | toString a
 parenthesise x = let s = toString x in if (s.[0] == '(') s ("(" +++ s +++ ")")
 
+parseProperty :: !String -> Property
+parseProperty s = case parseString s of
+	Nothing -> abort $ "Could not parse '" +++ s +++ "' as a property\n"
+	Just p  -> p
+
 Start w
 # ([prog:args],w) = getCommandLine w
-| length args <> 2
-	# (io,w) = stdio w
-	# io = io <<< "Usage: " <<< prog <<< " DRN_IN DRN_OUT\n"
-	# (_,w) = fclose io w
-	= ("", w)
-# [drn_in,drn_out:_] = args
+| length args <> 2 = "Usage: " +++ prog +++ " DRN PROPERTIES"
+# [drn_in,props:_] = args
+
 # (dtmc,w) = parseDTMC drn_in w
+# (props,w) = readFileLines props w
+# props = map (parseProperty o trim) $ fromOk props
+
 # dtmc = addVars dtmc
 # dtmc = stateElimination dtmc
 # (z3,w) = startZ3 w
 # (dtmc,w) = z3AddVars dtmc z3 w
-# (dtmc,w) = assertProperties properties dtmc z3 w
+# (dtmc,w) = assertProperties props dtmc z3 w
 # (rC,dtmc) = repairConfig dtmc
 # w = seqSt (addAssert z3) rC.totality_restrictions w
-# (dtmcs,dtmc) = printDTMC dtmc
-# (_,w) = writeFile drn_out dtmcs w
 # (sat,w) = checkSat z3 w
-| sat = getModel z3 w
-| otherwise = ("Could not satisfy the property", w)
-where
-	properties :: Properties
-	properties = [prop]
-
-	prop :: Property
-	prop = (EQ, 0.5, 7) // Chance to reach state 7 is 0.5
+| sat
+	# (model,w) = getModel z3 w
+	= model
+| otherwise = "Could not satisfy the property"
diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl
index cb054e1..b4b7326 100644
--- a/Assignment2/src/Z3.icl
+++ b/Assignment2/src/Z3.icl
@@ -1,11 +1,9 @@
 implementation module Z3
 
-import System.Process
-import Text
-
 import StdString
 
-import StdDebug
+import System.Process
+import Text
 
 :: Z3 =
 	{ handle :: ProcessHandle
@@ -28,29 +26,26 @@ startZ3 w
 
 addAssert :: !Z3 !String !*World -> *World
 addAssert z3 s w
-# (_, w) = writePipe (trace_s ("(assert " <+ s <+ ")\n")) z3.Z3.stdIn w
+# (_, w) = writePipe ("(assert " <+ s <+ ")\n") z3.Z3.stdIn w
 = w
 
 addVariable :: !Z3 !String !*World -> *World
 addVariable z3 s w
-# (_, w) = writePipe (trace_s ("(declare-const " <+ s <+ " Real)\n")) z3.Z3.stdIn w
+# (_, w) = writePipe ("(declare-const " <+ s <+ " Real)\n") z3.Z3.stdIn w
 = w
 
 checkSat :: !Z3 !*World -> (!Bool, !*World)
 checkSat z3 w
-# (_, w) = writePipe (trace_s "(check-sat)\n") z3.Z3.stdIn w
+# (_, w) = writePipe "(check-sat)\n" z3.Z3.stdIn w
 # (out, w) = readPipeBlocking z3.Z3.stdOut w
 # out = fromOk out
 = (startsWith "sat" out, w)
 
 getModel :: !Z3 !*World -> (!String, !*World)
 getModel z3 w
-# (_, w) = writePipe (trace_s "(get-model)\n") z3.Z3.stdIn w
-# (_, w) = writePipe (trace_s "(exit)\n") z3.Z3.stdIn w
+# (_, w) = writePipe "(get-model)\n" z3.Z3.stdIn w
+# (_, w) = writePipe "(exit)\n" z3.Z3.stdIn w
 # (_, w) = waitForProcess z3.Z3.handle w
 # (out, w) = readPipeNonBlocking z3.Z3.stdOut w
 # out = fromOk out
 = (out, w)
-
-trace_s :: String -> String
-trace_s s = trace s s
diff --git a/Assignment2/src/die.properties b/Assignment2/src/die.properties
index c53d02c..f507f66 100644
--- a/Assignment2/src/die.properties
+++ b/Assignment2/src/die.properties
@@ -1 +1 @@
-P=? [F s=7 & d=2]
+(EQ, 0.5, 7)