From eeb31a9735f1a469525fb0eda420ec52c89064cd Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 22 Oct 2010 09:28:10 +0000 Subject: [PATCH] Simulator complains about invalid (-ve/NaN) probs/rates. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2184 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ModelType.java | 1 + prism/src/simulator/Choice.java | 1 + prism/src/simulator/ChoiceList.java | 8 ++++++++ prism/src/simulator/ChoiceListFlexi.java | 9 +++++++++ prism/src/simulator/ChoiceSingleton.java | 6 ++++++ prism/src/simulator/TransitionList.java | 13 ++++++++++++- prism/src/simulator/Updater.java | 18 ++++++++++++++++-- 7 files changed, 53 insertions(+), 3 deletions(-) diff --git a/prism/src/prism/ModelType.java b/prism/src/prism/ModelType.java index fdc75801..091d16d3 100644 --- a/prism/src/prism/ModelType.java +++ b/prism/src/prism/ModelType.java @@ -53,6 +53,7 @@ public enum ModelType { /** * Do the transitions in a choice sum to 1 for this model type? + * Can also use this to test whether models uses rates or probabilities. */ public boolean choicesSumToOne() { diff --git a/prism/src/simulator/Choice.java b/prism/src/simulator/Choice.java index 3762ac98..96ce3bca 100644 --- a/prism/src/simulator/Choice.java +++ b/prism/src/simulator/Choice.java @@ -45,4 +45,5 @@ public interface Choice public State computeTarget(int i, State currentState) throws PrismLangException; public void computeTarget(int i, State currentState, State newState) throws PrismLangException; public int getIndexByProbabilitySum(double x); + public void checkValid(ModelType modelType) throws PrismException; } diff --git a/prism/src/simulator/ChoiceList.java b/prism/src/simulator/ChoiceList.java index 9701a82a..587ae2cd 100644 --- a/prism/src/simulator/ChoiceList.java +++ b/prism/src/simulator/ChoiceList.java @@ -30,6 +30,8 @@ import java.util.*; import parser.*; import parser.ast.*; +import prism.ModelType; +import prism.PrismException; import prism.PrismLangException; public class ChoiceList implements Choice @@ -201,6 +203,12 @@ public class ChoiceList implements Choice return i - 1; } + @Override + public void checkValid(ModelType modelType) throws PrismException + { + // TODO + } + public String toString() { int i, n; diff --git a/prism/src/simulator/ChoiceListFlexi.java b/prism/src/simulator/ChoiceListFlexi.java index 7b5be61b..b2fc705f 100644 --- a/prism/src/simulator/ChoiceListFlexi.java +++ b/prism/src/simulator/ChoiceListFlexi.java @@ -30,6 +30,8 @@ import java.util.*; import parser.*; import parser.ast.*; +import prism.ModelType; +import prism.PrismException; import prism.PrismLangException; public class ChoiceListFlexi implements Choice @@ -284,6 +286,13 @@ public class ChoiceListFlexi implements Choice return i - 1; } + @Override + public void checkValid(ModelType modelType) throws PrismException + { + // Currently nothing to do here: + // Checks for bad probabilities/rates done earlier. + } + public String toString() { int i, n; diff --git a/prism/src/simulator/ChoiceSingleton.java b/prism/src/simulator/ChoiceSingleton.java index a9f7103b..c2c7d383 100644 --- a/prism/src/simulator/ChoiceSingleton.java +++ b/prism/src/simulator/ChoiceSingleton.java @@ -155,6 +155,12 @@ public class ChoiceSingleton implements Choice return (i == 0) ? command : null; } + @Override + public void checkValid(ModelType modelType) throws PrismException + { + // TODO + } + @Override public String toString() { diff --git a/prism/src/simulator/TransitionList.java b/prism/src/simulator/TransitionList.java index 7ed3a881..ee413af5 100644 --- a/prism/src/simulator/TransitionList.java +++ b/prism/src/simulator/TransitionList.java @@ -72,7 +72,18 @@ public class TransitionList numTransitions += tr.size(); probSum += tr.getProbabilitySum(); } - + + /** + * Check the validity of the available transitions for a given model type. + * Throw a PrismExecption if an error is found. + */ + public void checkValid(ModelType modelType) throws PrismException + { + for (Choice ch : choices) { + ch.checkValid(modelType); + } + } + // ACCESSORS /** diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index aa3ca518..29538d19 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -191,7 +191,11 @@ public class Updater transitionList.add(ch); } } - + + // Check validity of the computed transitions + // (not needed currently) + //transitionList.checkValid(modelType); + //System.out.println(transitionList); } @@ -272,7 +276,8 @@ public class Updater /** * Create a new Choice object (currently ChoiceListFlexi) based on an Updates object - * and a (global) state. If appropriate, check probabilities sum to 1 too. + * and a (global) state. Check for negative probabilities/rates and, if appropriate, + * check probabilities sum to 1 too. * @param moduleOrActionIndex Module/action for the choice, encoded as an integer (see Choice) * @param ups The Updates object * @param state Global state @@ -290,7 +295,16 @@ public class Updater n = ups.getNumUpdates(); sum = 0; for (i = 0; i < n; i++) { + // Compute probability/rate p = ups.getProbabilityInState(i, state); + // Check for negative/NaN probabilities/rates + if (Double.isNaN(p) || p < 0) { + String s = modelType.choicesSumToOne() ? "Probability" : "Rate"; + s += " is invalid (" + p + ") in state " + state.toString(modulesFile); + // Note: we indicate error in whole Updates object because the offending + // probability expression has probably been simplified from original form. + throw new PrismLangException(s, ups); + } sum += p; list = new ArrayList(); list.add(ups.getUpdate(i));