Added model checking of negated temporal operators (not simulator).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@736 bbc10eb1-c90d-0410-af57-cb519fbb1720

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]

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;

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

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