From 0d4ea5b904348953d62d1e960212e3198a152d26 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 7 Dec 2015 21:05:02 +0000
Subject: [PATCH] Simplify parsing of filter operators in ExpressionFilter.
 [from Steffen Marcker]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11015 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/ast/ExpressionFilter.java | 42 ++++++++--------------
 1 file changed, 14 insertions(+), 28 deletions(-)

diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java
index 20fa1155..b6dc597c 100644
--- a/prism/src/parser/ast/ExpressionFilter.java
+++ b/prism/src/parser/ast/ExpressionFilter.java
@@ -108,38 +108,24 @@ public class ExpressionFilter extends Expression
 
 	public void setOperator(String opName)
 	{
-		this.opName = opName;
-		if (opName.equals("min"))
-			opType = FilterOperator.MIN;
-		else if (opName.equals("max"))
-			opType = FilterOperator.MAX;
-		else if (opName.equals("argmin"))
-			opType = FilterOperator.ARGMIN;
-		else if (opName.equals("argmax"))
-			opType = FilterOperator.ARGMAX;
-		else if (opName.equals("count"))
-			opType = FilterOperator.COUNT;
-		else if (opName.equals("sum") || opName.equals("+"))
+		for (FilterOperator op : FilterOperator.values()) {
+			if (opName.equalsIgnoreCase(op.name())) {
+				opType = op;
+				return;
+			}
+		}
+		// handle shorthands
+		if ("+".equals(opName)) {
 			opType = FilterOperator.SUM;
-		else if (opName.equals("avg"))
-			opType = FilterOperator.AVG;
-		else if (opName.equals("first"))
-			opType = FilterOperator.FIRST;
-		else if (opName.equals("range"))
-			opType = FilterOperator.RANGE;
-		else if (opName.equals("forall") || opName.equals("&"))
+		} else if ("&".equals(opName)) {
 			opType = FilterOperator.FORALL;
-		else if (opName.equals("exists") || opName.equals("|"))
+		} else if ("|".equals(opName)) {
 			opType = FilterOperator.EXISTS;
-		else if (opName.equals("print"))
-			opType = FilterOperator.PRINT;
-		else if (opName.equals("printall"))
-			opType = FilterOperator.PRINTALL;
-		else if (opName.equals("state"))
-			opType = FilterOperator.STATE;
-		else opType = null;
+		} else {
+			opType = null;
+		}
 	}
-	
+
 	public void setOperand(Expression operand)
 	{
 		this.operand = operand;