diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index 701afb55..70b76288 100644 --- a/prism/src/param/ModelBuilder.java +++ b/prism/src/param/ModelBuilder.java @@ -367,6 +367,8 @@ public final class ModelBuilder extends PrismComponent throw new PrismNotSupportedException("Cannot do explicit-state reachability if there are multiple initial states"); } + boolean doProbChecks = getSettings().getBoolean(PrismSettings.PRISM_DO_PROB_CHECKS); + mainLog.print("\nComputing reachable states..."); mainLog.flush(); long timer = System.currentTimeMillis(); @@ -394,29 +396,43 @@ public final class ModelBuilder extends PrismComponent for (State state : statesList) { TransitionList tranlist = engine.calculateTransitions(state); int numChoices = tranlist.getNumChoices(); - Function sumOut; - if (isNonDet) { - sumOut = functionFactory.getOne(); - } else { - sumOut = functionFactory.getZero(); - for (int choiceNr = 0; choiceNr < numChoices; choiceNr++) { - ChoiceListFlexi choice = tranlist.getChoice(choiceNr); - int numSuccessors = choice.size(); - for (int succNr = 0; succNr < numSuccessors; succNr++) { - ChoiceListFlexi succ = tranlist.getChoice(choiceNr); - Expression probExpr = succ.getProbability(succNr); - sumOut = sumOut.add(expr2function(functionFactory, probExpr)); + + boolean computeSumOut = !isNonDet; + boolean checkChoiceSumEqualsOne = doProbChecks && model.getModelType().choicesSumToOne(); + + // sumOut = the sum over all outgoing choices from this state + Function sumOut = functionFactory.getZero(); + for (int choiceNr = 0; choiceNr < numChoices; choiceNr++) { + ChoiceListFlexi choice = tranlist.getChoice(choiceNr); + int numSuccessors = choice.size(); + + // sumOutForChoice = the sum over all outgoing transitions for this choice + Function sumOutForChoice = functionFactory.getZero(); + for (int succNr = 0; succNr < numSuccessors; succNr++) { + ChoiceListFlexi succ = tranlist.getChoice(choiceNr); + Expression probExpr = succ.getProbability(succNr); + Function probFunc = expr2function(functionFactory, probExpr); + if (computeSumOut) + sumOut = sumOut.add(probFunc); + if (checkChoiceSumEqualsOne) + sumOutForChoice = sumOutForChoice.add(probFunc); + } + if (checkChoiceSumEqualsOne) { + if (!sumOutForChoice.equals(functionFactory.getOne())) { + if (sumOutForChoice.isConstant()) { + // as the sum is constant, we know that it is really not 1 + throw new PrismLangException("Probabilities sum to " + sumOutForChoice.asBigRational() + " instead of 1 in state " + + state.toString(modulesFile) + " for some command"); + } else { + throw new PrismLangException("In state " + state.toString(modulesFile) + " the probabilities sum to " + + sumOutForChoice + " for some command, which can not be determined to be equal to 1 (to ignore, use -noprobchecks option)"); + } } } } - /* - if (modelType == ModelType.DTMC && !sumOut.equals(functionFactory.getOne())) { - throw new PrismException("parametric analysis only supports " - + "DTMC in which in each state exactly one command is activated " - + "and in which probabilities add up to exactly 1."); - } - */ + if (sumOut.isZero()) { + // set sumOut to 1 for deadlock state or if we are in nonDet model sumOut = functionFactory.getOne(); } for (int choiceNr = 0; choiceNr < numChoices; choiceNr++) { @@ -428,6 +444,10 @@ public final class ModelBuilder extends PrismComponent ChoiceListFlexi succ = tranlist.getChoice(choiceNr); State stateNew = succ.computeTarget(succNr, state); Expression probExpr = succ.getProbability(succNr); + // divide by sumOut + // for DTMC, this normalises over the choices + // for CTMC this builds the embedded DTMC + // for MDP this does nothing (sumOut is set to 1) Function probFn = expr2function(functionFactory, probExpr).divide(sumOut); model.addTransition(permut[states.get(stateNew)], probFn, action); }