From 9da9286c8c30472db937d18a1c248ed6e7db3299 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 16 Aug 2016 11:41:00 +0000 Subject: [PATCH] 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 | 6 +----- prism/src/prism/StateModelChecker.java | 5 ----- 2 files changed, 1 insertion(+), 10 deletions(-) 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);