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

Align parametric model construction with the non-parametric a little more. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11801 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 9 years ago
parent
048017bb24
commit
002257286d
3 changed files with 37 additions and 73 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. 97
      prism/src/param/ModelBuilder.java
  2. 2
      prism/src/param/ParamModel.java
  3. 11
      prism/src/prism/Prism.java

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

@ -57,8 +57,6 @@ public final class ModelBuilder extends PrismComponent
{
/** the ModelGeneratorSymbolic interface providing the model to be transformed to a {@code ParamModel} */
private ModelGeneratorSymbolic modelGenSym;
/** parametric model constructed */
private ParamModel model;
/** function factory used in the constructed parametric model */
private FunctionFactory functionFactory;
/** names of parameters */
@ -187,37 +185,6 @@ public final class ModelBuilder extends PrismComponent
}
}
// setters and getters
/**
* Set generator of model to be transformed to parametric Markov model.
*/
public void setModelGenerator(ModelGeneratorSymbolic modelGenSym) throws PrismException
{
this.modelGenSym = modelGenSym;
}
/**
* Set parameter informations.
* Obviously, all of {@code paramNames}, {@code lower}, {@code} upper
* must have the same length, and {@code lower} bounds of parameters must
* not be higher than {@code upper} bounds.
*
* @param paramNames names of parameters
* @param lower lower bounds of parameters
* @param upper upper bounds of parameters
*/
public void setParameters(String[] paramNames, String[] lower, String[] upper)
{
this.paramNames = paramNames;
this.lower = new BigRational[lower.length];
this.upper = new BigRational[upper.length];
for (int param = 0; param < lower.length; param++) {
this.lower[param] = new BigRational(lower[param]);
this.upper[param] = new BigRational(upper[param]);
}
}
/**
* Get the parameter names as a list of strings.
* @return the parameter names
@ -228,14 +195,32 @@ public final class ModelBuilder extends PrismComponent
}
/**
* Construct parametric Markov model.
* For this to work, module file, PRISM log, etc. must have been set
* beforehand.
*
* @throws PrismException in case the model cannot be constructed
* Construct a parametric model and return it.
* All of {@code paramNames}, {@code lower}, {@code} upper must have the same length,
* and {@code lower} bounds of parameters must not be higher than {@code upper} bounds.
* @param modelGenSym The ModelGeneratorSymbolic interface providing the model
* @param paramNames names of parameters
* @param lowerStr lower bounds of parameters
* @param upperStr upper bounds of parameters
*/
public void build() throws PrismException
public ParamModel constructModel(ModelGeneratorSymbolic modelGenSym, String[] paramNames, String[] lowerStr, String[] upperStr) throws PrismException
{
// No model construction for PTAs
if (modelGenSym.getModelType() == ModelType.PTA) {
throw new PrismNotSupportedException("You cannot build a PTA model explicitly, only perform model checking");
}
// Store model generator and parameter info
this.modelGenSym = modelGenSym;
this.paramNames = paramNames;
lower = new BigRational[lowerStr.length];
upper = new BigRational[upperStr.length];
for (int param = 0; param < lowerStr.length; param++) {
lower[param] = new BigRational(lowerStr[param]);
upper[param] = new BigRational(upperStr[param]);
}
// Create function factory
if (functionType.equals("JAS")) {
functionFactory = new JasFunctionFactory(paramNames, lower, upper);
} else if (functionType.equals("JAS-cached")) {
@ -243,18 +228,9 @@ public final class ModelBuilder extends PrismComponent
} else if (functionType.equals("DAG")) {
functionFactory = new DagFunctionFactory(paramNames, lower, upper, dagMaxError, false);
}
long time;
// And pass it to the model generator
modelGenSym.setSymbolic(this, functionFactory);
if (modelGenSym.getModelType() == ModelType.PTA) {
throw new PrismNotSupportedException("You cannot build a PTA model explicitly, only perform model checking");
}
mainLog.print("\nBuilding model...\n");
// build model
time = System.currentTimeMillis();
// First, set values for any constants in the model
// (but do this *symbolically* - partly because some constants are parameters and therefore unknown,
// but also to keep values like 1/3 as expressions rather than being converted to doubles,
@ -270,23 +246,16 @@ public final class ModelBuilder extends PrismComponent
return (expr != null) ? expr.deepCopy() : e;
}
});*/
ParamModel modelExpl = constructModel(modelGenSym);
// Build/return model
mainLog.print("\nBuilding model...\n");
long time = System.currentTimeMillis();
ParamModel modelExpl = doModelConstruction(modelGenSym);
time = System.currentTimeMillis() - time;
mainLog.print("\n"+modelExpl.infoStringTable());
mainLog.println("\nTime for model construction: " + time / 1000.0 + " seconds.");
model = modelExpl;
}
/**
* Returns the constructed parametric Markov model.
*
* @return constructed parametric Markov model
*/
public explicit.Model getModel()
{
return model;
return modelExpl;
}
/**
@ -353,7 +322,7 @@ public final class ModelBuilder extends PrismComponent
* @return parametric model constructed
* @throws PrismException thrown if model cannot be constructed
*/
private ParamModel constructModel(ModelGeneratorSymbolic modelGenSym) throws PrismException
private ParamModel doModelConstruction(ModelGeneratorSymbolic modelGenSym) throws PrismException
{
ModelType modelType;

2
prism/src/param/ParamModel.java
View File

@ -46,7 +46,7 @@ import explicit.ModelExplicit;
* This turned out the be the most convenient way to implement model checking
* for parametric models.
*/
final class ParamModel extends ModelExplicit
public final class ParamModel extends ModelExplicit
{
/** total number of nondeterministic choices over all states */
private int numTotalChoices;

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

@ -49,6 +49,7 @@ import jdd.JDDVars;
import mtbdd.PrismMTBDD;
import odd.ODDUtils;
import param.ModelBuilder;
import param.ParamModel;
import param.ParamModelChecker;
import param.ParamResult;
import parser.ExplicitFiles2ModulesFile;
@ -3093,10 +3094,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
String[] paramUpperBounds = new String[] { "1" };
// And execute parameteric model checking
param.ModelBuilder builder = new ModelBuilder(this);
builder.setModelGenerator(new ModulesFileModelGeneratorSymbolic(currentModulesFile, this));
builder.setParameters(paramNames, paramLowerBounds, paramUpperBounds);
builder.build();
explicit.Model modelExpl = builder.getModel();
ParamModel modelExpl = builder.constructModel(new ModulesFileModelGeneratorSymbolic(currentModulesFile, this), paramNames, paramLowerBounds, paramUpperBounds);
ParamModelChecker mc = new ParamModelChecker(this);
mc.setModelBuilder(builder);
mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds);
@ -3152,10 +3150,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
mainLog.println("Property constants: " + definedPFConstants);
param.ModelBuilder builder = new ModelBuilder(this);
builder.setModelGenerator(new ModulesFileModelGeneratorSymbolic(currentModulesFile, this));
builder.setParameters(paramNames, paramLowerBounds, paramUpperBounds);
builder.build();
explicit.Model modelExpl = builder.getModel();
ParamModel modelExpl = builder.constructModel(new ModulesFileModelGeneratorSymbolic(currentModulesFile, this), paramNames, paramLowerBounds, paramUpperBounds);
ParamModelChecker mc = new ParamModelChecker(this);
mc.setModelBuilder(builder);
mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds);

Write Preview
Loading…
Cancel
Save