diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 9b4bf763..5b161683 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -107,6 +107,42 @@ public abstract class Expression extends ASTElement accept(visitor); } + /** + * Determine whether expression is a valid "simple" path formula , i.e. a formula + * that could occur in the P operator of a PCTL/CSL formula (not LTL, PCTL*). + * This is defined as a single instance of a temporal operator (X, U, F, etc.), + * possibly negated. Strictly speaking, negations are not allowed in PCTL/CSL + * but they can always be converted to a dual formula which is. + */ + public boolean isSimplePathFormula() throws PrismLangException + { + // One (or more) top-level negations is allowed. + // Top-level parentheses also OK. + if (this instanceof ExpressionUnaryOp) { + ExpressionUnaryOp expr = (ExpressionUnaryOp) this; + int op = expr.getOperator(); + if (op == ExpressionUnaryOp.NOT || op == ExpressionUnaryOp.PARENTH) { + return expr.getOperand().isSimplePathFormula(); + } else { + return false; + } + } + // Otherwise, must be a temporal operator. + else if (this instanceof ExpressionTemporal) { + ExpressionTemporal expr = (ExpressionTemporal) this; + // And children, if present, must be state (not path) formulas + if (expr.getOperand1() != null && expr.getOperand1().getType() != Expression.BOOLEAN) { + return false; + } + if (expr.getOperand2() != null && expr.getOperand2().getType() != Expression.BOOLEAN) { + return false; + } + return true; + } + // Default: false. + return false; + } + // evaluate to an int // any typing issues cause an exception // [does nothing to the expression itself] diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index bd44a22b..d3475134 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -213,11 +213,11 @@ public class TypeCheck extends ASTTraverse case ExpressionBinaryOp.IMPLIES: case ExpressionBinaryOp.OR: case ExpressionBinaryOp.AND: - if (t1 != Expression.BOOLEAN) { + if (t1 != Expression.BOOLEAN && t1 != Expression.PATH_BOOLEAN) { throw new PrismLangException("Type error: " + e.getOperatorSymbol() + " applied to non-Boolean expression", e.getOperand1()); } - if (t2 != Expression.BOOLEAN) { + if (t2 != Expression.BOOLEAN && t2 != Expression.PATH_BOOLEAN) { throw new PrismLangException("Type error: " + e.getOperatorSymbol() + " applied to non-Boolean expression", e.getOperand2()); } @@ -225,6 +225,14 @@ public class TypeCheck extends ASTTraverse break; case ExpressionBinaryOp.EQ: case ExpressionBinaryOp.NE: + if (!(t1 == Expression.BOOLEAN || t1 == Expression.INT || t1 == Expression.DOUBLE)) { + throw new PrismLangException("Type error: " + e.getOperatorSymbol() + + " can only compare Boolean, ints or doubles", e.getOperand1()); + } + if (!(t2 == Expression.BOOLEAN || t2 == Expression.INT || t2 == Expression.DOUBLE)) { + throw new PrismLangException("Type error: " + e.getOperatorSymbol() + + " can only compare Boolean, ints or doubles", e.getOperand2()); + } if ((t1 == Expression.BOOLEAN && t2 != Expression.BOOLEAN) || (t2 == Expression.BOOLEAN && t1 != Expression.BOOLEAN)) { throw new PrismLangException("Type error: Can't compare Booleans with ints/doubles", e); @@ -235,33 +243,37 @@ public class TypeCheck extends ASTTraverse case ExpressionBinaryOp.GE: case ExpressionBinaryOp.LT: case ExpressionBinaryOp.LE: - if (!((t1 == Expression.INT || t1 == Expression.DOUBLE) && (t2 == Expression.INT || t2 == Expression.DOUBLE))) { + if (!(t1 == Expression.INT || t1 == Expression.DOUBLE)) { + throw new PrismLangException("Type error: " + e.getOperatorSymbol() + + " can only compare ints or doubles", e.getOperand1()); + } + if (!(t2 == Expression.INT || t2 == Expression.DOUBLE)) { throw new PrismLangException("Type error: " + e.getOperatorSymbol() - + " can only compare ints or doubles", e); + + " can only compare ints or doubles", e.getOperand2()); } e.setType(Expression.BOOLEAN); break; case ExpressionBinaryOp.PLUS: case ExpressionBinaryOp.MINUS: case ExpressionBinaryOp.TIMES: - if (t1 == Expression.BOOLEAN) { - throw new PrismLangException( - "Type error: " + e.getOperatorSymbol() + " cannot be applied to Boolean", e.getOperand1()); + if (!(t1 == Expression.INT || t1 == Expression.DOUBLE)) { + throw new PrismLangException("Type error: " + e.getOperatorSymbol() + + " can only be applied to ints or doubles", e.getOperand1()); } - if (t2 == Expression.BOOLEAN) { - throw new PrismLangException( - "Type error: " + e.getOperatorSymbol() + " cannot be applied to Boolean", e.getOperand2()); + if (!(t2 == Expression.INT || t2 == Expression.DOUBLE)) { + throw new PrismLangException("Type error: " + e.getOperatorSymbol() + + " can only be applied to ints or doubles", e.getOperand2()); } e.setType(t1 == Expression.DOUBLE || t2 == Expression.DOUBLE ? Expression.DOUBLE : Expression.INT); break; case ExpressionBinaryOp.DIVIDE: - if (t1 == Expression.BOOLEAN) { - throw new PrismLangException( - "Type error: " + e.getOperatorSymbol() + " cannot be applied to Boolean", e.getOperand1()); + if (!(t1 == Expression.INT || t1 == Expression.DOUBLE)) { + throw new PrismLangException("Type error: " + e.getOperatorSymbol() + + " can only be applied to ints or doubles", e.getOperand1()); } - if (t2 == Expression.BOOLEAN) { - throw new PrismLangException( - "Type error: " + e.getOperatorSymbol() + " cannot be applied to Boolean", e.getOperand2()); + if (!(t2 == Expression.INT || t2 == Expression.DOUBLE)) { + throw new PrismLangException("Type error: " + e.getOperatorSymbol() + + " can only be applied to ints or doubles", e.getOperand2()); } e.setType(Expression.DOUBLE); break; @@ -274,7 +286,7 @@ public class TypeCheck extends ASTTraverse switch (e.getOperator()) { case ExpressionUnaryOp.NOT: - if (t != Expression.BOOLEAN) { + if (t != Expression.BOOLEAN && t != Expression.PATH_BOOLEAN) { throw new PrismLangException("Type error: " + e.getOperatorSymbol() + " applied to non-Boolean expression", e.getOperand()); } @@ -282,8 +294,8 @@ public class TypeCheck extends ASTTraverse break; case ExpressionUnaryOp.MINUS: if (!(t == Expression.INT || t == Expression.DOUBLE)) { - throw new PrismLangException( - "Type error: " + e.getOperatorSymbol() + " cannot be applied to Boolean", e.getOperand()); + throw new PrismLangException("Type error: " + e.getOperatorSymbol() + + " can only be applied to ints or doubles", e.getOperand()); } e.setType(t); break; diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 4e0af91b..6921f114 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -115,7 +115,8 @@ public class NondetModelChecker extends StateModelChecker // Filter out non-reachable states from solution // (only necessary for symbolically stored vectors) - if (res instanceof StateProbsMTBDD) res.filter(reach); + if (res instanceof StateProbsMTBDD) + res.filter(reach); return res; } @@ -303,18 +304,34 @@ public class NondetModelChecker extends StateModelChecker // Contents of a P operator - protected StateProbs checkProbPathExpression(Expression expr, boolean qual, boolean min) + protected StateProbs checkProbPathExpression(Expression expr, boolean qual, boolean min) throws PrismException + { + // Test whether this is a simple path formula (i.e. PCTL) + // and then pass control to appropriate method. + if (expr.isSimplePathFormula()) { + return checkProbPathExpressionSimple(expr, qual, min); + } else { + throw new PrismException("LTL-style path formulas are not supported"); + } + } + + protected StateProbs checkProbPathExpressionSimple(Expression expr, boolean qual, boolean min) throws PrismException { StateProbs probs = null; - // Logical operators + // Negation/parentheses if (expr instanceof ExpressionUnaryOp) { ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr; + // Parentheses + if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) { + // Recurse + probs = checkProbPathExpressionSimple(exprUnary.getOperand(), qual, min); + } // Negation - if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { + else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { // Flip min/max, then subtract from 1 - probs = checkProbPathExpression(exprUnary.getOperand(), qual, !min); + probs = checkProbPathExpressionSimple(exprUnary.getOperand(), qual, !min); probs.subtractFromOne(); } } @@ -335,7 +352,7 @@ public class NondetModelChecker extends StateModelChecker } // Anything else - convert to until and recurse else { - probs = checkProbPathExpression(exprTemp.convertToUntilForm(), qual, min); + probs = checkProbPathExpressionSimple(exprTemp.convertToUntilForm(), qual, min); } } diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 8216e4d6..cabf8df5 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -125,7 +125,8 @@ public class ProbModelChecker extends StateModelChecker // Filter out non-reachable states from solution // (only necessary for symbolically stored vectors) - if (res instanceof StateProbsMTBDD) res.filter(reach); + if (res instanceof StateProbsMTBDD) + res.filter(reach); return res; } @@ -170,7 +171,7 @@ public class ProbModelChecker extends StateModelChecker // Print a warning if Pmin/Pmax used if (relOp.equals("min=") || relOp.equals("max=")) { - mainLog.print("\nWarning: \"Pmin=?\" and \"Pmax=?\" operators are identical to \"P=?\" for DTMCs\n"); + mainLog.print("\nWarning: \"Pmin=?\" and \"Pmax=?\" operators are identical to \"P=?\" for DTMCs/CTMCs\n"); } // Compute probabilities @@ -257,7 +258,7 @@ public class ProbModelChecker extends StateModelChecker // print a warning if Rmin/Rmax used if (relOp.equals("min=") || relOp.equals("max=")) { - mainLog.print("\nWarning: \"Rmin=?\" and \"Rmax=?\" operators are identical to \"R=?\" for DTMCs\n"); + mainLog.print("\nWarning: \"Rmin=?\" and \"Rmax=?\" operators are identical to \"R=?\" for DTMCs/CTMCs\n"); } // compute rewards @@ -506,16 +507,32 @@ public class ProbModelChecker extends StateModelChecker // Contents of a P operator protected StateProbs checkProbPathExpression(Expression expr, boolean qual) throws PrismException + { + // Test whether this is a simple path formula (i.e. PCTL) + // and then pass control to appropriate method. + if (expr.isSimplePathFormula()) { + return checkProbPathExpressionSimple(expr, qual); + } else { + throw new PrismException("LTL-style path formulas are not supported"); + } + } + + protected StateProbs checkProbPathExpressionSimple(Expression expr, boolean qual) throws PrismException { StateProbs probs = null; - // Logial operators + // Negation/parentheses if (expr instanceof ExpressionUnaryOp) { ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr; + // Parentheses + if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) { + // Recurse + probs = checkProbPathExpressionSimple(exprUnary.getOperand(), qual); + } // Negation - if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { + else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { // Compute, then subtract from 1 - probs = checkProbPathExpression(exprUnary.getOperand(), qual); + probs = checkProbPathExpressionSimple(exprUnary.getOperand(), qual); probs.subtractFromOne(); } } @@ -536,7 +553,7 @@ public class ProbModelChecker extends StateModelChecker } // Anything else - convert to until and recurse else { - probs = checkProbPathExpression(exprTemp.convertToUntilForm(), qual); + probs = checkProbPathExpressionSimple(exprTemp.convertToUntilForm(), qual); } } @@ -1580,7 +1597,7 @@ public class ProbModelChecker extends StateModelChecker // compute steady-state probabilities - // tr = the rate matrix for the whole ctmc + // tr = the rate matrix for the whole Markov chain // states = the subset of reachable states (e.g. bscc) for which // steady-state is to be done