Added new printall filter.

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

prism/src/explicit/StateModelChecker.java

@@ -630,6 +630,7 @@ public class StateModelChecker
 		// Compute result according to filter type
 		switch (op) {
 		case PRINT:
+		case PRINTALL:
 			// Format of print-out depends on type
 			if (expr.getType() instanceof TypeBool) {
 				// NB: 'usual' case for filter(print,...) on Booleans is to use no filter
@@ -637,8 +638,13 @@ public class StateModelChecker
 				mainLog.println(filterTrue ? ":" : " that are also in filter " + filter + ":");
 				vals.printFiltered(mainLog, bsFilter);
 			} else {
-				mainLog.println("\nResults (non-zero only) for filter " + filter + ":");
-				vals.printFiltered(mainLog, bsFilter);
+				if (op == FilterOperator.PRINT) {
+					mainLog.println("\nResults (non-zero only) for filter " + filter + ":");
+					vals.printFiltered(mainLog, bsFilter);
+				} else {
+					mainLog.println("\nResults (including zeros) for filter " + filter + ":");
+					vals.printFiltered(mainLog, bsFilter, false, false, true, true);
+				}
 			}
 			// Result vector is unchanged; for ARGMIN, don't store a single value (in resObj)
 			// Also, don't bother with explanation string

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, STATE;
+		MIN, MAX, ARGMIN, ARGMAX, COUNT, SUM, AVG, FIRST, RANGE, FORALL, EXISTS, PRINT, PRINTALL, 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("printall"))
+			opType = FilterOperator.PRINTALL;
 		else if (opName.equals("state"))
 			opType = FilterOperator.STATE;
 		else opType = null;
@@ -180,6 +182,7 @@ public class ExpressionFilter extends Expression
 	{
 		// Most filters return a single value, but there are some exceptions...
 		if (opType == FilterOperator.PRINT) return false;
+		else if (opType == FilterOperator.PRINTALL) return false;
 		else if (opType == FilterOperator.ARGMIN) return false;
 		else if (opType == FilterOperator.ARGMAX) return false;
 		else return true;

prism/src/parser/visitor/TypeCheck.java

@@ -572,6 +572,7 @@ public class TypeCheck extends ASTTraverse
 			break;
 		case FIRST:
 		case PRINT:
+		case PRINTALL:
 		case STATE:
 			// Anything goes
 			break;
@@ -586,6 +587,7 @@ public class TypeCheck extends ASTTraverse
 		case SUM:
 		case FIRST:
 		case PRINT:
+		case PRINTALL:
 		case STATE:
 			e.setType(t);
 			break;

prism/src/prism/StateModelChecker.java

@@ -1050,6 +1050,7 @@ public class StateModelChecker implements ModelChecker
 		op = expr.getOperatorType();
 		switch (op) {
 		case PRINT:
+		case PRINTALL:
 			// Format of print-out depends on type
 			if (expr.getType() instanceof TypeBool) {
 				// NB: 'usual' case for filter(print,...) on Booleans is to use no filter
@@ -1062,10 +1063,15 @@ public class StateModelChecker implements ModelChecker
 				JDD.Deref(dd);
 			} else {
 				// TODO: integer-typed case: either add to print method or store in StateValues
-				mainLog.println("\nResults (non-zero only) for filter " + filter + ":");
-				vals.printFiltered(mainLog, ddFilter);
+				if (op == FilterOperator.PRINT) {
+					mainLog.println("\nResults (non-zero only) for filter " + filter + ":");
+					vals.printFiltered(mainLog, ddFilter);
+				} else {
+					mainLog.println("\nResults (including zeros) for filter " + filter + ":");
+					vals.printFiltered(mainLog, ddFilter, false, false, true);
+				}
 			}
-			// Result vector is unchanged; for ARGMIN, don't store a single value (in resObj)
+			// Result vector is unchanged; for PRINT, don't store a single value (in resObj)
 			// Also, don't bother with explanation string
 			resVals = vals;
 			// Set vals to null to stop it being cleared below

prism/src/prism/StateValuesDV.java

@@ -361,7 +361,7 @@ public class StateValuesDV implements StateValues
 	{
 		print(log, printSparse, printMatlab, printStates, true);
 	}
-	
+
 	/**
 	 * Print vector to a log/file.
 	 * @param log The log
@@ -484,7 +484,7 @@ public class StateValuesDV implements StateValues
 	{
 		printFiltered(log, filter, printSparse, printMatlab, printStates, true);
 	}
-	
+
 	/**
 	 * Print part of a vector to a log/file (non-zero entries only).
 	 * @param log The log
@@ -494,7 +494,8 @@ public class StateValuesDV implements StateValues
 	 * @param printStates Print states (variable values) for each element? 
 	 * @param printIndices Print state indices for each element? 
 	 */
-	public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException
+	public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices)
+			throws PrismException
 	{
 		int i;
 
@@ -627,11 +628,10 @@ public class StateValuesDV implements StateValues
 							outputLog.print(",");
 					}
 					outputLog.print(")");
-				} else {
-					if (printIndices || printStates)
-						outputLog.print("=");
-					outputLog.println(d);
 				}
+				if (printIndices || printStates)
+					outputLog.print("=");
+				outputLog.println(d);
 			}
 			//return true;
 		} else {