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();