diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java
index b9e95d4d..7b6d47a1 100644
--- a/prism/src/explicit/CTMDPModelChecker.java
+++ b/prism/src/explicit/CTMDPModelChecker.java
@@ -126,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(null);
+ mc = new MDPModelChecker(this);
mc.inheritSettings(this);
res = mc.computeBoundedUntilProbs(mdp, null, target, k, min);
diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index 2c7f0428..2a0ebaff 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -263,6 +263,7 @@ public class DTMCModelChecker extends ProbModelChecker
BitSet acceptingBSCCs = mcLtl.findAcceptingBSCCsForRabin(dra, modelProduct, invMap);
mainLog.println("\nComputing reachability probabilities...");
mcProduct = new DTMCModelChecker(this);
+ mcProduct.inheritSettings(this);
probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((DTMC) modelProduct, acceptingBSCCs).soln, modelProduct);
// Mapping probabilities in the original model
diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java
index f104fbc2..6106c7cc 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/prism/src/explicit/MDPModelChecker.java
@@ -277,6 +277,7 @@ public class MDPModelChecker extends ProbModelChecker
BitSet acceptingMECs = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, invMap);
mainLog.println("\nComputing reachability probabilities...");
mcProduct = new MDPModelChecker(this);
+ mcProduct.inheritSettings(this);
probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP) modelProduct, acceptingMECs, false).soln, modelProduct);
// Subtract from 1 if we're model checking a negated formula for regular Pmin
diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index b23a78e6..7107a665 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -42,7 +42,7 @@ import explicit.rewards.MCRewards;
import explicit.rewards.MDPRewards;
/**
- * Super class for explicit-state probabilistic model checkers
+ * Super class for explicit-state probabilistic model checkers.
*/
public class ProbModelChecker extends StateModelChecker
{
@@ -142,89 +142,83 @@ public class ProbModelChecker extends StateModelChecker
public ProbModelChecker(PrismComponent parent) throws PrismException
{
super(parent);
- }
-
- // Settings methods
- /**
- * Set settings from a PRISMSettings object.
- */
- public void setSettings(PrismSettings settings) throws PrismException
- {
- super.setSettings(settings);
-
- if (settings == null)
- return;
-
- String s;
- // PRISM_LIN_EQ_METHOD
- s = settings.getString(PrismSettings.PRISM_LIN_EQ_METHOD);
- if (s.equals("Power")) {
- setLinEqMethod(LinEqMethod.POWER);
- } else if (s.equals("Jacobi")) {
- setLinEqMethod(LinEqMethod.JACOBI);
- } else if (s.equals("Gauss-Seidel")) {
- setLinEqMethod(LinEqMethod.GAUSS_SEIDEL);
- } else if (s.equals("Backwards Gauss-Seidel")) {
- setLinEqMethod(LinEqMethod.BACKWARDS_GAUSS_SEIDEL);
- } else if (s.equals("JOR")) {
- setLinEqMethod(LinEqMethod.JOR);
- } else if (s.equals("SOR")) {
- setLinEqMethod(LinEqMethod.SOR);
- } else if (s.equals("Backwards SOR")) {
- setLinEqMethod(LinEqMethod.BACKWARDS_SOR);
- } else {
- throw new PrismException("Explicit engine does not support linear equation solution method \"" + s + "\"");
- }
- // PRISM_MDP_SOLN_METHOD
- s = settings.getString(PrismSettings.PRISM_MDP_SOLN_METHOD);
- if (s.equals("Value iteration")) {
- setMDPSolnMethod(MDPSolnMethod.VALUE_ITERATION);
- } else if (s.equals("Gauss-Seidel")) {
- setMDPSolnMethod(MDPSolnMethod.GAUSS_SEIDEL);
- } else if (s.equals("Policy iteration")) {
- setMDPSolnMethod(MDPSolnMethod.POLICY_ITERATION);
- } else if (s.equals("Modified policy iteration")) {
- setMDPSolnMethod(MDPSolnMethod.MODIFIED_POLICY_ITERATION);
- } else if (s.equals("Linear programming")) {
- setMDPSolnMethod(MDPSolnMethod.LINEAR_PROGRAMMING);
- } else {
- throw new PrismException("Explicit engine does not support MDP solution method \"" + s + "\"");
- }
- // PRISM_TERM_CRIT
- s = settings.getString(PrismSettings.PRISM_TERM_CRIT);
- if (s.equals("Absolute")) {
- setTermCrit(TermCrit.ABSOLUTE);
- } else if (s.equals("Relative")) {
- setTermCrit(TermCrit.RELATIVE);
- } else {
- throw new PrismException("Unknown termination criterion \"" + s + "\"");
- }
- // PRISM_TERM_CRIT_PARAM
- setTermCritParam(settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM));
- // PRISM_MAX_ITERS
- setMaxIters(settings.getInteger(PrismSettings.PRISM_MAX_ITERS));
- // PRISM_PRECOMPUTATION
- setPrecomp(settings.getBoolean(PrismSettings.PRISM_PRECOMPUTATION));
- // PRISM_PROB0
- setProb0(settings.getBoolean(PrismSettings.PRISM_PROB0));
- // PRISM_PROB1
- setProb1(settings.getBoolean(PrismSettings.PRISM_PROB1));
- // PRISM_FAIRNESS
- if (settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) {
- throw new PrismException("The explicit engine does not support model checking MDPs under fairness");
+ // If present, initialise settings from PrismSettings
+ if (settings != null) {
+ String s;
+ // PRISM_LIN_EQ_METHOD
+ s = settings.getString(PrismSettings.PRISM_LIN_EQ_METHOD);
+ if (s.equals("Power")) {
+ setLinEqMethod(LinEqMethod.POWER);
+ } else if (s.equals("Jacobi")) {
+ setLinEqMethod(LinEqMethod.JACOBI);
+ } else if (s.equals("Gauss-Seidel")) {
+ setLinEqMethod(LinEqMethod.GAUSS_SEIDEL);
+ } else if (s.equals("Backwards Gauss-Seidel")) {
+ setLinEqMethod(LinEqMethod.BACKWARDS_GAUSS_SEIDEL);
+ } else if (s.equals("JOR")) {
+ setLinEqMethod(LinEqMethod.JOR);
+ } else if (s.equals("SOR")) {
+ setLinEqMethod(LinEqMethod.SOR);
+ } else if (s.equals("Backwards SOR")) {
+ setLinEqMethod(LinEqMethod.BACKWARDS_SOR);
+ } else {
+ throw new PrismException("Explicit engine does not support linear equation solution method \"" + s + "\"");
+ }
+ // PRISM_MDP_SOLN_METHOD
+ s = settings.getString(PrismSettings.PRISM_MDP_SOLN_METHOD);
+ if (s.equals("Value iteration")) {
+ setMDPSolnMethod(MDPSolnMethod.VALUE_ITERATION);
+ } else if (s.equals("Gauss-Seidel")) {
+ setMDPSolnMethod(MDPSolnMethod.GAUSS_SEIDEL);
+ } else if (s.equals("Policy iteration")) {
+ setMDPSolnMethod(MDPSolnMethod.POLICY_ITERATION);
+ } else if (s.equals("Modified policy iteration")) {
+ setMDPSolnMethod(MDPSolnMethod.MODIFIED_POLICY_ITERATION);
+ } else if (s.equals("Linear programming")) {
+ setMDPSolnMethod(MDPSolnMethod.LINEAR_PROGRAMMING);
+ } else {
+ throw new PrismException("Explicit engine does not support MDP solution method \"" + s + "\"");
+ }
+ // PRISM_TERM_CRIT
+ s = settings.getString(PrismSettings.PRISM_TERM_CRIT);
+ if (s.equals("Absolute")) {
+ setTermCrit(TermCrit.ABSOLUTE);
+ } else if (s.equals("Relative")) {
+ setTermCrit(TermCrit.RELATIVE);
+ } else {
+ throw new PrismException("Unknown termination criterion \"" + s + "\"");
+ }
+ // PRISM_TERM_CRIT_PARAM
+ setTermCritParam(settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM));
+ // PRISM_MAX_ITERS
+ setMaxIters(settings.getInteger(PrismSettings.PRISM_MAX_ITERS));
+ // PRISM_PRECOMPUTATION
+ setPrecomp(settings.getBoolean(PrismSettings.PRISM_PRECOMPUTATION));
+ // PRISM_PROB0
+ setProb0(settings.getBoolean(PrismSettings.PRISM_PROB0));
+ // PRISM_PROB1
+ setProb1(settings.getBoolean(PrismSettings.PRISM_PROB1));
+ // PRISM_FAIRNESS
+ if (settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) {
+ throw new PrismException("The explicit engine does not support model checking MDPs under fairness");
+ }
+
+ // PRISM_EXPORT_ADV
+ s = settings.getString(PrismSettings.PRISM_EXPORT_ADV);
+ if (!(s.equals("None")))
+ setExportAdv(true);
+ // PRISM_EXPORT_ADV_FILENAME
+ setExportAdvFilename(settings.getString(PrismSettings.PRISM_EXPORT_ADV_FILENAME));
}
-
- // PRISM_EXPORT_ADV
- s = settings.getString(PrismSettings.PRISM_EXPORT_ADV);
- if (!(s.equals("None")))
- setExportAdv(true);
- // PRISM_EXPORT_ADV_FILENAME
- setExportAdvFilename(settings.getString(PrismSettings.PRISM_EXPORT_ADV_FILENAME));
}
+
+ // Settings methods
/**
- * Inherit settings (and other info) from another model checker object.
+ * Inherit settings (and the log) from another ProbModelChecker object.
+ * For model checker objects that inherit a PrismSettings object, this is superfluous
+ * since this has been done already.
*/
public void inheritSettings(ProbModelChecker other)
{
diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java
index 90307d8c..714df8f4 100644
--- a/prism/src/explicit/StateModelChecker.java
+++ b/prism/src/explicit/StateModelChecker.java
@@ -36,8 +36,6 @@ import java.util.HashMap;
import java.util.List;
import java.util.Map;
-import explicit.SCCComputer.SCCMethod;
-
import parser.State;
import parser.Values;
import parser.ast.Expression;
@@ -70,7 +68,11 @@ import prism.PrismSettings;
import prism.Result;
/**
- * Super class for explicit-state model checkers
+ * Super class for explicit-state model checkers.
+ *
+ * This model checker class and its subclasses store their settings locally so
+ * that they can be configured and used without a PrismSettings object.
+ * Pass in null as a parent on creation to bypass the use of PrismSettings.
*/
public class StateModelChecker extends PrismComponent
{
@@ -79,13 +81,12 @@ public class StateModelChecker extends PrismComponent
// Verbosity level
protected int verbosity = 0;
-
+
// Additional flags/settings not included in PrismSettings
-
+
// Generate/store a strategy during model checking?
protected boolean genStrat = false;
-
-
+
// Model file (for reward structures, etc.)
protected ModulesFile modulesFile = null;
@@ -107,16 +108,27 @@ public class StateModelChecker extends PrismComponent
public StateModelChecker(PrismComponent parent) throws PrismException
{
super(parent);
+
+ // For explicit.StateModelChecker and its subclasses, we explicitly set 'settings'
+ // to null if there is no parent or if the parent has a null 'settings'.
+ // This allows us to choose to ignore the default one created by PrismComponent.
+ if (parent == null || parent.getSettings() == null)
+ setSettings(null);
+
+ // If present, initialise settings from PrismSettings
+ if (settings != null) {
+ verbosity = settings.getBoolean(PrismSettings.PRISM_VERBOSE) ? 10 : 1;
+ }
}
-
+
/**
- * Create a model checker (a subclass of this one) for a given model type
+ * 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
*/
@@ -148,20 +160,9 @@ public class StateModelChecker extends PrismComponent
// Settings methods
/**
- * Set settings from a PRISMSettings object.
- */
- public void setSettings(PrismSettings settings) throws PrismException
- {
- super.setSettings(settings);
-
- if (settings == null)
- return;
-
- verbosity = settings.getBoolean(PrismSettings.PRISM_VERBOSE) ? 10 : 1;
- }
-
- /**
- * Inherit settings (and other info) from another model checker object.
+ * Inherit settings (and the log) from another StateModelChecker object.
+ * For model checker objects that inherit a PrismSettings object, this is superfluous
+ * since this has been done already.
*/
public void inheritSettings(StateModelChecker other)
{
diff --git a/prism/src/prism/PrismComponent.java b/prism/src/prism/PrismComponent.java
index ce6a5193..9db8a943 100644
--- a/prism/src/prism/PrismComponent.java
+++ b/prism/src/prism/PrismComponent.java
@@ -29,15 +29,18 @@ 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.
+ *
+ * Depending on the (sub)class, the {@code settings} object may either be read
+ * from each time that a setting is required (thus respecting any changes that
+ * are made to it over time), or read from initially and then ignored.
+ * Mostly, these classes are freshly created to perform some task and then discarded,
+ * so there is no point making changes to {@code settings} after creation.
*/
public class PrismComponent
{
@@ -50,11 +53,6 @@ public class PrismComponent
/**
* 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();
@@ -74,37 +72,36 @@ public class PrismComponent
{
if (parent == null)
return;
-
setLog(parent.getLog());
setSettings(parent.getSettings());
}
- // Log
+ // Setters (declared as final since they are called from the constructor)
/**
* Set log ("mainLog") for output.
*/
- public void setLog(PrismLog log)
+ public final void setLog(PrismLog mainLog)
{
- this.mainLog = log;
+ this.mainLog = mainLog;
}
/**
- * Get log ("mainLog") for output.
+ * Set PRISMSettings object.
*/
- public PrismLog getLog()
+ public final void setSettings(PrismSettings settings) throws PrismException
{
- return mainLog;
+ this.settings = settings;
}
-
- // Settings
+
+ // Getters
/**
- * Set settings from a PRISMSettings object.
+ * Get log ("mainLog") for output.
*/
- public void setSettings(PrismSettings settings) throws PrismException
+ public PrismLog getLog()
{
- this.settings = settings;
+ return mainLog;
}
/**