1 package Analysis.Disjoint;
8 ///////////////////////////////////////////
10 // This class is an immutable Canonical, so
12 // 0) construct them with a factory pattern
13 // to ensure only canonical versions escape
15 // 1) any operation that modifies a Canonical
16 // is a static method in the Canonical class
18 // 2) operations that just read this object
19 // should be defined here
21 // 3) every Canonical subclass hashCode should
22 // throw an error if the hash ever changes
24 ///////////////////////////////////////////
26 // a reach set is a set of reach states
28 public class ReachSet extends Canonical {
30 protected HashSet<ReachState> reachStates;
33 public static ReachSet factory() {
34 ReachSet out = new ReachSet();
35 out = (ReachSet) Canonical.makeCanonical( out );
39 public static ReachSet factory( ReachState state ) {
41 assert state.isCanonical();
42 ReachSet out = new ReachSet();
43 out.reachStates.add( state );
44 out = (ReachSet) Canonical.makeCanonical( out );
48 protected ReachSet() {
49 reachStates = new HashSet<ReachState>();
53 public Iterator<ReachState> iterator() {
54 return reachStates.iterator();
58 return reachStates.size();
61 public boolean isEmpty() {
62 return reachStates.isEmpty();
65 // this should be a hash table so we can do this by key
66 public ReachState containsIgnorePreds( ReachState state ) {
69 Iterator<ReachState> stateItr = this.reachStates.iterator();
70 while( stateItr.hasNext() ) {
71 ReachState stateThis = stateItr.next();
72 if( stateThis.equalsIgnorePreds( state ) ) {
80 public boolean containsSuperSet( ReachState state ) {
81 return containsSuperSet( state, false );
84 public boolean containsStrictSuperSet( ReachState state ) {
85 return containsSuperSet( state, true );
88 public boolean containsSuperSet( ReachState state,
92 if( !strict && reachStates.contains( state ) ) {
96 Iterator<ReachState> itr = iterator();
97 while( itr.hasNext() ) {
98 ReachState stateThis = itr.next();
100 if( !state.equals( stateThis ) &&
101 state.isSubset( stateThis ) ) {
105 if( state.isSubset( stateThis ) ) {
115 public boolean containsTuple( ReachTuple rt ) {
116 Iterator<ReachState> itr = iterator();
117 while( itr.hasNext() ) {
118 ReachState state = itr.next();
119 if( state.containsTuple( rt ) ) {
126 public ReachSet getStatesWithBoth( ReachTuple rt1,
129 ReachSet out = new ReachSet();
131 Iterator<ReachState> itr = iterator();
132 while( itr.hasNext() ) {
133 ReachState state = itr.next();
134 if( state.containsTuple( rt1 ) &&
135 state.containsTuple( rt2 ) ) {
136 out.reachStates.add( state );
140 out = (ReachSet) Canonical.makeCanonical( out );
144 // used to assert each state in the set is
146 public boolean containsNoDuplicates() {
147 Vector<ReachState> v = new Vector( reachStates );
148 for( int i = 0; i < v.size(); ++i ) {
149 ReachState s1 = v.get( i );
150 for( int j = i+1; j < v.size(); ++j ) {
151 ReachState s2 = v.get( j );
152 if( s1.equals( s2 ) ) {
153 assert s1.isCanonical();
154 assert s2.isCanonical();
163 public boolean equalsSpecific( Object o ) {
168 if( !(o instanceof ReachSet) ) {
172 ReachSet rs = (ReachSet) o;
173 return reachStates.equals( rs.reachStates );
177 public int hashCodeSpecific() {
178 return reachStates.hashCode();
182 public String toStringEscNewline( boolean hideSubsetReachability ) {
185 Iterator<ReachState> i = this.iterator();
186 while( i.hasNext() ) {
187 ReachState state = i.next();
189 // skip this if there is a superset already
190 if( hideSubsetReachability &&
191 containsStrictSuperSet( state ) ) {
206 public String toString() {
207 return toString( false );
210 public String toString( boolean hideSubsetReachability ) {
212 ReachSet toPrint = this;
214 if( hideSubsetReachability ) {
215 // make a new reach set with subset states removed
216 toPrint = ReachSet.factory();
218 Iterator<ReachState> i = this.iterator();
219 while( i.hasNext() ) {
220 ReachState state = i.next();
222 if( containsStrictSuperSet( state ) ) {
226 toPrint = Canonical.add( toPrint, state );
232 Iterator<ReachState> i = toPrint.iterator();
233 while( i.hasNext() ) {
234 ReachState state = i.next();