From 700a13f030b1321b4f5c4a3fba80cffe2f8b3a3c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 5 Feb 2017 22:58:19 +0000 Subject: [PATCH] Refactoring in explicit CTMC model checker to reuse existing methods. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11973 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 23 +++-------------------- 1 file changed, 3 insertions(+), 20 deletions(-) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index e75417ac..4d9eb3d5 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -33,7 +33,6 @@ import explicit.rewards.MCRewards; import explicit.rewards.Rewards; import explicit.rewards.StateRewardsArray; import parser.ast.*; -import parser.type.*; import prism.*; /** @@ -254,25 +253,9 @@ public class CTMCModelChecker extends ProbModelChecker */ public StateValues doTransient(CTMC ctmc, double t, StateValues initDist) throws PrismException { - ModelCheckerResult res = null; - StateValues initDistNew = null, probs = null; - - // Build initial distribution (if not specified) - if (initDist == null) { - initDistNew = new StateValues(TypeDouble.getInstance(), new Double(0.0), ctmc); - double initVal = 1.0 / ctmc.getNumInitialStates(); - for (int in : ctmc.getInitialStates()) { - initDistNew.setDoubleValue(in, initVal); - } - } else { - initDistNew = initDist; - } - - // Compute transient probabilities - res = computeTransientProbs(ctmc, t, initDistNew.getDoubleArray()); - probs = StateValues.createFromDoubleArray(res.soln, ctmc); - - return probs; + StateValues initDistNew = (initDist == null) ? buildInitialDistribution(ctmc) : initDist; + ModelCheckerResult res = computeTransientProbs(ctmc, t, initDistNew.getDoubleArray()); + return StateValues.createFromDoubleArray(res.soln, ctmc); } // Numerical computation functions