From 2dc08f6fb18c8ae03e269e1042cfbd1a59c882ed Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 28 Aug 2017 12:45:47 +0200 Subject: [PATCH] param: store whether the parametric engine is used for exact or parametric analysis, adapt log output / errors --- prism/src/param/ModelBuilder.java | 17 ++++--- prism/src/param/ParamMode.java | 63 ++++++++++++++++++++++++++ prism/src/param/ParamModelChecker.java | 47 +++++++++++-------- prism/src/param/ParamResult.java | 11 +++-- prism/src/param/ValueComputer.java | 4 +- prism/src/prism/Prism.java | 8 ++-- 6 files changed, 115 insertions(+), 35 deletions(-) create mode 100644 prism/src/param/ParamMode.java diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index 11fb6d84..d9a3c59c 100644 --- a/prism/src/param/ModelBuilder.java +++ b/prism/src/param/ModelBuilder.java @@ -55,6 +55,8 @@ import prism.PrismSettings; */ public final class ModelBuilder extends PrismComponent { + /** mode (parametric / exact) */ + private final ParamMode mode; /** the ModelGeneratorSymbolic interface providing the model to be transformed to a {@code ParamModel} */ private ModelGeneratorSymbolic modelGenSym; /** function factory used in the constructed parametric model */ @@ -76,9 +78,10 @@ public final class ModelBuilder extends PrismComponent /** * Constructor */ - public ModelBuilder(PrismComponent parent) throws PrismException + public ModelBuilder(PrismComponent parent, ParamMode mode) throws PrismException { super(parent); + this.mode = mode; // If present, initialise settings from PrismSettings if (settings != null) { functionType = settings.getString(PrismSettings.PRISM_PARAM_FUNCTION); @@ -132,7 +135,7 @@ public final class ModelBuilder extends PrismComponent case ExpressionBinaryOp.DIVIDE: return f1.divide(f2); default: - throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented"); + throw new PrismNotSupportedException("For " + mode.engine() + ", analysis with rate/probability of " + expr + " not implemented"); } } else if (expr instanceof ExpressionUnaryOp) { ExpressionUnaryOp unExpr = ((ExpressionUnaryOp) expr); @@ -143,7 +146,7 @@ public final class ModelBuilder extends PrismComponent case ExpressionUnaryOp.PARENTH: return f; default: - throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented"); + throw new PrismNotSupportedException("For " + mode.engine() + ", analysis with rate/probability of " + expr + " not implemented"); } } else if (expr instanceof ExpressionITE){ ExpressionITE iteExpr = (ExpressionITE) expr; @@ -165,7 +168,7 @@ public final class ModelBuilder extends PrismComponent // Do nothing here, exception is thrown below } } - throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented"); + throw new PrismNotSupportedException("For " + mode.engine() + ", analysis with rate/probability of " + expr + " not implemented"); } else if (expr instanceof ExpressionFunc) { // functions (min, max, floor, ...) are supported if // they don't refer to parametric constants in their arguments @@ -178,10 +181,10 @@ public final class ModelBuilder extends PrismComponent return factory.fromBigRational(value); } catch (PrismException e) { // Most likely, a parametric constant occurred. - throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented"); + throw new PrismNotSupportedException("For " + mode.engine() + ", analysis with rate/probability of " + expr + " not implemented"); } } else { - throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented"); + throw new PrismNotSupportedException("For " + mode.engine() + ", analysis with rate/probability of " + expr + " not implemented"); } } @@ -248,7 +251,7 @@ public final class ModelBuilder extends PrismComponent });*/ // Build/return model - mainLog.print("\nBuilding model...\n"); + mainLog.print("\nBuilding model (" + mode.engine() + ")...\n"); long time = System.currentTimeMillis(); ParamModel modelExpl = doModelConstruction(modelGenSym); time = System.currentTimeMillis() - time; diff --git a/prism/src/param/ParamMode.java b/prism/src/param/ParamMode.java new file mode 100644 index 00000000..94b38269 --- /dev/null +++ b/prism/src/param/ParamMode.java @@ -0,0 +1,63 @@ +//============================================================================== +// +// Copyright (c) 2017- +// Authors: +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + + +package param; + +/** Mode (parametric / exact) */ +public enum ParamMode { + /** Parametric analysis mode for the parametric engine */ + PARAMETRIC("parametric"), + /** Exact analysis mode (i.e., using constant functions) for the parametric engine */ + EXACT("exact"); + + /** The mode name */ + private final String name; + + /** Private constructor */ + private ParamMode(String name) + { + this.name = name; + } + + /** Get either "parametric" or "exact", depending on mode. */ + public String toString() + { + return name; + } + + /** Get "parametric engine" or "exact engine", depending on mode. */ + public String engine() + { + return name + " engine"; + } + + /** Get "Parametric engine" or "Exact engine", depending on mode. */ + public String Engine() + { + return name.substring(0,1).toUpperCase() + name.substring(1) + " engine"; + } +} \ No newline at end of file diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 7112dd15..4149a8bf 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -117,6 +117,9 @@ final public class ParamModelChecker extends PrismComponent // Flags/settings + /** The mode (parametric or exact)? */ + private ParamMode mode; + // Verbosity level private int verbosity = 0; @@ -140,10 +143,11 @@ final public class ParamModelChecker extends PrismComponent /** * Constructor */ - public ParamModelChecker(PrismComponent parent) throws PrismException + public ParamModelChecker(PrismComponent parent, ParamMode mode) throws PrismException { super(parent); - + this.mode = mode; + // If present, initialise settings from PrismSettings if (settings != null) { verbosity = settings.getBoolean(PrismSettings.PRISM_VERBOSE) ? 10 : 1; @@ -204,6 +208,11 @@ final public class ParamModelChecker extends PrismComponent constantValues.addValues(propertiesFile.getConstantValues()); } + public ParamMode getMode() + { + return mode; + } + // Model checking functions /** @@ -220,7 +229,7 @@ final public class ParamModelChecker extends PrismComponent constraintChecker = new ConstraintChecker(numRandomPoints); regionFactory = new BoxRegionFactory(functionFactory, constraintChecker, precision, model.getNumStates(), model.getFirstInitialState(), simplifyRegions, splitMethod); - valueComputer = new ValueComputer(this, paramModel, regionFactory, precision, eliminationOrder, bisimType); + valueComputer = new ValueComputer(this, mode, paramModel, regionFactory, precision, eliminationOrder, bisimType); long timer = 0; @@ -247,7 +256,7 @@ final public class ParamModelChecker extends PrismComponent // Store result result = new Result(); vals.clearExceptInit(); - result.setResult(new ParamResult(vals, modelBuilder, functionFactory)); + result.setResult(new ParamResult(mode, vals, modelBuilder, functionFactory)); /* // Output plot to tex file if (paramLower.length == 2) { @@ -315,7 +324,7 @@ final public class ParamModelChecker extends PrismComponent break; default: throw new PrismNotSupportedException("operator \"" + ExpressionBinaryOp.opSymbols[parserOp] - + "\" not currently supported for parametric analyses"); + + "\" not currently supported for " + mode + " analyses"); } return regionOp; } @@ -335,7 +344,7 @@ final public class ParamModelChecker extends PrismComponent break; default: throw new PrismNotSupportedException("operator \"" + ExpressionBinaryOp.opSymbols[parserOp] - + "\" not currently supported for parametric analyses"); + + "\" not currently supported for " + mode + " analyses"); } return regionOp; } @@ -399,13 +408,13 @@ final public class ParamModelChecker extends PrismComponent BigRational exprRat = new BigRational(exprStr); stateValues.setStateValue(state, functionFactory.fromBigRational(exprRat)); } else { - throw new PrismNotSupportedException("model checking expresssion " + expr + " not supported for parametric models"); + throw new PrismNotSupportedException("model checking expresssion " + expr + " not supported for " + mode + " models"); } } else if (exprVar instanceof ExpressionConstant) { ExpressionConstant exprConst = (ExpressionConstant) exprVar; stateValues.setStateValue(state, functionFactory.getVar(exprConst.getName())); } else { - throw new PrismNotSupportedException("cannot handle expression " + expr + " in parametric analysis"); + throw new PrismNotSupportedException("cannot handle expression " + expr + " in " + mode + " analysis"); } } else { if (exprVar.getType() instanceof TypeBool) { @@ -548,7 +557,7 @@ final public class ParamModelChecker extends PrismComponent case MAX: case ARGMIN: case ARGMAX: - throw new PrismNotSupportedException("operation not implemented for parametric models"); + throw new PrismNotSupportedException("operation not implemented for " + mode + " models"); case COUNT: resVals = vals.op(Region.COUNT, bsFilter); break; @@ -565,7 +574,7 @@ final public class ParamModelChecker extends PrismComponent resVals = vals.op(Region.FIRST, bsFilter); break; case RANGE: - throw new PrismNotSupportedException("operation not implemented for parametric models"); + throw new PrismNotSupportedException("operation not implemented for " + mode + " models"); case FORALL: resVals = vals.op(Region.FORALL, bsFilter); break; @@ -873,7 +882,7 @@ final public class ParamModelChecker extends PrismComponent // Compute probabilities if (!expr.getExpression().isSimplePathFormula()) { - throw new PrismNotSupportedException("Parametric engine does not yet handle LTL-style path formulas"); + throw new PrismNotSupportedException(mode.Engine() + " does not yet handle LTL-style path formulas"); } probs = checkProbPathFormulaSimple(model, expr.getExpression(), min, needStates); probs.clearNotNeeded(needStates); @@ -912,7 +921,7 @@ final public class ParamModelChecker extends PrismComponent // Next if (exprTemp.getOperator() == ExpressionTemporal.P_X) { - throw new PrismNotSupportedException("Next operator not supported by parametric engine"); + throw new PrismNotSupportedException("Next operator not supported by " + mode + " engine"); } // Until else if (exprTemp.getOperator() == ExpressionTemporal.P_U) { @@ -948,11 +957,11 @@ final public class ParamModelChecker extends PrismComponent //RegionValues probs; switch (modelType) { case CTMC: - throw new PrismNotSupportedException("Bounded until operator not supported by parametric engine"); + throw new PrismNotSupportedException("Bounded until operator not supported by " + mode + " engine"); case DTMC: - throw new PrismNotSupportedException("Bounded until operator not supported by parametric engine"); + throw new PrismNotSupportedException("Bounded until operator not supported by " + mode + " engine"); case MDP: - throw new PrismNotSupportedException("Bounded until operator not supported by parametric engine"); + throw new PrismNotSupportedException("Bounded until operator not supported by " + mode + " engine"); default: throw new PrismNotSupportedException("Cannot model check for a " + modelType); } @@ -1013,7 +1022,7 @@ final public class ParamModelChecker extends PrismComponent rewards = checkRewardSteady(model, rew, exprTemp, min, needStates); break; default: - throw new PrismNotSupportedException("Parametric engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator"); + throw new PrismNotSupportedException(mode.Engine() + " does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator"); } } else if (expr.getType() instanceof TypePathBool || expr.getType() instanceof TypeBool) { rewards = checkRewardPathFormula(model, rew, expr, min, needStates); @@ -1034,7 +1043,7 @@ final public class ParamModelChecker extends PrismComponent if (Expression.isReach(expr)) { return checkRewardReach(model, rew, (ExpressionTemporal) expr, min, needStates); } else if (Expression.isCoSafeLTLSyntactic(expr, true)) { - throw new PrismNotSupportedException("Parametric engine does not yet support co-safe reward computation"); + throw new PrismNotSupportedException(mode.Engine() + " does not yet support co-safe reward computation"); } else { throw new PrismException("R operator contains a path formula that is not syntactically co-safe: " + expr); } @@ -1052,7 +1061,7 @@ final public class ParamModelChecker extends PrismComponent private RegionValues checkRewardSteady(ParamModel model, ParamRewardStruct rew, ExpressionTemporal expr, boolean min, BitSet needStates) throws PrismException { if (model.getModelType() != ModelType.DTMC && model.getModelType() != ModelType.CTMC) { - throw new PrismNotSupportedException("Parametric long-run average rewards are only supported for DTMCs and CTMCs"); + throw new PrismNotSupportedException(mode.Engine() + " long-run average rewards are only supported for DTMCs and CTMCs"); } RegionValues allTrue = regionFactory.completeCover(true); BitSet needStatesInner = new BitSet(needStates.size()); @@ -1158,7 +1167,7 @@ final public class ParamModelChecker extends PrismComponent RegionValues b = checkExpression(model,expr, needStatesInner); if (model.getModelType() != ModelType.DTMC && model.getModelType() != ModelType.CTMC) { - throw new PrismNotSupportedException("Parametric engine currently only implements steady state for DTMCs and CTMCs."); + throw new PrismNotSupportedException(mode.Engine() + " currently only implements steady state for DTMCs and CTMCs."); } return valueComputer.computeSteadyState(b, min, null); } diff --git a/prism/src/param/ParamResult.java b/prism/src/param/ParamResult.java index 2f0dedd7..10dcbb9f 100644 --- a/prism/src/param/ParamResult.java +++ b/prism/src/param/ParamResult.java @@ -48,6 +48,8 @@ import prism.PrismNotSupportedException; */ public class ParamResult { + /** The computation mode (parametric / exact) */ + private ParamMode mode; /** The actual result */ private RegionValues regionValues; /** The model builder (for accessing expr2func) */ @@ -61,8 +63,9 @@ public class ParamResult * @param modelBuilder the model builder used during checking * @param factory the function factory used during checking */ - public ParamResult(RegionValues regionValues, ModelBuilder modelBuilder, FunctionFactory factory) + public ParamResult(ParamMode mode, RegionValues regionValues, ModelBuilder modelBuilder, FunctionFactory factory) { + this.mode = mode; this.regionValues = regionValues; this.modelBuilder = modelBuilder; this.factory = factory; @@ -98,7 +101,7 @@ public class ParamResult public Object getSimpleResult(Type propertyType) throws PrismException { if (regionValues.getNumRegions() != 1) - throw new PrismException("Unexpected result from parametric model checker"); + throw new PrismException("Unexpected result from " + mode + " model checker"); if (propertyType.equals(TypeBool.getInstance())) { // boolean result @@ -163,7 +166,7 @@ public class ParamResult private boolean test(Type propertyType, Expression expected, String strExpected) throws PrismException { if (regionValues.getNumRegions() != 1) { - throw new PrismNotSupportedException("Testing parametric results with multiple regions not supported"); + throw new PrismNotSupportedException("Testing " + mode + " results with multiple regions not supported"); } if (propertyType.equals(TypeBool.getInstance())) { @@ -180,7 +183,7 @@ public class ParamResult try { funcExpected = modelBuilder.expr2function(factory, expected); } catch (PrismException e) { - throw new PrismException("Invalid (or unsupported) RESULT specification \"" + strExpected + "\" for parametric property"); + throw new PrismException("Invalid (or unsupported) RESULT specification \"" + strExpected + "\" for " + mode + " property"); } param.Function func = regionValues.getResult(0).getInitStateValueAsFunction(); diff --git a/prism/src/param/ValueComputer.java b/prism/src/param/ValueComputer.java index 2cdfcfa2..8c1f45dc 100644 --- a/prism/src/param/ValueComputer.java +++ b/prism/src/param/ValueComputer.java @@ -226,6 +226,7 @@ final class ValueComputer extends PrismComponent } } + private ParamMode mode; private ParamModel model; private RegionFactory regionFactory; private FunctionFactory functionFactory; @@ -236,8 +237,9 @@ final class ValueComputer extends PrismComponent private StateEliminator.EliminationOrder eliminationOrder; private Lumper.BisimType bisimType; - ValueComputer(PrismComponent parent, ParamModel model, RegionFactory regionFactory, BigRational precision, StateEliminator.EliminationOrder eliminationOrder, Lumper.BisimType bisimType) { + ValueComputer(PrismComponent parent, ParamMode mode, ParamModel model, RegionFactory regionFactory, BigRational precision, StateEliminator.EliminationOrder eliminationOrder, Lumper.BisimType bisimType) { super(parent); + this.mode = mode; this.model = model; this.regionFactory = regionFactory; this.functionFactory = regionFactory.getFunctionFactory(); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index e9be3172..6f38b966 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3159,9 +3159,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener String[] paramLowerBounds = new String[] { "0" }; String[] paramUpperBounds = new String[] { "1" }; // And execute parameteric model checking - param.ModelBuilder builder = new ModelBuilder(this); + param.ModelBuilder builder = new ModelBuilder(this, param.ParamMode.EXACT); ParamModel modelExpl = builder.constructModel(new ModulesFileModelGeneratorSymbolic(currentModulesFile, this), paramNames, paramLowerBounds, paramUpperBounds); - ParamModelChecker mc = new ParamModelChecker(this); + ParamModelChecker mc = new ParamModelChecker(this, param.ParamMode.EXACT); mc.setModelBuilder(builder); mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds); mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile); @@ -3233,9 +3233,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener if (definedPFConstants != null && definedPFConstants.getNumValues() > 0) mainLog.println("Property constants: " + definedPFConstants); - param.ModelBuilder builder = new ModelBuilder(this); + param.ModelBuilder builder = new ModelBuilder(this, param.ParamMode.PARAMETRIC); ParamModel modelExpl = builder.constructModel(new ModulesFileModelGeneratorSymbolic(currentModulesFile, this), paramNames, paramLowerBounds, paramUpperBounds); - ParamModelChecker mc = new ParamModelChecker(this); + ParamModelChecker mc = new ParamModelChecker(this, param.ParamMode.PARAMETRIC); mc.setModelBuilder(builder); mc.setParameters(paramNames, paramLowerBounds, paramUpperBounds); mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile);