From e28c7d0c4aa4a1cf287bc46c80bfefcdb00587bd Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 8 Dec 2008 10:52:55 +0000 Subject: [PATCH] Bugfix: output infinite loop when too many satisfying states. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@879 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/StateModelChecker.java | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index b1f5034c..25d78875 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -178,10 +178,11 @@ public class StateModelChecker implements ModelChecker // See if satisfied in all/initial states boolean satAll = states.includesAll(reach); boolean satInit = states.includesAll(start); + int numSat = states.size(); // Print number of satisfying states to log mainLog.print("\nNumber of satisfying states: "); - mainLog.print(states.size()); + mainLog.print(numSat == -1 ? ">"+Integer.MAX_VALUE : ""+numSat); if (satAll) { mainLog.print(" (all)"); } else if (satInit) { @@ -243,9 +244,11 @@ public class StateModelChecker implements ModelChecker JDD.Ref(ddFilter); tmp = JDD.And(tmp, ddFilter); states = new StateListMTBDD(tmp, model); - mainLog.print("There are " + states.size() + " states with this minimum value (+/- " - + termCritParam + ")"); - if (!verbose && states.size() > 10) { + int numSat = states.size(); + mainLog.print("There are "); + mainLog.print(numSat == -1 ? ">"+Integer.MAX_VALUE : ""+numSat); + mainLog.print(" states with this minimum value (+/- " + termCritParam + ")"); + if (!verbose && (numSat == -1 || numSat > 10)) { mainLog .print(".\nThe first 10 states are displayed below. To view them all, use verbose mode.\n"); states.print(mainLog, 10); @@ -263,9 +266,11 @@ public class StateModelChecker implements ModelChecker JDD.Ref(ddFilter); tmp = JDD.And(tmp, ddFilter); states = new StateListMTBDD(tmp, model); - mainLog.print("There are " + states.size() + " states with this maximum value (+/- " - + termCritParam + ")"); - if (!verbose && states.size() > 10) { + int numSat = states.size(); + mainLog.print("There are "); + mainLog.print(numSat == -1 ? ">"+Integer.MAX_VALUE : ""+numSat); + mainLog.print(" states with this maximum value (+/- " + termCritParam + ")"); + if (!verbose && (numSat == -1 || numSat > 10)) { mainLog .print(".\nThe first 10 states are displayed below. To view them all, use verbose mode.\n"); states.print(mainLog, 10);