  int local_state_plus_danger(State &S, int withd, int withs);
  int global_state_plus_danger(State &S, int withd, int withs);
  int hamming_distance(State &S);
  typedef struct Destination_Entity{
    int p; /* process */
    int s; /* state */
    unsigned short op_typ;
    struct Destination_Entity *next;
  } Destination_Entity;
  typedef struct Destination_Entity_List{
    int aux;
    Destination_Entity *list;
  }Destination_Entity_List;
  Destination_Entity_List  *destination_entities_list;
  void search_destinations(State &S,int p, int s);
  void construct_destination_entities_lists(State &S);
  int old_nr_pr;

int Protocol_Heuristic::global_state_plus_danger(State &S, int withd, int withs){
  int m,i,j;
  int d,min_d;
  int p,s,cv;
  PackedState *old_now;
  int *dangerous_states_combination;
  int *Q; /* set of queues */
  Trans *t;
  int cond;
  int ncombinations;
  int *selected_processes;
  int nselected_processes;
  
  /* If it it is not a real state, but a rendezvous try, return h(pred) */
  if(S.ps->boq!=-1)  return S.pred->h;

  /* save old now */
  old_now=now;
  /* set now as current state for comp with Spin */
  now=S.ps;
  
  selected_processes=new int[S.ps->_nr_pr];
  /* See if the trans from pred was atomic */
  if(!S.move.o_t){ /* No move => root */
    /* Process info of all currently active processes: the init */
    nselected_processes=0;
    for(i=j=0; i<S.ps->_nr_pr; i++){
      p=((P0 *)(((uchar *)now)+proc_offset[i]))->_t; /* p = proc_type of i */
      if(ndangerous_states[p]!=0 && dangerous_process(p) && !blocked(S,S.move.pr)){
	selected_processes[j]=i;j++;
      }
    }
    nselected_processes=j;
    /*}  in the practice has a negatice effect */
    /* else if(S.move.o_t->atom&2){ /* If transition was atomic...*/
    /* Process info of the process in the atomic region. */
    /*p=((P0 *)(((uchar *)now)+proc_offset[S.move.pr]))->_t; /* p = proc_type of i */
    /*  if(ndangerous_states[p]!=0 && dangerous_process(p) && !blocked(S,S.move.pr)){
	selected_processes[0]=S.move.pr;
	nselected_processes=1;
	} else return 0;*/
  } else {
    /* Process info of all currently active not dangerous processes */
    i=0; j=0;
    p=((P0 *)(((uchar *)now)+proc_offset[i]))->_t; /* p = proc_type of i */
    if(ndangerous_states[p]==0 || !dangerous_process(p) && !blocked(S,i))
      ncombinations=1;
    else
      ncombinations=ndangerous_states[p];
    for(i=1; i<S.ps->_nr_pr; i++){
      p=((P0 *)(((uchar *)now)+proc_offset[i]))->_t; /* p = proc_type of i */
      if(ndangerous_states[p]!=0 && dangerous_process(p) && !blocked(S,i)){
	  ncombinations*=ndangerous_states[p];
	  if (ncombinations>MAX_COMBINATIONS){
	    //printf("Too Many Combinations!");
	    break;
	  } else{
	    selected_processes[j]=i; j++;
	  }
      }
    }
    nselected_processes=j;
    //printf(" %d combinations.\n",ncombinations);
  }
  if(nselected_processes==0) return 0;
  //printf(" Processing only  processes ");
  for(j=0; j<nselected_processes; j++){
      //printf("(%d)",selected_processes[j]);
  }
  //printf("\n");
  
  /* allocate combination */
  dangerous_states_combination=new int[now->_nr_pr];
  /* allocate queues set */
  Q=new int[now->_nr_qs];
  
  /*printf("Remembering Dangerous States (%d processes)...\n",now->_nr_pr); 
    for(i=proc0; i<=procf; i++){
    printf("\tFor process %d\n",i);
    p=((P0 *)(((uchar *)now)+proc_offset[i]))->_t;
    for(m=0; m<ndangerous_states[p]; m++){
	this_p=pptr(i);
	printf("\t\ts%d:",dangerous_states[p][m].state);
	for(t=dangerous_states[p][m].trans; t; t=t->nxt){
	printf("(%d,Q%d)",srinc_set(t->tpe[0]),(*(t->cond_variable))());	  
	}
	printf("\n");
	}
      }*/
  
  for(j=0; j<nselected_processes; j++){ /* init combination */
    i=selected_processes[j];
    /* dangerous_state_combination[i] is an index in the dangerous_states table */
    dangerous_states_combination[i]=0;
    }
  min_d=maxh;
  //printf("Beginning Heuristic Calc...\n");
  do{
    d=0;
    /* calc distance for this combination */
    //printf("\tcalc distance for this combination: ");
      for(j=0; j<nselected_processes; j++){
	i=selected_processes[j];
	p=((P0 *)(((uchar *)now)+proc_offset[i]))->_t; /* p = proc_type of i */
      }
      //printf("\n");
      
      /* calc Q and add its info to d */
      //printf("\t\tcalc Q and add its info to d\n");
      for(cv=0; cv<now->_nr_qs; cv++){
	Q[cv]=0; /* init Q */
      }
      
      for(j=0; j<nselected_processes; j++){
	i=selected_processes[j];
	p=((P0 *)(((uchar *)now)+proc_offset[i]))->_t; /* p = proc_type of i */
	s=((P0 *)pptr(i))->_p; /* s = state of i */
	this_p=pptr(i); /* for cond_variable() */
	//printf("\t\t\tProcessing queues of process %d\n",i);
	for(t=dangerous_states[p][dangerous_states_combination[i]].trans; t; t=t->nxt){
	  cond=srinc_set(t->tpe[0]); /* cond = type of condition over queue */
	  cv=t->lextok_tree->lft->val();
	  //printf("\t\t\t\tProcessing queue Q%d:",cv);
	  if(!Q[cv-1]){ /* If queue has not been added */
	    Q[cv-1]=cond; /* add queue */
	    if(withd) d+=steps_until(t->lextok_tree,0);
	  } else if((cond==Q_EMPT_F && Q[cv-1]==Q_FULL_F)
		    ||(cond==Q_FULL_F && Q[cv-1]==Q_EMPT_F)){
	    //printf("Combination not dangerous!\n");
	    /* if this combination is not dangerous, skip all computation */
	    goto NEXT_COMBINATION; /* and go to the next combination */
	  }
	}
      }
      
      
      /* calc the sum of the local distances to dangerous states */
      //printf("\t\tcalc the sum of the local distances to dangerous states\n");
      for(j=0; j<nselected_processes; j++){
	i=selected_processes[j];
	p=((P0 *)(((uchar *)now)+proc_offset[i]))->_t; /* p = proc_type of i */
	//printf("\t\t\tAdding %d\n",distances[p][inv_mapping[p][s]][inv_mapping[p][dangerous_states[p][dangerous_states_combination[i]].state]]);
	s=((P0 *)pptr(i))->_p; /* s = state of i */
	d+=distances[p][inv_mapping[p][s]][inv_mapping[p][dangerous_states[p][dangerous_states_combination[i]].state]];
      }
      
      /* actualize mind if necessary */
      if(d<min_d) min_d=d;
      
  NEXT_COMBINATION:
      /* calc next combination */
      //printf("\t\tDistance for this combination is %d\n",d);
      //printf("\tcalc next combination\n");
      m=0;
      for(j=0; j<nselected_processes; j++){
	i=selected_processes[j];
	p=((P0 *)(((uchar *)now)+proc_offset[i]))->_t; /* p=process type of i */
	if(dangerous_states_combination[i]==(ndangerous_states[p]-1)){
	  //printf("\t\tLast Dangerous state in Proc. Propagating trigger\n");
	  m++; /* propagate trigger if last */
	  dangerous_states_combination[i]=0;
	} else {
	  //printf("\t\tSetting next dangerous state in proc\n");
	  dangerous_states_combination[i]++;
	}
      }	  
  }while(m<nselected_processes); /* while trigger not out of combination */
  now=old_now; /* restore now */
  delete selected_processes; // delete garbage
  delete dangerous_states_combination; // delete garbage
  delete Q; // delete garbage
  //printf("Heuristic Value is %d\n",min_d);
  if(min_d>maxh) return maxh;
  return min_d;
}

int Protocol_Heuristic::local_state_plus_danger(State &S, int withd, int withs){
  int i,j,p;
  int dsd,sude; /* distance to dangerous state, steps until danger effective */
  int current_state;
  int local_h,global_h;
  Trans *t;
  PackedState *old_now;
  int proc0,procf;
  
  /* If it it is not a real state, but a rendezvous try, return h(pred) */
  if(S.ps->boq!=-1)  return S.pred->h;

  /* See if the trans from pred was atomic */
  if(!S.move.o_t){ /* No move => root */
    /* Try to exectue all currently active processes */
    procf=S.ps->_nr_pr-1;
    proc0=0;
    /*} In the practice has a negatice effect */
    /* else if(S.move.o_t->atom&2){ /* If transition was atomic...*/
    /*proc0=procf=S.move.pr;*/ /* In the practice has a negatice effect */
  } else {
    /* Try to exectue all currently active processes */
    procf=S.ps->_nr_pr-1;
    proc0=0;
  }
  
  old_now=now;
  now=S.ps;
  global_h=0;
  
  for(i=proc0; i<=procf; i++){
    p=((P0 *)(((uchar *)now)+proc_offset[i]))->_t;
    if(!dangerous_process(p) || ndangerous_states[p]==0) continue;
    current_state=((P0 *)pptr(i))->_p;
    this_p=pptr(i); /* for steps_until() */
    //printf("Process %d in state%d\n",i,current_state);
    local_h=maxh;
    for(j=0; j<ndangerous_states[p]; j++){
      if(withs)
	dsd=distances[p][inv_mapping[p][current_state]][inv_mapping[p][dangerous_states[p][j].state]];
      else dsd=0;
      //printf("\tDistance to danger %d is %d\n",dangerous_states[p][j].state,dsd);
      sude=0;
      for(t=dangerous_states[p][j].trans; t && withd; t=t->nxt){
	sude+=steps_until(t->lextok_tree,0);
	/* steps until transition is not executable or assertion is false */
	//printf("\t\tSUDE is %d\n",sude);
      }
      if((dsd+sude)<local_h) local_h=dsd+sude;
    }
    //printf("\tLocal h is %d\n",local_h);
    global_h+=local_h;
  }
  //printf("Global h is %d\n",global_h);
  now=old_now;
  if(global_h>maxh) return maxh;
  return global_h;
}
