From 22076843353448809fcea00092dc735765b4cb23 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 28 Aug 2017 12:45:48 +0200 Subject: [PATCH] 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 | 19 +++++++++-- prism/src/param/ValueComputer.java | 54 +++++++++++++++++++++++++++--- 2 files changed, 67 insertions(+), 6 deletions(-) diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index 7eb9d4db..c2268b3b 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -588,11 +588,16 @@ public final class ParamModel extends ModelExplicit implements MDPGeneric + * 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 MDPGeneric0 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(); diff --git a/prism/src/param/ValueComputer.java b/prism/src/param/ValueComputer.java index a165bbfa..a2b9303f 100644 --- a/prism/src/param/ValueComputer.java +++ b/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). + *
+ * 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). + *
+ * In exact mode, throws an exception if there are negative rewards (not supported for MDPs). + *
+ * 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; + } } }