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

param: store whether the parametric engine is used for exact or parametric analysis, adapt log output / errors

master
Joachim Klein 8 years ago
committed by Dave Parker
parent
135d8e4ac1
commit
2dc08f6fb1
6 changed files with 115 additions and 35 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. 17
      prism/src/param/ModelBuilder.java
  2. 63
      prism/src/param/ParamMode.java
  3. 47
      prism/src/param/ParamModelChecker.java
  4. 11
      prism/src/param/ParamResult.java
  5. 4
      prism/src/param/ValueComputer.java
  6. 8
      prism/src/prism/Prism.java

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

@ -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;

63
prism/src/param/ParamMode.java
View File

@ -0,0 +1,63 @@
//==============================================================================
//
// Copyright (c) 2017-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de> (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";
}
}

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

@ -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);
}

11
prism/src/param/ParamResult.java
View File

@ -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();

4
prism/src/param/ValueComputer.java
View File

@ -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();

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

@ -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);

Write Preview
Loading…
Cancel
Save