Repair/RepairCompiler/MCC/IR/Termination.java

   1 package MCC.IR;
   2 import java.util.*;
   3 import MCC.State;
   4
   5 public class Termination {
   6     HashSet conjunctions;
   7     Hashtable conjunctionmap;
   8
   9     HashSet abstractrepair;
  10
  11     HashSet scopenodes;
  12     Hashtable scopesatisfy;
  13     Hashtable scopefalsify;
  14
  15     State state;
  16
  17     public Termination(State state) {
  18         this.state=state;
  19         conjunctions=new HashSet();
  20         conjunctionmap=new Hashtable();
  21         abstractrepair=new HashSet();
  22         scopenodes=new HashSet();
  23         scopesatisfy=new Hashtable();
  24         scopefalsify=new Hashtable();
  25
  26         generateconjunctionnodes();
  27         generaterepairnodes();
  28         generateabstractedges();
  29         generatedatastructureupdatenodes();
  30         generatescopenodes();
  31     }
  32
  33     void generateconjunctionnodes() {
  34         Vector constraints=state.vConstraints;
  35         for(int i=0;i<constraints.size();i++) {
  36             Constraint c=(Constraint)constraints.get(i);
  37             DNFConstraint dnf=c.dnfconstraint;
  38             for(int j=0;j<dnf.size();j++) {
  39                 TermNode tn=new TermNode(c,dnf.get(j));
  40                 GraphNode gn=new GraphNode("Conjunction"+i+","+j,tn);
  41                 conjunctions.add(gn);
  42                 conjunctionmap.put(c,gn);
  43             }
  44         }
  45     }
  46
  47     void generateabstractedges() {
  48         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
  49             GraphNode gn=(GraphNode)absiterator.next();
  50             TermNode tn=(TermNode)gn.getOwner();
  51             AbstractRepair ar=(AbstractRepair)tn.getAbstract();
  52
  53             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
  54                 GraphNode gn2=(GraphNode)conjiterator.next();
  55                 TermNode tn2=(TermNode)gn2.getOwner();
  56                 Conjunction conj=tn2.getConjunction();
  57                 for(int i=0;i<conj.size();i++) {
  58                     DNFPredicate dp=conj.get(i);
  59                     if (AbstractInterferes.interferes(ar,dp)) {
  60                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
  61                         gn.addEdge(e);
  62                         break;
  63                     }
  64                 }
  65             }
  66         }
  67     }
  68
  69
  70     void generaterepairnodes() {
  71         for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
  72             GraphNode gn=(GraphNode)conjiterator.next();
  73             TermNode tn=(TermNode)gn.getOwner();
  74             Conjunction conj=tn.getConjunction();
  75             for(int i=0;i<conj.size();i++) {
  76                 DNFPredicate dp=conj.get(i);
  77                 int[] array=dp.getPredicate().getRepairs(dp.isNegated());
  78                 Descriptor d=dp.getPredicate().getDescriptor();
  79                 for(int j=0;j<array.length;j++) {
  80                     AbstractRepair ar=new AbstractRepair(dp,array[j],d);
  81                     TermNode tn2=new TermNode(ar);
  82                     GraphNode gn2=new GraphNode(gn.getLabel()+"-"+i+","+j,tn2);
  83                     GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
  84                     gn.addEdge(e);
  85                     abstractrepair.add(gn2);
  86                 }
  87             }
  88         }
  89     }
  90
  91     void generatedatastructureupdatenodes() {
  92         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
  93             GraphNode gn=(GraphNode)absiterator.next();
  94             TermNode tn=(TermNode) gn.getOwner();
  95             AbstractRepair ar=tn.getAbstract();
  96             if (ar.getType()==AbstractRepair.ADDTOSET) {
  97                 generateaddtoset(ar);
  98             } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
  99                 generateremovefromset(ar);
 100             } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
 101                 generateaddtorelation(ar);
 102             } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
 103                 generateremovefromrelation(ar);
 104             } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 105                 generatemodifyrelation(ar);
 106             }
 107         }
 108     }
 109
 110     void generateaddtoset(AbstractRepair ar) {
 111         for(int i=0;i<state.vRules.size();i++) {
 112             Rule r=(Rule) state.vRules.get(i);
 113             if (r.getInclusion() instanceof SetInclusion) {
 114                 if (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()) {
 115                     //Generate add instruction
 116
 117
 118                 }
 119             }
 120         }
 121     }
 122
 123     void generatescopenodes() {
 124         for(int i=0;i<state.vRules.size();i++) {
 125             Rule r=(Rule) state.vRules.get(i);
 126             ScopeNode satisfy=new ScopeNode(r,true);
 127             TermNode tnsatisfy=new TermNode(satisfy);
 128             GraphNode gnsatisfy=new GraphNode("Satisfy Rule"+i,tnsatisfy);
 129
 130             ScopeNode falsify=new ScopeNode(r,false);
 131             TermNode tnfalsify=new TermNode(falsify);
 132             GraphNode gnfalsify=new GraphNode("Falsify Rule"+i,tnfalsify);
 133             scopesatisfy.put(r,gnsatisfy);
 134             scopefalsify.put(r,gnfalsify);
 135             scopenodes.add(gnsatisfy);
 136             scopenodes.add(gnfalsify);
 137         }
 138     }
 139 }