From 7b8d489ee2b60ec04d634f0204106e2eace3d0ad Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 15 Aug 2016 08:30:01 +0000 Subject: [PATCH] param/exact: support for ITE and functions in probability expressions If-then-else expressions: The if-expression can not refer to a parametric constant. Other functions (min, max, floor, ...): Arguments can not refer to parametric constants and evaluating the function exactly has to be supported. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11615 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/param/ModelBuilder.java | 37 +++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index 28702e4a..22cdb709 100644 --- a/prism/src/param/ModelBuilder.java +++ b/prism/src/param/ModelBuilder.java @@ -35,6 +35,8 @@ import parser.ast.ConstantList; import parser.ast.Expression; import parser.ast.ExpressionBinaryOp; import parser.ast.ExpressionConstant; +import parser.ast.ExpressionFunc; +import parser.ast.ExpressionITE; import parser.ast.ExpressionLiteral; import parser.ast.ExpressionUnaryOp; import parser.ast.ModulesFile; @@ -149,6 +151,41 @@ public final class ModelBuilder extends PrismComponent default: throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented"); } + } else if (expr instanceof ExpressionITE){ + ExpressionITE iteExpr = (ExpressionITE) expr; + // ITE expressions where the if-expression does not + // depend on a parametric constant are supported + if (iteExpr.getOperand1().isConstant()) { + try { + // non-parametric constants and state variable values have + // been already partially expanded, so if this evaluation + // succeeds there are no parametric constants involved + boolean ifValue = iteExpr.getOperand1().evaluateBoolean(); + if (ifValue) { + return expr2function(factory, iteExpr.getOperand2()); + } else { + return expr2function(factory, iteExpr.getOperand3()); + } + } catch (PrismException e) { + // Most likely, a parametric constant occurred. + // Do nothing here, exception is thrown below + } + } + throw new PrismNotSupportedException("parametric 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 + // and can be exactly evaluated + try { + // non-parametric constants and state variable values have + // been already partially expanded, so if this evaluation + // succeeds there are no parametric constants involved + BigRational value = expr.evaluateExact(); + 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"); + } } else { throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented"); }