3 files changed, 8 insertions, 5 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 45abd4d..4bb6c18 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -242,7 +242,7 @@ where
 	= ([s:rest],ss)
 
 	totality :: !State -> String
-	totality s = "(= 1 (" <+ parseInfix expr <+ "))"
+	totality s = "(= 1 " <+ parenthesise (parseInfix expr) <+ ")"
 	where
 		expr = "(" <+ (join ")+(" $ 'M'.elems s.transitions) <+ ")"
 
@@ -265,7 +265,7 @@ assertProperty (prob, target) dtmc z3 w
 # formula = 'M'.get target init.transitions
 | isNothing formula = abort "Cannot reach property target from initial state"
 # formula = fromJust formula
-# formula = "(= (" <+ prob <+ ") (" <+ parseInfix formula <+ "))"
+# formula = "(= " <+ prob <+ " " <+ parenthesise (parseInfix formula) <+ ")"
 # w = addAssert z3 formula w
 = (dtmc, w)
 
@@ -275,6 +275,9 @@ z3AddVars dtmc z3 w
 # w = seqSt (addVariable z3) param w
 = (dtmc,w)
 
+parenthesise :: !a -> String | toString a
+parenthesise x = let s = toString x in if (s.[0] == '(') s ("(" +++ s +++ ")")
+
 Start w
 # ([prog:args],w) = getCommandLine w
 | length args <> 2
diff --git a/Assignment2/src/Z3.dcl b/Assignment2/src/Z3.dcl
index e7555cf..8628d5d 100644
--- a/Assignment2/src/Z3.dcl
+++ b/Assignment2/src/Z3.dcl
@@ -5,8 +5,8 @@ from System.Process import :: ProcessHandle, :: ProcessIO
 :: Z3
 
 startZ3 :: !*World -> (!Z3, !*World)
-addAssert :: !Z3 !String !*World -> !*World
-addVariable :: !Z3 !String !*World -> !*World
+addAssert :: !Z3 !String !*World -> *World
+addVariable :: !Z3 !String !*World -> *World
 checkSat :: !Z3 !*World -> (!Bool, !*World)
 
 // Note: getModel terminates z3
diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl
index 2efe664..cb054e1 100644
--- a/Assignment2/src/Z3.icl
+++ b/Assignment2/src/Z3.icl
@@ -53,4 +53,4 @@ getModel z3 w
 = (out, w)
 
 trace_s :: String -> String
-trace_s s = trace_n s s
+trace_s s = trace s s