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

@@ -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;
 	}
 	

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";
 		}
 	}
 	

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:

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() + "\"");