+ // another useful assertion for debugging
+ public boolean noEmptyReachSetsInGraph() {
+
+ Iterator hrnItr = id2hrn.entrySet().iterator();
+ while( hrnItr.hasNext() ) {
+ Map.Entry me = (Map.Entry) hrnItr.next();
+ HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+
+ if( !hrn.isOutOfContext() &&
+ !hrn.isWiped() &&
+ hrn.getAlpha().isEmpty()
+ ) {
+ System.out.println( "!!! "+hrn+" has an empty ReachSet !!!" );
+ return false;
+ }
+
+ Iterator<RefEdge> edgeItr = hrn.iteratorToReferencers();
+ while( edgeItr.hasNext() ) {
+ RefEdge edge = edgeItr.next();
+
+ if( edge.getBeta().isEmpty() ) {
+ System.out.println( "!!! "+edge+" has an empty ReachSet !!!" );
+ return false;
+ }
+ }
+ }
+
+ return true;
+ }
+
+
+ public boolean everyReachStateWTrue() {
+
+ Iterator hrnItr = id2hrn.entrySet().iterator();
+ while( hrnItr.hasNext() ) {
+ Map.Entry me = (Map.Entry) hrnItr.next();
+ HeapRegionNode hrn = (HeapRegionNode) me.getValue();
+
+ {
+ Iterator<ReachState> stateItr = hrn.getAlpha().iterator();
+ while( stateItr.hasNext() ) {
+ ReachState state = stateItr.next();
+
+ if( !state.getPreds().equals( predsTrue ) ) {
+ return false;
+ }
+ }
+ }
+
+ Iterator<RefEdge> edgeItr = hrn.iteratorToReferencers();
+ while( edgeItr.hasNext() ) {
+ RefEdge edge = edgeItr.next();
+
+ Iterator<ReachState> stateItr = edge.getBeta().iterator();
+ while( stateItr.hasNext() ) {
+ ReachState state = stateItr.next();
+
+ if( !state.getPreds().equals( predsTrue ) ) {
+ return false;
+ }
+ }
+ }
+ }
+
+ return true;
+ }
+
+