From e77138a79fa3d9b9c99a5111266e61e5d5b0b3ef Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 28 Jan 2015 14:09:55 +0000 Subject: [PATCH] computeRestrictedNext() for ProbModelChecker, NondetModelChecker, DTMCModelChecker and MDPModelChecker. [Joachim Klein] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9571 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 27 ++++++++++++++ prism/src/explicit/MDPModelChecker.java | 30 ++++++++++++++++ prism/src/prism/NondetModelChecker.java | 45 ++++++++++++++++++++++++ prism/src/prism/ProbModelChecker.java | 34 ++++++++++++++++++ 4 files changed, 136 insertions(+) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index f1620558..8c08ec10 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -362,6 +362,33 @@ public class DTMCModelChecker extends ProbModelChecker return res; } + /** + * Given a value vector x, compute the probability: + * v(s) = Sum_s' P(s,s')*x(s') for s labeled with a, + * v(s) = 0 for s not labeled with a. + * + * @param dtmc the DTMC model + * @param a the set of states labeled with a + * @param x the value vector + */ + protected double[] computeRestrictedNext(DTMC dtmc, BitSet a, double[] x) + { + double[] soln; + int n; + + // Store num states + n = dtmc.getNumStates(); + + // initialized to 0.0 + soln = new double[n]; + + // Next-step probabilities multiplication + // restricted to a states + dtmc.mvMult(x, soln, a, false); + + return soln; + } + /** * Compute reachability probabilities. * i.e. compute the probability of reaching a state in {@code target}. diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 0b25d94e..78034e4c 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -187,6 +187,36 @@ public class MDPModelChecker extends ProbModelChecker return res; } + /** + * Given a value vector x, compute the probability: + * v(s) = min/max sched [ Sum_s' P_sched(s,s')*x(s') ] for s labeled with a, + * v(s) = 0 for s not labeled with a. + * + * Clears the StateValues object x. + * + * @param tr the transition matrix + * @param a the set of states labeled with a + * @param x the value vector + * @param min compute min instead of max + */ + public double[] computeRestrictedNext(MDP mdp, BitSet a, double[] x, boolean min) + { + int n; + double soln[]; + + // Store num states + n = mdp.getNumStates(); + + // initialized to 0.0 + soln = new double[n]; + + // Next-step probabilities multiplication + // restricted to a states + mdp.mvMultMinMax(x, min, soln, a, false, null); + + return soln; + } + /** * Compute reachability probabilities. * i.e. compute the min/max probability of reaching a state in {@code target}. diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 2f4e861e..0018dfaf 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1156,6 +1156,51 @@ public class NondetModelChecker extends NonProbModelChecker return probs; } + /** + * Given a value vector x, compute the probability: + * v(s) = min/max sched [ Sum_s' P_sched(s,s')*x(s') ] for s labeled with a, + * v(s) = 0 for s not labeled with a. + * + * Clears the StateValues object x. + * + * @param tr the transition matrix + * @param a the set of states labeled with a + * @param x the value vector + * @param min compute min instead of max + */ + protected StateValues computeRestrictedNext(JDDNode tr, JDDNode a, StateValues x, boolean min) + { + JDDNode tmp; + StateValuesMTBDD probs = null; + + // ensure that values are given in MTBDD format + StateValuesMTBDD ddX = x.convertToStateValuesMTBDD(); + + tmp = ddX.getJDDNode(); + JDD.Ref(tmp); + tmp = JDD.PermuteVariables(tmp, allDDRowVars, allDDColVars); + JDD.Ref(tr); + tmp = JDD.MatrixMultiply(tr, tmp, allDDColVars, JDD.BOULDER); + // (then min or max) + if (min) { + // min + JDD.Ref(nondetMask); + tmp = JDD.Apply(JDD.MAX, tmp, nondetMask); + tmp = JDD.MinAbstract(tmp, allDDNondetVars); + } else { + // max + tmp = JDD.MaxAbstract(tmp, allDDNondetVars); + } + + // label is 0/1 BDD, MIN sets all values to 0 for states not in a + JDD.Ref(a); + tmp = JDD.Apply(JDD.MIN, tmp, a); + + probs = new StateValuesMTBDD(tmp, model); + ddX.clear(); + return probs; + } + // compute probabilities for bounded until protected StateValues computeBoundedUntilProbs(JDDNode tr, JDDNode tr01, JDDNode b1, JDDNode b2, int time, boolean min) throws PrismException diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 82449b29..0032c0b2 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -1123,6 +1123,40 @@ public class ProbModelChecker extends NonProbModelChecker return probs; } + /** + * Given a value vector x, compute the probability: + * v(s) = Sum_s' P(s,s')*x(s') for s labeled with a, + * v(s) = 0 for s not labeled with a. + * + * Clears the StateValues object x. + * + * @param tr the transition matrix + * @param a the set of states labeled with a + * @param x the value vector + */ + protected StateValues computeRestrictedNext(JDDNode tr, JDDNode a, StateValues x) + { + JDDNode tmp; + StateValuesMTBDD probs = null; + + // ensure that values are given in MTBDD format + StateValuesMTBDD ddX = x.convertToStateValuesMTBDD(); + + tmp = ddX.getJDDNode(); + JDD.Ref(tmp); + tmp = JDD.PermuteVariables(tmp, allDDRowVars, allDDColVars); + JDD.Ref(tr); + tmp = JDD.MatrixMultiply(tr, tmp, allDDColVars, JDD.BOULDER); + + // label is 0/1 BDD, MIN sets all values to 0 for states not in a + JDD.Ref(a); + tmp = JDD.Apply(JDD.MIN, tmp, a); + + ddX.clear(); + probs = new StateValuesMTBDD(tmp, model); + return probs; + } + // compute probabilities for bounded until protected StateValues computeBoundedUntilProbs(JDDNode tr, JDDNode tr01, JDDNode b1, JDDNode b2, int time) throws PrismException