9 #include "typeparser.h"
20 #include "processabstract.h"
21 #include "processobject.h"
22 #include "processconcrete.h"
23 #include "normalizer.h"
24 #include "Hashtable.h"
26 #include "bitreader.h"
27 #include "DefaultGuidance2.h"
28 #include "DefaultGuidance.h"
29 #include "DefaultGuidance3.h"
31 #include "fieldcheck.h"
37 Hashtable * model::gethashtable() {
41 bitreader * model::getbitreader() {
45 Guidance * model::getguidance() {
49 model::model(char *abstractfile, char *modelfile, char *spacefile, char *structfile, char *concretefile, char *rangefile)
51 parsestructfile(structfile);
54 //Hashtable first for lookups
55 env=new Hashtable((unsigned int (*)(void *)) & hashstring,(int (*)(void *,void *)) &equivalentstrings);
56 // env->put(&bstring,new Element(&badstruct,getstructure("arrayofstructs")));//should be of badstruct
57 parseabstractfile(abstractfile);
58 parsemodelfile(modelfile);
59 parsespacefile(spacefile);
60 parseconcretefile(concretefile);
61 // parserangefile(rangefile);
62 // committing out because of memory problems
64 br=new bitreader(this,env);
65 guidance=new DefGuidance(this); // for the file system benchmark
68 repair=new Repair(this);
69 if (!repair->analyzetermination()) {
71 printf("Constraint set might not terminate and can't be repaired!\n");
75 fc=new FieldCheck(this);
79 typmap=new typemap(this);
83 // typmap->reset(); Don't rebuild trees
84 domainrelation->reset();
87 typemap * model::gettypemap() {
91 Repair * model::getrepair() {
95 NormalForm * model::getnormalform(Constraint *c) {
96 for (int i=0;i<numconstraint;i++) {
97 if (c==constraintarray[i])
98 return constraintnormal[i];
100 printf("Error finding normal form\n");
104 int model::getnumconstraints() {
105 return numconstraint;
108 NormalForm * model::getnormalform(int i) {
109 return constraintnormal[i];
112 Constraint * model::getconstraint(int i) {
113 return constraintarray[i];
117 // processes the model definition rules
118 void model::doabstraction() {
119 struct timeval begin,end;
121 gettimeofday(&begin,NULL);
123 pa=new processabstract(this);
125 /* Process rules until we reach a fixpoint*/
126 /* First the normal rules */
129 for(int i=0;i<numrules;i++) {
130 if(!rulearray[i]->isdelayed()) {
132 pa->processrule(rulearray[i]);
133 if (pa->dirtyflagstatus())
139 /* Then the delayed rules */
142 for(int i=0;i<numrules;i++) {
143 if(rulearray[i]->isdelayed()) {
145 pa->processrule(rulearray[i]);
146 if (pa->dirtyflagstatus())
151 gettimeofday(&end,NULL);
152 time=(end.tv_sec-begin.tv_sec)*1000000+end.tv_usec-begin.tv_usec;
153 printf("Time used for abstraction(us): %ld\n",time);
159 void model::triggerrule(Element *ele,char *set) {
160 for(int i=0;i<numrules;i++) {
161 if(rulearray[i]->isstatic()) {
162 pa->processrule(rulearray[i], ele, set);
168 // processes the external constraints
169 void model::doconcrete() {
170 struct timeval begin,end;
172 gettimeofday(&begin,NULL);
174 processconcrete *pr=new processconcrete(this);
175 for(int i=0;i<numconcrete;i++) {
176 pr->processrule(concretearray[i]);
178 gettimeofday(&end,NULL);
179 time=(end.tv_sec-begin.tv_sec)*1000000+end.tv_usec-begin.tv_usec;
180 printf("Time used for concretization(us): %ld\n",time);
188 // inserts faults that break the specifications
189 void model::breakspec()
191 srandom((unsigned) time(NULL));
193 processobject *po = new processobject(this);
195 // takes each satisfied constraint and breaks it with probability prob_breakconstraint
196 for (int i=0; i<numconstraint; i++)
198 Constraint *c = getconstraint(i);
199 if (po->issatisfied(c))
200 if (random()<prob_breakconstraint*RAND_MAX)
201 po->breakconstraint(c);
209 // inserts faults that don not break the specifications
210 void model::inserterrors()
212 printf("\nmodel::inserterrors CALLED\n\n");
214 srandom((unsigned) time(NULL));
216 processobject *po = new processobject(this);
218 // takes each satisfied constraint and modifies it with probability prob_modifyconstraint
220 for (int i=0; i<numconstraint; i++)
222 Constraint *c = getconstraint(i);
224 printf("Constraint: ");
226 if (po->issatisfied(c))
227 printf(" is satisfied\n");
228 else printf(" is not satisfied\n");
231 if (po->issatisfied(c))
235 printf("r=%ld\n", r);
237 if (r<prob_modifyconstraint*RAND_MAX)
238 po->modifyconstraint(c);
247 // processes the internal constraints
248 // returns true only if no violated constraints were found
249 bool model::docheck()
251 struct timeval begin,end;
254 processobject *po=new processobject(this);
256 gettimeofday(&begin,NULL);
260 /* Process rules until we reach a fixpoint*/
261 for(int i=0;i<numconstraint;i++) {
262 if (!po->processconstraint(constraintarray[i]))
268 t=true; //Got to keep running
272 gettimeofday(&end,NULL);
273 time=(end.tv_sec-begin.tv_sec)*1000000+end.tv_usec-begin.tv_usec;
274 printf("Time used for check(us): %ld\n",time);
277 //printf("return from docheck()");
282 DomainRelation * model::getdomainrelation() {
283 return domainrelation;
288 /* reads the testspace file, which keeps the sets and relations involved;
289 these sets and relations are managed by "domainrelation" */
290 void model::parsespacefile(char *spacefile) {
291 ifstream *ifs=new ifstream();
292 ifs->open(spacefile);
293 Reader *r=new Reader(ifs);
294 Dparser *p=new Dparser(r);
295 domainrelation=p->parsesetrelation();
297 #ifdef DEBUGMANYMESSAGES
298 domainrelation->print();
307 /* reads the teststruct file, which keeps the structure definitions;
308 these definitions are kept in "structurearray" */
309 void model::parsestructfile(char *structfile) {
310 ifstream *ifs=new ifstream();
311 ifs->open(structfile);
312 Reader *r=new Reader(ifs);
313 Typeparser *p=new Typeparser(r);
314 List *list=new List();
317 structure *st=p->parsestructure();
321 #ifdef DEBUGMANYMESSAGES
329 structurearray=new structure *[list->size()];
330 list->toArray((void **)structurearray);
331 numstarray=list->size();
339 /* parses the testabstract file, which contains the model definition rules
340 these rules are kept in "rulearray" */
341 void model::parseabstractfile(char *abstractfile) {
342 ifstream *ifs=new ifstream();
343 ifs->open(abstractfile);
344 Reader *r=new Reader(ifs);
345 AParser *p=new AParser(r);
346 List *list=new List();
349 Rule *ru=p->parserule();
354 #ifdef DEBUGMANYMESSAGES
361 rulearray=new Rule *[list->size()];
362 list->toArray((void **)rulearray);
363 numrules=list->size();
364 numrulenormal=countstatic;
365 rulenormal=new NormalForm *[countstatic];
367 for(int i=0;i<numrules;i++) {
368 if(rulearray[i]->isstatic()) {
369 rulenormal[count++]=new NormalForm(rulearray[i]);
379 /* parses the testconcrete file, which contains the external constraints;
380 these constraints are kept in "concretearray" */
381 void model::parseconcretefile(char *abstractfile) {
382 ifstream *ifs=new ifstream();
383 ifs->open(abstractfile);
384 Reader *r=new Reader(ifs);
385 CParser *p=new CParser(r);
386 List *list=new List();
388 Rule *ru=p->parserule();
391 #ifdef DEBUGMANYMESSAGES
398 concretearray=new Rule *[list->size()];
399 list->toArray((void **)concretearray);
400 numconcrete=list->size();
409 /* parses the testmodel file, which contains the internal constraints
410 these constraints are kept in constraintarray;
411 the constraints in normal form are kept in constraintnormal */
412 void model::parsemodelfile(char *modelfile) {
413 ifstream* ifs=new ifstream();
414 ifs->open(modelfile);
415 Reader *r=new Reader(ifs);
416 Parser *p=new Parser(r);
417 List *list=new List();
419 Constraint *c=p->parseconstraint();
422 #ifdef DEBUGMANYMESSAGES
429 constraintarray=new Constraint *[list->size()];
430 list->toArray((void **)constraintarray);
431 numconstraint=list->size();
432 constraintnormal=new NormalForm *[list->size()];
433 for(int i=0;i<list->size();i++)
434 constraintnormal[i]=new NormalForm(constraintarray[i]);
443 /* reads the testrange file, which keeps the ranges of the relations
444 of the form "relation: A -> token".
445 This information is used only by the fault injection mechanism.
446 This file should be read only after the testspace file.
448 void model::parserangefile(char *rangefile)
450 ifstream *ifs=new ifstream();
451 ifs->open(rangefile);
452 Reader *r = new Reader(ifs);
453 RParser *rp = new RParser(r);
456 char* relation = rp->parserelation();
458 if (relation != NULL)
460 #ifdef DEBUGMANYMESSAGES
461 printf("Reading relation: %s\n", relation);
465 // find the given relation, whose range should be of type "token"
466 DRelation *drel = domainrelation->getrelation(relation);
467 if (strcmp(drel->getrange(), "token") != 0)
469 printf("Error! Range of %s should be of type token.", relation);
473 WorkSet *ws = rp->parseworkset();
474 #ifdef DEBUGMANYMESSAGES
475 printf("The range for %s is:\n", relation);
476 void *obj = ws->firstelement();
479 printf("%s ", (char *) obj);
480 obj = ws->getnextelement(obj);
485 drel->settokenrange(ws);
500 structure * model::getstructure(char *name) {
501 for(int i=0;i<numstarray;i++) {
502 if (equivalentstrings(name,structurearray[i]->getname())) {
504 return structurearray[i];
510 FieldCheck * model::getfieldcheck() {
514 int model::getnumrulenormal() {
515 return numrulenormal;
518 NormalForm * model::getrulenormal(int i) {
519 return rulenormal[i];
522 bool model::subtypeof(structure *sub,structure *super) {
526 if (sub->getsubtype()==NULL)
528 sub=getstructure(sub->getsubtype()->getname());
530 printf("Error in subtypeof\n");
531 return false; /* Should get here*/