Add properties

2 files changed, 61 insertions, 25 deletions

diff --git a/Assignment2/src/DTMC.dcl b/Assignment2/src/DTMC.dcl
index 5b491ae..b663431 100644
--- a/Assignment2/src/DTMC.dcl
+++ b/Assignment2/src/DTMC.dcl
@@ -5,8 +5,9 @@ from Data.Maybe import :: Maybe
 from System.FilePath import :: FilePath
 
 :: *DTMC =
-	{ nr_states :: !Int
-	, states    :: !*{Maybe State}
+	{ nr_states  :: !Int
+	, parameters :: ![String]
+	, states     :: !*{Maybe State}
 	}
 
 :: State =
@@ -22,4 +23,10 @@ from System.FilePath import :: FilePath
 stateElimination :: !*DTMC -> *DTMC
 parseDTMC :: !FilePath !*World -> *(!*DTMC, !*World)
 printDTMC :: !*DTMC -> *(!String, !*DTMC)
-addVars :: *DTMC -> *DTMC
+addVars :: !*DTMC -> *DTMC
+
+:: RepairConfig =
+	{ totality_restrictions :: ![String]
+	}
+
+repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC)
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index c532dfb..d9286fd 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -141,8 +141,9 @@ parseDTMCFromLines lines
 # [nr_states:_:lines] = tl $ dropWhile ((<>) "@nr_states") lines
 # states = map parseState $ groupLines "\t" [] lines
 =
-	{ nr_states = toInt nr_states
-	, states    = {Just s \\ s <- states}
+	{ nr_states  = toInt nr_states
+	, parameters = []
+	, states     = {Just s \\ s <- states}
 	}
 where
 	parseState :: ![String] -> State
@@ -170,12 +171,13 @@ where
 	| otherwise            = [reverse current:groupLines head [line] lines]
 
 printDTMC :: !*DTMC -> *(!String, !*DTMC)
-printDTMC dtmc=:{nr_states,states}
+printDTMC dtmc=:{nr_states,parameters,states}
 # (state_strings,states) = printStates 0 states
-# s = join "\n"
+# s = join "\n" $
 	[ "@type: DTMC"
-	, "@parameters\n"
-	, "@reward_models\n"
+	, "@parameters"
+	] ++ if (isEmpty parameters) [""] parameters ++
+	[ "@reward_models\n"
 	, "@nr_states"
 	, toString nr_states
 	, "@model"
@@ -197,25 +199,52 @@ where
 	# (reprs,ss) = printStates (i+1) ss
 	= (repr ++ reprs,ss)
 
-addVars :: *DTMC -> *DTMC
-addVars dtmc = {DTMC | nr_states = dtmc.nr_states, states = addVarsS 0 dtmc.nr_states dtmc.states}
+addVars :: !*DTMC -> *DTMC
+addVars dtmc=:{nr_states} = addVarsS (nr_states-1) dtmc
 where
-	addVarsS :: !Int !Int !*{Maybe State} -> *{Maybe State}
-	addVarsS fi m ss
-	| fi >= m = ss
-	| otherwise = addVarsS (fi + 1) m (addVarsT fi 0 m ss)
+	addVarsS :: !Int !*DTMC -> *DTMC
+	addVarsS i dtmc=:{states}
+	| i < 0 = dtmc
+	# (s,states) = states![i]
+	# dtmc & states = states
+	| isNothing s = dtmc
+	# s = fromJust s
+	# dtmc = seqSt (uncurry $ addVar i) ('M'.toList s.transitions) dtmc
+	= addVarsS (i-1) dtmc
+
+	addVar :: !Int !Int !String !*DTMC -> *DTMC
+	addVar f t prob dtmc=:{parameters}
+	# (s,dtmc) = dtmc!states.[f]
+	# s = fromJust s
+	# s & transitions = 'M'.put t ("((" <+ prob <+ ") + " <+ var <+ ")") s.transitions
+	# dtmc & states.[f] = Just s
+	# dtmc & parameters = [var:parameters]
+	= dtmc
+	where
+		var = "v" <+ f <+ "_" <+ t
 
-	addVarsT :: !Int !Int !Int !*{Maybe State} -> *{Maybe State}
-	addVarsT fi ti m ss
-	| ti >= m = ss
-	# (s, ss) = ss![fi]
-	= case s of
-		Nothing -> ss
-		(Just s) -> addVarsT fi (ti + 1) m {ss & [fi] = Just {s & transitions = alter (addVar fi ti) ti s.transitions}}
+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)
 
-	addVar :: Int Int (Maybe String) -> Maybe String
-	addVar _ _ Nothing = Nothing
-	addVar f t (Just fn) = Just ("((" <+ fn <+ ") + v" <+ f <+ "_" <+ t <+ ")")
+	totality :: !State -> String
+	totality s = "(= 1 (" <+ parseInfix expr <+ "))"
+	where
+		expr = "(" <+ (join ")+(" $ 'M'.elems s.transitions) <+ ")"
 
 findInitial :: !*DTMC -> (!State, !*DTMC)
 findInitial dtmc=:{nr_states,states}