diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 521cc4d7..c6523986 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -577,7 +577,7 @@ public class LTLModelChecker tmp = JDD.SumAbstract(tmp, model.getAllDDColVars()); // If the sum for a (state,action) tuple is 1, // there is an action that remains in the stable set with prob 1 - tmp = JDD.GreaterThan(tmp, 1 - prism.getUpdateSumRoundOff()); + tmp = JDD.GreaterThan(tmp, 1 - prism.getSumRoundOff()); // Without fairness, we just need one action per state current = JDD.ThereExists(tmp, model.getAllDDNondetVars()); } @@ -603,7 +603,7 @@ public class LTLModelChecker mask = JDD.SumAbstract(mask, model.getAllDDColVars()); // If the sum for a (state,action) tuple is 1, // there is an action that remains in the stable set with prob 1 - mask = JDD.GreaterThan(mask, 1 - prism.getUpdateSumRoundOff()); + mask = JDD.GreaterThan(mask, 1 - prism.getSumRoundOff()); // select the transitions starting in these tuples JDD.Ref(model.getTrans01()); JDDNode stableTrans01 = JDD.And(model.getTrans01(), mask); diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 1e1547fa..1ac154d8 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -1380,7 +1380,7 @@ public class Modules2MTBDD throw new PrismLangException(s, command); } // check min sums - 1 (ish) for dtmcs/mdps, 0 for ctmcs - if (type != ModulesFile.STOCHASTIC && dmin < 1-prism.getUpdateSumRoundOff()) { + if (type != ModulesFile.STOCHASTIC && dmin < 1-prism.getSumRoundOff()) { JDD.Deref(tmp); String s = "Probabilities in command " + (l+1) + " of module \"" + module.getName() + "\" sum to less than one"; s += " (e.g. " + dmin + ") for some states. "; @@ -1397,7 +1397,7 @@ public class Modules2MTBDD throw new PrismLangException(s, command); } // check max sums - 1 (ish) for dtmcs/mdps, infinity for ctmcs - if (type != ModulesFile.STOCHASTIC && dmax > 1+prism.getUpdateSumRoundOff()) { + if (type != ModulesFile.STOCHASTIC && dmax > 1+prism.getSumRoundOff()) { JDD.Deref(tmp); String s = "Probabilities in command " + (l+1) + " of module \"" + module.getName() + "\" sum to more than one"; s += " (e.g. " + dmax + ") for some states. "; diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index bb2d4b4a..6f894860 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -110,6 +110,10 @@ public class Prism implements PrismSettingsListener // 2 - (s l ... l r c ... r c) (s l ... l r c ... r c) ... private int ordering; + // Round-off threshold for places where doubles are summed and compared to integers + // (e.g. checking that probabilities sum to 1 in an update). + private double sumRoundOff; + //------------------------------------------------------------------------------ // Logs //------------------------------------------------------------------------------ @@ -309,12 +313,6 @@ public class Prism implements PrismSettingsListener settings.set(PrismSettings.PRISM_SCC_METHOD, i-1); // note index offset correction } - public void setUpdateSumRoundOff(double d) throws PrismException - { - settings.set(PrismSettings.PRISM_UPDATE_SUM_ROUND_OFF, d); - } - - // set methods for miscellaneous options public void setDoReach(boolean b) throws PrismException @@ -337,6 +335,11 @@ public class Prism implements PrismSettingsListener ordering = i; } + public void setSumRoundOff(double d) throws PrismException + { + sumRoundOff = d; + } + // get methods public static String getVersion() @@ -414,9 +417,6 @@ public class Prism implements PrismSettingsListener public int getSCCMethod() { return settings.getInteger(PrismSettings.PRISM_SCC_METHOD)+1; } //NOTE THE CORRECTION for the ChoiceSetting index - public double getUpdateSumRoundOff() - { return settings.getDouble(PrismSettings.PRISM_UPDATE_SUM_ROUND_OFF); } - // get methods for miscellaneous options public boolean getDoReach() @@ -431,6 +431,9 @@ public class Prism implements PrismSettingsListener public int getOrdering() { return ordering; } + public double getSumRoundOff() + { return sumRoundOff; } + // get/release (exclusive) access to the prism parser // note: this mutex mechanism is based on public domain code by Doug Lea diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 2c5f97cc..b37586fc 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -89,7 +89,6 @@ public class PrismSettings implements Observer public static final String PRISM_EXTRA_DD_INFO = "prism.extraDDInfo"; public static final String PRISM_EXTRA_REACH_INFO = "prism.extraReachInfo"; public static final String PRISM_SCC_METHOD = "prism.sccMethod"; - public static final String PRISM_UPDATE_SUM_ROUND_OFF = "prism.updateSumRoundOff"; //GUI Model public static final String MODEL_AUTO_PARSE = "model.autoParse"; @@ -186,8 +185,7 @@ public class PrismSettings implements Observer { BOOLEAN_TYPE, PRISM_DO_SS_DETECTION, "Use steady-state detection", "3.0", new Boolean(true), "0,", "Use steady-state detection during CTMC transient probability computation." }, { BOOLEAN_TYPE, PRISM_EXTRA_DD_INFO, "Extra MTBDD information", "3.2", new Boolean(false), "0,", "Display extra information about (MT)BDDs used during and after model construction." }, { BOOLEAN_TYPE, PRISM_EXTRA_REACH_INFO, "Extra reachability information", "3.2", new Boolean(false), "0,", "Display extra information about progress of reachability during model construction." }, - { CHOICE_TYPE, PRISM_SCC_METHOD, "SCC decomposition method", "3.2", "Lockstep", "Xie-Beerel,Lockstep,SCC-Find", "Which algorithm to use for decomposing a graph into strongly connected components (SCCs)." }, - { DOUBLE_TYPE, PRISM_UPDATE_SUM_ROUND_OFF, "Update probability sum round off", "3.2.dev", new Double(10e-6), "0.0,", "Epsilon value used by PRISM for update probabilities that should sum to 1" } + { CHOICE_TYPE, PRISM_SCC_METHOD, "SCC decomposition method", "3.2", "Lockstep", "Xie-Beerel,Lockstep,SCC-Find", "Which algorithm to use for decomposing a graph into strongly connected components (SCCs)." } }, { { BOOLEAN_TYPE, MODEL_AUTO_PARSE, "Auto parse", "3.0", new Boolean(true), "", "Parse PRISM models automatically as they are loaded/edited in the text editor." },