2 files changed, 36 insertions, 2 deletions
diff --git a/Assignment2/src/DTMC.dcl b/Assignment2/src/DTMC.dcl
index c0b2a57..b663431 100644
--- a/Assignment2/src/DTMC.dcl
+++ b/Assignment2/src/DTMC.dcl
@@ -16,6 +16,10 @@ from System.FilePath import :: FilePath
 	, init        :: !Bool
 	}
 
+// Note that state_id must be an absorbing state
+// (Probability, state_id)
+:: Property :== (Real, Int)
+
 stateElimination :: !*DTMC -> *DTMC
 parseDTMC :: !FilePath !*World -> *(!*DTMC, !*World)
 printDTMC :: !*DTMC -> *(!String, !*DTMC)
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 95a1b7c..d9286fd 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -7,6 +7,7 @@ import StdFile
 from StdFunc import o
 import StdInt
 import StdList
+from StdMisc import abort
 import StdString
 import StdTuple
 
@@ -22,6 +23,7 @@ import System.FilePath
 import Text
 
 import Expression
+import Z3
 
 paths :: !*DTMC -> *([[Int]], !*DTMC)
 paths dtmc=:{nr_states,states}
@@ -244,6 +246,29 @@ where
 	where
 		expr = "(" <+ (join ")+(" $ 'M'.elems s.transitions) <+ ")"
 
+findInitial :: !*DTMC -> (!State, !*DTMC)
+findInitial dtmc=:{nr_states,states}
+# (init,states) = findInitial` (nr_states-1) states
+# dtmc & states = states
+= (init, dtmc)
+where
+	findInitial` :: !Int !*{Maybe State} -> *(!State, !*{Maybe State})
+	findInitial` i states
+	| i < 0 = abort "No initial state"
+	# (state, states) = states![i]
+	| isJust state && (fromJust state).init = (fromJust state, states)
+	| otherwise = findInitial` (i - 1) states
+
+assertProperty :: !Property !*DTMC !Z3 !*World -> (*DTMC, *World)
+assertProperty (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"
+# formula = fromJust formula
+# formula = "(= (" <+ prob <+ ") (" <+ parseInfix formula <+ "))"
+# w = addAssert z3 formula w
+= (dtmc, w)
+
 Start w
 # ([prog:args],w) = getCommandLine w
 | length args <> 2
@@ -255,6 +280,11 @@ Start w
 # (dtmc,w) = parseDTMC drn_in w
 # dtmc = addVars dtmc
 # dtmc = stateElimination dtmc
-# (dtmcs,dtmc) = printDTMC dtmc
-# (_,w) = writeFile drn_out dtmcs w
+# (z3,w) = startZ3 w
+# (dtmc,w) = assertProperty prop dtmc z3 w
+//# (dtmcs,dtmc) = printDTMC dtmc
+//# (_,w) = writeFile drn_out dtmcs w
 = w
+where
+	prop :: Property
+	prop = (0.5, 7) // Chance to reach state 7 is 0.5