adssemantics.c

这个工具集提供以下结构化分析和UML分析中所用的图形化绘图工具：ER-diagrams, data and event flow diagrams and state-transition diagr

 	    pv->SetBool(True);
 	    Found=True;
	    break; // jump out of for-loop
 	  }
 	}
	if (!Found) pv->SetBool(False);
	  */
      }
      if (pv->GetProp()->GetType()!=SENDEVENT) pnew.add(pv); // do not add old send events
    }
    for (generated.first();!generated.done();generated.next()){
      PropVal *pv=new PropVal(generated.cur(),True);
      pnew.add(pv);
    }
    knew->SetPropList(pnew); // the new list of properties

    // Update timers
    ClockManager cmnew=from->GetClockManager();
    if (!cmnew.Update(zero,off)){
      std::cout << "loc " << knew->GetId()  << " causes the problem\n"; //
      std::cout << "from\n";
      from->WriteScreen();
      std::cout << "to\n";
      knew->WriteScreen();
      abort();
    } 
    knew->SetClockManager(cmnew);
    List <ClockConstraint *> notrespondedto;
    knew->GetClockConstraints(&notrespondedto);
    for (off->first();!off->done();off->next()){
      if (notrespondedto.find(off->cur())>-1){
	notrespondedto.remove(off->cur());
      }
    }
    knew->SetClockConstraints(notrespondedto); // the new clock constraints

 
    Bag <ADSHyperEdge *> enab;
    ComputeEnabled(ah,knew,&enab); // compute the bag of enabled hyperedges in the new state
    if ((enab.length()==0)&&(generated.count()==0)){ // this new state is stable, so stop superstep
      //  Transforming unstable state into stable state
      knew->makeStable();
    }
    return knew;
  }
  else{
    error("The step is inconsistent!\n"); // can never occur, if Consistent(..) is true
    return NULL;
  }
}


void ADSSem::ComputeEnabled(ADSHyperGraph *h, ADSValuation *ak, 
			       Bag <ADSHyperEdge *> *enab){
  Bag <Subject *> relcfg;
  ak->GetConfig(&relcfg);    // the RELEVANT configuration: C with all action state nodes removed, joined with the terminated action state nodes
  // reason: a hyperedge having an action state node as source is only enabled if the corresponding activity has terminated
  Bag <Subject *> term;
  ak->GetTerminated((Bag <ATDActionStateNode *> *)&term);  // terminated action state nodes

  // remove action state nodes from rel
  List <Subject *> relcfgset;
  relcfg.GetSet(&relcfgset);
  for (relcfgset.first();!relcfgset.done();relcfgset.next()){
    if (relcfgset.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
      relcfg.add(relcfgset.cur(),-(relcfg.count(relcfgset.cur()))); // rel-AS
    }
  }
  relcfg.join(term); // add term to rel


  Bag <ATDActionStateNode *> running; // the bag of activities now executing
  Bag <Subject *> cfg; // the configuration bag
  ak->GetConfig(&cfg);  
  List <Subject *> cfgset; // the configuration set
  cfg.GetSet(&cfgset);    
  for (cfgset.first();!cfgset.done();cfgset.next()){
    if (cfgset.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
      int l=cfg.count(cfgset.cur());
      int m=relcfg.count(cfgset.cur());
      if ((l-m) < 0 ) { // more activity instances are terminated than there are in the configuration: this is impossible
	  error ("More activities terminate than are running: I am confused!\n");
	  ak->WriteScreen();
	  return;
      };
      running.add((ATDActionStateNode *)cfgset.cur(),(l-m));	  
    }
  }
  
  relcfgset.empty();
  relcfg.GetSet(&relcfgset);
 


  List <ADSHyperEdge *> rel;   // the list of relevant hyperedges
  h->GetHyperEdgesFrom((List <HyperEdge *> *)&rel,&relcfgset); // the SET of relevant hyperedges
  List <PropVal *> p;
  ak->GetPropList(&p); // the set of relevant properties



  List <ATDActionStateNode *> runningset;
  running.GetSet(&runningset);  

  // compute enab by 
  for (rel.first();!rel.done();rel.next()){  // for each relevant hyperedge
    bool eval=True; // false if the guard of rel.cur() cannot be evaluated
    List <Prop *> ptemp;
    rel.cur()->GetPropList(ptemp); // the properties of rel.cur()

    List <ADSVar *> evalnow;  // variables that need to be evalatued for the guard of rel.cur()
    for (ptemp.first();!ptemp.done();ptemp.next()){
      if (ptemp.cur()->isInternal()){	 
	List <ADSVar *> vtemp;
	rel.cur()->GetVarList(vtemp);
	for (vtemp.first();!vtemp.done();vtemp.next()){
	  if (evalnow.find(vtemp.cur())<0) evalnow.add(vtemp.cur());	    
	}
      }
    }


    for (runningset.first();!runningset.done();runningset.next()){
      //      string s=*runningset.cur()->GetName();
      //      ADSActivity *a=h->FindAct(s);
      ADSActivity *a=runningset.cur()->GetActivity();
      for (evalnow.first();!evalnow.done();evalnow.next()){
	if (a->isUpdated(evalnow.cur())){ // a updates some variable in rel.cur()'s guard, so the rel.cur() cannot be taken	
	  eval=False; // guard cannot be evaluated!
	  break;
	}
      }
      if (!eval) break; // guard cannot be evaluated!
    }     

    // check in predicate
    List <Subject *> inlist;
    rel.cur()->GetInNodes(&inlist);
    Bag <Subject *> inbag(inlist,1);
    if (!cfg.contains(inbag)) eval=False;

    // check not in predicate
    List <Subject *> notinlist;
    rel.cur()->GetNotInNodes(&notinlist);
    for (notinlist.first();!notinlist.done();notinlist.next()){
      if (cfg.count(notinlist.cur())>0){
	eval=False;
	break;
      }
    }    

    string s=rel.cur()->GetLabel();
    if ( (eval) && ParseLabel(&s,&p) ){ // guard can be evaluated and parsed
      bool b=True; // bool to test whether edge is not disabled by clock constraint
      if (rel.cur()->hasClockConstraint()){
	List <ClockConstraint *> currentTimeouts;
	ak->GetClockConstraints(&currentTimeouts);
	if (currentTimeouts.find(rel.cur()->GetClockConstraint())<0) {
	  b=False; // rel.cur() cannot be taken since its clock constraint is not true
	}
      }
      if (b){ // rel.cur() is enabled 
	// compute how many instances n of rel.cur() are enabled
	int n=relcfg.length(); // guaranteed upperbound on maximal number of instances of one edge
	List <Subject *> *source=rel.cur()->GetSubject1();
	for (source->first();!source->done(); source->next()){
	  int i=relcfg.count(source->cur());       // 
	  if (i<n)  n=i; // possibly new lower upperbound		 
	};
	enab->add(rel.cur(),n); // how many times?
      }  
    }
  }

}



// return true if an action state node in b1 interferes (has conflict) with an action state node in b2
// assumption: source and target are sets rather than multisets
// if bool same is true then b1==b2, otherwise not.
bool interfering1(ADSHyperGraph *ah, Bag <Subject *> *b1, Bag <Subject *> *b2, bool same) {
  List <ATDActionStateNode *> al1;  // al1 contains all action state nodes of b1
  List <Subject *>  b1set;
  b1->GetSet(&b1set);
  for (b1set.first();!b1set.done();b1set.next()){
    if (b1set.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
      al1.add((ATDActionStateNode *)b1set.cur());
    }
  } 


  List <ATDActionStateNode *> al2;  // al2 contains all action state nodes of b2
  List <Subject *> b2set;
  b2->GetSet(&b2set);
  for (b2set.first();!b2set.done();b2set.next()){
    if (b2set.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
      al2.add((ATDActionStateNode *)b2set.cur());
    }
  } 

  int a1len=al1.count();
  int a2len=al2.count();
  for (int i=0;i<a1len;i++){
    for (int j=0;j<a2len;j++){
      if ((same) && (i==j)) continue;  // if b1==b2 then node interferes by definition by itself, so skip this case
      if (ah->GetInterference(al1[i],al2[j])) return True; // conflict found
    }
  }
  return False; // no conflict found
}






// Test whether the step is consistent
bool ADSSem::Consistent(ADSHyperGraph *ah, 
			   Bag <Subject *> cfg, 
			   Bag <ADSHyperEdge *> step){
  Bag <Subject *> left; // the bag of states that are left
  Bag <Subject *> newconfig; // the new config
  List <ADSHyperEdge *> stepset;
  step.GetSet(&stepset);
  for (stepset.first();!stepset.done();stepset.next()){
    int number = step.count(stepset.cur());
    List <Subject *> *ltemp=stepset.cur()->GetSubject1();
    for (ltemp->first();!ltemp->done();ltemp->next()){
      left.add(ltemp->cur(),number);
    }
  }
  newconfig.join(cfg); // initialize newconfig with cfg
  bool result= (newconfig.diff(left));  // can states be left?
  if (!result) 
    return False;
  else // states can be left, now check for interference
    {       
      for (stepset.first();!stepset.done();stepset.next()){
	List <Subject *> *ltemp=stepset.cur()->GetSubject2(); // get target
	Bag <Subject *> target(*ltemp, step.count(stepset.cur()));  
	if (interfering1(ah,&target,&target,True)) return False; // interfering target
      	if (interfering1(ah,&newconfig,&target,False)) return False;// interfering old config
      }
      return True;
    }
}


// if consistent, newconfig contains the next configuration
// termresp is the set of terminated action states nodes that is reacted upon
bool ADSSem::NextStateAfterStep(ADSHyperGraph *ah, 
			   Bag <Subject *> cfg, 
			   Bag <ADSHyperEdge *> step, 
			   Bag <Subject *> *newconfig, 
			   Bag <ATDActionStateNode *> *termresp,
			   List <ClockConstraint *> *zero,
			   List <ClockConstraint *> *off,
			   List <Prop *> *generated){

  if (!Consistent(ah,cfg,step)) {
    error("Trying to take a non-step step!\n");
    return False;
  }
  Bag <Subject *> left; // the bag of states that are left
  List <ADSHyperEdge *> stepset;
  step.GetSet(&stepset);
  for (stepset.first();!stepset.done();stepset.next()){
    int number = step.count(stepset.cur());
    List <Subject *> *ltemp=stepset.cur()->GetSubject1();
    for (ltemp->first();!ltemp->done();ltemp->next()){
      left.add(ltemp->cur(),number);
    }
  }
  newconfig->join(cfg); // initialize newconfig with cfg
  newconfig->diff(left);  // can states be left?
 
  // compute termresp
  List <Subject *> leftcfg;
  left.GetSet(&leftcfg);
  for (leftcfg.first();!leftcfg.done();leftcfg.next()){
    if (leftcfg.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
      termresp->add((ATDActionStateNode *)leftcfg.cur(),left.count(leftcfg.cur()));
    }
  }
      
  // compute entered states
  Bag <Subject *> entered;
  for (stepset.first();!stepset.done();stepset.next()){
    List <Subject *> *ltemp=stepset.cur()->GetSubject2(); // get target
    int number = step.count(stepset.cur());
    for (ltemp->first();!ltemp->done();ltemp->next()){
      entered.add(ltemp->cur(),number);
    }
    // update generated
    Prop *p=stepset.cur()->GetSendEvent();
    if ((p) &&(!generated->contains(p))) generated->add(p);
  }

  // compute zero
  List <Subject *> elist;
  List <ADSHyperEdge *> rel;
  entered.GetSet(&elist);
  ah->GetHyperEdgesFrom((List <HyperEdge *> *)&rel, &elist);
  for (rel.first();!rel.done();rel.next()){
    if (rel.cur()->hasClockConstraint()){
      if (!zero->contains(rel.cur()->GetClockConstraint())){ // may go wrong incase of unsafe activity diagram
	zero->add(rel.cur()->GetClockConstraint());
      }
    }
  }

  // compute off
  List <ADSHyperEdge *> oldrel;
  List <Subject *> oldcfg;
  cfg.GetSet(&oldcfg);
  ah->GetHyperEdgesFrom((List <HyperEdge *> *)&oldrel, &oldcfg);
  




  List <ADSHyperEdge *> stillrel;
  List <Subject *> stillcfg;
  newconfig->GetSet(&stillcfg);
  ah->GetHyperEdgesFrom((List <HyperEdge *> *)&stillrel, &stillcfg);
  for (oldrel.first();!oldrel.done();oldrel.next()){
    if (stillrel.find(oldrel.cur())<0){ // oldrel.cur becomes disabled
      if (oldrel.cur()->hasClockConstraint())
	off->add(oldrel.cur()->GetClockConstraint());
    }
  }
  newconfig->join(entered);
  return True;
}


// parse the label to evaluate it
bool ADSSem::ParseLabel(const string *str, List <PropVal *> *p) {
  unsigned i;
  unsigned c=p->count();
  for (i=0;i<c;i++){ // initialise the parser
    ::propname[i]= (char *) malloc (1+strlen((*p)[i]->GetProp()->GetName().getstr()));
    strcpy(::propname[i],(*p)[i]->GetProp()->GetName().getstr());
    ::proptype[i]=(int)(*p)[i]->GetProp()->GetType();
    ::boollist[i]=(int)(*p)[i]->GetBool();   
  }
  ::count=p->count();
  YY_BUFFER_STATE y = ::adsedgelabelevaluation_scan_string(str->getstr());
  strcpy(::adsedgelabelevaluation_constraint, "");
  (::outcome)=0;
  ::isin=0;
  adsedgelabelevaluationparse();
  bool b =(bool) ::outcome;
  adsedgelabelevaluation_delete_buffer(y);
  return b;
}





//---------
// Asumption: hyperedges that leave no action state node
// cannot have a guard label
// In other words, the only data that is used is updated by activities


// if step is finished in current state, next step is started in next state

// void ADSSem::ComputeImpCKS(ADSHyperGraph *h, ADSCks *c){

  /*
  List <ADSValuation *> unprocessed; // valuations to be processed


  // define ip
  List<Prop *> ip; // the set of internal properties (only data)
  h->GetIntPropList(ip);
  int ipcount = ip.count(); // number of internal properties
  unsigned long int subsetsip = 1<< ipcount; 

  // compute the initial valuation
  ADSValuation *knew=new ADSValuation(c,unstable); // the initial valuation
  List <Subject *> initStates; // the list of initial states (if correct will contain a single element only) 
  h->GetNodes(&initStates, Code::ATD_INITIAL_STATE_NODE);
  if (initStates.count()==1){ // there can be only one initial state
    Bag <Subject *> b(initStates,1); // the initial configuration
    knew->SetConfig(b);
    List <PropVal *> pl;
    List <Prop *> extproplist;
    h->GetPropList(extproplist);
    for (extproplist.first();!extproplist.done();extproplist.next()){
      PropVal *pv=new PropVal(extproplist.cur(),False); // initially every external property (including events) is false (WHAT ABOUT INTERNAL PROPERTIES??)
      pl.add(pv);
    }
    knew->SetPropList(pl);
    knew->SetQueue(pl);
    c->AddNode(knew); // add the initial valuation to c
    
    unprocessed.add(knew); // add the initial valuation to unprocessed
    while (unprocessed.count()>0) { // while some valuations need to be processed
      // pick the first valuation in unprocessed
      unprocessed.first(); 
      ADSValuation *adk=unprocessed.cur(); 
      
      // compute running activity instances
      
      Bag <Subject *> cfg; // the current configuration bag
      adk->GetConfig(&cfg);
      List <Subject *> cfgl; // the current configuration set
      cfg.GetSet(&cfgl);   
      
      
      Bag <ATDActionStateNode *> term,qterm; // the terminated action state nodes
      adk->GetTerminated(&term);
      adk->GetQTerminated(&qterm);
      term.join(qterm); // term now contains all terminated activity instances
  
      // define a. a's is used to generate activity termination events.
      List<ATDActionStateNode *> a; // bag of running activities 

      // fill a & check whether cfgl!= FINAL
      bool final=True;
      for (cfgl.first();!cfgl.done();cfgl.next()){
	if (cfgl.cur()->GetClassType()!=Code::ATD_FINAL_STATE_NODE) final=False;
	if (cfgl.cur()->GetClassType()==Code::ATD_ACTION_STATE_NODE){
	  //	std::cout <<"Action state" << cfgl.cur()->GetId() << "\n";
	  int i;
	  int l=cfg.count(cfgl.cur()) - term.count((ATDActionStateNode *)cfgl.cur()); // only activities that have not yet terminated can terminate!
	  for (i=0;i<l;i++){
	    a.add((ATDActionStateNode *)cfgl.cur());
	  }
	}
      }
      
      if (final) { // final state is reached, so no event possible
	// skip this unprocessed loop
	// ....
	unprocessed.remove(adk);
	continue;