From 4b3d54bd1c51eaa15f65e94553b1f4233eeaaec4 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 23 Jul 2013 15:31:50 +0000 Subject: [PATCH] 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 | 17 ++++++++--------- prism/src/pta/PTAModelChecker.java | 19 ++++++------------- 2 files changed, 14 insertions(+), 22 deletions(-) diff --git a/prism/src/pta/Modules2PTA.java b/prism/src/pta/Modules2PTA.java index 3eb25e14..83128942 100644 --- a/prism/src/pta/Modules2PTA.java +++ b/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"); } } diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 4034ce3e..dc0cc779 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/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);