From 71ca9d28af2cf2eb78c76181a5307f8a2847951d Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 16 May 2011 11:29:26 +0000
Subject: [PATCH] Final (pre-4.0) fixes to filters: added "state" filter, which
 gives result for a filter which must satisfy exactly one state, and make this
 the translation for old-style {state} filter.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2910 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/ast/ExpressionFilter.java |  4 ++-
 prism/src/parser/ast/Filter.java           |  4 +--
 prism/src/parser/visitor/TypeCheck.java    |  2 ++
 prism/src/prism/StateModelChecker.java     | 29 +++++++++++++++++++++-
 4 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java
index 73e94eca..f9b839e6 100644
--- a/prism/src/parser/ast/ExpressionFilter.java
+++ b/prism/src/parser/ast/ExpressionFilter.java
@@ -34,7 +34,7 @@ public class ExpressionFilter extends Expression
 {
 	// Enums for  types of filter
 	public enum FilterOperator {
-		MIN, MAX, ARGMIN, ARGMAX, COUNT, SUM, AVG, FIRST, RANGE, FORALL, EXISTS, PRINT;
+		MIN, MAX, ARGMIN, ARGMAX, COUNT, SUM, AVG, FIRST, RANGE, FORALL, EXISTS, PRINT, STATE;
 	};
 
 	// Operator used in filter
@@ -97,6 +97,8 @@ public class ExpressionFilter extends Expression
 			opType = FilterOperator.EXISTS;
 		else if (opName.equals("print"))
 			opType = FilterOperator.PRINT;
+		else if (opName.equals("state"))
+			opType = FilterOperator.STATE;
 		else opType = null;
 	}
 	
diff --git a/prism/src/parser/ast/Filter.java b/prism/src/parser/ast/Filter.java
index 50811124..b0353ce5 100644
--- a/prism/src/parser/ast/Filter.java
+++ b/prism/src/parser/ast/Filter.java
@@ -36,7 +36,7 @@ public class Filter extends ASTElement
 {
 	private Expression expr = null;
 	// Either "min" or "max", or neither or both.
-	// In the latter two cases, this means "range"
+	// In the latter two cases, this means "state" or "range"
 	private boolean minReq = false;
 	private boolean maxReq = false;
 
@@ -90,7 +90,7 @@ public class Filter extends ASTElement
 		if (minReq) {
 			return maxReq ? "range" : "min";
 		} else {
-			return maxReq ? "max" : "range";
+			return maxReq ? "max" : "state";
 		}
 	}
 	
diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java
index b78edbe2..61103478 100644
--- a/prism/src/parser/visitor/TypeCheck.java
+++ b/prism/src/parser/visitor/TypeCheck.java
@@ -577,6 +577,7 @@ public class TypeCheck extends ASTTraverse
 			break;
 		case FIRST:
 		case PRINT:
+		case STATE:
 			// Anything goes
 			break;
 		default:
@@ -590,6 +591,7 @@ public class TypeCheck extends ASTTraverse
 		case SUM:
 		case FIRST:
 		case PRINT:
+		case STATE:
 			e.setType(t);
 			break;
 		case RANGE:
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 94cc7fee..22a31f1c 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -163,7 +163,7 @@ public class StateModelChecker implements ModelChecker
 				// Result is for the initial state, if there is just one,
 				// or the range over all initial states, if multiple
 				if (model.getNumStartStates() == 1) {
-					exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init"));
+					exprFilter = new ExpressionFilter("state", expr, new ExpressionLabel("init"));
 				} else {
 					exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init"));
 				}
@@ -1248,6 +1248,33 @@ public class StateModelChecker implements ModelChecker
 			// Derefs
 			JDD.Deref(dd);
 			break;
+		case STATE:
+			// Check filter satisfied by exactly one state
+			if (statesFilter.size() != 1) {
+				String s = "Filter should be satisfied in exactly 1 state";
+				s += " (but \"" + filter + "\" is true in " + statesFilter.size() + " states)";
+				throw new PrismException(s);
+			}
+			// Find first (only) value
+			d = vals.firstFromBDD(ddFilter);
+			// Store as object/vector
+			if (expr.getType() instanceof TypeInt) {
+				resObj = new Integer((int) d);
+			} else if (expr.getType() instanceof TypeDouble) {
+				resObj = new Double(d);
+			} else {
+				resObj = new Boolean(d > 0);
+			}
+			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Create explanation of result and print some details to log
+			resultExpl = "Value in ";
+			if (filterInit) {
+				resultExpl += "the initial state";
+			} else {
+				resultExpl += "the filter state";
+			}
+			mainLog.println("\n" + resultExpl + ": " + resObj);
+			break;
 		default:
 			JDD.Deref(ddFilter);
 			throw new PrismException("Unrecognised filter type \"" + expr.getOperatorName() + "\"");