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

@@ -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}.

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}.

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

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