From b543dca6bafa7353f4cac992c44b9269f182ce06 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 28 Aug 2017 12:45:48 +0200 Subject: [PATCH] param / exact ValueComputer: skip policy iteration for DTMC/CTMCs and directly compute the values --- prism/src/param/ValueComputer.java | 37 ++++++++++++++++++++++++------ 1 file changed, 30 insertions(+), 7 deletions(-) diff --git a/prism/src/param/ValueComputer.java b/prism/src/param/ValueComputer.java index 1582edf5..a23370d1 100644 --- a/prism/src/param/ValueComputer.java +++ b/prism/src/param/ValueComputer.java @@ -36,7 +36,7 @@ import common.IterableBitSet; import common.IterableStateSet; import prism.PrismComponent; import prism.PrismException; - +import prism.PrismNotSupportedException; /** * Computes values for properties of a parametric Markov model. @@ -266,12 +266,6 @@ final class ValueComputer extends PrismComponent private RegionValues computeUnbounded(Region region, StateValues b1, StateValues b2, boolean min, ParamRewardStruct rew) throws PrismException { - BigRational requiredVolume = region.volume().multiply(BigRational.ONE.subtract(precision)); - RegionValues result = new RegionValues(regionFactory); - RegionsTODO todo = new RegionsTODO(); - todo.add(region); - BigRational volume = BigRational.ZERO; - if (rew != null) { // determine infinity states explicit.MDPModelChecker mcExplicit = new explicit.MDPModelChecker(this); @@ -286,6 +280,35 @@ final class ValueComputer extends PrismComponent } } + switch (model.getModelType()) { + case CTMC: + case DTMC: + return computeUnboundedMC(region, b1, b2, rew); + case MDP: + return computeUnboundedMDP(region, b1, b2, min, rew); + default: + throw new PrismNotSupportedException("Parametric unbounded reachability computation not supported for " + model.getModelType()); + } + } + + private RegionValues computeUnboundedMC(Region region, StateValues b1, StateValues b2, ParamRewardStruct rew) + { + // Convert to MutablePMC, using trivial scheduler (take first choice everywhere) + Scheduler trivialScheduler = new Scheduler(model); + + MutablePMC pmc = buildAlterablePMCForReach(model, b1, b2, trivialScheduler, rew); + StateValues values = computeValues(pmc, model.getFirstInitialState()); + return regionFactory.completeCover(values); + } + + private RegionValues computeUnboundedMDP(Region region, StateValues b1, StateValues b2, boolean min, ParamRewardStruct rew) throws PrismException + { + BigRational requiredVolume = region.volume().multiply(BigRational.ONE.subtract(precision)); + RegionValues result = new RegionValues(regionFactory); + RegionsTODO todo = new RegionsTODO(); + todo.add(region); + BigRational volume = BigRational.ZERO; + Scheduler initialScheduler = new Scheduler(model); precomputeScheduler(model, initialScheduler, b1, b2, rew, min);