diff --git a/prism/src/prism/PrismComponent.java b/prism/src/prism/PrismComponent.java index 3578ffb8..38304249 100644 --- a/prism/src/prism/PrismComponent.java +++ b/prism/src/prism/PrismComponent.java @@ -70,7 +70,7 @@ public class PrismComponent /** * Create a PrismComponent object, inheriting state from another ("parent") PrismComponent. */ - public PrismComponent(PrismComponent parent) throws PrismException + public PrismComponent(PrismComponent parent) { if (parent == null) return; @@ -91,7 +91,7 @@ public class PrismComponent /** * Set PRISMSettings object. */ - public final void setSettings(PrismSettings settings) throws PrismException + public final void setSettings(PrismSettings settings) { this.settings = settings; } diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 6d8afbb9..0b27372b 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -43,11 +43,12 @@ import parser.ast.ModulesFile; import parser.ast.PropertiesFile; import parser.type.Type; import prism.ModelType; -import prism.Prism; +import prism.PrismComponent; import prism.PrismException; import prism.PrismFileLog; import prism.PrismLangException; import prism.PrismLog; +import prism.PrismSettings; import prism.PrismUtils; import prism.ResultsCollection; import prism.UndefinedConstants; @@ -94,12 +95,8 @@ import userinterface.graph.Graph; *
  • {@link #modelCheckExperiment} * */ -public class SimulatorEngine +public class SimulatorEngine extends PrismComponent { - // PRISM stuff - protected Prism prism; - protected PrismLog mainLog; - // The current parsed model + info private ModulesFile modulesFile; private ModelType modelType; @@ -150,10 +147,9 @@ public class SimulatorEngine /** * Constructor for the simulator engine. */ - public SimulatorEngine(Prism prism) + public SimulatorEngine(PrismComponent parent) { - this.prism = prism; - setMainLog(prism.getMainLog()); + super(parent); modulesFile = null; modelType = null; varList = null; @@ -174,22 +170,6 @@ public class SimulatorEngine rng = new RandomNumberGenerator(); } - /** - * Set the log to which any output is sent. - */ - public void setMainLog(PrismLog log) - { - mainLog = log; - } - - /** - * Get access to the parent Prism object - */ - public Prism getPrism() - { - return prism; - } - // ------------------------------------------------------------------------------ // Path creation and modification // ------------------------------------------------------------------------------ @@ -728,7 +708,8 @@ public class SimulatorEngine transitionList = new TransitionList(); // Create updater for model - updater = new Updater(this, modulesFile, varList); + updater = new Updater(modulesFile, varList); + updater.setSumRoundOff(settings.getDouble(PrismSettings.PRISM_SUM_ROUND_OFF)); // Clear storage for strategy strategy = null; diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index 54b833f2..16c3ba50 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -34,10 +34,10 @@ import prism.*; public class Updater { - // Parent simulator/prism - protected SimulatorEngine simulator; - protected Prism prism; - + // Settings: + // The precision to which we check probabilities sum to 1 + protected double sumRoundOff = 1e-5; + // Model to which the path corresponds protected ModulesFile modulesFile; protected ModelType modelType; @@ -62,14 +62,12 @@ public class Updater // (where j=0 denotes independent, otherwise 1-indexed action label) protected BitSet enabledModules[]; - public Updater(SimulatorEngine simulator, ModulesFile modulesFile, VarList varList) + public Updater(ModulesFile modulesFile, VarList varList) { int i, j; String s; // Get info from simulator/model - this.simulator = simulator; - prism = simulator.getPrism(); this.modulesFile = modulesFile; modelType = modulesFile.getModelType(); numModules = modulesFile.getNumModules(); @@ -104,6 +102,22 @@ public class Updater } } + /** + * Set the precision to which we check that probabilities sum to 1. + */ + public void setSumRoundOff(double sumRoundOff) + { + this.sumRoundOff = sumRoundOff; + } + + /** + * Get the precision to which we check that probabilities sum to 1. + */ + public double getSumRoundOff() + { + return sumRoundOff; + } + /** * Determine the set of outgoing transitions from state 'state' and store in 'transitionList'. * @param state State from which to explore @@ -334,7 +348,7 @@ public class Updater throw new PrismLangException(msg, ups); } // Check distribution sums to 1 (if required, and if is non-empty) - if (ch.size() > 0 && modelType.choicesSumToOne() && Math.abs(sum - 1) > prism.getSumRoundOff()) { + if (ch.size() > 0 && modelType.choicesSumToOne() && Math.abs(sum - 1) > sumRoundOff) { throw new PrismLangException("Probabilities sum to " + sum + " in state " + state.toString(modulesFile), ups); } return ch;