diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 90b1ce3f..9aa2df74 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/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); diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 3a115ebd..3dde5a7f 100644 --- a/prism/src/prism/StateModelChecker.java +++ 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);