s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Refinements to PrismComponent interface, and to explicit.StateModelChecker handling of settings (originally due to bug caused by calling overridable methods in explicit model checking constructors). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7200 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
6f1408812e
commit
c68d4a4946
6 changed files with 119 additions and 125 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      prism/src/explicit/CTMDPModelChecker.java
  2. 1
      prism/src/explicit/DTMCModelChecker.java
  3. 1
      prism/src/explicit/MDPModelChecker.java
  4. 152
      prism/src/explicit/ProbModelChecker.java
  5. 49
      prism/src/explicit/StateModelChecker.java
  6. 39
      prism/src/prism/PrismComponent.java

2
prism/src/explicit/CTMDPModelChecker.java
View File

@ -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);

1
prism/src/explicit/DTMCModelChecker.java
View File

@ -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

1
prism/src/explicit/MDPModelChecker.java
View File

@ -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

152
prism/src/explicit/ProbModelChecker.java
View File

@ -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)
{

49
prism/src/explicit/StateModelChecker.java
View File

@ -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.
* <br>
* 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)
{

39
prism/src/prism/PrismComponent.java
View File

@ -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:
* <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.
*
* 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;
}
/**

Write Preview
Loading…
Cancel
Save