State elimination works on the die example

1 files changed, 108 insertions, 2 deletions

diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 3b8b2a7..abcfd06 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -11,7 +11,7 @@ import StdString
 import StdTuple
 
 import Data.Error
-from Data.Func import $, seqSt
+from Data.Func import $, mapSt, seqSt
 import Data.List
 import qualified Data.Map as M
 from Data.Map import :: Map
@@ -20,6 +20,112 @@ import System.File
 import System.FilePath
 import Text
 
+paths :: !*DTMC -> *([[Int]], !*DTMC)
+paths dtmc=:{nr_states,states}
+# (inits,states) = getInitStates (nr_states-1) states
+# (ps,states) = mapSt (paths` []) inits states
+= (flatten ps, {dtmc & states=states})
+where
+	getInitStates :: !Int !*{Maybe State} -> *(![Int], !*{Maybe State})
+	getInitStates i ss
+	| i < 0 = ([], ss)
+	# (s,ss) = ss![i]
+	| isNothing s = ([], ss)
+	# s = fromJust s
+	| s.init
+		# (inits,ss) = getInitStates (i-1) ss
+		= ([i:inits],ss)
+	= getInitStates (i-1) ss
+
+	paths` :: ![Int] !Int !*{Maybe State} -> *(![[Int]], !*{Maybe State})
+	paths` seen cur ss
+	| isMember cur seen = ([], ss)
+	# (s,ss) = ss![cur]
+	| isNothing s = ([], ss)
+	# s = fromJust s
+	| isAbsorbing s = ([[cur]], ss)
+	# succ = 'M'.keys s.transitions
+	# (pss,ss) = mapSt (paths` [cur:seen]) succ ss
+	= ([[cur:p] \\ ps <- pss, p <- ps], ss)
+
+stateElimination :: !*DTMC -> *DTMC
+stateElimination dtmc=:{nr_states}
+# (ps,dtmc) = paths dtmc
+= case [p \\ p=:[_:_:_:_] <- ps] of
+	[]    -> {dtmc & states=prune (nr_states-1) dtmc.states}
+	[p:_] -> stateElimination {dtmc & states=uncurry elim (penultimate_trans p) dtmc.states}
+		with
+			penultimate_trans [x,y,_] = (x,y)
+			penultimate_trans [_:xs] = penultimate_trans xs
+where
+	prune :: !Int !*{Maybe State} -> *{Maybe State}
+	prune i ss
+	| i < 0 = ss
+	# (Just s,ss) = ss![i]
+	| s.init || isAbsorbing s = prune (i-1) ss
+	| otherwise               = prune (i-1) $ remove i (nr_states-1) ss
+	where
+		remove :: !Int !Int !*{Maybe State} -> *{Maybe State}
+		remove i j ss
+		| j < 0 = {ss & [i]=Nothing}
+		# (s,ss) = ss![j]
+		| isNothing s = remove i (j-1) ss
+		# s = fromJust s
+		= remove i (j-1) ss
+
+	elim :: !Int !Int !*{Maybe State} -> *{Maybe State}
+	elim s1 s ss
+	# (Just s1s,ss) = ss![s1]
+	# prob = 'M'.get s s1s.transitions
+
+	# (succ,ss) = ss![s]
+	| isNothing succ = ss
+	# succ = fromJust succ
+	| succ.init || isAbsorbing succ = ss
+	# succ = succ.transitions
+
+	# self_prob = fromMaybe "0" $ 'M'.get s succ
+	# succ = 'M'.toList succ
+	| s1 == s
+		# ss = seqSt (uncurry $ update_eq self_prob) succ ss
+		# (Just s1s,ss) = ss![s1]
+		# ss & [s1] = Just {s1s & transitions='M'.del s s1s.transitions}
+		= ss
+	| otherwise
+		# ss = seqSt (uncurry $ update_ne self_prob) succ ss
+		# (Just s1s,ss) = ss![s1]
+		# ss & [s1] = Just {s1s & transitions='M'.del s s1s.transitions}
+		= ss
+	where
+		update_eq :: !String !Int !String !*{Maybe State} -> *{Maybe State}
+		update_eq self_prob s2 prob2 ss
+		| s == s2 = ss
+		# (Just s1s,ss) = ss![s1]
+		# ss & [s1] = Just
+			{ s1s
+			& transitions = 'M'.put s2
+				("(" +++ prob2 +++ ")/(1-(" +++ self_prob +++ "))")
+				s1s.transitions
+			}
+		= ss
+
+		update_ne :: !String !Int !String !*{Maybe State} -> *{Maybe State}
+		update_ne self_prob s2 prob2 ss
+		| s == s2 = ss
+		# (Just s1s,ss) = ss![s1]
+		# ps1s2 = fromMaybe "0" $ 'M'.get s2 s1s.transitions
+		# ps1s = fromMaybe "0" $ 'M'.get s s1s.transitions
+		# ss & [s1] = Just
+			{ s1s
+			& transitions = 'M'.put s2
+				(ps1s2 +++ "+(" +++ ps1s +++ ")*(" +++ prob2 +++ ")/(1-(" +++ self_prob +++ "))")
+				s1s.transitions
+			}
+		= ss
+
+isAbsorbing :: !State -> Bool
+isAbsorbing s = all ((==) s.state_id) [to \\ (to,_) <- 'M'.toList s.transitions]
+
 parseDTMC :: !FilePath !*World -> *(!DTMC, !*World)
 parseDTMC fp w
 # (lines,w) = readFileLines fp w
@@ -60,4 +166,4 @@ where
 
 Start w
 # (dtmc,w) = parseDTMC "die.drn" w
-= stateElimination dtmc
+= [(s.state_id, 'M'.toList s.transitions, '\n') \\ Just s <-: (stateElimination dtmc).states]