Robust/src/Analysis/Disjoint/SMFEState.java

   1 package Analysis.Disjoint;
   2
   3 import java.util.*;
   4 import java.io.*;
   5
   6 import IR.*;
   7 import IR.Flat.*;
   8
   9 //////////////////////////////////////////////
  10 //
  11 //  SMFEState is part of a
  12 //  (S)tate (M)achine (F)or (E)ffects.
  13 //
  14 //  StateMachineForEffects describes an intial
  15 //  state and the effect transtions a DFJ
  16 //  traverser should make from the current state
  17 //  when searching for possible runtime conflicts.
  18 //
  19 //////////////////////////////////////////////
  20
  21 public class SMFEState {
  22
  23   // uniquely identifies this state
  24   protected FlatNode id;
  25
  26   // all possible effects in this state
  27   protected Set<Effect> effects;
  28
  29   // the given effect allows a transition to a
  30   // set of new states
  31   protected Hashtable< Effect, Set<SMFEState> > e2states;
  32
  33
  34   public SMFEState( FlatNode id ) {
  35     this.id = id;
  36     effects  = new HashSet<Effect>();
  37     e2states = new Hashtable< Effect, Set<SMFEState> >();
  38   }
  39
  40   public void addEffect( Effect e ) {
  41     effects.add( e );
  42   }
  43
  44   // the given effect allows the transition to the new state
  45   public void addTransition( Effect    effect,
  46                              SMFEState stateTo
  47                              ) {
  48
  49     Set<SMFEState> states = e2states.get( effect );
  50     if( states == null ) {
  51       states = new HashSet<SMFEState>();
  52       e2states.put( effect, states );
  53     }
  54     states.add( stateTo );
  55   }
  56
  57   public FlatNode getID() {
  58     return id;
  59   }
  60
  61
  62   public boolean equals( Object o ) {
  63     if( o == null ) {
  64       return false;
  65     }
  66
  67     if( !(o instanceof SMFEState) ) {
  68       return false;
  69     }
  70
  71     SMFEState state = (SMFEState) o;
  72
  73     return id.equals( state.id );
  74   }
  75
  76   public int hashCode() {
  77     return id.hashCode();
  78   }
  79
  80
  81   public String toStringDOT() {
  82
  83     // first create the state as a node in DOT graph
  84     String s = "  "+id.nodeid+
  85       "[shape=box,label=\"";
  86
  87     if( effects.size() == 1 ) {
  88       s += effects.iterator().next().toString();
  89
  90     } else if( effects.size() > 1 ) {
  91
  92       Iterator<Effect> eItr = effects.iterator();
  93       while( eItr.hasNext() ) {
  94         Effect e = eItr.next();
  95         s += e.toString();
  96
  97         if( eItr.hasNext() ) {
  98           s += "\\n";
  99         }
 100       }
 101     }
 102
 103     s += "\"];";
 104
 105     // then each transition is an edge
 106     Iterator<Effect> eItr = e2states.keySet().iterator();
 107     while( eItr.hasNext() ) {
 108       Effect         e      = eItr.next();
 109       Set<SMFEState> states = e2states.get( e );
 110
 111       Iterator<SMFEState> sItr = states.iterator();
 112       while( sItr.hasNext() ) {
 113         SMFEState state = sItr.next();
 114
 115         s += "\n  "+
 116           id.nodeid+" -> "+state.id.nodeid+
 117           "[label=\""+e+"\"];";
 118       }
 119     }
 120
 121     return s;
 122   }
 123 }