Assert simple formula in z3

2 files changed, 39 insertions, 2 deletions

diff --git a/Assignment2/src/DTMC.dcl b/Assignment2/src/DTMC.dcl
index 26cbe19..5b491ae 100644
--- a/Assignment2/src/DTMC.dcl
+++ b/Assignment2/src/DTMC.dcl
@@ -15,6 +15,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 1d9bafd..b2d88cf 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
 
@@ -21,6 +22,9 @@ import System.File
 import System.FilePath
 import Text
 
+import Expression
+import Z3
+
 paths :: !*DTMC -> *([[Int]], !*DTMC)
 paths dtmc=:{nr_states,states}
 # (inits,states) = getInitStates (nr_states-1) states
@@ -213,6 +217,30 @@ where
 	addVar _ _ Nothing = Nothing
 	addVar f t (Just fn) = Just ("((" <+ fn <+ ") + v" <+ f <+ "_" <+ t <+ ")")
 
+findInitial :: !*DTMC -> (!State, !*DTMC)
+findInitial dtmc
+# (states, dtmc) = dtmc!states
+# (m, dtmc) = dtmc!nr_states
+= findInitial` 0 m states
+where
+	findInitial` :: !Int !Int !*{Maybe State} -> State
+	findInitial` i m states
+	| i >= m = abort "No initial state"
+	# (state, states) = states![i]
+	| state.init = state
+	| otherwise = findInitial` (i + 1) m 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 = "((" <+ formula <+ ") = " <+ prob <+ ")"
+# formula = parseInfix formula
+# (z3, w) = addAssert z3 (toString formula) w
+= (dtmc, w)
+
 Start w
 # ([prog:args],w) = getCommandLine w
 | length args <> 2
@@ -224,6 +252,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