//////////////////////////////////////////////////////////////////////////////////
// This file is part of Toolkit for Conceptual Modeling (TCM).
// (c) copyright 2001, Universiteit Twente.
// Author: Rik Eshuis (eshuis@cs.utwente.nl).
//
// 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);
	      //	    }
	      // }
	} 
      }


	
      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()))){
 	    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;
      }  
      
      int acount = a.count();
      unsigned long int subsetsa = 1<<acount;
      
      int ccount=0;
      if ((adk->GetClockManager().ExistScheduled())&&(!(adk->GetClockManager().ExistTimeouts()))) ccount=1;
      unsigned long int subsetsc = 1<<ccount;

      // PLEASE NOTE: I ASSUME THAT THERE ARE NO CHANGE EVENTS 
      List <Prop *> notinq=extproplist; // the set of properties not in queue
      List <PropVal *> q; // existing q, it can only contain events
      adk->GetQueue(&q);
      for (q.first();!q.done();q.next()){
	if (q.cur()->GetBool()) notinq.remove(q.cur()->GetProp()); // remove properties that are in queue
	
      }
      for (notinq.first();!notinq.done();){
	if (notinq.cur()->GetType()!=EVENT){
	  notinq.removecur();
	}
	else
	  notinq.next();
      }
      // notinq now only contains events not in q
      int pnotinq_len=notinq.count(); // 
      
      unsigned long int subsets_pnotinq_len = 1 << pnotinq_len;
      
      



      // fill newq
      int index;
      for ( index=0;index<subsets_pnotinq_len;index++){
	List <PropVal *> newq; // the new queue
	
	for (q.first();!q.done();q.next()){
	  if (q.cur()->GetBool()) newq.add(q.cur()); // put old events in new queue
	}

	 
	for (int j=0;j<pnotinq_len;j++){
	  if ((1<<j) & index){
	    PropVal *pvt=new PropVal(notinq[j],True); // only for events	    
	    newq.add(pvt);
	  }
	  else{
	    PropVal *pvf=new PropVal(notinq[j],False);
	    newq.add(pvf);
	  }
	}



	// NOTE
	// assumption: now every event has valuation true or false in newq
	// END OF NOTE

	unsigned long int c2;
	for (c2=0;c2<subsetsa;c2++){ // for all possibe subsets of a
	  

	  // compute the terminated queue activity instances
	  Bag <ATDActionStateNode *> newqterm;
	  // 	  newqterm.join(qterm); niet nodig vanwege AddQTerminated procedure
	  for (int ctemp=0;ctemp<acount;ctemp++){
	    if ((1<<ctemp) &  c2) {
	      newqterm.add(a[ctemp]);
	    }
	  }  


	  unsigned long int c3;
	  ClockManager cmnew=adk->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 " << adk->GetId() << "\n";;
	    }
	    
	    List <ClockConstraint *> timeout;
	    if ((adk->HasClockConstraints()) || ((cmnew.ExistTimeouts()))) cmnew.GetTimeouts(&timeout); // timeout can be empty if !ExistScheduled
	    
	    if ((index==0) && (c2==0) && (c3==0) && (adk->isStable())) continue; // no change is no change

	    
	




	    if (adk->isStable()){ // router is not busy processing any event

	      // either (a) an external event from newq or (b) a termination event from newqterm is processed or (c) a temporal event is processed
	      
	      // case (a)
	      for (newq.first();!newq.done();newq.next()){
		if (!newq.cur()->GetBool()) continue;
		List <PropVal *> newproplist;
		newproplist.add(newq.cur());  // pick a random event if event is true
		// preserve the old internal properties (data).
		List <PropVal *> oldpropvallist;
		adk->GetPropList(&oldpropvallist);
		for (oldpropvallist.first();!oldpropvallist.done();oldpropvallist.next()){
		  if (oldpropvallist.cur()->GetProp()->isInternal()) 
		    newproplist.add(oldpropvallist.cur());
		}


		List <PropVal *> newnewq;
		newnewq=newq;
		newnewq.remove(newq.cur());
		PropVal *pvf=new PropVal(newq.cur()->GetProp(),False);
		newnewq.add(pvf);
		
		ADSValuation *adknew=new ADSValuation(*adk,unstable); // make new state	     
		adknew->SetQueue(newnewq);	      
		adknew->AddQTerminated(newqterm);
		adknew->SetPropList(newproplist);
		adknew->SetQClockConstraints(timeout);
		adknew->SetClockManager(cmnew);
	      

		ADSValuation *oldadk=c->FindSimilarNode(adknew);
		if (!oldadk){ // adknew does not yet exist in c
		  // if (!c->ExistsSimilarNode(adknew)){ // adknew 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;
		  }
		  //	    std::cout << "\nAFDDSF";
		  //	      eadkl.next(); // next in list
		}
		else{
		  //		ADSValuation *old=c->FindSimilarNode(adknew); // adknew 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;
		}    
		
	      }


	      // case (b)
	      List <ATDActionStateNode *> qtermlist;
	      qterm.GetSet(&qtermlist);
	      if (qtermlist.count()==0){
		newqterm.GetSet(&qtermlist);
	      }
	      
	      for (qtermlist.first();!qtermlist.done();qtermlist.next()) {
		Bag <ATDActionStateNode *> newterm;
		adk->GetTerminated(&newterm);
		newterm.add(qtermlist.cur());  // pick a random event, insert into newterm
		newqterm.add(qtermlist.cur(),-1); // and remove from qterm
		
		
		term.add(qtermlist.cur()); // only needed for inspection of `canbeupdated'

		ADSActivity *act=qtermlist.cur()->GetActivity();
		List <ADSVar *> varl;
		act->GetUpdateList(varl);

		unsigned long int c4;  // depending upon c2 (computing al) !!!!!
		unsigned long int subsetsvarl = 1 << varl.count();
		for (c4=0; c4<subsetsvarl;c4++) {
		

		  List <PropVal *> ipl;
		  int ctemp;
		  for (ctemp=0;ctemp<varl.count();ctemp++){
		    if ((1<<ctemp) &  c4) {
		      for (ip.first();!ip.done();ip.next()){
			if (ip.cur()->GetVar()==varl[ctemp]){
			  PropVal *pv=new PropVal(ip.cur(),True);
			  ipl.add(pv);
			}
		      }	    
		    }
		    else{
		      for (ip.first();!ip.done();ip.next()){
			if (ip.cur()->GetVar()==varl[ctemp]){
			  PropVal *pv=new PropVal(ip.cur(),False);
			  ipl.add(pv);
			}
		      }
		    } 
		  }
		  
		  List <PropVal *> oldproplist;
		  adk->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);
		    }
		  }
		



		  
		  ADSValuation *adknew=new ADSValuation(*adk,unstable); // make new state
		  
		  adknew->SetPropList(ipl);
		  adknew->SetQueue(newq);
		  adknew->AddQTerminated(newqterm);
		  adknew->AddTerminated(newterm);
		  
		  adknew->SetQClockConstraints(timeout);
		  adknew->SetClockManager(cmnew);


		  
		  ADSValuation *oldadk=c->FindSimilarNode(adknew);
		  if (!oldadk){ // adknew does not yet exist in c

		    //	if (!c->ExistsSimilarNode(adknew)){ // adknew 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
		    if (!c->ExistsSimilarEdge(ktnew)){ // if the transition did not yet exist
		      c->AddEdge(ktnew);
		    }
		    else delete ktnew; // else delete the transition
		    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;
		    }
		    //	    std::cout << "\nAFDDSF";
		    //	      eadkl.next(); // next in list
		  }
		  else{
		    //	  ADSValuation *old=c->FindSimilarNode(adknew); // adknew 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;
		  }    
		  
		}
		
	      }


	      // case (c) temporal event
	      
	      for (timeout.first();!timeout.done();timeout.next()){

		
		ADSValuation *adknew=new ADSValuation(*adk,unstable); // make new state

	
		List <ClockConstraint *> newtimeout;
		newtimeout.add(timeout.cur());

		List <ClockConstraint *> newqtimeout;
		newqtimeout=timeout;
		newqtimeout.remove(timeout.cur());

		adknew->SetQueue(newq);
		adknew->AddQTerminated(newqterm);
		adknew->SetQClockConstraints(newqtimeout);
		adknew->SetClockConstraints(newtimeout);
		adknew->SetClockManager(cmnew);

		ADSValuation *oldadk=c->FindSimilarNode(adknew);
		if (!oldadk){ // adknew does not yet exist in c

		  //	if (!c->ExistsSimilarNode(adknew)){ // adknew 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
		  if (!c->ExistsSimilarEdge(ktnew)){ // if the transition did not yet exist
		    c->AddEdge(ktnew);
		  }
		  else delete ktnew; // else delete the transition
		  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;
		  }
		  //	    std::cout << "\nAFDDSF";
		  //	      eadkl.next(); // next in list
		}
		else{
		  //	  ADSValuation *old=c->FindSimilarNode(adknew); // adknew 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;
		}  
		
	      }
	      


	    }
	    else if (!adk->isStable()){
	      // HET GAAT MIS OMDAT terminated BIJ BEREKENEN STAP. MOET TERMINATED ALS F BESCHOUWEN
	      // gerepareerd
	    
	      //  if (!adk->isStable()){ 
	      // adk is unstable, but step is not yet finished
	      // only set the new queue
	      // CASE 1


	      if (!((index==0) && (c2==0))){ // only if there is some change 
		ADSValuation *adknew=new ADSValuation(*adk,unstable);
		adknew->SetQueue(newq);
		adknew->AddQTerminated(newqterm);
		adknew->SetQClockConstraints(timeout);
		
		ADSValuation *oldadk=c->FindSimilarNode(adknew);
		if (!oldadk){ // adknew does not yet exist in c
	      
		  // code repeated , make separate procedure someday
		  //     if (!c->ExistsSimilarNode(adknew)){ // adknew 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;
		  }
		  //	    std::cout << "\nAFDDSF";
		  //	      eadkl.next(); // next in list
		}
		else{
		  //		ADSValuation *old=c->FindSimilarNode(adknew); // adknew 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;
		}   
	      }
	    
	      // CASE 2
	      // adk is unstable, hence a reaction (step) can 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();	      
	      
	      for (int ii=0;ii<slength;ii++){

	
		ADSValuation *klnew=TakeStep(h,c,adk,steplist[ii]); // take the step. This results in a unique next valuation, could be stable or unstable.
		
	      



		// TODO 
		// 
		// make this next valuation unstable
		// DO NOT DO




		ADSValuation *oldadk=c->FindSimilarNode(klnew);
		if (!oldadk){ 
		  
		  //	      if (!c->ExistsSimilarNode(klnew)){
		  c->AddNode(klnew);
		  unprocessed.add(klnew);
		  ADSTransition *ktnew = new ADSTransition(c,adk,klnew,steplist[ii]); // 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,oldadk,steplist[ii]); 
		  if (!c->ExistsSimilarEdge(ktnew)){
		    c->AddEdge(ktnew);
		  }	 
		  else delete ktnew;
		}
	      }
	    } // end else
	  }
	}
      }
      unprocessed.remove(adk); // adk is processed so remove it	      
    }
  }

*/

// }