Refactoring: Expression.convertSimplePathFormulaToCanonicalForm(), converts to (negated) a U b or X a. Use in model checkers. [Joachim Klein]

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

prism/src/explicit/ProbModelChecker.java

@@ -570,27 +570,22 @@ public class ProbModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkProbPathFormulaSimple(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
+		boolean negated = false;
 		StateValues probs = null;
 
-		// Negation/parentheses
-		if (expr instanceof ExpressionUnaryOp) {
-			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
-			// Parentheses
-			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
-				// Recurse
-				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), minMax, statesOfInterest);
-			}
+		expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
+
 		// Negation
-			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
-				// Compute, then subtract from 1 
-				probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), minMax.negate(), statesOfInterest);
-				probs.timesConstant(-1.0);
-				probs.plusConstant(1.0);
+		if (expr instanceof ExpressionUnaryOp &&
+		    ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {
+			negated = true;
+			minMax = minMax.negate();
+			expr = ((ExpressionUnaryOp)expr).getOperand();
 		}
-		}
-		// Temporal operators
-		else if (expr instanceof ExpressionTemporal) {
+
+		if (expr instanceof ExpressionTemporal) {
  			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
+
 			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
 				probs = checkProbNext(model, exprTemp, minMax, statesOfInterest);
@@ -603,15 +598,17 @@ public class ProbModelChecker extends NonProbModelChecker
 					probs = checkProbUntil(model, exprTemp, minMax, statesOfInterest);
 				}
 			}
-			// Anything else - convert to until and recurse
-			else {
-				probs = checkProbPathFormulaSimple(model, exprTemp.convertToUntilForm(), minMax, statesOfInterest);
-			}
 		}
 
 		if (probs == null)
 			throw new PrismException("Unrecognised path operator in P operator");
 
+		if (negated) {
+			// Subtract from 1 for negation
+			probs.timesConstant(-1.0);
+			probs.plusConstant(1.0);
+		}
+
 		return probs;
 	}
 

prism/src/parser/ast/Expression.java

@@ -716,6 +716,78 @@ public abstract class Expression extends ASTElement
 		}
 		return false;
 	}
+
+	/**
+	 * Converts an Expression that is a simple path formula to a canonical form:
+	 * Either a single non-negated next-step operator
+	 * or a single until-operator, optionally preceded by a single negation.
+	 * Parentheses are removed.
+	 * @param expr the simple path formula
+	 * @return the canonical expression
+	 */
+	public static Expression convertSimplePathFormulaToCanonicalForm(Expression expr) throws PrismLangException
+	{
+		boolean negated = false;
+
+		if (!expr.isSimplePathFormula()) {
+			throw new PrismLangException("Expression is not a simple path formula.");
+		}
+
+		// Negation/parentheses
+		while (expr instanceof ExpressionUnaryOp) {
+			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
+			// remove parentheses
+			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
+				expr = exprUnary.getOperand();
+			}
+			// deal with negation
+			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
+				negated = !negated;
+				expr = exprUnary.getOperand();
+			} else {
+				throw new PrismLangException("Expression is not a simple path formula: Unexpected unary operator "+exprUnary.getOperatorSymbol());
+			}
+		}
+
+		// Temporal operator
+		if (expr instanceof ExpressionTemporal) {
+			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
+			// Next
+			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
+				if (negated) {
+					if (exprTemp.hasBounds()) throw new PrismLangException("Next-Step operator should not have bounds!");
+
+					// ! X expr  <=> X ! expr
+					return new ExpressionTemporal(ExpressionTemporal.P_X, null,
+					                              Expression.Not(Expression.Parenth(exprTemp.getOperand2())));
+				} else {
+					// X expr
+					return exprTemp;
+				}
+			} else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
+				// Until
+				expr = exprTemp;
+			} else {
+				// other operators: convert
+				expr = exprTemp.convertToUntilForm();
+			}
+		} else {
+			throw new PrismLangException("Expression is not a simple path formula: Unsupported expression "+expr.toString());
+		}
+
+		if (negated) {
+			if (expr instanceof ExpressionUnaryOp &&
+			    ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {
+				// remove the outer negation
+				return ((ExpressionUnaryOp)expr).getOperand();
+			} else {
+				// negate
+				return Expression.Not(expr);
+			}
+		}
+
+		return expr;
+	}
 }
 
 //------------------------------------------------------------------------------

prism/src/prism/NondetModelChecker.java

@@ -667,25 +667,21 @@ public class NondetModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual, boolean min) throws PrismException
 	{
+		boolean negated = false;
 		StateValues probs = null;
 
-		// Negation/parentheses
-		if (expr instanceof ExpressionUnaryOp) {
-			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
-			// Parentheses
-			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
-				// Recurse
-				probs = checkProbPathFormulaSimple(exprUnary.getOperand(), qual, min);
-			}
+		expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
+
 		// Negation
-			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
-				// Flip min/max, then subtract from 1
-				probs = checkProbPathFormulaSimple(exprUnary.getOperand(), qual, !min);
-				probs.subtractFromOne();
+		if (expr instanceof ExpressionUnaryOp &&
+		    ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {
+			// mark as negated, switch from min to max and vice versa
+			negated = true;
+			min = !min;
+			expr = ((ExpressionUnaryOp)expr).getOperand();
 		}
-		}
-		// Temporal operators
-		else if (expr instanceof ExpressionTemporal) {
+
+		if (expr instanceof ExpressionTemporal) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
@@ -699,15 +695,16 @@ public class NondetModelChecker extends NonProbModelChecker
 					probs = checkProbUntil(exprTemp, qual, min);
 				}
 			}
-			// Anything else - convert to until and recurse
-			else {
-				probs = checkProbPathFormulaSimple(exprTemp.convertToUntilForm(), qual, min);
-			}
 		}
 
 		if (probs == null)
 			throw new PrismException("Unrecognised path operator in P operator");
 
+		if (negated) {
+			// Subtract from 1 for negation
+			probs.subtractFromOne();
+		}
+
 		return probs;
 	}
 

prism/src/prism/ProbModelChecker.java

@@ -441,25 +441,19 @@ public class ProbModelChecker extends NonProbModelChecker
 
 	protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual) throws PrismException
 	{
+		boolean negated = false;
 		StateValues probs = null;
 
-		// Negation/parentheses
-		if (expr instanceof ExpressionUnaryOp) {
-			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
-			// Parentheses
-			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
-				// Recurse
-				probs = checkProbPathFormulaSimple(exprUnary.getOperand(), qual);
-			}
+		expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
+
 		// Negation
-			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
-				// Compute, then subtract from 1 
-				probs = checkProbPathFormulaSimple(exprUnary.getOperand(), qual);
-				probs.subtractFromOne();
+		if (expr instanceof ExpressionUnaryOp &&
+		    ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {
+			negated = true;
+			expr = ((ExpressionUnaryOp)expr).getOperand();
 		}
-		}
-		// Temporal operators
-		else if (expr instanceof ExpressionTemporal) {
+
+		if (expr instanceof ExpressionTemporal) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
@@ -473,15 +467,16 @@ public class ProbModelChecker extends NonProbModelChecker
 					probs = checkProbUntil(exprTemp, qual);
 				}
 			}
-			// Anything else - convert to until and recurse
-			else {
-				probs = checkProbPathFormulaSimple(exprTemp.convertToUntilForm(), qual);
-			}
 		}
 
 		if (probs == null)
 			throw new PrismException("Unrecognised path operator in P operator");
 
+		if (negated) {
+			// Subtract from 1 for negation
+			probs.subtractFromOne();
+		}
+
 		return probs;
 	}