Repair/RepairInterpreter/repair.cc

   1 #include <stdlib.h>
   2 #include <stdio.h>
   3 #include "repair.h"
   4 #include "model.h"
   5 #include "normalizer.h"
   6 #include "list.h"
   7 #include "Action.h"
   8 #include "processobject.h"
   9 #include "ActionInSet.h"
  10 #include "ActionNotInSet.h"
  11 #include "ActionGEQ1.h"
  12 #include "ActionEQ1.h"
  13 #include "ActionAssign.h"
  14 #include "ActionNormal.h"
  15 #include "Relation.h"
  16 #include "omodel.h"
  17 #include "dmodel.h"
  18 #include "set.h"
  19 #include "common.h"
  20 #include "fieldcheck.h"
  21 #include "Hashtable.h"
  22
  23 Repair::Repair(model *m) {
  24   globalmodel=m;
  25   removedsentences=NULL;
  26   List *list=new List();
  27   /*  list->addobject(); --build action array */
  28   list->addobject(new ActionGEQ1(m->getdomainrelation(),m));
  29   list->addobject(new ActionEQ1(m->getdomainrelation(),m));
  30   list->addobject(new ActionAssign(m->getdomainrelation(),m));
  31   //  list->addobject(new ActionNotAssign(m->getdomainrelation()));
  32   list->addobject(new ActionInSet(m->getdomainrelation(),m));
  33   list->addobject(new ActionNotInSet(m->getdomainrelation(),m));
  34   numactions=list->size();
  35   repairactions=new Action *[list->size()];
  36   list->toArray((void **)repairactions);
  37   delete(list);
  38 }
  39
  40
  41 void Repair::repaireleexpr(Constraint *c, processobject *po, Elementexpr *ee, Hashtable *env) {
  42   /* We're here because we have a bad elementexpr */
  43   switch(ee->gettype()) {
  44   case ELEMENTEXPR_SUB:
  45   case ELEMENTEXPR_ADD:
  46   case ELEMENTEXPR_MULT:
  47     repaireleexpr(c,po,ee->getleft(),env);
  48     repaireleexpr(c,po,ee->getright(),env);
  49     return;
  50   case ELEMENTEXPR_RELATION: {
  51     /* Could have problem here */
  52     repaireleexpr(c,po,ee->getleft(),env);
  53     Element *e=evaluateexpr(ee,env,globalmodel);
  54     if (e==NULL) {
  55       /* found bad relation */
  56       FieldCheck *fc=globalmodel->getfieldcheck();
  57       char *set=NULL;
  58
  59       {
  60         Elementexpr *left=ee->getleft();
  61         int tleft=left->gettype();
  62         if (tleft==ELEMENTEXPR_LABEL) {
  63           set=getset(c, left->getlabel()->label());
  64         } else if (tleft==ELEMENTEXPR_RELATION) {
  65           DRelation *drl=globalmodel->getdomainrelation()->getrelation(left->getrelation()->getname());
  66           set=drl->getrange();
  67         } else {
  68           ee->print();
  69           printf("Can't determine domain-shouldn't be here because of static analysis...\n");
  70           exit(-1);
  71         }
  72       }
  73
  74       Element *e2=evaluateexpr(ee->getleft(),env,globalmodel);
  75       int index=fc->getindexthatprovides(ee->getrelation()->getname(), set);
  76       Hashtable *env2=new Hashtable((unsigned int (*)(void *)) & hashstring,(int (*)(void *,void *)) &equivalentstrings);
  77       env2->setparent(env);
  78       Constraint *crep=globalmodel->getconstraint(index);
  79       DomainRelation *dr=globalmodel->getdomainrelation();
  80       for(int j=0;j<crep->numquants();j++) {
  81         Quantifier *qrep=crep->getquant(j);
  82         char *label=qrep->getlabel()->label();
  83         char *setname=qrep->getset()->getname();
  84         DomainSet *dset=dr->getset(setname);
  85         if (dset->getset()->contains(e2)) {
  86           env2->put(label,e2);
  87         } else {
  88           env2->put(label,dset->getset()->firstelement()); /*This shouldn't happen right now*/
  89           printf("Funnyness in repair.cc\n");
  90         }
  91       }
  92       this->repairconstraint(globalmodel->getconstraint(index),po,env2);
  93       delete(e2);
  94       delete(env2);
  95     } else
  96       delete(e);
  97     return;
  98   }
  99   default:
 100     return;
 101   }
 102 }
 103
 104
 105 void Repair::repairconstraint(Constraint *c, processobject *po, Hashtable *env) {
 106   NormalForm *nf=globalmodel->getnormalform(c);
 107   CoerceSentence *coercionstate=nf->closestmatch(removedsentences,po,env);
 108   /* Now we just need to coerce the predicates!!!*/
 109   for(int i=0;i<coercionstate->getnumpredicates();i++) {
 110     CoercePredicate *cp=coercionstate->getpredicate(i);
 111     int status=po->processpredicate(cp->getpredicate(),env);
 112     while (status==PFAIL) {
 113       /* Bad dereference...need to fix things*/
 114       repaireleexpr(c, po,cp->getpredicate()->geteleexpr(), env);
 115       status=po->processpredicate(cp->getpredicate(),env);
 116     }
 117
 118     if (status!=cp->getcoercebool()) {
 119       /*Need to coerce*/
 120       Action *act=findrepairaction(cp);
 121       act->repairpredicate(env,cp);
 122       /* Data structure fixed - well eventually*/
 123     }
 124   }
 125 }
 126
 127
 128 // returns the action that can repair the given predicate
 129 Action * Repair::findrepairaction(CoercePredicate *cp) {
 130   for(int i=0;i<numactions;i++) {
 131     if (repairactions[i]->canrepairpredicate(cp))
 132       return repairactions[i];
 133   }
 134   return NULL;
 135 }
 136
 137
 138
 139 // returns the action that can break the given predicate
 140 Action * Repair::findbreakaction(CoercePredicate *cp)
 141 {
 142   return findrepairaction(cp);
 143 }
 144
 145
 146 bool Repair::analyzetermination() {
 147   WorkRelation *wr=new WorkRelation(true);
 148   buildmap(wr);
 149   /* Map built */
 150   WorkSet *cycleset=searchcycles(wr);
 151   if (!cycleset->isEmpty()) {
 152     WorkSet *removeedges=new WorkSet(true);
 153     for(int i=1;i<=cycleset->size();i++) {
 154       if (breakcycles(removeedges, i, cycleset,wr)) {
 155         removedsentences=removeedges;
 156         printf("Modified constraints for repairability!\n");
 157         outputgraph(removeedges, wr, "cycle.dot");
 158         return true;
 159       }
 160     }
 161     delete(removeedges);
 162     return false;
 163   } else {
 164     outputgraph(NULL,wr, "cycle.dot");
 165     return true;
 166   }
 167 }
 168
 169
 170
 171 bool Repair::breakcycles(WorkSet *removeedge, int number, WorkSet *cyclelinks, WorkRelation *wr) {
 172   for(CoerceSentence *cs=(CoerceSentence *)cyclelinks->firstelement();
 173       cs!=NULL;cs=(CoerceSentence *)cyclelinks->getnextelement(cs)) {
 174     if (!removeedge->contains(cs)) {
 175       removeedge->addobject(cs);
 176       if (number==1) {
 177         if (!checkforcycles(removeedge, wr))
 178           return true;
 179       } else {
 180         if (breakcycles(removeedge,number-1,cyclelinks,wr))
 181           return true;
 182       }
 183       removeedge->removeobject(cs);
 184     }
 185   }
 186   return false;
 187 }
 188
 189 void Repair::outputgraph(WorkSet *removededges, WorkRelation *wr, char *filename) {
 190   FILE * dotfile=fopen(filename,"w");
 191   fprintf(dotfile,"digraph cyclegraph {\n");
 192   fprintf(dotfile,"ratio=auto\n");
 193   for(int i=0;i<globalmodel->getnumconstraints();i++) {
 194     NormalForm *nf=globalmodel->getnormalform(i);
 195     fprintf(dotfile, "%lu[label=\"",nf);
 196     nf->fprint(dotfile);
 197     fprintf(dotfile,"\"];\n");
 198     for(int j=0;j<nf->getnumsentences();j++) {
 199       CoerceSentence *cs=nf->getsentence(j);
 200       for(int i=0;i<cs->getnumpredicates();i++) {
 201         CoercePredicate *cp=cs->getpredicate(i);
 202         fprintf(dotfile,"%lu -> %lu [style=dashed]\n",nf,cp);
 203         WorkSet *setofnf=wr->getset(cp);
 204         if (setofnf!=NULL) {
 205           NormalForm *nf2=(NormalForm*)setofnf->firstelement();
 206           while(nf2!=NULL) {
 207             /* cp interferes with nf2 */
 208             bool removed=(removededges!=NULL)&&removededges->contains(cs); /*tells what color of edge to generate*/
 209             if (removed)
 210               fprintf(dotfile,"%lu -> %lu [style=dotted]\n",cp,nf2);
 211             else
 212               fprintf(dotfile,"%lu -> %lu\n",cp,nf2);
 213             nf2=(NormalForm *)setofnf->getnextelement(nf2);
 214           }
 215         }
 216       }
 217     }
 218   }
 219   fprintf(dotfile,"}\n");
 220   fclose(dotfile);
 221 }
 222
 223 bool Repair::checkforcycles(WorkSet *removededges, WorkRelation *wr) {
 224   /* Check that there are no cycles and
 225      that system is solvable */
 226   for(int i=0;i<globalmodel->getnumconstraints();i++) {
 227     NormalForm *nf=globalmodel->getnormalform(i);
 228     bool good=false;
 229     for(int j=0;j<nf->getnumsentences();j++) {
 230       if (!removededges->contains(nf->getsentence(j))) {
 231         CoerceSentence *cs=nf->getsentence(j);
 232         bool allgood=true;
 233         for(int k=0;k<cs->getnumpredicates();k++) {
 234           if(cs->getpredicate(k)->isrule()&&
 235              findrepairaction(cs->getpredicate(k))==NULL) {
 236             allgood=false;
 237             break;
 238           }
 239         }
 240         if(allgood) {
 241           good=true;
 242           break;
 243         }
 244       }
 245     }
 246     if (!good)
 247       return true;
 248   }
 249   WorkSet *tmpset=new WorkSet(true);
 250   for(int i=0;i<globalmodel->getnumconstraints();i++) {
 251     NormalForm *nf=globalmodel->getnormalform(i);
 252     bool good=false;
 253     for(int j=0;j<nf->getnumsentences();j++) {
 254       CoerceSentence *cs=nf->getsentence(j);
 255       if (checkcycles(cs,removededges,tmpset,wr)) {
 256         delete(tmpset);
 257         return true;
 258       }
 259     }
 260   }
 261   delete(tmpset);
 262   return false; /*yeah...no cycles*/
 263 }
 264
 265
 266
 267 bool Repair::checkcycles(CoerceSentence *cs,WorkSet *removededges, WorkSet *searchset,WorkRelation *wr) {
 268   if (searchset->contains(cs)) {
 269     /* found cycle */
 270     return true;
 271   }
 272   if (removededges->contains(cs))
 273     return false; /* this edge is removed...don't consider it*/
 274
 275   searchset->addobject(cs);
 276   for(int i=0;i<cs->getnumpredicates();i++) {
 277     CoercePredicate *cp=cs->getpredicate(i);
 278     WorkSet *setofnf=wr->getset(cp);
 279     if (setofnf!=NULL) {
 280       /* Might not mess up anything */
 281       NormalForm *nf=(NormalForm*)setofnf->firstelement();
 282       while(nf!=NULL) {
 283         for(int j=0;j<nf->getnumsentences();j++) {
 284           CoerceSentence *cssearch=nf->getsentence(j);
 285           if (checkcycles(cssearch, removededges, searchset, wr))
 286             return true;
 287         }
 288         nf=(NormalForm *)setofnf->getnextelement(nf);
 289       }
 290     }
 291   }
 292   searchset->removeobject(cs);
 293   return false;
 294 }
 295
 296
 297
 298 WorkSet * Repair::searchcycles(WorkRelation *wr) {
 299   /* Do cycle search */
 300   WorkSet *cycleset=new WorkSet(true);
 301   WorkSet *searchset=new WorkSet(true);
 302   for(int i=0;i<globalmodel->getnumconstraints();i++) {
 303     NormalForm *nf=globalmodel->getnormalform(i);
 304     for(int j=0;j<nf->getnumsentences();j++) {
 305       detectcycles(nf->getsentence(j),searchset,cycleset,wr);
 306     }
 307   }
 308   delete(searchset);
 309   return cycleset;
 310 }
 311
 312
 313
 314 void Repair::detectcycles(CoerceSentence *cs,WorkSet *searchset,WorkSet *cycleset, WorkRelation *wr) {
 315   if (searchset->contains(cs)) {
 316     /* found cycle */
 317     CoerceSentence *csptr=(CoerceSentence *)searchset->firstelement();
 318     while(csptr!=NULL) {
 319       cycleset->addobject(csptr);
 320       csptr=(CoerceSentence *)searchset->getnextelement(csptr);
 321     }
 322     return;
 323   }
 324   searchset->addobject(cs);
 325   for(int i=0;i<cs->getnumpredicates();i++) {
 326     CoercePredicate *cp=cs->getpredicate(i);
 327     WorkSet *setofnf=wr->getset(cp);
 328     if (setofnf!=NULL) {
 329       /* Might not have any interference edges*/
 330       NormalForm *nf=(NormalForm*)setofnf->firstelement();
 331       while(nf!=NULL) {
 332         for(int j=0;j<nf->getnumsentences();j++) {
 333           CoerceSentence *cssearch=nf->getsentence(j);
 334           detectcycles(cssearch, searchset, cycleset, wr);
 335         }
 336         nf=(NormalForm*)setofnf->getnextelement(nf);
 337       }
 338     }
 339   }
 340   searchset->removeobject(cs);
 341 }
 342
 343
 344
 345 void Repair::buildmap(WorkRelation *wr) {
 346   for(int i=0;i<globalmodel->getnumconstraints();i++) {
 347     NormalForm *nf=globalmodel->getnormalform(i);
 348     for(int j=0;j<nf->getnumsentences();j++) {
 349       CoerceSentence *cs=nf->getsentence(j);
 350       for (int k=0;k<cs->getnumpredicates();k++) {
 351         Action *repairaction=findrepairaction(cs->getpredicate(k));
 352         if (repairaction==NULL) {
 353           /* Nothing will repair this */
 354           cs->getpredicate(k)->getpredicate()->print();
 355           printf(" can't be repaired!!!");
 356           exit(-1);
 357         }
 358         checkpredicate(repairaction,wr, globalmodel->getconstraint(i),cs->getpredicate(k));
 359       }
 360     }
 361   }
 362   ActionNormal *repairnormal=new ActionNormal(globalmodel);
 363   for(int i=0;i<globalmodel->getnumrulenormal();i++) {
 364     NormalForm *nf=globalmodel->getrulenormal(i);
 365     CoercePredicate *cpo=nf->getsentence(0)->getpredicate(0);
 366     /* Check for conflicts between abstraction functions */
 367     for(int j=0;j<globalmodel->getnumrulenormal();j++) {
 368       NormalForm *nfn=globalmodel->getrulenormal(j);
 369       CoercePredicate *cpn=nfn->getsentence(0)->getpredicate(0);
 370       if (!cpo->istuple()&&
 371           equivalentstrings(cpo->getrelset(),cpn->gettriggerset()))
 372         wr->put(cpo,nfn);
 373     }
 374
 375     /* Check for conflict between abstraction functions and model constraints */
 376     for(int i2=0;i2<globalmodel->getnumconstraints();i2++) {
 377       NormalForm *nf2=globalmodel->getnormalform(i2);
 378       for(int j2=0;j2<nf2->getnumsentences();j2++) {
 379         CoerceSentence *cs2=nf2->getsentence(j2);
 380         for (int k2=0;k2<cs2->getnumpredicates();k2++) {
 381           if (repairnormal->conflict(NULL,cpo,globalmodel->getconstraint(i2),cs2->getpredicate(k2)))
 382             wr->put(cpo,nf2);
 383         }
 384       }
 385     }
 386   }
 387   delete(repairnormal);
 388 }
 389
 390
 391
 392 void Repair::checkpredicate(Action *repair,WorkRelation *wr, Constraint *c,CoercePredicate *cp) {
 393   for(int i=0;i<globalmodel->getnumconstraints();i++) {
 394     NormalForm *nf=globalmodel->getnormalform(i);
 395     for(int j=0;j<nf->getnumsentences();j++) {
 396       CoerceSentence *cs=nf->getsentence(j);
 397       for (int k=0;k<cs->getnumpredicates();k++) {
 398         if (repair->conflict(c,cp,globalmodel->getconstraint(i),cs->getpredicate(k)))
 399           wr->put(cp, nf);
 400       }
 401     }
 402   }
 403   for(int i=0;i<globalmodel->getnumrulenormal();i++) {
 404     NormalForm *nf=globalmodel->getrulenormal(i);
 405     if (repair->conflict(c,cp,NULL, nf->getsentence(0)->getpredicate(0)))
 406       wr->put(cp,nf);
 407   }
 408 }
 409