adssemantics.c

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

//////////////////////////////////////////////////////////////////////////////////
// This file is part of Toolkit for Conceptual Modeling (TCM).
// (c) copyright 2001, Universiteit Twente.
// Author: Rik Eshuis ([e-mail]).
//
// TCM is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// TCM is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with TCM; if not, write to the Free Software
// Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
////////////////////////////////////////////////////////////////////////////////
#include "adsactivity.h"
#include "adssemantics.h"
#include "adshyperedge.h"
#include "adscks.h"
#include "graph.h"
#include "initialstate.h"
#include <ctype.h>
#include "lstring.h"
#include "adspropertyvaluation.h"
#include "adsedgelabelevaluationparse.h"
#include <stdlib.h>
#include "bag.h"
#include "adsvariable.h"
#include "outputfile.h"



bool ADSSem::inparallel(ADSHyperGraph *ah,Subject *a, Subject *b){
  ADSCks *c=new ADSCks(ah);
  tokengame(ah,c);
  List <ADSValuation *> nodes;
  c->GetNodes((List<Subject *> *)&nodes);
  for (nodes.first();!nodes.done();nodes.next()){
    Bag <Subject *> cfg; // the current configuration bag
    nodes.cur()->GetConfig(&cfg);
    if ((cfg.count(a)>0) && (cfg.count(b)>0)){
      return True;
    }
  }
  return False;
}


void ADSSem::tokengame(ADSHyperGraph *h,ADSCks *c){
  List <ADSValuation *> unprocessed; // valuations to be processed
  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);
    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(); 
      //      std::cout << "."; // progress indication 
      //      std::cout.flush();
      ADSValuation *adk=unprocessed.cur();     
      Bag <Subject *> cfg; // the current configuration bag
      adk->GetConfig(&cfg);
      List <Subject *> cfgl; // the current configuration set
      cfg.GetSet(&cfgl);   
      
      
      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()){
	Bag <Subject *> left(*(rel.cur()->GetSubject1()),1);
	Bag <Subject *> enter(*(rel.cur()->GetSubject2()),1);
	cfg.diff(left);
	cfg.join(enter);
	ADSValuation *adknew= new ADSValuation(c,unstable);
	adknew->SetConfig(cfg);
	ADSValuation *oldadk=c->FindSimilarNode(adknew);
	if (!oldadk){ // eadkl.cur() does not yet exist in c
	  c->AddNode(adknew); // so add it to c
	  unprocessed.add(adknew); // and to unprocessed
	  ADSTransition *ktnew = new ADSTransition(c,adk,adknew); // make a new transition	    
	  c->AddEdge(ktnew);
	  string str;
	  if (c->GrowsInfinite(adknew,str)){
	    string s="The activity diagram is infinite (state "+ str + " is unbounded)!\n";
	    char s1[100];
	    strcpy(s1,s.getstr());
	    error(s1);
	    return;
	  }
	}
	else{
	  //  ADSValuation *old=c->FindSimilarNode(eadkl.cur()); // eadkl.cur() exists already, so find this old copy
	  ADSTransition *ktnew = new ADSTransition(c,adk,oldadk); // make a transition
	  if (!c->ExistsSimilarEdge(ktnew)){
	    c->AddEdge(ktnew);
	  }	    
	  else delete ktnew;
	}    
	
	cfg.diff(enter);
	cfg.join(left);
      }
      unprocessed.remove(adk); // adk is processed so remove it
    }  
  }
}

// for debugging only
void PrintBag(Bag <Subject *> *b){
  List <Subject *> l;
  b->GetList(l);
  for (l.first();!l.done();l.next()){
    std::cout << l.cur()->GetId() <<":\t" << b->count(l.cur()) <<"\n";
  }
}

// for debugging only
void PrintBag(Bag <ATDActionStateNode *> *b){
  List <ATDActionStateNode *> l;
  b->GetList(l);
  for (l.first();!l.done();l.next()){
    std::cout << l.cur()->GetId() <<":\t" << b->count(l.cur()) <<"\n";
  }
}




// Execute event step from current location ak
// Result locations are returned (note that some may already have been part
// of the CLKS, so these can be skipped?)
// CLKS *c is updated


// true iff there is an activity `a' in `b' 
// such that in `a' variabe `v' is updated
//bool canbeUpdated(ADSHyperGraph *h,Bag <ATDActionStateNode *> b, ADSVar *v){
//  List <ATDActionStateNode *> l;
//  b.GetSet(&l);
//  for (l.first();!l.done();l.next()){
//    string s=*l.cur()->GetName();
//    ADSActivity *a=h->FindAct(s);
//    if (a->isUpdated(v)) return True;
//  }
//  return False;
//}


// find given a list of PropVal the Val of a Prop
PropVal *getPropVal(List <PropVal *> *plist, Prop *p){
	for (plist->first();!plist->done();plist->next()){
		if (*(plist->cur()->GetProp())==*p){
			return plist->cur();
		}
	}
	return NULL;
}


// the actual execution algorithm
// the semantics maps h into c.
// loop in which states are processed. By performing transitions new
// states are added.
void ADSSem::ComputeCKS(ADSHyperGraph *h, ADSCks *c, bool reduce){
  List <ADSValuation *> unprocessed; // valuations to be processed

//  int counter=0;		//unused

  // 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
      pl.add(pv);
    }
    knew->SetPropList(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(); 
      //      std::cout << "."; // progress indication 
      //      std::cout.flush();
      ADSValuation *adk=unprocessed.cur(); 
  
      // update bounds
      Bag <Subject *> tmpcfg;
      adk->GetConfig(&tmpcfg);
      h->UpdateBounds(&tmpcfg);

      if (adk->isStable()){ 
	List<ADSValuation *> eadkl; // list of new unstable states that can be reached from adk by executing an event transition
	if (reduce){
	  InterleavedEvent(h,adk,&eadkl,reduce); // compute eadkl
	}
	else{
	  Event(h,adk,&eadkl,reduce);
	}
	for (eadkl.first();!eadkl.done();){ 	  
	  ADSValuation *oldadk=c->FindSimilarNode(eadkl.cur());
	  if (!oldadk){ // eadkl.cur() does not yet exist in c
	    c->AddNode(eadkl.cur()); // so add it to c
	    unprocessed.add(eadkl.cur()); // and to unprocessed
	    ADSTransition *ktnew = new ADSTransition(c,adk,eadkl.cur()); // make a new transition	    
	    c->AddEdge(ktnew);
	    string str;
	    if (c->GrowsInfinite(eadkl.cur(),str)){
	      string s="The activity diagram is infinite (state "+ str + " is unbounded)!\n";
	      char s1[100];
	      strcpy(s1,s.getstr());
	      error(s1);
	      return;
	    }
	    eadkl.next(); // next in list
	  }
	  else{
	    //  ADSValuation *old=c->FindSimilarNode(eadkl.cur()); // eadkl.cur() exists already, so find this old copy
	    ADSTransition *ktnew = new ADSTransition(c,adk,oldadk); // make a transition
	    if (!c->ExistsSimilarEdge(ktnew)){
	      c->AddEdge(ktnew);
	    }	    
	    else delete ktnew;
	    eadkl.removecur(); // remove eadkl.cur() from list
	  }          
	}
      }
      else{ // adk is unstable, hence a reaction (step) must be taken
	Bag <ADSHyperEdge *> enab; // the bag of enabled hyperedges
	ComputeEnabled(h,adk,&enab); // fill enab with enabled hyperedges

	List<Bag<ADSHyperEdge *> *> steplist; // the list of all possible steps
	Step(h,adk,&enab,&steplist); // compute steplist (list of steps)
	
	// not every step in the steplist is maximal
	// therefore the maximal steps are filtered out next
       
	int slength=steplist.count();
	int i;

	for (i=0;i<slength;i++){	  
	  ADSValuation *klnew=TakeStep(h,c,adk,steplist[i]); // take the step. This results in a unique next valuation
	  ADSValuation *oldklnew = c->FindSimilarNode(klnew);
	  if (!oldklnew){
	    c->AddNode(klnew);
	    unprocessed.add(klnew);
	    ADSTransition *ktnew = new ADSTransition(c,adk,klnew,steplist[i]); // make a transition in which a step is taken	   
	    c->AddEdge(ktnew);
	    string str;
	    if (c->GrowsInfinite(klnew,str)){
	      string s="The activity diagram is infinite (state "+ str + " is unbounded)!\n";
	      char s1[100];
	      strcpy(s1,s.getstr());
	      error(s1);
	      return;
	    }
	  }
	  else{  // there exists already a similar node
	    //	    ADSValuation *old=c->FindSimilarNode(klnew);
	    delete klnew;
	    ADSTransition *ktnew = new ADSTransition(c,adk,oldklnew,steplist[i]); 
	    if (!c->ExistsSimilarEdge(ktnew)){
	      c->AddEdge(ktnew);
	    }	 
	    else delete ktnew;
	  }
	}
      }
      unprocessed.remove(adk); // adk is processed so remove it
    }
  }   
}




// Compute all the possible next unstable states in eadkl, given stable valuation ak
// only_relevant is true <-> irrelevant events are not considered
void ADSSem::Event(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 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; 	// unused
  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<subsetsep;c1++){ // for all possibe subsets of ep

    List <PropVal *> epl; // the valuation of properties
    int ctemp;
    for (ctemp=0;ctemp<epcount;ctemp++){
      if ((1<<ctemp) & c1 ){
	PropVal *pv=new PropVal(ep[ctemp],True);
	epl.add(pv);
      }
      else{
	PropVal *pv=new PropVal(ep[ctemp],False);
	epl.add(pv);
      }
    } 
	  
    unsigned long int c2;
    for (c2=0;c2<subsetsa;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


      for (ctemp=0;ctemp<acount;ctemp++){
	if ((1<<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);
	      //	    }
	      // }