From 3c44acb8e1ef2b88d6a8a45c83084eca2966bd20 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 28 Feb 2012 20:55:53 +0000 Subject: [PATCH] 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 | 10 ++++++++-- prism/src/parser/ast/ExpressionFilter.java | 5 ++++- prism/src/parser/visitor/TypeCheck.java | 2 ++ prism/src/prism/StateModelChecker.java | 12 +++++++++--- prism/src/prism/StateValuesDV.java | 14 +++++++------- 5 files changed, 30 insertions(+), 13 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 045e441f..976a1f1d 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/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 diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java index f9b839e6..d4fdff38 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, 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; diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index cf54dc70..6c44c4cf 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/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; diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index db5e7c65..48a60d0c 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/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 diff --git a/prism/src/prism/StateValuesDV.java b/prism/src/prism/StateValuesDV.java index 9976c618..f2ab0b87 100644 --- a/prism/src/prism/StateValuesDV.java +++ b/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 {