Minor code refactoring.

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

prism/src/explicit/FastAdaptiveUniformisationModelChecker.java

@@ -32,29 +32,27 @@ import parser.ast.Expression;
 import parser.ast.ExpressionProb;
 import parser.ast.ExpressionReward;
 import parser.ast.ExpressionTemporal;
+import parser.ast.LabelList;
 import parser.ast.ModulesFile;
 import parser.ast.PropertiesFile;
-import parser.ast.LabelList;
-import prism.Prism;
+import parser.ast.RewardStruct;
+import prism.PrismComponent;
 import prism.PrismException;
-import prism.PrismLog;
 import prism.Result;
 import simulator.PrismModelExplorer;
-import parser.ast.RewardStruct;
+import simulator.SimulatorEngine;
 
 /**
  * CTMC model checker based on fast adaptive uniformisation.
  */
-public class FastAdaptiveUniformisationModelChecker
+public class FastAdaptiveUniformisationModelChecker extends PrismComponent
 {
-	// Prism object
-	private Prism prism;
-	// Log
-	private PrismLog mainLog;
 	// Model file
 	private ModulesFile modulesFile;
 	// Properties file
 	private PropertiesFile propertiesFile;
+	// Simulator engine
+	private SimulatorEngine engine;
 	// Constants from model
 	private Values constantValues;
 	// Labels from the model
@@ -65,12 +63,12 @@ public class FastAdaptiveUniformisationModelChecker
 	/**
 	 * Constructor.
 	 */
-	public FastAdaptiveUniformisationModelChecker(Prism prism, ModulesFile modulesFile, PropertiesFile propertiesFile) throws PrismException
+	public FastAdaptiveUniformisationModelChecker(PrismComponent parent, ModulesFile modulesFile, PropertiesFile propertiesFile, SimulatorEngine engine) throws PrismException
 	{
-		this.prism = prism;
-		mainLog = prism.getMainLog();
+		super(parent);
 		this.modulesFile = modulesFile;
 		this.propertiesFile = propertiesFile;
+		this.engine = engine;
 
 		// Get combined constant values from model/properties
 		constantValues = new Values();
@@ -161,8 +159,8 @@ public class FastAdaptiveUniformisationModelChecker
 		}
 
 		mainLog.println("Starting transient probability computation using fast adaptive uniformisation...");
-		PrismModelExplorer modelExplorer = new PrismModelExplorer(prism.getSimulator(), modulesFile);
-		FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(prism.getSettings(), modelExplorer);
+		PrismModelExplorer modelExplorer = new PrismModelExplorer(engine, modulesFile);
+		FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer);
 		fau.setConstantValues(constantValues);
 
 		Expression op1 = exprTemp.getOperand1();
@@ -250,8 +248,8 @@ public class FastAdaptiveUniformisationModelChecker
 	private Result checkExpressionReward(ExpressionReward expr) throws PrismException
 	{
 		mainLog.println("Starting transient probability computation using fast adaptive uniformisation...");
-		PrismModelExplorer modelExplorer = new PrismModelExplorer(prism.getSimulator(), modulesFile);
-		FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(prism.getSettings(), modelExplorer);
+		PrismModelExplorer modelExplorer = new PrismModelExplorer(engine, modulesFile);
+		FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer);
 		ExpressionTemporal temporal = (ExpressionTemporal) expr.getExpression();
 		switch (temporal.getOperator()) {
 		case ExpressionTemporal.R_I:

prism/src/prism/Prism.java

@@ -2649,7 +2649,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		// For fast adaptive uniformisation
 		if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) {
 			FastAdaptiveUniformisationModelChecker fauMC;
-			fauMC = new FastAdaptiveUniformisationModelChecker(this, currentModulesFile, propertiesFile);
+			fauMC = new FastAdaptiveUniformisationModelChecker(this, currentModulesFile, propertiesFile, getSimulator());
 			return fauMC.check(prop.getExpression());
 		}
 		// Auto-switch engine if required