From a81aec5199f02efc4d4fdfdc1d0f3a277362deb9 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 23 Feb 2016 16:36:51 +0000
Subject: [PATCH] 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 | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/prism/src/parser/visitor/Simplify.java b/prism/src/parser/visitor/Simplify.java
index e4c91398..bb339268 100644
--- a/prism/src/parser/visitor/Simplify.java
+++ b/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;