adssemantics.c

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

	} 
      }


	
      List <PropVal *> oldproplist;
      ak->GetPropList(&oldproplist);
      
      for (ip.first();!ip.done();ip.next()){
	if (!varl.contains(ip.cur()->GetVar())){ 
	  // retrieve old value
	  PropVal *pv=getPropVal(&oldproplist,ip.cur()); // take old value
	  if (pv!=NULL) ipl.add(pv);
	}
      }


      /// check that a string variable is not assigned two different values
      int iplcount=ipl.count();
      int xx,yy;
      bool found=False;
      
      for (xx=0;xx<iplcount;xx++){
	for (yy=xx+1;yy<iplcount;yy++){
	  if ((ipl[xx]->GetProp()->GetVar()==ipl[yy]->GetProp()->GetVar()) && (!(ipl[xx]->GetProp()==ipl[yy]->GetProp()))&& (ipl[xx]->GetBool()&&ipl[yy]->GetBool())){
	    found=True;
	  }
	} 
      }
      

      if (found) continue; // two assignments to same string variable is impossible, so skip this valuation





	unsigned long int c3;
	ClockManager cmnew=ak->GetClockManager();
	for (c3=0;c3<subsetsc;c3++){ // for all possibe subsets of c (1)
	  if (c3){
	    if (!cmnew.Tick()) std::cout << "I cannot tick in state " << ak->GetId() << "\n";;
	  }
	  
	  List <ClockConstraint *> timeout;
	  if ((ak->HasClockConstraints()) || ((cmnew.ExistTimeouts()))) cmnew.GetTimeouts(&timeout); // timeout can be empty if !ExistScheduled
	  
	  
	  if (c1==0 && c2==0 && c3==0) continue; // no change is not interesting 	
	  
	  // compute the valuations of the properties
	  
	  
	
	  List <PropVal *> pl; // the new proplist
	  pl=epl; // initialise with external props ...
	  if (only_relevant){
	    List<Prop *> eplist; // the set of external properties; add properties in eplist but not in ep to ep.
	    h->GetExtPropList(eplist);
	    for (eplist.first();!eplist.done();eplist.next()){
	      if (!ep.contains(eplist.cur())){
		PropVal *pv=new PropVal(eplist.cur(),False);
		pl.add(pv);
	      }
	    }
	  }
	  for (ipl.first();!ipl.done();ipl.next()){
	    pl.add(ipl.cur()); // ... and add internal props
	  }
	  
	  ADSValuation *klnew= new ADSValuation(*ak,unstable); // use old config only
	  klnew->SetPropList(pl);   
	  klnew->AddTerminated(al);
	  klnew->SetClockConstraints(timeout);
	  klnew->SetClockManager(cmnew);
	  if (c3 && (!c1) && (!c2) && (!cmnew.ExistTimeouts())) // there has only been a tick and this tick did not trigger any events
	    klnew->makeStable();
	  eadkl->add(klnew);
	  //	  teller++;
	}
      }
    } 
  }  
}

// Compute all the possible next unstable states in eadkl, given stable valuation ak
// only_relevant is true <-> irrelevant events are not considered
void ADSSem::InterleavedEvent(ADSHyperGraph *h, ADSValuation *ak,List <ADSValuation *> *eadkl, bool only_relevant){

  Bag <Subject *> cfg; // the current configuration bag
  ak->GetConfig(&cfg);
  List <Subject *> cfgl; // the current configuration set
  cfg.GetSet(&cfgl);   


  Bag <ATDActionStateNode *> term; // the terminated action state nodes
  ak->GetTerminated(&term);
  
  // define ep
  List<Prop *> ep; // the set of external properties
  //h->GetExtPropList(ep);
  
  if (only_relevant){ 
    List <ADSHyperEdge *> rel;   // the list of relevant hyperedges
    h->GetHyperEdgesFrom((List <HyperEdge *> *)&rel,&cfgl); // the SET of relevant hyperedges
    for (rel.first();!rel.done();rel.next()){
      List <Prop *> proplist;
      rel.cur()->GetPropList(proplist);
      for (proplist.first();!proplist.done();proplist.next()){
	if (proplist.cur()->isInternal()) continue;
	if (!ep.contains(proplist.cur())) ep.add(proplist.cur());
      }
    }
  }
  else{
    h->GetExtPropList(ep);
  }

  // define ip
  List<Prop *> ip; // the set of internal properties
  h->GetIntPropList(ip);

  // 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){
	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
    return;
  }  



  // compute proper subsets of a and p and        
  int epcount = ep.count(); // number of external properties
//  int ipcount = ip.count(); // number of internal properties : unused
  int acount = a.count(); // number of running activity instances
  int ccount=0;
  if ((ak->GetClockManager().ExistScheduled())&&(!(ak->GetClockManager().ExistTimeouts()))) ccount=1;

  
  //  unsigned long int subsetsep = 1<< epcount; 
  // unsigned long int subsetsip = 1<< ipcount; 
  //  unsigned long int subsetsa = 1<< acount;
  //  unsigned long int subsetsc = 1<< ccount;


 

  //  int teller=0;

  unsigned long int c1; // counter on subsets of ep
  for (c1=0;c1<static_cast<unsigned>(epcount);c1++){ // for all possibe subsets of ep

    List <PropVal *> epl; // the valuation of properties
    int ctemp;
    for (ctemp=0;ctemp<epcount;ctemp++){
      if (static_cast <unsigned> (ctemp) == c1){
	PropVal *pv=new PropVal(ep[ctemp],True);
	epl.add(pv);
      }
      else{
	PropVal *pv=new PropVal(ep[ctemp],False);
	epl.add(pv);
      }
    } 

    List <PropVal *> pl; // the new proplist
    pl=epl; // initialise with external props ...
    if (only_relevant){
      List<Prop *> eplist; // the set of external properties; add properties in eplist but not in ep to ep.
      h->GetExtPropList(eplist);
      for (eplist.first();!eplist.done();eplist.next()){
	if (!ep.contains(eplist.cur())){
	  PropVal *pv=new PropVal(eplist.cur(),False);
	  pl.add(pv);
	}
      }
    }

    List <PropVal *> oldproplist;
    ak->GetPropList(&oldproplist);
    for (ip.first();!ip.done();ip.next()){
      PropVal *pv=getPropVal(&oldproplist,ip.cur()); // take old value
      if (pv!=NULL) pl.add(pv);
    }

    
    ADSValuation *klnew= new ADSValuation(*ak,unstable); // use old config only
    klnew->SetPropList(pl);   
    //    klnew->AddTerminated(al);
    // klnew->SetClockConstraints(timeout);
    // klnew->SetClockManager(cmnew);
    //   if (c3 && (!c1) && (!c2) && (!cmnew.ExistTimeouts())) // there has only been a tick and this tick did not trigger any events
    //      klnew->makeStable();
    eadkl->add(klnew);
    //	  teller++;

  }



	  
  unsigned long int c2;
  for (c2=0;c2<static_cast<unsigned>(acount);c2++){ // for all possibe subsets of a
  
    // compute the terminated activity instances
    Bag <ATDActionStateNode *> al; 
    List <ADSVar *> varl; // list of variables that are updated in terminating activities

    int ctemp;
    for (ctemp=0;ctemp<acount;ctemp++){
      if (static_cast<unsigned>(ctemp) == c2) {
	al.add(a[ctemp]);
	ADSActivity *act=a[ctemp]->GetActivity();
	List <ADSVar *> vartemp;
	act->GetUpdateList(vartemp);
	for (vartemp.first();!vartemp.done();vartemp.next()){
	  if (!varl.contains(vartemp.cur())) // update varl
	    varl.add(vartemp.cur());	  
	}
      }
    }

    List <Prop *> updatedpropl; // list of properties that are updated in terminating activities
    for (ip.first();!ip.done();ip.next()){
      if (varl.contains(ip.cur()->GetVar())){
	updatedpropl.add(ip.cur());
      }	
    }


    unsigned long int c4;  // depending upon c2 (computing al) !!!!!
    //   unsigned long int subsetsvarl = 1 << varl.count();
    int upcount= updatedpropl.count();
    unsigned long int subsetsup =1 << upcount;

    for (c4=0; c4<subsetsup;c4++) {      
      List <PropVal *> ipl;
  
      for (ctemp=0;ctemp<upcount;ctemp++){
	if ((1<< ctemp)&c4) {
	  //	  for (ip.first();!ip.done();ip.next()){
	  //	    if (ip.cur()->GetVar()==varl[ctemp]){
	      PropVal *pv=new PropVal(updatedpropl[ctemp],True);
	      ipl.add(pv);
	      //	    }
	      //}	    
	}
	else{
	  //	  for (ip.first();!ip.done();ip.next()){
	  //	    if (ip.cur()->GetVar()==varl[ctemp]){
	      PropVal *pv=new PropVal(updatedpropl[ctemp],False);
	      ipl.add(pv);
	      //	    }
	      // }
	} 
      }


      ///
      int iplcount=ipl.count();
      int xx,yy;
      bool found=False;
    
      for (xx=0;xx<iplcount;xx++){
	//	ip[xx]->Write();
	for (yy=xx+1;yy<iplcount;yy++){
	  if ((ipl[xx]->GetProp()->GetVar()==ipl[yy]->GetProp()->GetVar()) && (!(ipl[xx]->GetProp()==ipl[yy]->GetProp()))&& (ipl[xx]->GetBool()&&ipl[yy]->GetBool())){
	    found=True;
	  }
	} 
      }
      

      if (found) continue; // two assignments to same string variable is impossible, so skip this valuation

	///
      
      List <PropVal *> oldproplist;
      ak->GetPropList(&oldproplist);
      
      for (ip.first();!ip.done();ip.next()){
	if (!varl.contains(ip.cur()->GetVar())){ 
	  // retrieve old value
	  PropVal *pv=getPropVal(&oldproplist,ip.cur()); // take old value
	  if (pv!=NULL) ipl.add(pv);
	}
      }
    
      List <PropVal *> pl; // the new proplist

      //     List <PropVal *> oldproplist;
      //      ak->GetPropList(&oldproplist);
      for (ep.first();!ep.done();ep.next()){
	PropVal *pv=getPropVal(&oldproplist,ep.cur()); // take old value
	if (pv!=NULL) pl.add(pv);
      }

      if (only_relevant){
	List<Prop *> eplist; // the set of external properties; add properties in eplist but not in ep to ep.
	h->GetExtPropList(eplist);
	for (eplist.first();!eplist.done();eplist.next()){
	  if (!ep.contains(eplist.cur())){
	    PropVal *pv=new PropVal(eplist.cur(),False);
	    pl.add(pv);
	  }
	}
      }
      for (ipl.first();!ipl.done();ipl.next()){
	pl.add(ipl.cur()); // ... and add internal props
      }

      ADSValuation *klnew= new ADSValuation(*ak,unstable); // use old config only
      klnew->SetPropList(pl);   
      klnew->AddTerminated(al);
      //   klnew->SetClockConstraints(timeout);
      //      klnew->SetClockManager(cmnew);
      //     if (c3 && (!c1) && (!c2) && (!cmnew.ExistTimeouts())) // there has only been a tick and this tick did not trigger any events
      //	klnew->makeStable();
      eadkl->add(klnew);
    //	  teller++;


    }

  }




  unsigned long int c3;
  ClockManager cmnew=ak->GetClockManager();
  for (c3=0;c3<static_cast <unsigned>(ccount);c3++){ // for all possibe subsets of c (1)
    //if (c3){
      if (!cmnew.Tick()) std::cout << "I cannot tick in state " << ak->GetId() << "\n";;
   // }
    
    List <ClockConstraint *> timeout;
    if ((ak->HasClockConstraints()) || ((cmnew.ExistTimeouts()))) cmnew.GetTimeouts(&timeout); // timeout can be empty if !ExistScheduled
    

    ADSValuation *klnew= new ADSValuation(*ak,unstable); // use old config only

    klnew->SetClockConstraints(timeout);
    klnew->SetClockManager(cmnew);
    if ((!cmnew.ExistTimeouts())){ // there has only been a tick and this tick did not trigger any events
      klnew->makeStable();
    }
    eadkl->add(klnew);
    //	  teller++;
  }
}






void ADSSem::Step(
		  ADSHyperGraph *h, 
		     ADSValuation *ak, 
		     Bag<ADSHyperEdge *> *step,
		     List<Bag<ADSHyperEdge *> *> *steplist){ 


  // compute maximal, consistent sublists

  Bag <Subject *> cfg;
  ak->GetConfig(&cfg);    // the configuration

  if (Consistent(h,cfg,*step)) { // step is consistent... 
    Bag<ADSHyperEdge *> *newstep=new Bag<ADSHyperEdge *>(*step);
    steplist->add(newstep); // ... so add it to steplist
  }
  else{    //  Step is INconsistent
    List <ADSHyperEdge *> l; // set of hyperedges in bag.
    step->GetSet(&l);
    for (l.first();!l.done();l.next()) {
      if (h->isConflicting(step,l.cur())){
	step->remove(l.cur()); // for each elementtype remove one instance
	Step(h,ak,step,steplist ); // Try this reduced step
	step->add(l.cur());	
      }            
    }
  }
}


ADSValuation *ADSSem::TakeStep(ADSHyperGraph *ah,
			 ADSCks *c,
			 ADSValuation *from,
			 Bag <ADSHyperEdge *> *step){
  Bag <Subject *> cfg;
  from->GetConfig(&cfg);    // the configuration

  Bag <Subject *> *newcfg= new Bag<Subject *>;  // the new configuration
  Bag <ATDActionStateNode *> *termresp= new Bag <ATDActionStateNode *>; //the terminated action state nodes responded to
  List <ClockConstraint *> *zero=new List <ClockConstraint *>;
  List <ClockConstraint *> *off=new List <ClockConstraint *>;
  List <Prop *> generated; // list of events generated in the step

  if (NextStateAfterStep(ah,cfg,*step,newcfg,termresp,zero,off,&generated)) { // compute the next valuation of the variables

    ADSValuation *knew = new ADSValuation(c,unstable);  // compute the new location

    // update config
    knew->SetConfig(*newcfg);  // the new configuration

    // update terminated action state nodes
    Bag <ATDActionStateNode *> termnotresp;
    from->GetTerminated(&termnotresp);
    if (!termnotresp.diff(*termresp)) {
      error("Error in computing bag difference");
      return False;
    }
    knew->AddTerminated(termnotresp); // the new bag of terminated action state nodes
    
    // update properties
    List <PropVal *> p;
    from->GetPropList(&p);
    List <PropVal *> pnew;
    for (p.first();!p.done();p.next()){ // reset the events
      PropVal *pv=new PropVal(*p.cur());
      if (pv->GetProp()->GetType()==EVENT){
	pv->SetBool(False);
	  /*
	bool Found=False;
	for (generated.first();!generated.done();generated.next()){
 	  if (*generated.cur()==(*(pv->GetProp()))){