Remove some output to the log when processing filters (the number of satisfying states reported by this code can be wrong if the model checker optimises and only checks states satisfying the filter).

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

prism/src/explicit/StateModelChecker.java

@@ -1024,11 +1024,7 @@ public class StateModelChecker extends PrismComponent
 		case FORALL:
 			// Get access to BitSet for this
 			bs = vals.getBitSet();
-			// Print some info to log
-			mainLog.print("\nNumber of states satisfying " + expr.getOperand() + ": ");
-			mainLog.print(bs.cardinality());
-			mainLog.println(bs.cardinality() == model.getNumStates() ? " (all in model)" : "");
-			// Check "for all" over filter
+state			// Check "for all" over filter
 			b = vals.forallOverBitSet(bsFilter);
 			// Store as object/vector
 			resObj = new Boolean(b);

prism/src/prism/StateModelChecker.java

@@ -1233,11 +1233,6 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		case FORALL:
 			// Get access to BDD for this
 			dd = vals.convertToStateValuesMTBDD().getJDDNode();
-			// Print some info to log
-			mainLog.print("\nNumber of states satisfying " + expr.getOperand() + ": ");
-			states = new StateListMTBDD(dd, model);
-			mainLog.print(states.sizeString());
-			mainLog.println(states.includesAll(reach) ? " (all in model)" : "");
 			// Check "for all" over filter, store result
 			JDD.Ref(ddFilter);
 			dd = JDD.And(dd, ddFilter);