Start collecting properties

1 files changed, 25 insertions, 0 deletions

diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index d555782..95a1b7c 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -21,6 +21,8 @@ import System.File
 import System.FilePath
 import Text
 
+import Expression
+
 paths :: !*DTMC -> *([[Int]], !*DTMC)
 paths dtmc=:{nr_states,states}
 # (inits,states) = getInitStates (nr_states-1) states
@@ -219,6 +221,29 @@ where
 	where
 		var = "v" <+ f <+ "_" <+ t
 
+repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC)
+repairConfig dtmc=:{nr_states,states}
+# (ss,states) = collectStates (nr_states-1) states
+# dtmc & states = states
+# config =
+	{ totality_restrictions = map totality ss
+	}
+= (config, dtmc)
+where
+	collectStates :: !Int !*{Maybe State} -> *(![State], !*{Maybe State})
+	collectStates i ss
+	| i < 0 = ([], ss)
+	# (s,ss) = ss![i]
+	| isNothing s = ([], ss)
+	# s = fromJust s
+	# (rest,ss) = collectStates (i-1) ss
+	= ([s:rest],ss)
+
+	totality :: !State -> String
+	totality s = "(= 1 (" <+ parseInfix expr <+ "))"
+	where
+		expr = "(" <+ (join ")+(" $ 'M'.elems s.transitions) <+ ")"
+
 Start w
 # ([prog:args],w) = getCommandLine w
 | length args <> 2