param: Handle models that are malformed

The parametric engine works under the assumption that models
are well-defined, i.e., that parameter valuations will lead
to graph-preserving probabilities, etc.

If we encounter a point in a region where these assumptions
don't hold, we now treat this by splitting the region. Regions
with such an improper midpoint that are below the precision
threshold are considered to be undefined and further processing
is aborted.

In particular, this treatment ensures that we never perform
policy iteration on a model with parameter instantiation
that is not well defined / supported. E.g., if there
were negative rewards for such a point, policy iteration
would previously not necessarily terminate.

prism/src/param/ParamModel.java

@@ -588,11 +588,16 @@ public final class ParamModel extends ModelExplicit implements MDPGeneric<Functi
 	 * Instantiates the parametric model at a given point.
 	 * All transition probabilities, etc. will be evaluated and set as
 	 * probabilities of the concrete model at the given point. 
+	 * <br>
+	 * If {@code checkWellDefinedness} is {@code true}, checks that the
+	 * instantiated probabilities are actually probabilities and graph-preserving.
+	 * If that is not the case, this method then returns {@code null}.
 	 * 
 	 * @param point point to instantiate model at
+	 * @param checkWellDefinedness should we check that the model is well-defined?
 	 * @return nonparametric model instantiated at {@code point}
 	 */
-	ParamModel instantiate(Point point)
+	ParamModel instantiate(Point point, boolean checkWellDefinedness)
 	{
 		ParamModel result = new ParamModel();
 		result.setModelType(getModelType());
@@ -601,7 +606,17 @@ public final class ParamModel extends ModelExplicit implements MDPGeneric<Functi
 		for (int state = 0; state < numStates; state++) {
 			for (int choice = stateBegin(state); choice < stateEnd(state); choice++) {
 				for (int succ = choiceBegin(choice); succ < choiceEnd(choice); succ++) {
-					result.addTransition(succState(succ), functionFactory.fromBigRational(succProb(succ).evaluate(point)), labels[succ]);
+					BigRational p = succProb(succ).evaluate(point);
+					if (checkWellDefinedness) {
+						if (p.isSpecial() || p.compareTo(BigRational.ONE) == 1 || p.signum() <= 0) {
+							// For graph-preservation, probabilities have to be >0 and <=1
+							// Note: for CTMCs, succProb yields the probabilities of the embedded
+							// DTMC, while the rates are available separately (sumLeaving)
+							return null;
+						}
+					}
+					result.addTransition(succState(succ), functionFactory.fromBigRational(p), labels[succ]);
+
 				}
 				result.setSumLeaving(functionFactory.fromBigRational(this.sumLeaving(choice).evaluate(point)));
 				result.finishChoice();

prism/src/param/ValueComputer.java

@@ -310,7 +310,8 @@ final class ValueComputer extends PrismComponent
 
 	private RegionValues computeUnboundedMDP(Region region, StateValues b1, StateValues b2, boolean min, ParamRewardStruct rew) throws PrismException
 	{
-		BigRational requiredVolume = region.volume().multiply(BigRational.ONE.subtract(precision));
+		BigRational precisionForThisRegion = region.volume().multiply(precision);
+		BigRational requiredVolume = region.volume().subtract(precisionForThisRegion);
 		RegionValues result = new RegionValues(regionFactory);
 		RegionsTODO todo = new RegionsTODO();
 		todo.add(region);
@@ -323,6 +324,20 @@ final class ValueComputer extends PrismComponent
 			Region currentRegion = todo.poll();
 			Point midPoint = ((BoxRegion)currentRegion).getMidPoint();
 			Scheduler scheduler = computeOptConcreteReachScheduler(midPoint, model, b1, b2, min, rew, initialScheduler);
+			if (scheduler == null) {
+				// midpoint leads to non-well-defined model
+				if (currentRegion.volume().compareTo(precisionForThisRegion) <= 0) {
+					// region is below precision threshold, treat as undefined
+					// and adjust required volume
+					requiredVolume = requiredVolume.subtract(currentRegion.volume());
+				} else {
+					// we split the current region
+					// TODO: Would be nice to try and analyse the well-definedness constraints
+					todo.addAll(currentRegion.split());
+				}
+				continue;
+			}
+
 			ResultCacheEntry resultCacheEntry = lookupValues(PropType.REACH, b1, b2, rew, scheduler, min);
 			Function[] compare;
 			StateValues values;
@@ -393,14 +408,45 @@ final class ValueComputer extends PrismComponent
 		return resultCacheEntry;
 	}
 
+	/**
+	 * Compute an optimal scheduler for Pmin/Pmax[ b1 U b2 ] or Rmin/Rmax[ b1 U b2 ]
+	 * at the given parameter instantiation (point).
+	 * <br>
+	 * In parametric mode, returns {@code null} if the given point leads to a model
+	 * that is not well-formed, i.e., where transition probabilities are not actually
+	 * probabilities or graph-preserving, or the rewards are negative (not supported for MDPs).
+	 * <br>
+	 * In exact mode, throws an exception if there are negative rewards (not supported for MDPs).
+	 * <br>
+	 * This method expects an initial scheduler that ensures that policy iteration
+	 * will converge.
+	 *
+	 * @param point The point (parameter valuation) where the model should be instantiated
+	 * @param model the model
+	 * @param b1 the set of 'safe' states
+	 * @param b2 the set of 'target' states
+	 * @param min compute min or max? true = min
+	 * @param rew if non-null, compute reachability reward
+	 * @param initialScheduler an initial scheduler
+	 * @return an optimal scheduler
+	 */
 	Scheduler computeOptConcreteReachScheduler(Point point, ParamModel model, StateValues b1, StateValues b2, boolean min, ParamRewardStruct rew, Scheduler initialScheduler) throws PrismException
 	{
-		ParamModel concrete = model.instantiate(point);
+		ParamModel concrete = model.instantiate(point, true);
+		if (concrete == null) {
+			// point leads to non-welldefined model
+			return null;
+		}
 		ParamRewardStruct rewConcrete = null;
 		if (rew != null) {
 			rewConcrete = rew.instantiate(point);
-			if (mode == ParamMode.EXACT && rewConcrete.hasNegativeRewards()) {
-				throw new PrismNotSupportedException(mode.Engine() + " currently does not support negative rewards in reachability reward computations");
+			if (rewConcrete.hasNegativeRewards()) {
+				if (mode == ParamMode.EXACT) {
+					throw new PrismNotSupportedException(mode.Engine() + " currently does not support negative rewards in reachability reward computations");
+				} else {
+					// point leads to negative values in reward structure => unsupported
+					return null;
+				}
 			}
 		}