Repair/RepairCompiler/MCC/IR/Termination.java

   1 package MCC.IR;
   2 import java.util.*;
   3 import java.io.*;
   4 import MCC.State;
   5
   6 public class Termination {
   7     HashSet conjunctions;
   8     Hashtable conjunctionmap;
   9
  10     HashSet abstractrepair;
  11     HashSet updatenodes;
  12     HashSet consequencenodes;
  13
  14     HashSet scopenodes;
  15     Hashtable scopesatisfy;
  16     Hashtable scopefalsify;
  17     Hashtable consequence;
  18
  19     State state;
  20
  21     public Termination(State state) {
  22         this.state=state;
  23         conjunctions=new HashSet();
  24         conjunctionmap=new Hashtable();
  25         abstractrepair=new HashSet();
  26         scopenodes=new HashSet();
  27         scopesatisfy=new Hashtable();
  28         scopefalsify=new Hashtable();
  29         consequence=new Hashtable();
  30         updatenodes=new HashSet();
  31         consequencenodes=new HashSet();
  32
  33         generateconjunctionnodes();
  34         generatescopenodes();
  35         generaterepairnodes();
  36         generatedatastructureupdatenodes();
  37
  38         generateabstractedges();
  39         generatescopeedges();
  40         generateupdateedges();
  41
  42         HashSet superset=new HashSet();
  43         superset.addAll(conjunctions);
  44         superset.addAll(abstractrepair);
  45         superset.addAll(updatenodes);
  46         superset.addAll(scopenodes);
  47         superset.addAll(consequencenodes);
  48         try {
  49             GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
  50         } catch (Exception e) {
  51             e.printStackTrace();
  52             System.exit(-1);
  53         }
  54     }
  55
  56     void generateconjunctionnodes() {
  57         Vector constraints=state.vConstraints;
  58         for(int i=0;i<constraints.size();i++) {
  59             Constraint c=(Constraint)constraints.get(i);
  60             DNFConstraint dnf=c.dnfconstraint;
  61             for(int j=0;j<dnf.size();j++) {
  62                 TermNode tn=new TermNode(c,dnf.get(j));
  63                 GraphNode gn=new GraphNode("Conj"+i+"A"+j,
  64                                            "Conj ("+i+","+j+") "+dnf.get(j).name()
  65                                            ,tn);
  66                 conjunctions.add(gn);
  67                 conjunctionmap.put(c,gn);
  68             }
  69         }
  70     }
  71
  72     void generateupdateedges() {
  73         for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
  74             GraphNode gn=(GraphNode)updateiterator.next();
  75             TermNode tn=(TermNode)gn.getOwner();
  76             MultUpdateNode mun=tn.getUpdate();
  77             /* Cycle through the rules to look for possible conflicts */
  78             for(int i=0;i<state.vRules.size();i++) {
  79                 Rule r=(Rule) state.vRules.get(i);
  80                 if (ConcreteInterferes.interferes(mun,r,true)) {
  81                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
  82                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
  83                     gn.addEdge(e);
  84                 }
  85                 if (ConcreteInterferes.interferes(mun,r,false)) {
  86                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
  87                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
  88                     gn.addEdge(e);
  89                 }
  90             }
  91         }
  92     }
  93
  94     void generateabstractedges() {
  95         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
  96             GraphNode gn=(GraphNode)absiterator.next();
  97             TermNode tn=(TermNode)gn.getOwner();
  98             AbstractRepair ar=(AbstractRepair)tn.getAbstract();
  99
 100             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 101                 GraphNode gn2=(GraphNode)conjiterator.next();
 102                 TermNode tn2=(TermNode)gn2.getOwner();
 103                 Conjunction conj=tn2.getConjunction();
 104                 for(int i=0;i<conj.size();i++) {
 105                     DNFPredicate dp=conj.get(i);
 106                     if (AbstractInterferes.interferes(ar,dp)) {
 107                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 108                         gn.addEdge(e);
 109                         break;
 110                     }
 111                 }
 112             }
 113         }
 114     }
 115
 116     void generatescopeedges() {
 117         for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 118             GraphNode gn=(GraphNode)scopeiterator.next();
 119             TermNode tn=(TermNode)gn.getOwner();
 120             ScopeNode sn=tn.getScope();
 121
 122             /* Interference edges with conjunctions */
 123             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 124                 GraphNode gn2=(GraphNode)conjiterator.next();
 125                 TermNode tn2=(TermNode)gn2.getOwner();
 126                 Conjunction conj=tn2.getConjunction();
 127                 for(int i=0;i<conj.size();i++) {
 128                     DNFPredicate dp=conj.get(i);
 129                     if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)) {
 130                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 131                         GraphNode gnconseq=(GraphNode)consequence.get(sn);
 132                         gnconseq.addEdge(e);
 133                         break;
 134                     }
 135                 }
 136             }
 137
 138             /* Now see if this could effect other model defintion rules */
 139             for(int i=0;i<state.vRules.size();i++) {
 140                 Rule r=(Rule) state.vRules.get(i);
 141                 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
 142                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 143                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 144                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 145                     gnconseq.addEdge(e);
 146                 }
 147                 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
 148                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 149                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 150                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 151                     gnconseq.addEdge(e);
 152                 }
 153             }
 154         }
 155     }
 156
 157
 158     void generaterepairnodes() {
 159         for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 160             GraphNode gn=(GraphNode)conjiterator.next();
 161             TermNode tn=(TermNode)gn.getOwner();
 162             Conjunction conj=tn.getConjunction();
 163             for(int i=0;i<conj.size();i++) {
 164                 DNFPredicate dp=conj.get(i);
 165                 int[] array=dp.getPredicate().getRepairs(dp.isNegated());
 166                 Descriptor d=dp.getPredicate().getDescriptor();
 167                 for(int j=0;j<array.length;j++) {
 168                     AbstractRepair ar=new AbstractRepair(dp,array[j],d);
 169                     TermNode tn2=new TermNode(ar);
 170                     GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),tn2);
 171                     GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
 172                     gn.addEdge(e);
 173                     abstractrepair.add(gn2);
 174                 }
 175             }
 176         }
 177     }
 178
 179     void generatedatastructureupdatenodes() {
 180         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 181             GraphNode gn=(GraphNode)absiterator.next();
 182             TermNode tn=(TermNode) gn.getOwner();
 183             AbstractRepair ar=tn.getAbstract();
 184             if (ar.getType()==AbstractRepair.ADDTOSET) {
 185                 generateaddtosetrelation(gn,ar);
 186             } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
 187                 generateremovefromsetrelation(gn,ar);
 188             } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
 189                 generateaddtosetrelation(gn,ar);
 190             } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
 191                 generateremovefromsetrelation(gn,ar);
 192             } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 193                 generatemodifyrelation(gn,ar);
 194             }
 195         }
 196     }
 197
 198     int removefromcount=0;
 199     void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
 200         Vector possiblerules=new Vector();
 201         for(int i=0;i<state.vRules.size();i++) {
 202             Rule r=(Rule) state.vRules.get(i);
 203             if ((r.getInclusion() instanceof SetInclusion)&&
 204                 (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
 205                 possiblerules.add(r);
 206             if ((r.getInclusion() instanceof RelationInclusion)&&
 207                 (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
 208                 possiblerules.add(r);
 209         }
 210         int[] count=new int[possiblerules.size()];
 211         while(remains(count,possiblerules)) {
 212             MultUpdateNode mun=new MultUpdateNode(ar);
 213             boolean goodflag=true;
 214             for(int i=0;i<possiblerules.size();i++) {
 215                 Rule r=(Rule)possiblerules.get(i);
 216                 UpdateNode un=new UpdateNode();
 217                 /* Construct bindings */
 218                 Vector bindings=new Vector();
 219                 constructbindings(bindings, r,true);
 220                 if (count[i]<r.numQuantifiers()) {
 221                     /* Remove quantifier */
 222                     Quantifier q=r.getQuantifier(count[i]);
 223                     if (q instanceof RelationQuantifier) {
 224                         RelationQuantifier rq=(RelationQuantifier)q;
 225                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 226                         toe.td=ReservedTypeDescriptor.INT;
 227                         Updates u=new Updates(toe,true);
 228                         un.addUpdate(u);
 229                     } else if (q instanceof SetQuantifier) {
 230                         SetQuantifier sq=(SetQuantifier)q;
 231                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 232                         eoe.td=ReservedTypeDescriptor.INT;
 233                         Updates u=new Updates(eoe,true);
 234                         un.addUpdate(u);
 235                     } else {goodflag=false;break;}
 236                 } else {
 237                     int c=count[i]-r.numQuantifiers();
 238                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
 239                         goodflag=false;break;
 240                     }
 241                 }
 242                 mun.addUpdate(un);
 243             }
 244             if (goodflag) {
 245                 TermNode tn=new TermNode(mun);
 246                 GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
 247                 GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
 248                 removefromcount++;
 249                 gn.addEdge(e);
 250                 updatenodes.add(gn2);
 251             }
 252             increment(count,possiblerules);
 253         }
 254     }
 255
 256     static void increment(int count[], Vector rules) {
 257         count[0]++;
 258         for(int i=0;i<(rules.size()-1);i++) {
 259             if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
 260                 count[i+1]++;
 261                 count[i]=0;
 262             } else break;
 263         }
 264     }
 265
 266     static boolean remains(int count[], Vector rules) {
 267         for(int i=0;i<rules.size();i++) {
 268             if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
 269                 return false;
 270             }
 271         }
 272         return true;
 273     }
 274
 275     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
 276     }
 277
 278
 279     boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
 280         boolean goodupdate=true;
 281         Inclusion inc=r.getInclusion();
 282         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 283             Quantifier q=(Quantifier)iterator.next();
 284             if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
 285                 VarDescriptor vd=null;
 286                 SetDescriptor set=null;
 287                 if (q instanceof SetQuantifier) {
 288                     vd=((SetQuantifier)q).getVar();
 289                 } else
 290                     vd=((ForQuantifier)q).getVar();
 291                 if(inc instanceof SetInclusion) {
 292                     SetInclusion si=(SetInclusion)inc;
 293                     if ((si.elementexpr instanceof VarExpr)&&
 294                         (((VarExpr)si.elementexpr).getVar()==vd)) {
 295                         /* Can solve for v */
 296                         Binding binding=new Binding(vd,0);
 297                         bindings.add(binding);
 298                     } else
 299                         goodupdate=false;
 300                 } else if (inc instanceof RelationInclusion) {
 301                     RelationInclusion ri=(RelationInclusion)inc;
 302                     boolean f1=true;
 303                     boolean f2=true;
 304                     if ((ri.getLeftExpr() instanceof VarExpr)&&
 305                         (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 306                                 /* Can solve for v */
 307                         Binding binding=new Binding(vd,0);
 308                         bindings.add(binding);
 309                     } else f1=false;
 310                     if ((ri.getRightExpr() instanceof VarExpr)&&
 311                         (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 312                                 /* Can solve for v */
 313                         Binding binding=new Binding(vd,0);
 314                         bindings.add(binding);
 315                     } else f2=false;
 316                     if (!(f1||f2))
 317                         goodupdate=false;
 318                 } else throw new Error("Inclusion not recognized");
 319                 if (!goodupdate)
 320                     if (isremoval) {
 321                         Binding binding=new Binding(vd);
 322                         bindings.add(binding);
 323                         goodupdate=true;
 324                     } else
 325                         break;
 326             } else if (q instanceof RelationQuantifier) {
 327                 RelationQuantifier rq=(RelationQuantifier)q;
 328                 for(int k=0;k<2;k++) {
 329                     VarDescriptor vd=(k==0)?rq.x:rq.y;
 330                     if(inc instanceof SetInclusion) {
 331                         SetInclusion si=(SetInclusion)inc;
 332                         if ((si.elementexpr instanceof VarExpr)&&
 333                             (((VarExpr)si.elementexpr).getVar()==vd)) {
 334                             /* Can solve for v */
 335                             Binding binding=new Binding(vd,0);
 336                             bindings.add(binding);
 337                         } else
 338                             goodupdate=false;
 339                     } else if (inc instanceof RelationInclusion) {
 340                         RelationInclusion ri=(RelationInclusion)inc;
 341                         boolean f1=true;
 342                         boolean f2=true;
 343                         if ((ri.getLeftExpr() instanceof VarExpr)&&
 344                             (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 345                             /* Can solve for v */
 346                             Binding binding=new Binding(vd,0);
 347                             bindings.add(binding);
 348                         } else f1=false;
 349                         if ((ri.getRightExpr() instanceof VarExpr)&&
 350                             (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 351                             /* Can solve for v */
 352                             Binding binding=new Binding(vd,0);
 353                             bindings.add(binding);
 354                         } else f2=false;
 355                         if (!(f1||f2))
 356                             goodupdate=false;
 357                     } else throw new Error("Inclusion not recognized");
 358                     if (!goodupdate)
 359                         if (isremoval) {
 360                             Binding binding=new Binding(vd);
 361                             bindings.add(binding);
 362                             goodupdate=true;
 363                         } else
 364                             break;
 365                 }
 366                 if (!goodupdate)
 367                     break;
 368             } else throw new Error("Quantifier not recognized");
 369         }
 370         return goodupdate;
 371     }
 372
 373     static int addtocount=0;
 374     void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
 375         System.out.println("Attempting to generate add to set");
 376         System.out.println(ar.getPredicate().getPredicate().name());
 377         System.out.println(ar.getPredicate().isNegated());
 378         for(int i=0;i<state.vRules.size();i++) {
 379             Rule r=(Rule) state.vRules.get(i);
 380             /* See if this is a good rule*/
 381             System.out.println(r.getGuardExpr().name());
 382             if ((r.getInclusion() instanceof SetInclusion&&
 383                 ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
 384                 (r.getInclusion() instanceof RelationInclusion&&
 385                  ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
 386
 387                 /* First solve for quantifiers */
 388                 Vector bindings=new Vector();
 389                 /* Construct bindings */
 390                 System.out.println("Attempting to generate add to set: #2");
 391                 if (!constructbindings(bindings,r,false))
 392                     continue;
 393                 System.out.println("Attempting to generate add to set: #3");
 394                 //Generate add instruction
 395                 DNFRule dnfrule=r.getDNFGuardExpr();
 396                 for(int j=0;j<dnfrule.size();j++) {
 397                     Inclusion inc=r.getInclusion();
 398                     UpdateNode un=new UpdateNode();
 399                     un.addBindings(bindings);
 400                     /* Now build update for tuple/set inclusion condition */
 401                     if(inc instanceof SetInclusion) {
 402                         SetInclusion si=(SetInclusion)inc;
 403                         if (!(si.elementexpr instanceof VarExpr)) {
 404                             Updates up=new Updates(si.elementexpr,0);
 405                             un.addUpdate(up);
 406                         } else {
 407                             VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
 408                             if (un.getBinding(vd)==null) {
 409                                 Updates up=new Updates(si.elementexpr,0);
 410                                 un.addUpdate(up);
 411                             }
 412                         }
 413                     } else if (inc instanceof RelationInclusion) {
 414                         RelationInclusion ri=(RelationInclusion)inc;
 415                         if (!(ri.getLeftExpr() instanceof VarExpr)) {
 416                             Updates up=new Updates(ri.getLeftExpr(),0);
 417                             un.addUpdate(up);
 418                         } else {
 419                             VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
 420                             if (un.getBinding(vd)==null) {
 421                                 Updates up=new Updates(ri.getLeftExpr(),0);
 422                                 un.addUpdate(up);
 423                             }
 424                         }
 425                         if (!(ri.getRightExpr() instanceof VarExpr)) {
 426                             Updates up=new Updates(ri.getRightExpr(),1);
 427                             un.addUpdate(up);
 428                         } else {
 429                             VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
 430                             if (un.getBinding(vd)==null) {
 431                                 Updates up=new Updates(ri.getRightExpr(),1);
 432                                 un.addUpdate(up);
 433                             }
 434                         }
 435                     }
 436                     //Finally build necessary updates to satisfy conjunction
 437                     RuleConjunction ruleconj=dnfrule.get(j);
 438                     /* Add in updates for quantifiers */
 439                     System.out.println("Attempting to generate add to set #4");
 440                     if (processquantifers(un, r)&&debugdd()&&
 441                         processconjunction(un,ruleconj)) {
 442                         System.out.println("Attempting to generate add to set #5");
 443                         MultUpdateNode mun=new MultUpdateNode(ar);
 444                         mun.addUpdate(un);
 445                         TermNode tn=new TermNode(mun);
 446                         GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
 447                         GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
 448                         addtocount++;
 449                         gn.addEdge(e);
 450                         updatenodes.add(gn2);}
 451                 }
 452             }
 453         }
 454     }
 455
 456     boolean debugdd() {
 457         System.out.println("Attempting to generate add to set DD");
 458         return true;
 459     }
 460
 461     boolean processquantifers(UpdateNode un, Rule r) {
 462         boolean goodupdate=true;
 463         Inclusion inc=r.getInclusion();
 464         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 465             Quantifier q=(Quantifier)iterator.next();
 466             /* Add quantifier */
 467             /* FIXME: Analysis to determine when this update is necessary */
 468             if (q instanceof RelationQuantifier) {
 469                 RelationQuantifier rq=(RelationQuantifier)q;
 470                 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 471                 toe.td=ReservedTypeDescriptor.INT;
 472                 Updates u=new Updates(toe,false);
 473                 un.addUpdate(u);
 474             } else if (q instanceof SetQuantifier) {
 475                 SetQuantifier sq=(SetQuantifier)q;
 476                 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 477                 eoe.td=ReservedTypeDescriptor.INT;
 478                 Updates u=new Updates(eoe,false);
 479                 un.addUpdate(u);
 480             } else {goodupdate=false; break;}
 481         }
 482         return goodupdate;
 483     }
 484
 485     boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj){
 486         boolean okay=true;
 487         for(int k=0;k<ruleconj.size();k++) {
 488             DNFExpr de=ruleconj.get(k);
 489             Expr e=de.getExpr();
 490             if (e instanceof OpExpr) {
 491                 OpExpr ex=(OpExpr)de.getExpr();
 492                 Opcode op=ex.getOpcode();
 493                 Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
 494                 un.addUpdate(up);
 495             } else if (e instanceof ElementOfExpr) {
 496                 Updates up=new Updates(e,de.getNegation());
 497                 un.addUpdate(up);
 498             } else if (e instanceof TupleOfExpr) {
 499                 Updates up=new Updates(e,de.getNegation());
 500                 un.addUpdate(up);
 501             } else if (e instanceof BooleanLiteralExpr) {
 502                 boolean truth=((BooleanLiteralExpr)e).getValue();
 503                 if (de.getNegation())
 504                     truth=!truth;
 505                 if (!truth) {
 506                     okay=false;
 507                     break;
 508                 }
 509             } else {
 510                 System.out.println(e.getClass().getName());
 511                 throw new Error("Error #213");
 512             }
 513         }
 514         return okay;
 515     }
 516
 517     void generatescopenodes() {
 518         for(int i=0;i<state.vRules.size();i++) {
 519             Rule r=(Rule) state.vRules.get(i);
 520             ScopeNode satisfy=new ScopeNode(r,true);
 521             TermNode tnsatisfy=new TermNode(satisfy);
 522             GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
 523             ConsequenceNode cnsatisfy=new ConsequenceNode();
 524             TermNode ctnsatisfy=new TermNode(cnsatisfy);
 525             GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
 526             consequence.put(satisfy,cgnsatisfy);
 527             GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
 528             gnsatisfy.addEdge(esat);
 529             consequencenodes.add(cgnsatisfy);
 530             scopesatisfy.put(r,gnsatisfy);
 531             scopenodes.add(gnsatisfy);
 532
 533             ScopeNode falsify=new ScopeNode(r,false);
 534             TermNode tnfalsify=new TermNode(falsify);
 535             GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
 536             ConsequenceNode cnfalsify=new ConsequenceNode();
 537             TermNode ctnfalsify=new TermNode(cnfalsify);
 538             GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
 539             consequence.put(falsify,cgnfalsify);
 540             GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
 541             gnfalsify.addEdge(efals);
 542             consequencenodes.add(cgnfalsify);
 543             scopefalsify.put(r,gnfalsify);
 544             scopenodes.add(gnfalsify);
 545         }
 546     }
 547 }