Simplify: add handling for ExpressionITE (fixes a PTA bug) [by Linda Leuschner]

Add handling for ExpressionITE to Simplify.

Incidentally, this fixes a bug in PTA handling, where guards with an
ITE operation where not properly simplified and thus unsupported, e.g.,
  s=0 ? true : false
as guard.


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

prism/src/parser/visitor/Simplify.java

@@ -166,6 +166,26 @@ public class Simplify extends ASTTraverseModify
 		return e;
 	}
 
+	public Object visit(ExpressionITE e) throws PrismLangException
+	{
+		// Apply recursively
+		e.setOperand1((Expression) (e.getOperand1().accept(this)));
+		e.setOperand2((Expression) (e.getOperand2().accept(this)));
+		e.setOperand3((Expression) (e.getOperand3().accept(this)));
+
+		// If 'if' operand is true, replace with 'then' part
+		if (Expression.isTrue(e.getOperand1())) {
+			return e.getOperand2();
+		}
+
+		// If 'if' operand is false, replace with 'else' part
+		if (Expression.isFalse(e.getOperand1())) {
+			return e.getOperand3();
+		}
+
+		return e;
+	}
+
 	public Object visit(ExpressionFunc e) throws PrismLangException
 	{
 		int i, n;