From e1b22b5a9dbf7e37d7e6bd0a249b3107b825620f Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 19 Aug 2016 14:02:31 +0000 Subject: [PATCH] param/exact: warn if some probability/rate is zero in an update The transitions are explored twice during model construction, once to find the reachable states and the second time to actually build the transition structure of the model. We suppress the warning in the first pass so that it does not appear twice. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11656 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/param/ModelBuilder.java | 4 ++-- prism/src/param/SymbolicEngine.java | 9 ++++++++- 2 files changed, 10 insertions(+), 3 deletions(-) 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);