diff options
Diffstat (limited to 'Assignment2/src/DTMC.icl')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 50 |
1 files changed, 28 insertions, 22 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index 9c36b5b..c9696cf 100644 --- a/Assignment2/src/DTMC.icl +++ b/Assignment2/src/DTMC.icl @@ -71,15 +71,10 @@ where | 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 + | otherwise = prune (i-1) $ remove i 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 + remove :: !Int !*{Maybe State} -> *{Maybe State} + remove i ss = {ss & [i]=Nothing} elim :: !Int !Int !*{Maybe State} -> *{Maybe State} elim s1 s ss @@ -92,7 +87,7 @@ where | succ.init || isAbsorbing succ = ss # succ = succ.transitions - # self_prob = fromMaybe "0" $ 'M'.get s succ + # self_prob = fromMaybe "0.0" $ 'M'.get s succ # succ = 'M'.toList succ | s1 == s # ss = seqSt (uncurry $ update_eq self_prob) succ ss @@ -112,7 +107,7 @@ where # ss & [s1] = Just { s1s & transitions = 'M'.put s2 - ("(" +++ prob2 +++ ")/(1-(" +++ self_prob +++ "))") + ("(" +++ prob2 +++ ")/(1.0-(" +++ self_prob +++ "))") s1s.transitions } = ss @@ -121,12 +116,12 @@ where 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 + # ps1s2 = fromMaybe "0.0" $ 'M'.get s2 s1s.transitions + # ps1s = fromMaybe "0.0" $ 'M'.get s s1s.transitions # ss & [s1] = Just { s1s & transitions = 'M'.put s2 - (ps1s2 +++ "+(" +++ ps1s +++ ")*(" +++ prob2 +++ ")/(1-(" +++ self_prob +++ "))") + (ps1s2 +++ "+(" +++ ps1s +++ ")*(" +++ prob2 +++ ")/(1.0-(" +++ self_prob +++ "))") s1s.transitions } = ss @@ -226,14 +221,15 @@ where where var = "v" <+ f <+ "x" <+ t -repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC) -repairConfig dtmc=:{nr_states,states} +repairConfig :: !CostFunction !*DTMC -> *(!RepairConfig, !*DTMC) +repairConfig cf dtmc=:{nr_states,parameters,states} # (ss,states) = collectStates (nr_states-1) states # transs = concatMap collectTransitions ss # dtmc & states = states # config = { totality_restrictions = map totality ss , transition_restrictions = concatMap probabilityBounds transs + , minimalisation_goal = minimise cf parameters } = (config, dtmc) where @@ -250,16 +246,23 @@ where collectTransitions s = [(s.state_id, to, prob) \\ (to,prob) <- 'M'.toList s.transitions] totality :: !State -> String - totality s = "(= 1 " <+ parenthesise (parseInfix expr) <+ ")" + totality s = "(= 1.0 " <+ 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) <+ ")" + [ "(<= 0.0 " <+ parenthesise (parseInfix prob) <+ ")" + , "(>= 1.0 " <+ parenthesise (parseInfix prob) <+ ")" ] + minimise :: !CostFunction ![String] -> String + minimise cf params = foldr1 (\a b -> "(+ " <+ a <+ " " <+ b <+ ")") $ case cf of + NumberModifiedTransitions -> + ["(if (= 0.0 " <+ p <+ ") 0.0 1.0)" \\ p <- params] + SumSquaredErrors -> + ["(* " <+ p <+ " " <+ p <+ ")" \\ p <- params] + findInitial :: !*DTMC -> (!State, !*DTMC) findInitial dtmc=:{nr_states,states} # (init,states) = findInitial` (nr_states-1) states @@ -320,14 +323,17 @@ Start w # dtmc = addVars dtmc # dtmc = stateElimination dtmc +# (config,dtmc) = repairConfig SumSquaredErrors dtmc + # (z3,w) = startZ3 w # (dtmc,w) = z3AddVars dtmc z3 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 +# w = seqSt (addAssert z3) config.totality_restrictions w +# w = seqSt (addAssert z3) config.transition_restrictions w +//# w = addMinimize z3 config.minimalisation_goal w // TODO: not supported by Z3! + # (sat,w) = checkSat z3 w | sat # (model,w) = getModel z3 w = model -| otherwise = "Could not satisfy the property\n" += "Could not satisfy the property\n" |