diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index 36254a09..11fb6d84 100644 --- a/prism/src/param/ModelBuilder.java +++ b/prism/src/param/ModelBuilder.java @@ -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; diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index 0e091803..0a5b8d84 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -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; diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index ea4427ed..782a3d96 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -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);