Add properties to make transition probabilities remain in [0,1]

2 files changed, 18 insertions, 5 deletions

diff --git a/Assignment2/src/DTMC.dcl b/Assignment2/src/DTMC.dcl
index 233739b..98ef581 100644
--- a/Assignment2/src/DTMC.dcl
+++ b/Assignment2/src/DTMC.dcl
@@ -33,7 +33,8 @@ printDTMC :: !*DTMC -> *(!String, !*DTMC)
 addVars :: !*DTMC -> *DTMC
 
 :: RepairConfig =
-	{ totality_restrictions :: ![String]
+	{ totality_restrictions   :: ![String]
+	, transition_restrictions :: ![String]
 	}
 
 repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC)
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 83c5ac1..9c36b5b 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -229,9 +229,11 @@ where
 repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC)
 repairConfig dtmc=:{nr_states,states}
 # (ss,states) = collectStates (nr_states-1) states
+# transs = concatMap collectTransitions ss
 # dtmc & states = states
 # config =
-	{ totality_restrictions = map totality ss
+	{ totality_restrictions   = map totality ss
+	, transition_restrictions = concatMap probabilityBounds transs
 	}
 = (config, dtmc)
 where
@@ -239,16 +241,25 @@ where
 	collectStates i ss
 	| i < 0 = ([], ss)
 	# (s,ss) = ss![i]
-	| isNothing s = ([], ss)
+	| isNothing s = collectStates (i-1) ss
 	# s = fromJust s
 	# (rest,ss) = collectStates (i-1) ss
 	= ([s:rest],ss)
 
+	collectTransitions :: !State -> [(!Int,!Int,!String)]
+	collectTransitions s = [(s.state_id, to, prob) \\ (to,prob) <- 'M'.toList s.transitions]
+
 	totality :: !State -> String
 	totality s = "(= 1 " <+ parenthesise (parseInfix expr) <+ ")"
 	where
 		expr = "(" <+ (join ")+(" $ 'M'.elems s.transitions) <+ ")"
 
+	probabilityBounds :: !(!Int, !Int, !String) -> [String]
+	probabilityBounds (_,_,prob) =
+		[ "(<= 0 " <+ parenthesise (parseInfix prob) <+ ")"
+		, "(>= 1 " <+ parenthesise (parseInfix prob) <+ ")"
+		]
+
 findInitial :: !*DTMC -> (!State, !*DTMC)
 findInitial dtmc=:{nr_states,states}
 # (init,states) = findInitial` (nr_states-1) states
@@ -300,7 +311,7 @@ parseProperty s = case parseString s of
 
 Start w
 # ([prog:args],w) = getCommandLine w
-| length args <> 2 = "Usage: " +++ prog +++ " DRN PROPERTIES"
+| length args <> 2 = "Usage: " +++ prog +++ " DRN PROPERTIES\n"
 # [drn_in,props:_] = args
 
 # (dtmc,w) = parseDTMC drn_in w
@@ -314,8 +325,9 @@ Start w
 # (dtmc,w) = assertProperties props dtmc z3 w
 # (rC,dtmc) = repairConfig dtmc
 # w = seqSt (addAssert z3) rC.totality_restrictions w
+# w = seqSt (addAssert z3) rC.transition_restrictions w
 # (sat,w) = checkSat z3 w
 | sat
 	# (model,w) = getModel z3 w
 	= model
-| otherwise = "Could not satisfy the property"
+| otherwise = "Could not satisfy the property\n"