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

Code refactoring. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7589 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
21b4fcf292
commit
10e896da5b
3 changed files with 65 additions and 127 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. 88
      prism/src/param/ModelBuilder.java
  2. 95
      prism/src/param/ParamModelChecker.java
  3. 9
      prism/src/prism/Prism.java

88
prism/src/param/ModelBuilder.java
View File

@ -37,6 +37,7 @@ import parser.ast.ExpressionLiteral;
import parser.ast.ExpressionUnaryOp;
import parser.ast.ModulesFile;
import prism.ModelType;
import prism.PrismComponent;
import prism.PrismException;
import prism.PrismLog;
import prism.PrismSettings;
@ -49,11 +50,10 @@ import explicit.StateStorage;
* @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
* @see ParamModel
*/
public final class ModelBuilder {
public final class ModelBuilder extends PrismComponent
{
/** {@code ModulesFile} to be transformed to a {@code ParamModel} */
private ModulesFile modulesFile;
/** main log to write user info to */
private PrismLog mainLog;
/** parametric model constructed from {@code modulesFile} */
private ParamModel model;
/** function factory used in the constructed parametric model */
@ -69,6 +69,19 @@ public final class ModelBuilder {
/** maximal error probability of DAG function representation */
private double dagMaxError;
/**
* Constructor
*/
public ModelBuilder(PrismComponent parent) throws PrismException
{
super(parent);
// If present, initialise settings from PrismSettings
if (settings != null) {
functionType = settings.getString(PrismSettings.PRISM_PARAM_FUNCTION);
dagMaxError = settings.getDouble(PrismSettings.PRISM_PARAM_DAG_MAX_ERROR);
}
}
/**
* Transform PRISM expression to rational function.
* If successful, a function representing the given expression will be
@ -81,12 +94,12 @@ public final class ModelBuilder {
* @return rational function representing the given PRISM expression
* @throws PrismException thrown if {@code expr} cannot be represented as rational function
*/
Function expr2function(FunctionFactory factory, Expression expr) throws PrismException {
Function expr2function(FunctionFactory factory, Expression expr) throws PrismException
{
if (expr instanceof ExpressionLiteral) {
String exprString = ((ExpressionLiteral) expr).getString();
if (exprString == null || exprString.equals("")) {
throw new PrismException("cannot convert from literal "
+ "for which no string is set");
throw new PrismException("cannot convert from literal " + "for which no string is set");
}
return factory.fromBigRational(new BigRational(exprString));
} else if (expr instanceof ExpressionConstant) {
@ -116,8 +129,7 @@ public final class ModelBuilder {
case ExpressionBinaryOp.DIVIDE:
return f1.divide(f2);
default:
throw new PrismException("parametric analysis with rate/probability of " + expr
+ " not implemented");
throw new PrismException("parametric analysis with rate/probability of " + expr + " not implemented");
}
} else if (expr instanceof ExpressionUnaryOp) {
ExpressionUnaryOp unExpr = ((ExpressionUnaryOp) expr);
@ -128,17 +140,15 @@ public final class ModelBuilder {
case ExpressionUnaryOp.PARENTH:
return f;
default:
throw new PrismException("parametric analysis with rate/probability of " + expr
+ " not implemented");
}
throw new PrismException("parametric analysis with rate/probability of " + expr + " not implemented");
}
} else {
throw new PrismException("parametric analysis with rate/probability of " + expr
+ " not implemented");
throw new PrismException("parametric analysis with rate/probability of " + expr + " not implemented");
}
}
// setters and getters
/**
* Set modules file to be transformed to parametric Markov model.
*
@ -148,17 +158,7 @@ public final class ModelBuilder {
{
this.modulesFile = modulesFile;
}
/**
* Set PRISM main log to write user info to.
*
* @param mainLog PRISM main log to write user info to
*/
public void setMainLong(PrismLog mainLog)
{
this.mainLog = mainLog;
}
/**
* Set parameter informations.
* Obviously, all of {@code paramNames}, {@code lower}, {@code} upper
@ -169,7 +169,8 @@ public final class ModelBuilder {
* @param lower lower bounds of parameters
* @param upper upper bounds of parameters
*/
public void setParameters(String[] paramNames, String[] lower, String[] upper) {
public void setParameters(String[] paramNames, String[] lower, String[] upper)
{
this.paramNames = paramNames;
this.lower = new BigRational[lower.length];
this.upper = new BigRational[upper.length];
@ -178,7 +179,7 @@ public final class ModelBuilder {
this.upper[param] = new BigRational(upper[param]);
}
}
/**
* Construct parametric Markov model.
* For this to work, module file, PRISM log, etc. must have been set
@ -193,7 +194,7 @@ public final class ModelBuilder {
} else if (functionType.equals("JAS-cached")) {
functionFactory = new CachedFunctionFactory(new JasFunctionFactory(paramNames, lower, upper));
} else if (functionType.equals("DAG")) {
functionFactory = new DagFunctionFactory(paramNames, lower, upper, dagMaxError, false);
functionFactory = new DagFunctionFactory(paramNames, lower, upper, dagMaxError, false);
}
long time;
@ -212,7 +213,7 @@ public final class ModelBuilder {
mainLog.println("\nTime for model construction: " + time / 1000.0 + " seconds.");
model = modelExpl;
}
/**
* Returns the constructed parametric Markov model.
*
@ -222,7 +223,7 @@ public final class ModelBuilder {
{
return model;
}
/**
* Reserves memory needed for parametric model and reserves necessary space.
* Afterwards, transition probabilities etc. can be added.
@ -235,13 +236,13 @@ public final class ModelBuilder {
* @throws PrismException thrown if problems in underlying methods occur
*/
private void reserveMemoryAndExploreStates(ModulesFile modulesFile, ParamModel model, ModelType modelType, SymbolicEngine engine, StateStorage<State> states)
throws PrismException
throws PrismException
{
boolean isNonDet = modelType == ModelType.MDP;
int numStates = 0;
int numTotalChoices = 0;
int numTotalSuccessors = 0;
LinkedList<State> explore = new LinkedList<State>();
State state = modulesFile.getDefaultInitialState();
@ -262,7 +263,7 @@ public final class ModelBuilder {
int numSuccessors = tranlist.getChoice(choiceNr).size();
numTotalSuccessors += numSuccessors;
for (int succNr = 0; succNr < numSuccessors; succNr++) {
State stateNew = tranlist.getChoice(choiceNr).computeTarget(succNr, state);
State stateNew = tranlist.getChoice(choiceNr).computeTarget(succNr, state);
if (states.add(stateNew)) {
numStates++;
explore.add(stateNew);
@ -280,7 +281,7 @@ public final class ModelBuilder {
model.reserveMem(numStates, numTotalChoices, numTotalSuccessors);
}
/**
* Construct model once function factory etc. has been allocated.
*
@ -350,7 +351,7 @@ public final class ModelBuilder {
for (int choiceNr = 0; choiceNr < numChoices; choiceNr++) {
ChoiceListFlexi choice = tranlist.getChoice(choiceNr);
int a = tranlist.getTransitionModuleOrActionIndex(tranlist.getTotalIndexOfTransition(choiceNr, 0));
String action = a < 0 ? null : modulesFile.getSynch(a - 1);
String action = a < 0 ? null : modulesFile.getSynch(a - 1);
int numSuccessors = choice.size();
for (int succNr = 0; succNr < numSuccessors; succNr++) {
ChoiceListFlexi succ = tranlist.getChoice(choiceNr);
@ -380,21 +381,10 @@ public final class ModelBuilder {
stateNr++;
}
model.setFunctionFactory(functionFactory);
mainLog.print("Reachable states exploration and model construction");
mainLog.println(" done in " + ((System.currentTimeMillis() - timer) / 1000.0) + " secs.");
return model;
}
/**
* Sets information from PRISM setting relevant to construct parametric model.
* This involves, for instance, the type of function representation.
*
* @param settings PRISM setting relevant to construct parametric model
*/
public void setSettings(PrismSettings settings) {
functionType = settings.getString(PrismSettings.PRISM_PARAM_FUNCTION);
dagMaxError = settings.getDouble(PrismSettings.PRISM_PARAM_DAG_MAX_ERROR);
return model;
}
}

95
prism/src/param/ParamModelChecker.java
View File

@ -68,6 +68,7 @@ import parser.ast.*;
import parser.ast.ExpressionFilter.FilterOperator;
import parser.type.*;
import prism.ModelType;
import prism.PrismComponent;
import prism.PrismException;
import prism.PrismLog;
import prism.PrismPrintStreamLog;
@ -79,7 +80,7 @@ import prism.Result;
*
* @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
*/
final public class ParamModelChecker
final public class ParamModelChecker extends PrismComponent
{
// Log for output (default to System.out)
private PrismLog mainLog = new PrismPrintStreamLog(System.out);
@ -118,47 +119,15 @@ final public class ParamModelChecker
private ModelBuilder modelBuilder;
// Setters/getters
/**
* Set log for output.
*/
public void setLog(PrismLog log)
{
this.mainLog = log;
}
/**
* Get log for output.
* Constructor
*/
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
/**
* Set settings from a PRISMSettings object.
* @throws PrismException
*/
public void setSettings(PrismSettings settings) throws PrismException
public ParamModelChecker(PrismComponent parent) throws PrismException
{
super(parent);
// If present, initialise settings from PrismSettings
if (settings != null) {
verbosity = settings.getBoolean(PrismSettings.PRISM_VERBOSE) ? 10 : 1;
precision = new BigRational(settings.getString(PrismSettings.PRISM_PARAM_PRECISION));
String splitMethodString = settings.getString(PrismSettings.PRISM_PARAM_SPLIT);
@ -197,40 +166,24 @@ final public class ParamModelChecker
throw new PrismException("unknown bisimulation type " + bisimTypeString);
}
simplifyRegions = settings.getBoolean(PrismSettings.PRISM_PARAM_SUBSUME_REGIONS);
}
}
// Setters/getters
/**
* Inherit settings (and other info) from another model checker object.
*/
public void inheritSettings(ParamModelChecker other)
{
setLog(other.getLog());
setVerbosity(other.getVerbosity());
}
/**
* Print summary of current settings.
*/
public void printSettings()
{
mainLog.print("verbosity = " + verbosity + " ");
}
// Set methods for flags/settings
/**
* Set verbosity level, i.e. amount of output produced.
* 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 setVerbosity(int verbosity)
{
this.verbosity = verbosity;
}
// Get methods for flags/settings
public int getVerbosity()
public void setModulesFileAndPropertiesFile(ModulesFile modulesFile, PropertiesFile propertiesFile)
{
return verbosity;
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
@ -953,7 +906,7 @@ final public class ParamModelChecker
probs = checkProbPathFormulaSimple(model, expr.getExpression(), min, needStates);
probs.clearNotNeeded(needStates);
if (getVerbosity() > 5) {
if (verbosity > 5) {
mainLog.print("\nProbabilities (non-zero only) for all states:\n");
mainLog.print(probs);
}
@ -1086,7 +1039,7 @@ final public class ParamModelChecker
rews.clearNotNeeded(needStates);
// Print out probabilities
if (getVerbosity() > 5) {
if (verbosity > 5) {
mainLog.print("\nProbabilities (non-zero only) for all states:\n");
mainLog.print(rews);
}
@ -1231,7 +1184,7 @@ final public class ParamModelChecker
probs = checkProbSteadyState(model, expr.getExpression(), min, needStates);
probs.clearNotNeeded(needStates);
if (getVerbosity() > 5) {
if (verbosity > 5) {
mainLog.print("\nProbabilities (non-zero only) for all states:\n");
mainLog.print(probs);
}

9
prism/src/prism/Prism.java
View File

@ -3693,7 +3693,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
public Result modelCheckParametric(PropertiesFile propertiesFile, Property prop, String[] paramNames, String[] paramLowerBounds, String[] paramUpperBounds)
throws PrismException
{
if (paramNames == null) {
throw new PrismException("Must specify some parameters when using " + "the parametric analysis");
}
@ -3701,17 +3700,13 @@ public class Prism extends PrismComponent implements PrismSettingsListener
for (int pnr = 0; pnr < paramNames.length; pnr++) {
constlist.removeValue(paramNames[pnr]);
}
param.ModelBuilder builder = new ModelBuilder();
param.ModelBuilder builder = new ModelBuilder(this);
builder.setModulesFile(currentModulesFile);
builder.setMainLong(mainLog);
builder.setParameters(paramNames, paramLowerBounds, paramUpperBounds);
builder.setSettings(settings);
builder.build();
explicit.Model modelExpl = builder.getModel();
ParamModelChecker mc = new ParamModelChecker();
ParamModelChecker mc = new ParamModelChecker(this);
mc.setModelBuilder(builder);
mc.setLog(mainLog);
mc.setSettings(settings);
mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds);
mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile);
return mc.check(modelExpl, prop.getExpression());

Write Preview
Loading…
Cancel
Save