diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index e9d48b0e..a378a252 100644 --- a/prism/src/param/ModelBuilder.java +++ b/prism/src/param/ModelBuilder.java @@ -322,7 +322,7 @@ public final class ModelBuilder extends PrismComponent while (!explore.isEmpty()) { state = explore.removeFirst(); - TransitionList tranlist = engine.calculateTransitions(state); + TransitionList tranlist = engine.calculateTransitions(state, true); // Suppress warnings int numChoices = tranlist.getNumChoices(); if (isNonDet) { numTotalChoices += numChoices; @@ -394,7 +394,7 @@ public final class ModelBuilder extends PrismComponent model.addInitialState(permut[0]); int stateNr = 0; for (State state : statesList) { - TransitionList tranlist = engine.calculateTransitions(state); + TransitionList tranlist = engine.calculateTransitions(state, false); int numChoices = tranlist.getNumChoices(); boolean computeSumOut = !isNonDet; diff --git a/prism/src/param/SymbolicEngine.java b/prism/src/param/SymbolicEngine.java index dc314257..8b16008c 100644 --- a/prism/src/param/SymbolicEngine.java +++ b/prism/src/param/SymbolicEngine.java @@ -70,6 +70,9 @@ public class SymbolicEngine protected ModelBuilder modelBuilder; protected FunctionFactory functionFactory; + // flag that suppresses warnings during calculateTransitions + private boolean noWarnings = false; + public SymbolicEngine(ModulesFile modulesFile, ModelBuilder modelBuilder, FunctionFactory functionFactory) { this.modelBuilder = modelBuilder; @@ -137,12 +140,14 @@ public class SymbolicEngine } } - public TransitionList calculateTransitions(State state) throws PrismException + public TransitionList calculateTransitions(State state, boolean noWarnings) throws PrismException { List chs; int i, j, k, l, n, count; TransitionList transitionList = new TransitionList(); + this.noWarnings = noWarnings; + // Clear lists/bitsets transitionList.clear(); for (i = 0; i < numModules; i++) { @@ -295,6 +300,8 @@ public class SymbolicEngine Function pFn = modelBuilder.expr2function(functionFactory, p); if (pFn.isZero()) { // function for probability / rate is zero, don't add the corresponding transition + if (!noWarnings) + modelBuilder.getLog().printWarning("Update has zero " + (modelType.continuousTime() ? "rate" : "probability") + " (" + p + (p.hasPosition() ? ", " + p.getBeginString() : "") +")"); continue; } ch.add(pFn, list);