Convert a few more classes to PrismComponents.

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

prism/src/pta/Modules2PTA.java

@@ -40,12 +40,11 @@ import prism.*;
  * Class that converts a PRISM modelling language description
  * of a PTA into data structures in the pta package.
  */
-public class Modules2PTA
+public class Modules2PTA extends PrismComponent
 {
-	// Prism object
-	private Prism prism;
-	// Log
-	private PrismLog mainLog;
+	// Setting(s)
+	protected double sumRoundOff;
+
 	// Model to be converted
 	private ModulesFile modulesFile;
 	// Constants from model
@@ -54,10 +53,10 @@ public class Modules2PTA
 	/**
 	 * Constructor.
 	 */
-	public Modules2PTA(Prism prism, ModulesFile modulesFile)
+	public Modules2PTA(PrismComponent parent, ModulesFile modulesFile) throws PrismException
 	{
-		this.prism = prism;
-		mainLog = prism.getMainLog();
+		super(parent);
+		sumRoundOff = settings.getDouble(PrismSettings.PRISM_SUM_ROUND_OFF);
 		this.modulesFile = modulesFile;
 		constantValues = modulesFile.getConstantValues();
 	}
@@ -296,7 +295,7 @@ public class Modules2PTA
 					edge.setDestination(tr.getSource());
 			}
 			// Check probabilities sum to one (ish)
-			if (!PrismUtils.doublesAreCloseAbs(probSum, 1.0, prism.getSumRoundOff())) {
+			if (!PrismUtils.doublesAreCloseAbs(probSum, 1.0, sumRoundOff)) {
 				throw new PrismLangException("Probabilities do not sum to one (" + probSum + ") in PTA");
 			}
 		}

prism/src/pta/PTAModelChecker.java

@@ -33,18 +33,12 @@ import parser.ast.*;
 import parser.type.*;
 import parser.visitor.ASTTraverseModify;
 import prism.*;
-import simulator.sampler.Sampler;
-import explicit.*;
 
 /**
  * Model checker for probabilistic timed automata (PTAs).
  */
-public class PTAModelChecker
+public class PTAModelChecker extends PrismComponent
 {
-	// Prism object
-	private Prism prism;
-	// Log
-	private PrismLog mainLog;
 	// Model file
 	private ModulesFile modulesFile;
 	// Properties file
@@ -61,10 +55,9 @@ public class PTAModelChecker
 	/**
 	 * Constructor.
 	 */
-	public PTAModelChecker(Prism prism, ModulesFile modulesFile, PropertiesFile propertiesFile) throws PrismException
+	public PTAModelChecker(PrismComponent parent, ModulesFile modulesFile, PropertiesFile propertiesFile) throws PrismException
 	{
-		this.prism = prism;
-		mainLog = prism.getMainLog();
+		super(parent);
 		this.modulesFile = modulesFile;
 		this.propertiesFile = propertiesFile;
 
@@ -118,7 +111,7 @@ public class PTAModelChecker
 		
 		// Translate ModulesFile object into a PTA object
 		mainLog.println("\nBuilding PTA...");
-		m2pta = new Modules2PTA(prism, modulesFile);
+		m2pta = new Modules2PTA(this, modulesFile);
 		pta = m2pta.translate();
 		mainLog.println("\nPTA: " + pta.infoString());
 
@@ -308,13 +301,13 @@ public class PTAModelChecker
 	private double computeProbabilisticReachability(BitSet targetLocs, boolean min) throws PrismException
 	{
 		// Determine which method to use for computation
-		String ptaMethod = prism.getSettings().getString(PrismSettings.PRISM_PTA_METHOD);
+		String ptaMethod = settings.getString(PrismSettings.PRISM_PTA_METHOD);
 
 		// Do probability computation through abstraction/refinement/stochastic games  
 		if (ptaMethod.equals("Stochastic games")) {
 			PTAAbstractRefine ptaAR;
 			ptaAR = new PTAAbstractRefine();
-			String arOptions = prism.getSettings().getString(PrismSettings.PRISM_AR_OPTIONS);
+			String arOptions = settings.getString(PrismSettings.PRISM_AR_OPTIONS);
 			ptaAR.setLog(mainLog);
 			ptaAR.parseOptions(arOptions.split(","));
 			return ptaAR.forwardsReachAbstractRefine(pta, targetLocs, null, min);