Code tweaks: make Updater independent of PRISM/sim + make SimEngine into PrismComponent.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7639 bbc10eb1-c90d-0410-af57-cb519fbb1720

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;
 	}

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;
  * <LI> {@link #modelCheckExperiment}
  * </UL>
  */
-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;

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;