From 10e896da5b2563703d20d3a48d810f118b54c8d8 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 12 Nov 2013 22:00:44 +0000 Subject: [PATCH] Code refactoring. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7589 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/param/ModelBuilder.java | 88 +++++++++++------------- prism/src/param/ParamModelChecker.java | 95 +++++++------------------- prism/src/prism/Prism.java | 9 +-- 3 files changed, 65 insertions(+), 127 deletions(-) diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index 2532ed45..98c4026c 100644 --- a/prism/src/param/ModelBuilder.java +++ b/prism/src/param/ModelBuilder.java @@ -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 (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 states) - throws PrismException + throws PrismException { boolean isNonDet = modelType == ModelType.MDP; int numStates = 0; int numTotalChoices = 0; int numTotalSuccessors = 0; - + LinkedList explore = new LinkedList(); 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; } } diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index de08abd4..c23a43f3 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -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 (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); } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 5850984e..f3c0e507 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -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());