New PrismComponent class: refactoring for various model checking components.

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

prism/src/explicit/CTMCModelChecker.java

@@ -43,6 +43,14 @@ import prism.*;
  */
 public class CTMCModelChecker extends DTMCModelChecker
 {
+	/**
+	 * Create a new CTMCModelChecker, inherit basic state from parent (unless null).
+	 */
+	public CTMCModelChecker(PrismComponent parent) throws PrismException
+	{
+		super(parent);
+	}
+	
 	// Model checking functions
 
 	/**
@@ -742,7 +750,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 		BitSet target;
 		Map<String, BitSet> labels;
 		try {
-			mc = new CTMCModelChecker();
+			mc = new CTMCModelChecker(null);
 			ctmc = new CTMCSimple();
 			ctmc.buildFromPrismExplicit(args[0]);
 			//System.out.println(dtmc);

prism/src/explicit/CTMDPModelChecker.java

@@ -30,6 +30,7 @@ import java.util.BitSet;
 import java.util.Map;
 
 import parser.ast.ExpressionTemporal;
+import prism.PrismComponent;
 import prism.PrismException;
 
 /**
@@ -40,6 +41,16 @@ import prism.PrismException;
  */
 public class CTMDPModelChecker extends MDPModelChecker
 {
+	/**
+	 * Create a new CTMDPModelChecker, inherit basic state from parent (unless null).
+	 */
+	public CTMDPModelChecker(PrismComponent parent) throws PrismException
+	{
+		super(parent);
+	}
+	
+	// Model checking functions
+
 	protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, boolean min) throws PrismException
 	{
 		double uTime;
@@ -115,7 +126,7 @@ public class CTMDPModelChecker extends MDPModelChecker
 		mainLog.println("q = " + q + ", k = " + k + ", tau = " + tau);
 		mdp = ctmdp.buildDiscretisedMDP(tau);
 		mainLog.println(mdp);
-		mc = new MDPModelChecker();
+		mc = new MDPModelChecker(null);
 		mc.inheritSettings(this);
 		res = mc.computeBoundedUntilProbs(mdp, null, target, k, min);
 
@@ -243,7 +254,7 @@ public class CTMDPModelChecker extends MDPModelChecker
 		Map<String, BitSet> labels;
 		boolean min = true;
 		try {
-			mc = new CTMDPModelChecker();
+			mc = new CTMDPModelChecker(null);
 			ctmdp = new CTMDPSimple();
 			ctmdp.buildFromPrismExplicit(args[0]);
 			System.out.println(ctmdp);

prism/src/explicit/DTMCModelChecker.java

@@ -40,6 +40,7 @@ import parser.type.TypeDouble;
 import parser.visitor.ASTTraverse;
 import prism.DRA;
 import prism.Pair;
+import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismLangException;
 import prism.PrismUtils;
@@ -50,6 +51,14 @@ import explicit.rewards.MCRewards;
  */
 public class DTMCModelChecker extends ProbModelChecker
 {
+	/**
+	 * Create a new DTMCModelChecker, inherit basic state from parent (unless null).
+	 */
+	public DTMCModelChecker(PrismComponent parent) throws PrismException
+	{
+		super(parent);
+	}
+	
 	// Model checking functions
 
 	/**
@@ -253,7 +262,7 @@ public class DTMCModelChecker extends ProbModelChecker
 		mainLog.println("\nFinding accepting BSCCs...");
 		BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCs(dra, modelProduct, invMap, sccMethod);
 		mainLog.println("\nComputing reachability probabilities...");
-		mcProduct = new DTMCModelChecker();
+		mcProduct = new DTMCModelChecker(this);
 		probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acceptingBSCCs).soln, modelProduct);
 
 		// Mapping probabilities in the original model
@@ -1619,7 +1628,7 @@ public class DTMCModelChecker extends ProbModelChecker
 
 				// 1. Read in from .tra and .lab files
 				//    Run as: PRISM_MAINCLASS=explicit.DTMCModelChecker bin/prism dtmc.tra dtmc.lab target_label
-				mc = new DTMCModelChecker();
+				mc = new DTMCModelChecker(null);
 				dtmc = new DTMCSimple();
 				dtmc.buildFromPrismExplicit(args[0]);
 				//System.out.println(dtmc);
@@ -1640,7 +1649,7 @@ public class DTMCModelChecker extends ProbModelChecker
 				// 2. Build DTMC directly
 				//    Run as: PRISM_MAINCLASS=explicit.DTMCModelChecker bin/prism
 				//    (example taken from p.14 of Lec 5 of http://www.prismmodelchecker.org/lectures/pmc/) 
-				mc = new DTMCModelChecker();
+				mc = new DTMCModelChecker(null);
 				dtmc = new DTMCSimple(6);
 				dtmc.setProbability(0, 1, 0.1);
 				dtmc.setProbability(0, 2, 0.9);

prism/src/explicit/MDPModelChecker.java

@@ -34,6 +34,7 @@ import java.util.Map;
 import parser.ast.Expression;
 import parser.ast.ExpressionTemporal;
 import parser.ast.ExpressionUnaryOp;
+import prism.PrismComponent;
 import prism.PrismDevNullLog;
 import prism.PrismException;
 import prism.PrismFileLog;
@@ -47,6 +48,14 @@ import explicit.rewards.MDPRewards;
  */
 public class MDPModelChecker extends ProbModelChecker
 {
+	/**
+	 * Create a new MDPModelChecker, inherit basic state from parent (unless null).
+	 */
+	public MDPModelChecker(PrismComponent parent) throws PrismException
+	{
+		super(parent);
+	}
+	
 	// Model checking functions
 
 	/**
@@ -858,7 +867,7 @@ public class MDPModelChecker extends ProbModelChecker
 		mainLog.println("Starting policy iteration (" + (min ? "min" : "max") + ")...");
 
 		// Create a DTMC model checker (for solving policies)
-		mcDTMC = new DTMCModelChecker();
+		mcDTMC = new DTMCModelChecker(this);
 		mcDTMC.inheritSettings(this);
 		mcDTMC.setLog(new PrismDevNullLog());
 
@@ -952,7 +961,7 @@ public class MDPModelChecker extends ProbModelChecker
 		mainLog.println("Starting modified policy iteration (" + (min ? "min" : "max") + ")...");
 
 		// Create a DTMC model checker (for solving policies)
-		mcDTMC = new DTMCModelChecker();
+		mcDTMC = new DTMCModelChecker(this);
 		mcDTMC.inheritSettings(this);
 		mcDTMC.setLog(new PrismDevNullLog());
 
@@ -1552,7 +1561,7 @@ public class MDPModelChecker extends ProbModelChecker
 		Map<String, BitSet> labels;
 		boolean min = true;
 		try {
-			mc = new MDPModelChecker();
+			mc = new MDPModelChecker(null);
 			mdp = new MDPSimple();
 			mdp.buildFromPrismExplicit(args[0]);
 			//System.out.println(mdp);

prism/src/explicit/PrismExplicit.java

@@ -40,12 +40,8 @@ import explicit.StateModelChecker;
  * The intention is to minimise dependencies on the Prism class by anything in this package.
  * This makes these classes easier to use independently.
  */
-public class PrismExplicit
+public class PrismExplicit extends PrismComponent
 {
-	// Parent Prism object
-	private PrismLog mainLog = null;
-	private PrismSettings settings = null;
-
 	public PrismExplicit(PrismLog mainLog, PrismSettings settings)
 	{
 		this.mainLog = mainLog;
@@ -205,25 +201,23 @@ public class PrismExplicit
 		expr.checkValid(model.getModelType());
 		switch (model.getModelType()) {
 		case DTMC:
-			mc = new DTMCModelChecker();
+			mc = new DTMCModelChecker(this);
 			break;
 		case MDP:
-			mc = new MDPModelChecker();
+			mc = new MDPModelChecker(this);
 			break;
 		case CTMC:
-			mc = new CTMCModelChecker();
+			mc = new CTMCModelChecker(this);
 			break;
 		case CTMDP:
-			mc = new CTMDPModelChecker();
+			mc = new CTMDPModelChecker(this);
 			break;
 		case STPG:
-			mc = new STPGModelChecker();
+			mc = new STPGModelChecker(this);
 			break;
 		default:
 			throw new PrismException("Unknown model type " + model.getModelType());
 		}
-		mc.setLog(mainLog);
-		mc.setSettings(settings);
 
 		// Do model checking
 		mc.setModulesFileAndPropertiesFile(modulesFile, propertiesFile);
@@ -265,9 +259,7 @@ public class PrismExplicit
 		l = System.currentTimeMillis();
 
 		if (model.getModelType() == ModelType.DTMC) {
-			DTMCModelChecker mcDTMC = new DTMCModelChecker();
-			mcDTMC.setLog(mainLog);
-			mcDTMC.setSettings(settings);
+			DTMCModelChecker mcDTMC = new DTMCModelChecker(this);
 			probs = mcDTMC.doSteadyState((DTMC) model);
 		}
 		else if (model.getModelType() == ModelType.CTMC) {
@@ -343,9 +335,7 @@ public class PrismExplicit
 		}
 		else if (model.getModelType() == ModelType.CTMC) {
 			mainLog.println("\nComputing transient probabilities (time = " + time + ")...");
-			CTMCModelChecker mcCTMC = new CTMCModelChecker();
-			mcCTMC.setLog(mainLog);
-			mcCTMC.setSettings(settings);
+			CTMCModelChecker mcCTMC = new CTMCModelChecker(this);
 			probs = mcCTMC.doTransient((CTMC) model, time, fileIn);
 		}
 		else {

prism/src/explicit/PrismSTPGAbstractRefine.java

@@ -106,7 +106,7 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 		}
 
 		// Get initial/target (concrete) states
-		labels = new StateModelChecker().loadLabelsFile(labFile);
+		labels = new StateModelChecker(null).loadLabelsFile(labFile);
 		initialConcrete = labels.get("init");
 		targetConcrete = labels.get(targetLabel);
 		if (targetConcrete == null)
@@ -361,7 +361,7 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 		ModelCheckerResult res = null;
 		switch (modelType) {
 		case DTMC:
-			DTMCModelChecker mcDtmc = new DTMCModelChecker();
+			DTMCModelChecker mcDtmc = new DTMCModelChecker(null);
 			mcDtmc.inheritSettings(mcOptions);
 			switch (propertyType) {
 			case PROB_REACH:
@@ -375,7 +375,7 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 			}
 			break;
 		case CTMC:
-			CTMCModelChecker mcCtmc = new CTMCModelChecker();
+			CTMCModelChecker mcCtmc = new CTMCModelChecker(null);
 			mcCtmc.inheritSettings(mcOptions);
 			switch (propertyType) {
 			/*case PROB_REACH:
@@ -389,7 +389,7 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 			}
 			break;
 		case MDP:
-			MDPModelChecker mcMdp = new MDPModelChecker();
+			MDPModelChecker mcMdp = new MDPModelChecker(null);
 			mcMdp.inheritSettings(mcOptions);
 			switch (propertyType) {
 			case PROB_REACH:

prism/src/explicit/ProbModelChecker.java

@@ -34,6 +34,7 @@ import parser.ast.ExpressionReward;
 import parser.ast.ExpressionSS;
 import parser.ast.RewardStruct;
 import prism.ModelType;
+import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismSettings;
 import explicit.rewards.ConstructRewards;
@@ -135,6 +136,14 @@ public class ProbModelChecker extends StateModelChecker
 		VALUE_ITERATION, GAUSS_SEIDEL, POLICY_ITERATION, MODIFIED_POLICY_ITERATION, LINEAR_PROGRAMMING
 	};
 
+	/**
+	 * Create a new ProbModelChecker, inherit basic state from parent (unless null).
+	 */
+	public ProbModelChecker(PrismComponent parent) throws PrismException
+	{
+		super(parent);
+	}
+	
 	// Settings methods
 
 	/**

prism/src/explicit/QuantAbstractRefine.java

@@ -152,7 +152,11 @@ public abstract class QuantAbstractRefine
 		// By default, log output goes to System.out.
 		setLog(new PrismPrintStreamLog(System.out));
 		// Create dummy model checker to store options
-		mcOptions = new ProbModelChecker();
+		try {
+			mcOptions = new ProbModelChecker(null);
+		} catch (PrismException e) {
+			// Won't happen
+		}
 	}
 
 	/**
@@ -467,15 +471,15 @@ public abstract class QuantAbstractRefine
 		switch (modelType) {
 		case DTMC:
 			abstractionType = ModelType.MDP;
-			mc = new MDPModelChecker();
+			mc = new MDPModelChecker(null);
 			break;
 		case CTMC:
 			abstractionType = ModelType.CTMDP;
-			mc = new CTMDPModelChecker();
+			mc = new CTMDPModelChecker(null);
 			break;
 		case MDP:
 			abstractionType = ModelType.STPG;
-			mc = new STPGModelChecker();
+			mc = new STPGModelChecker(null);
 			break;
 		default:
 			throw new PrismException("Cannot handle model type " + modelType);

prism/src/explicit/STPGAbstrSimple.java

@@ -1138,7 +1138,7 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS
 			System.out.println(stpg);
 
 			// Model check
-			mc = new STPGModelChecker();
+			mc = new STPGModelChecker(null);
 			//mc.setVerbosity(2);
 			target = new BitSet();
 			target.set(3);

prism/src/explicit/STPGModelChecker.java

@@ -34,6 +34,7 @@ import java.util.Map;
 import parser.ast.Expression;
 import parser.ast.ExpressionTemporal;
 import parser.ast.ExpressionUnaryOp;
+import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismFileLog;
 import prism.PrismLog;
@@ -45,6 +46,14 @@ import explicit.rewards.STPGRewards;
  */
 public class STPGModelChecker extends ProbModelChecker
 {
+	/**
+	 * Create a new STPGModelChecker, inherit basic state from parent (unless null).
+	 */
+	public STPGModelChecker(PrismComponent parent) throws PrismException
+	{
+		super(parent);
+	}
+	
 	// Model checking functions
 
 	/**
@@ -1060,7 +1069,7 @@ public class STPGModelChecker extends ProbModelChecker
 		Map<String, BitSet> labels;
 		boolean min1 = true, min2 = true;
 		try {
-			mc = new STPGModelChecker();
+			mc = new STPGModelChecker(null);
 			stpg = new STPGAbstrSimple();
 			stpg.buildFromPrismExplicit(args[0]);
 			//System.out.println(stpg);

prism/src/explicit/StateModelChecker.java

@@ -63,27 +63,23 @@ import parser.type.TypeDouble;
 import parser.type.TypeInt;
 import prism.Filter;
 import prism.ModelType;
+import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismLangException;
-import prism.PrismLog;
-import prism.PrismPrintStreamLog;
 import prism.PrismSettings;
 import prism.Result;
 
 /**
  * Super class for explicit-state model checkers
  */
-public class StateModelChecker
+public class StateModelChecker extends PrismComponent
 {
-	// Log for output (default to System.out)
-	protected PrismLog mainLog = new PrismPrintStreamLog(System.out);
-
-	// PRISM settings object
-	//protected PrismSettings settings = new PrismSettings();
-
-	// Flags/settings
+	// Flags/settings that can be extracted from PrismSettings
 	// (NB: defaults do not necessarily coincide with PRISM)
 
+	// Verbosity level
+	protected int verbosity = 0;
+	
 	// Method used for numerical solution
 	protected SCCMethod sccMethod = SCCMethod.TARJAN;
 
@@ -92,6 +88,7 @@ public class StateModelChecker
 	// Generate/store a strategy during model checking?
 	protected boolean genStrat = false;
 	
+	
 	// Model file (for reward structures, etc.)
 	protected ModulesFile modulesFile = null;
 
@@ -107,27 +104,43 @@ public class StateModelChecker
 	// The result of model checking will be stored here
 	protected Result result;
 
+	/**
+	 * Create a new StateModelChecker, inherit basic state from parent (unless null).
+	 */
+	public StateModelChecker(PrismComponent parent) throws PrismException
+	{
+		super(parent);
+	}
+	
 	/**
 	 * Create a model checker (a subclass of this one) for a given model type
 	 */
 	public static StateModelChecker createModelChecker(ModelType modelType) throws PrismException
+	{
+		return createModelChecker(modelType, null);
+	}
+	
+	/**
+	 * Create a model checker (a subclass of this one) for a given model type
+	 */
+	public static StateModelChecker createModelChecker(ModelType modelType, PrismComponent parent) throws PrismException
 	{
 		explicit.StateModelChecker mc = null;
 		switch (modelType) {
 		case DTMC:
-			mc = new DTMCModelChecker();
+			mc = new DTMCModelChecker(parent);
 			break;
 		case MDP:
-			mc = new MDPModelChecker();
+			mc = new MDPModelChecker(parent);
 			break;
 		case CTMC:
-			mc = new CTMCModelChecker();
+			mc = new CTMCModelChecker(parent);
 			break;
 		case CTMDP:
-			mc = new CTMDPModelChecker();
+			mc = new CTMDPModelChecker(parent);
 			break;
 		case STPG:
-			mc = new STPGModelChecker();
+			mc = new STPGModelChecker(parent);
 			break;
 		default:
 			throw new PrismException("Cannot create model checker for model type " + modelType);
@@ -135,44 +148,6 @@ public class StateModelChecker
 		return mc;
 	}
 
-	// Flags/settings
-
-	// Verbosity level
-	protected int verbosity = 0;
-
-	// Setters/getters
-
-	/**
-	 * Set log for output.
-	 */
-	public void setLog(PrismLog log)
-	{
-		this.mainLog = log;
-	}
-
-	/**
-	 * Get log for output.
-	 */
-	public PrismLog getLog()
-	{
-		return mainLog;
-	}
-
-	/**
-	 * Set the attached model file (for e.g. reward structures when model checking)
-	 * and the attached properties file (for e.g. constants/labels when model checking)
-	 */
-	public void setModulesFileAndPropertiesFile(ModulesFile modulesFile, PropertiesFile propertiesFile)
-	{
-		this.modulesFile = modulesFile;
-		this.propertiesFile = propertiesFile;
-		// Get combined constant values from model/properties
-		constantValues = new Values();
-		constantValues.addValues(modulesFile.getConstantValues());
-		if (propertiesFile != null)
-			constantValues.addValues(propertiesFile.getConstantValues());
-	}
-
 	// Settings methods
 
 	/**
@@ -180,6 +155,8 @@ public class StateModelChecker
 	 */
 	public void setSettings(PrismSettings settings) throws PrismException
 	{
+		super.setSettings(settings);
+		
 		if (settings == null)
 			return;
 
@@ -236,6 +213,23 @@ public class StateModelChecker
 		return genStrat;
 	}
 
+	// Other setters/getters
+
+	/**
+	 * Set the attached model file (for e.g. reward structures when model checking)
+	 * and the attached properties file (for e.g. constants/labels when model checking)
+	 */
+	public void setModulesFileAndPropertiesFile(ModulesFile modulesFile, PropertiesFile propertiesFile)
+	{
+		this.modulesFile = modulesFile;
+		this.propertiesFile = propertiesFile;
+		// Get combined constant values from model/properties
+		constantValues = new Values();
+		constantValues.addValues(modulesFile.getConstantValues());
+		if (propertiesFile != null)
+			constantValues.addValues(propertiesFile.getConstantValues());
+	}
+
 	// Model checking functions
 
 	/**

prism/src/prism/Prism.java

@@ -36,7 +36,6 @@ import java.io.FileWriter;
 import java.io.IOException;
 import java.util.ArrayList;
 import java.util.List;
-import java.util.Vector;
 
 import jdd.JDD;
 import jdd.JDDNode;
@@ -57,7 +56,6 @@ import parser.ast.LabelList;
 import parser.ast.ModulesFile;
 import parser.ast.PropertiesFile;
 import parser.ast.Property;
-import parser.type.TypeBool;
 import pta.DigitalClocks;
 import pta.PTAModelChecker;
 import simulator.GenerateSimulationPath;
@@ -79,7 +77,7 @@ import explicit.FastAdaptiveUniformisationModelChecker;
  * Main class for all PRISM's core functionality.
  * This is independent of the user interface (command line or gui).
  */
-public class Prism implements PrismSettingsListener
+public class Prism extends PrismComponent implements PrismSettingsListener
 {
 	/** PRISM version (e.g. "4.0.3"). Read from prism.Version. */
 	private static String version = prism.Version.versionString;
@@ -159,9 +157,6 @@ public class Prism implements PrismSettingsListener
 	// Settings / flags / options
 	//------------------------------------------------------------------------------
 
-	// Main PRISM settings
-	private PrismSettings settings;
-
 	// Export parsed PRISM model?
 	protected boolean exportPrism = false;
 	protected File exportPrismFile = null;
@@ -210,8 +205,7 @@ public class Prism implements PrismSettingsListener
 	// Logs
 	//------------------------------------------------------------------------------
 
-	private PrismLog mainLog; // one log for most output
-	private PrismLog techLog; // another one for technical/diagnostic output
+	private PrismLog techLog; // log for technical/diagnostic output
 
 	//------------------------------------------------------------------------------
 	// Parsers/translators/model checkers/simulators/etc.
@@ -975,7 +969,7 @@ public class Prism implements PrismSettingsListener
 	 * Get an SCCComputer object.
 	 * Type (i.e. algorithm) depends on SCCMethod PRISM option.
 	 */
-	public SCCComputer getSCCComputer(Model model)
+	public SCCComputer getSCCComputer(Model model) throws PrismException
 	{
 		return getSCCComputer(model.getReach(), model.getTrans01(), model.getAllDDRowVars(), model.getAllDDColVars());
 	}
@@ -984,7 +978,7 @@ public class Prism implements PrismSettingsListener
 	 * Get an SCCComputer object.
 	 * Type (i.e. algorithm) depends on SCCMethod PRISM option.
 	 */
-	public SCCComputer getSCCComputer(JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars)
+	public SCCComputer getSCCComputer(JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) throws PrismException
 	{
 		SCCComputer sccComputer;
 		switch (getSCCMethod()) {
@@ -2900,9 +2894,7 @@ public class Prism implements PrismSettingsListener
 			}
 		} else {
 			if (currentModelExpl.getModelType() == ModelType.DTMC) {
-				DTMCModelChecker mcDTMC = new DTMCModelChecker();
-				mcDTMC.setLog(mainLog);
-				mcDTMC.setSettings(settings);
+				DTMCModelChecker mcDTMC = new DTMCModelChecker(this);
 				probsExpl = mcDTMC.doSteadyState((DTMC) currentModelExpl, (File) null);
 				//TODO: probsExpl = mcDTMC.doSteadyState((DTMC) currentModelExpl, fileIn);
 			} else if (currentModelType == ModelType.CTMC) {
@@ -3013,9 +3005,7 @@ public class Prism implements PrismSettingsListener
 			if (currentModelType == ModelType.DTMC) {
 				throw new PrismException("Not implemented yet");
 			} else if (currentModelType == ModelType.CTMC) {
-				CTMCModelChecker mcCTMC = new CTMCModelChecker();
-				mcCTMC.setLog(mainLog);
-				mcCTMC.setSettings(settings);
+				CTMCModelChecker mcCTMC = new CTMCModelChecker(this);
 				probsExpl = mcCTMC.doTransient((CTMC) currentModelExpl, time, fileIn);
 			} else {
 				throw new PrismException("Transient probabilities only computed for DTMCs/CTMCs");
@@ -3121,9 +3111,7 @@ public class Prism implements PrismSettingsListener
 				}
 			} else {
 				if (currentModelType.continuousTime()) {
-					CTMCModelChecker mc = new CTMCModelChecker();
-					mc.setLog(mainLog);
-					mc.setSettings(settings);
+					CTMCModelChecker mc = new CTMCModelChecker(this);
 					if (i == 0) {
 						initDistExpl = mc.readDistributionFromFile(fileIn, currentModelExpl);
 						initTimeDouble = 0;
@@ -3271,9 +3259,7 @@ public class Prism implements PrismSettingsListener
 	private explicit.StateModelChecker createModelCheckerExplicit(PropertiesFile propertiesFile) throws PrismException
 	{
 		// Create model checker
-		explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(currentModelType);
-		mc.setLog(mainLog);
-		mc.setSettings(settings);
+		explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(currentModelType, this);
 		mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile);
 		// Pass any additional local settings
 		mc.setGenStrat(genStrat);

prism/src/prism/PrismComponent.java

@@ -0,0 +1,117 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package prism;
+
+/**
+ * Base class for "components" of PRISM, i.e. classes that implement
+ * a particular piece of functionality required for model checking.
+ * Stores:
+ * <ul>
+ * <li> A PrismLog ({@code mainLog}) for output 
+ * <li> A PrismSettings object ({@code settings})
+ * </ul>
+ * These are usually freshly created to perform some task and then discarded.
+ * In particular, settings are usually extracted from a PrismSettings object
+ * upon creation, which is stored (to pass on to child PrismComponent objects)
+ * but is not then monitored to detect when changes are made to settings later. 
+ */
+public class PrismComponent
+{
+	/**
+	 * Log for output.
+	 * Defaults to System.out, so that is always available.
+	 */
+	protected PrismLog mainLog = new PrismPrintStreamLog(System.out);
+
+	/**
+	 * PRISM settings object.
+	 * Defaults to a fresh PrismSettings() object containing PRISM defaults.
+	 * 
+	 * The idea is that settings are not extracted into local storage of
+	 * Used (optionally) to initialise settings.
+	 * Retained to allow it to be passed on to child PrismComponent objects.
+	 * It is not monitored to detect when changes are made to settings later.
+	 */
+	protected PrismSettings settings = new PrismSettings();
+
+	// Constructors
+	
+	/**
+	 * Default constructor.
+	 */
+	public PrismComponent()
+	{
+	}
+
+	/**
+	 * Create a PrismComponent object, inheriting state from another ("parent") PrismComponent.
+	 */
+	public PrismComponent(PrismComponent parent) throws PrismException
+	{
+		if (parent == null)
+			return;
+		
+		setLog(parent.getLog());
+		setSettings(parent.getSettings());
+	}
+	
+	// Log
+	
+	/**
+	 * Set log ("mainLog") for output.
+	 */
+	public void setLog(PrismLog log)
+	{
+		this.mainLog = log;
+	}
+
+	/**
+	 * Get log ("mainLog") for output.
+	 */
+	public PrismLog getLog()
+	{
+		return mainLog;
+	}
+
+	// Settings
+	
+	/**
+	 * Set settings from a PRISMSettings object.
+	 */
+	public void setSettings(PrismSettings settings) throws PrismException
+	{
+		this.settings = settings;
+	}
+	
+	/**
+	 * Get the locally stored PRISMSettings object.
+	 */
+	public PrismSettings getSettings()
+	{
+		return settings;
+	}
+}

prism/src/prism/SCCComputer.java

@@ -35,9 +35,8 @@ import jdd.*;
  * Abstract class for classes that compute (B)SCCs,
  * i.e. (bottom) strongly connected components, for a model's transition graph.
  */
-public abstract class SCCComputer
+public abstract class SCCComputer extends PrismComponent
 {
-	protected Prism prism;
 	protected PrismLog mainLog;
 
 	// model info
@@ -56,10 +55,9 @@ public abstract class SCCComputer
 	// Get methods
 	
 	// Constructor
-	public SCCComputer(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars)
+	public SCCComputer(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) throws PrismException
 	{
-		this.prism = prism;
-		mainLog = prism.getMainLog();
+		super(prism);
 		this.trans01 = trans01;
 		this.reach = reach;
 		this.allDDRowVars = allDDRowVars;

prism/src/prism/SCCComputerLockstep.java

@@ -51,7 +51,7 @@ public class SCCComputerLockstep extends SCCComputer
 	
 	// Constructor
 	
-	public SCCComputerLockstep(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars)
+	public SCCComputerLockstep(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) throws PrismException
 	{
 		super(prism, reach, trans01, allDDRowVars, allDDColVars);
 	}

prism/src/prism/SCCComputerSCCFind.java

@@ -52,7 +52,7 @@ public class SCCComputerSCCFind extends SCCComputer
 	
 	// Constructor
 	
-	public SCCComputerSCCFind(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars)
+	public SCCComputerSCCFind(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) throws PrismException
 	{
 		super(prism, reach, trans01, allDDRowVars, allDDColVars);
 	}
@@ -147,7 +147,7 @@ public class SCCComputerSCCFind extends SCCComputer
 			JDD.Ref(edges);
 			pre = preimage(current, edges);
 			current = JDD.And(current, JDD.And(img, pre));
-			if (prism.getVerbose()) {
+			if (settings.getBoolean(PrismSettings.PRISM_VERBOSE)) {
 				mainLog.println("Trimming pass " + i + ":");
 				JDD.PrintVector(current, allDDRowVars);
 				i++;

prism/src/prism/SCCComputerXB.java

@@ -37,7 +37,7 @@ public class SCCComputerXB extends SCCComputer
 {
 	// Constructor
 	
-	public SCCComputerXB(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars)
+	public SCCComputerXB(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) throws PrismException
 	{
 		super(prism, reach, trans01, allDDRowVars, allDDColVars);
 	}

prism/src/pta/PTAModelCheckerCL.java

@@ -180,7 +180,7 @@ public class PTAModelCheckerCL
 				ForwardsReach forwardsReach = new ForwardsReach();
 				ReachabilityGraph graph = forwardsReach.buildForwardsGraph(pta, targetLocs, targetConstraint);
 				MDP mdp = graph.buildMDP(forwardsReach.getInitialStates());
-				new MDPModelChecker().computeReachProbs(mdp, forwardsReach.getTarget(), min);
+				new MDPModelChecker(null).computeReachProbs(mdp, forwardsReach.getTarget(), min);
 			}
 
 		} catch (PrismException e) {