diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 40c2724c..ef2ecc08 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/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 labels; try { - mc = new CTMCModelChecker(); + mc = new CTMCModelChecker(null); ctmc = new CTMCSimple(); ctmc.buildFromPrismExplicit(args[0]); //System.out.println(dtmc); diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index b40a8dab..b9e95d4d 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/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 labels; boolean min = true; try { - mc = new CTMDPModelChecker(); + mc = new CTMDPModelChecker(null); ctmdp = new CTMDPSimple(); ctmdp.buildFromPrismExplicit(args[0]); System.out.println(ctmdp); diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index d2c144b9..504db354 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/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); diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 22bcb658..e61598a2 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/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 labels; boolean min = true; try { - mc = new MDPModelChecker(); + mc = new MDPModelChecker(null); mdp = new MDPSimple(); mdp.buildFromPrismExplicit(args[0]); //System.out.println(mdp); diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index 4ed2acb0..d211e924 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/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 { diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java index 2c8a0841..f7341be5 100644 --- a/prism/src/explicit/PrismSTPGAbstractRefine.java +++ b/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: diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index f9bc14cc..1044d39c 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/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 /** diff --git a/prism/src/explicit/QuantAbstractRefine.java b/prism/src/explicit/QuantAbstractRefine.java index 8074bae0..eec5b0db 100644 --- a/prism/src/explicit/QuantAbstractRefine.java +++ b/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); diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index 152cde5e..f0a4f622 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/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); diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 8afe885b..0351eb94 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/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 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); diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 4cb46864..f1bc8aef 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/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 /** diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index ef521706..f88acfbe 100644 --- a/prism/src/prism/Prism.java +++ b/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); diff --git a/prism/src/prism/PrismComponent.java b/prism/src/prism/PrismComponent.java new file mode 100644 index 00000000..ce6a5193 --- /dev/null +++ b/prism/src/prism/PrismComponent.java @@ -0,0 +1,117 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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: + *
    + *
  • A PrismLog ({@code mainLog}) for output + *
  • A PrismSettings object ({@code settings}) + *
+ * 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; + } +} diff --git a/prism/src/prism/SCCComputer.java b/prism/src/prism/SCCComputer.java index e6063857..ed66a8af 100644 --- a/prism/src/prism/SCCComputer.java +++ b/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; diff --git a/prism/src/prism/SCCComputerLockstep.java b/prism/src/prism/SCCComputerLockstep.java index 2eea385a..4b4351eb 100644 --- a/prism/src/prism/SCCComputerLockstep.java +++ b/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); } diff --git a/prism/src/prism/SCCComputerSCCFind.java b/prism/src/prism/SCCComputerSCCFind.java index 88079537..eae836e7 100644 --- a/prism/src/prism/SCCComputerSCCFind.java +++ b/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++; diff --git a/prism/src/prism/SCCComputerXB.java b/prism/src/prism/SCCComputerXB.java index 3c92b665..bb782094 100644 --- a/prism/src/prism/SCCComputerXB.java +++ b/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); } diff --git a/prism/src/pta/PTAModelCheckerCL.java b/prism/src/pta/PTAModelCheckerCL.java index 758b0d6f..6668da2e 100644 --- a/prism/src/pta/PTAModelCheckerCL.java +++ b/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) {