Browse Source

parametric / exact ValueComputer: treat MDP with maximum of 1 choice per state as a DTMC, skip policy iteration

master
Joachim Klein 8 years ago
committed by Dave Parker
parent
commit
c997b76f2a
  1. 3
      prism/src/param/ValueComputer.java

3
prism/src/param/ValueComputer.java

@ -285,6 +285,9 @@ final class ValueComputer extends PrismComponent
case DTMC:
return computeUnboundedMC(region, b1, b2, rew);
case MDP:
if (model.getMaxNumChoices() == 1) {
return computeUnboundedMC(region, b1, b2, rew);
}
return computeUnboundedMDP(region, b1, b2, min, rew);
default:
throw new PrismNotSupportedException("Parametric unbounded reachability computation not supported for " + model.getModelType());

Loading…
Cancel
Save