/* Copyright (c) 2001 by the Institute for Computer Science,               */
/* Alberts-Ludwigs-University of Freiburg, Germany.                        */
/* All Rights Reserved.  This software is for educational purposes only.   */
/* Permission is given to distribute this code provided that this intro-   */
/* ductory message is not removed and no monies are exchanged.             */
/* No guarantee is expressed or implied by the distribution of this code.  */
/* Software written by Alberto Lluch Lafuente and Stefan Edelkamp.         */
/* References:                                                             */
/* - Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue,              */
/*   Directed Explicit Model Checking with HSF-SPIN, to appear in:         */
/*   Proc. 8th International SPIN Workshop on Model Checking Software,     */
/*   Springer LNCS 2057, Toronto, May 2001                                 */
/* - Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue,              */
/*   Protocol Verification with Heuristic Search,                          */
/*   Proc. AAAI Spring Symposium on Model-Based Validation of Inteligence, */
/*   AAAI, Stanford, April 2001.                                           */
/* Send bug-reports or questions to: lafuente@informatik.uni-freiburg.de   */

#ifndef _HEURISTICS_
#define _HEURISTICS_

/* Available Heuristics */
#define TRAIL_FILE 't'             /* Guided Simulation:
				      Trail file in spin's format is used to guide the search. */
#define INTERACTIVE 'i'            /* Interactive Simulation:
				      User is asked which successor to explore. */
#define BLIND 'b'                  /* No heuristic. */
#define ENABLED_TRANSITIONS 'e'    /* Number of enabled transitions. */
#define ACTIVE_PROCESSES 'a'       /* Number of processes that can progress. */
#define FORMULA_BASED 'f'          /* Formula based heuristic. */
#define HAMMING_DISTANCE 'h'       /* Hamming distance with given goal state. */
#define STATE_BASED 's'            /* FSM Distance to local states. */
#define SYMMETRY_FSM1 '1'          /* Admissible FSM Distance under symmetry. */
#define SYMMETRY_FSM2 '2'          /* Greedy FSM Distance under symmetry. */
#define SYMMETRY_FSM3 '3'          /* FSM Distance under symmetry as minimal assginment. */
#define ENDCLAIM 'c'               /* Distance to endstate in claim. */
#define RANDOMH 'r'                /* Random value. */
#define INTERLEAVING 'I'           /* Thread interleaving heuristic. */

#ifdef ARROWPROTOCOL
#define LINKINVERSIONS 'R'       /* Ad-hoc heuristic for the arrow protocol. */
#define HAMMINGGRAPH 'G'         /* Hamming distance only for the graph description */
#define DEGREES 'D'              /* Degree heuristic. */  
#endif

/* Dangerous transtitions and states */
#define USER_DEFINED_DANGER (Selected_Danger&1) /* consider user-defined dangerous states */
#define READ_IS_DANGER (Selected_Danger&2)      /* consider read operations as dangerous transitions */
#define SEND_IS_DANGER (Selected_Danger&4)      /* consider send operations as dangerous transitions */
#define CONDITION_IS_DANGER (Selected_Danger&8) /* consider conditions (bool. expr.) as dangerous transitions */

/* Parameters */
int Selected_Danger; /* User defined dangers (for deadlock detection): 0xCSRU
			C: User defined labels
			R: Read operations are dangerous
			S: Send operations are dangerous
			C: Conditions are dangerous */
char Selected_Heuristic; /* Selected heuristic funcition */
int Selected_History_Length; /* For the thread interleaving heuristic. */
#define DEFAULT_HISTORY_LENGTH 1
void print_heuristics(void); /* Prints out available heuristic functions. */
void print_dangers(void); /* Prints out available user defined dangers. */
#define DEFAULT_HEURISTIC BLIND
#define DEFAULT_DANGER 14 /* Conditions, read and send operations are dangerous. */
/* End Parameters */

#define MAX_COMBINATIONS 400000 /* For the experimental refinement of Hf. */

#define MY_XOR(x,y) (((!x)&&y)||(x&&(!y)))
#define MY_MIN(x,y) ((x<y)?x:y)
#define MY_MAX(x,y) ((x<y)?y:x)


class Protocol_Heuristic{
 public:
  Protocol_Heuristic(int _maxh); /* _maxh is the maximum value for the heuristic estimate. */
  void Init(void);
  int Heuristic(State *S); /* Heuristic estimate. Returns h value between 0.._maxh. */
  int maxh; /* Maximal value for the heuristic estimate. */

  /* Heuristic Functions */
  int active_processes(State *S);
  int enabled_transitions(State *S);
  int formula_based_h(State *S);
  int steps_until(HSF_Lextok *node, int t); /* Fundamental function for formula based heuristic. */
  int end_claim(State *S); /* Distance to endstate in claim.  */
  int state_based_h(State *S); /* Heuristic for a given state. Set with set_goal_state(). */
  int symmetry_fsm1(State *S); /* Heuristic for a given state. Set with set_goal_state(). */
  int symmetry_fsm2(State *S); /* Heuristic for a given state. Set with set_goal_state(). */
  int symmetry_fsm3(State *S); /* Heuristic for a given state. Set with set_goal_state(). */
  int hamming_distance(State *S); /* Heuristic for a given state. Set with set_goal_state().*/
  int thread_interleaving(State *S); /* Thread interleaving heuristic by Groce&Visser. */
  void set_goal_state(State *s); /* Sets a given state as state to search for. */
  State *goal_state; /* Goal state to search for. */
  
  /* Auxiliary variables, structures and functions */
  int *visited;
  int *mapping[_NP_];
  int *inv_mapping[_NP_];
  int nproctype_states[_NP_];
  int **distances[_NP_];
  int **new_distances;
  int is_dangerous(Trans *t);
  int dangerous_process(int process_type);
  void build_initial_dist_table(int p,int node);

  HSF_Lextok *deadlock_formula_fsm[_NP_]; /* Local deadlock formula (corresponding to each proctype). */
  HSF_Lextok *deadlock_formula; /* Deadlock formula. */
  HSF_Lextok *assertion_formula_fsm[_NP_]; /* Local assertion formula (corresponding to each proctype). */
  HSF_Lextok *assertion_formula; /* Assertion formula. */
  HSF_Lextok *error_formula;
  HSF_Lextok *new_formula(HSF_Lextok *lft, unsigned short ntyp,HSF_Lextok *rgt);
  void add_dangerous_state_to_formula(int fsm, int state, HSF_Lextok *formula);
  void construct_mapping_and_formula(int p,int node);
  void init_formula(void);
  void construct_global_formula(State *S);
  void print_formula(struct HSF_Lextok *node, int d, int with_values, int t);

  int range_max,range_min; /* To record the range of the heuristic function. */
  void print_range(void); /* Prints out the range of the heuristic function. */
  int old_nr_pr;
  int maxh_reached;

  /* For minimal assignment. */

  void improve(State *S);
  void printMatch(State *S);
  void  printGraph(State *S);
  int ONE_MAX;          /* number of nodes */
  int MAX_NODES;  /* nodes in [1..n], extra-node 0 */
  int MAX_COST;     /* max int */
  int EXTRA_NODE; /* another extra-node */
  int *match; /* matching from B in A */
  int *open;  /* search horizon. */
  int *hash;  /* visited list. */
  int *cost;  /* current priority for shortest path construction */
  int *pred;  /* predecessor edges in the shortest path tree */
  
};


/***** BEGIN OF INITS *****/

Protocol_Heuristic::Protocol_Heuristic(int _maxh){
  maxh=_maxh;
}

void Protocol_Heuristic::Init(void){
  range_max=0;
  range_min=maxh;
  maxh_reached=0;
  switch(Selected_Heuristic){
  case FORMULA_BASED:
  case ENDCLAIM:
  case STATE_BASED:
  case SYMMETRY_FSM1:
  case SYMMETRY_FSM2:    
  case SYMMETRY_FSM3:    
    init_formula(); break;
  }
}

int Protocol_Heuristic::Heuristic(State *S){
  /* Heuristic estimate. Returns a value between 0..maxh */
  int h;

  switch(Selected_Heuristic){
  case TRAIL_FILE:
  case INTERACTIVE:
  case BLIND:
    h=0; break;
  case ACTIVE_PROCESSES:
    h=active_processes(S); break;
  case ENABLED_TRANSITIONS:
    h=enabled_transitions(S); break;
  case FORMULA_BASED:
    h=formula_based_h(S); break;
  case ENDCLAIM:
    h=end_claim(S); break;
  case STATE_BASED:
    h=state_based_h(S); break;
  case SYMMETRY_FSM1:
#ifdef SYMMOD
    h=state_based_h(S); break;
#endif //
    h=symmetry_fsm1(S); break;
  case SYMMETRY_FSM2:
    h=symmetry_fsm2(S); break;
  case SYMMETRY_FSM3:
    h=symmetry_fsm3(S); break;
  case HAMMING_DISTANCE:
    h=hamming_distance(S); break;
  case RANDOMH:
    h=random()%maxh; break;
  case INTERLEAVING:
    h=thread_interleaving(S); break;
#ifdef ARROWPROTOCOL
  case HAMMINGGRAPH:
    if(!goal_state){
      printf("Error! Goal state not defined.\n");
      exit(0);
    }
    h=0;
    unsigned char the_byte;
    for(int i=0; i<10; i++){
      the_byte=(goal_state->ps->link[i])^(S->ps->link[i]);
      h+=(the_byte&0x1); the_byte>>1;
      h+=(the_byte&0x1); the_byte>>1;
      h+=(the_byte&0x1); the_byte>>1;
      h+=(the_byte&0x1); the_byte>>1;
      h+=(the_byte&0x1); the_byte>>1;
      h+=(the_byte&0x1); the_byte>>1;
      h+=(the_byte&0x1); the_byte>>1;
      h+=(the_byte&0x1);
    }
    break;

  case LINKINVERSIONS:

    if(!goal_state){
      printf("Error! Goal state not defined.\n");
      exit(0);
    }

    /* printf("Goal links are %d,%d,%d,%d,%d,%d,%d,%d,%d,%d\n", goal_state->ps->link[0], goal_state->ps->link[1], goal_state->ps->link[2], goal_state->ps->link[3], goal_state->ps->link[4], goal_state->ps->link[5], goal_state->ps->link[6], goal_state->ps->link[7], goal_state->ps->link[8], goal_state->ps->link[9]);*/

    h=(goal_state->ps->link[0] != S->ps->link[0])+(goal_state->ps->link[1] != S->ps->link[1])+(goal_state->ps->link[2] != S->ps->link[2])+(goal_state->ps->link[3] != S->ps->link[3])+(goal_state->ps->link[4] != S->ps->link[4])+(goal_state->ps->link[5] != S->ps->link[5])+(goal_state->ps->link[6] != S->ps->link[6])+(goal_state->ps->link[7] != S->ps->link[7])+(goal_state->ps->link[8] != S->ps->link[8])+(goal_state->ps->link[9] != S->ps->link[9]);
    break;

  case DEGREES:
    unsigned char indegree1[10],indegree2[10],aux1[11],aux2[11]; int j;
    for(int i=0; i<10; i++){
      indegree1[i]=0; indegree2[i]=0;
    }
    for(int i=0; i<10; i++){
      indegree1[S->ps->link[i]]++; indegree2[goal_state->ps->link[i]]++;
    }
    for(int i=0; i<11; i++){
      aux1[i]=0; aux2[i]=0; 
    }
    for(int i=0; i<10; i++){
      aux1[indegree1[i]]++; aux2[indegree2[i]]++;
    }
    j=0;
    for(int i=0; i<11; i++){
      while(aux1[i]>0){
	indegree1[j]=i; aux1[i]--; j++;
      }
    }
    j=0;
    for(int i=0; i<11; i++){
      while(aux2[i]>0){
	indegree2[j]=i; aux2[i]--; j++;
      }
    }
    h=0;
    for(int i=0; i<10; i++){
      h+= (indegree1[i]>=indegree2[i])? (indegree1[i]-indegree2[i]):(indegree2[i]-indegree1[i]);
    }
    break;

#endif
  default: printf("Error! Undefined Heuristic Function\n"); print_heuristics(); exit(0);
  }
  if(h<range_min) range_min=h; /* Statistics. */
  if(h>range_max) range_max=h;
  if(h<0){
    printf("Error! Negative heuristic value.\n"); bug(); exit(0);
  }
  if(h>maxh){
    if(!maxh_reached){
      printf("Warning! Heuristic estimate over maximum %d. Computed value is %d.\n",maxh,h);
      maxh_reached=1;
    }
    h=maxh;
  }
  return h;
}

/***** END OF INITS *****/



/***** BEGIN OF ACTIVENESS BASED HEURISTICS *****/

int Protocol_Heuristic::active_processes(State *S){
  Trans *t,*t_aux;
  char ot,ot_aux,o_pm_aux, m;
  short II, From, To, tt, II_aux, tt_aux;
  Trail *trpt;
  unsigned char* this_p_aux;
  int n;
  PackedState *old_now,*boq_now;
  PackedState aux_state1,aux_state2;

  /* If it it is not a real state, but a rendezvous try, return h(pred) */
  if(S->ps->boq!=-1)  return S->pred->h;
  
  old_now=now; 
  now=&aux_state1;
  memcpy((void*)now,(void *)S->ps,S->ps->_vsz);

  /* See if the trans from pred was atomic */
  if(!S->move.o_t){ /* No move => root */
    /* Try to exectue all currently active processes */
    From=now->_nr_pr-1;
    To=0;
  } else if(S->move.o_t->atom&2){ /* If transition was atomic...*/
    /* Continue executing the same process as in the previous trans. */
    From=To=S->move.pr;
  } else {
    /* Try to exectue all currently active processes */
    From=now->_nr_pr-1;
    To=0;
  }
  
  n=0;
  trpt=&S->move;
  trpt->tau = trpt->tau & ~(16|32|64); /* make sure these are off */
  for(II=From; II>=To; II-=1){
    this_p=pptr(II);
    tt=(short) ((P0 *)this_p)->_p;
    ot=(unsigned char) ((P0 *)this_p)->_t;
    for(t=trans[ot][tt]; t; t=t->nxt){
      m=do_transit(t,II,0); /* #include FORWARD_MOVES  */
      if(!m) continue;
      if(now->boq!=-1){
	this_p_aux=this_p; II_aux=II; tt_aux=tt; ot_aux=ot; t_aux=t; o_pm_aux=trpt->o_pm;
	boq_now=now;
	now=&aux_state2;
	memcpy((void*)now,(void *)boq_now,S->ps->_vsz);
	for(II=From; II>=To; II-=1){
	  this_p=pptr(II);
	  tt=(short) ((P0 *)this_p)->_p;
	  ot=(unsigned char) ((P0 *)this_p)->_t;
	  for(t=trans[ot][tt]; t; t=t->nxt){
	    m=do_transit(t,II,0); /* #include FORWARD_MOVES */
	    if(!m) continue;
	    n++;
	    goto LEAVE_RENDEZVOUS;
	  }
	}
      LEAVE_RENDEZVOUS:
	now=boq_now;
	memcpy((void*)now,(void *)S->ps,S->ps->_vsz);
	this_p=this_p_aux; II=II_aux; tt=tt_aux; ot=ot_aux; t=t_aux; trpt->o_pm=o_pm_aux;
      } else{
	memcpy((void*)now,(void *)S->ps,S->ps->_vsz);
	n++;
      }
      break;
    }
  }
  now=old_now;
  return n;
}

int Protocol_Heuristic::enabled_transitions(State *S){
  Trans *t,*t_aux;
  char ot,ot_aux,o_pm_aux, m;
  short II, From, To, tt, II_aux, tt_aux;
  Trail *trpt;
  unsigned char* this_p_aux;
  int n;
  PackedState *old_now,*boq_now;
  PackedState aux_state1,aux_state2;

  /* If it it is not a real state, but a rendezvous try, return h(pred) */
  if(S->ps->boq!=-1)  return S->pred->h;
  
  old_now=now;
  now=&aux_state1;
  memcpy((void*)now,(void *)S->ps,S->ps->_vsz); //*now=*S->ps;
  
  /* See if the trans from pred was atomic */
  if(!S->move.o_t){ /* No move => root */
    /* Try to exectue all currently active processes */
    From=now->_nr_pr-1;
    To=0;
  } else if(S->move.o_t->atom&2){ /* If transition was atomic...*/
    /* Continue executing the same process as in the previous trans. */
    From=To=S->move.pr;
  } else {
    /* Try to exectue all currently active processes */
    From=now->_nr_pr-1;
    To=0;
  }
  
  n=0;
  trpt=&S->move;
  trpt->tau = trpt->tau & ~(16|32|64); /* make sure these are off */
  for(II=From; II>=To; II-=1){
    this_p=pptr(II);
    tt=(short) ((P0 *)this_p)->_p;
    ot=(unsigned char) ((P0 *)this_p)->_t;
    for(t=trans[ot][tt]; t; t=t->nxt){
        m=do_transit(t,II,0); /* #include FORWARD_MOVES  */
	if(!m) continue;
	if(now->boq!=-1){
	this_p_aux=this_p; II_aux=II; tt_aux=tt; ot_aux=ot; t_aux=t; o_pm_aux=trpt->o_pm;
	boq_now=now;
	now=&aux_state2;
	memcpy((void*)now,(void *)boq_now,S->ps->_vsz);
	for(II=From; II>=To; II-=1){
	  this_p=pptr(II);
	  tt=(short) ((P0 *)this_p)->_p;
	  ot=(unsigned char) ((P0 *)this_p)->_t;
	  for(t=trans[ot][tt]; t; t=t->nxt){
            m=do_transit(t,II,0); /* #INCLUDE MOVE_FORWAD */
	    if(!m) continue;
	    n++;
	    goto LEAVE_RENDEZVOUS;
	  }
	}
      LEAVE_RENDEZVOUS:
	now=boq_now;
	*now=*S->ps;
	this_p=this_p_aux; II=II_aux; tt=tt_aux; ot=ot_aux;	t=t_aux; trpt->o_pm=o_pm_aux;
      } else{
	*now=*S->ps;
	n++;
      }
    }
  }
  now=old_now;
  return n;
}

/***** END OF ACTIVEESS BASED HEURISTICS ******/


/****** BEGIN OF STEPS_UNTIL() A VERY IMPORTANT FUNCTION */

int Protocol_Heuristic::steps_until(HSF_Lextok *node, int t){
  /* estimates number of steps until value/executability of lextok is t */
  /* now MUST point to the actual state */
  /* this_p MUST point to the actual process */
  int returning_value=0;
  int queue,tag,fsm;
  
  switch (node->ntyp) {
  case CONST: returning_value=MY_XOR(t,node->val())?maxh:0; break;
    
  case '!': returning_value=steps_until(node->lft, !t); break;
  case UMIN: returning_value=MY_XOR(t,node->val())?1:0; break;
  case '~': returning_value=MY_XOR(t,node->val())?1:0; break;
    
  case '/': returning_value=MY_XOR(t,node->val())?1:0; break;
  case '*': returning_value=MY_XOR(t,node->val())?1:0; break;
  case '-': returning_value=MY_XOR(t,node->val())?1:0; break;
  case '+': returning_value=MY_XOR(t,node->val())?1:0; break;
  case '%': returning_value=MY_XOR(t,node->val())?1:0; break;
  case '&': returning_value=MY_XOR(t,node->val())?1:0; break;
  case '^': returning_value=MY_XOR(t,node->val())?1:0; break;
  case '|': returning_value=MY_XOR(t,node->val())?1:0; break;
  case LT:
      if(MY_XOR(t,node->val())){
	returning_value=(node->lft->val())-(node->rgt->val()); /* Supp. incr and decr. */
	if(returning_value<0) returning_value=-returning_value;
      } else returning_value=0;
      break;
  case GT: 
      if(MY_XOR(t,node->val())){
	returning_value=(node->lft->val())-(node->rgt->val()); /* Supp. incr and decr. */
	if(returning_value<0) returning_value=-returning_value;
      } else returning_value=0;
      break;
  case LE: 
      if(MY_XOR(t,node->val())){
	returning_value=(node->lft->val())-(node->rgt->val()); /* Supp. incr and decr. */
	if(returning_value<0) returning_value=-returning_value;
	returning_value++;
      } else returning_value=0;
      break;
  case GE: 
      if(MY_XOR(t,node->val())){
	returning_value=(node->lft->val())-(node->rgt->val()); /* Supp. incr and decr. */
	if(returning_value<0) returning_value=-returning_value;
	returning_value++;
      } else returning_value=0;
      break;
  case NE: 
      if(MY_XOR(t,node->val())){
	returning_value=(node->lft->val())-(node->rgt->val()); /* Supp. incr and decr. */
	if(returning_value<0) returning_value=-returning_value;
      } else returning_value=0;
      break;
  case EQ:
    if(node->lft->ntyp!='p' && node->rgt->ntyp!='p'){ /* normal comparation */
      if(MY_XOR(t,node->val())){
	returning_value=(node->lft->val())-(node->rgt->val()); /* Supp. incr and decr. */
	if(returning_value<0) returning_value=-returning_value;
      } else returning_value=0;
    } else {/* fsm i at state j */
      if(node->lft->ntyp=='p'){
	fsm=(int)node->lft->lft;
	if(node->lft->rgt->val()+BASE>=(int)now->_nr_pr){
	  /* process is not active. */
	  returning_value=0; break;
	}
      }
      if(node->rgt->ntyp=='p'){
	fsm=(int)node->rgt->lft;
	if(node->rgt->rgt->val()+BASE>=(int)now->_nr_pr){
	  /* process is not active. */
         returning_value=0; break;
	}
      }
      returning_value=distances[fsm][inv_mapping[fsm][node->lft->val()]][inv_mapping[fsm][node->rgt->val()]];
    }
    break;
  case OR:
    if(t) returning_value=MY_MIN(steps_until(node->lft,1),steps_until(node->rgt,1));
    else  returning_value=steps_until(node->lft,0)+steps_until(node->rgt,0);
    break;
  case AND:
    if(t) returning_value=steps_until(node->lft,1)+steps_until(node->rgt,1);
    else returning_value=MY_MIN(steps_until(node->lft,0),steps_until(node->rgt,0));
    break;
  case LSHIFT: returning_value=MY_XOR(t,node->val())?1:0; break;
  case RSHIFT: returning_value=MY_XOR(t,node->val())?1:0; break;
    
  case TIMEOUT: returning_value=0; break; 
  case RUN: returning_value=0; break;
  case ENABLED: returning_value=0; break; /* ??? */
  case NONPROGRESS: returning_value=0; break;
  case PC_VAL: returning_value=0; break; /* ??? */
    
  case LEN:
    queue=node->lft->val(); if(!queue) returning_value=0;
    if((((Q0 *)qptr(queue-1))->Qlen)==0) returning_value=(t?1:0);
    else returning_value=(t?0:(((Q0 *)qptr(queue-1))->Qlen));
    break;
  case FULL: returning_value=0; break; 
    queue=node->lft->val(); if(!queue) returning_value=0;
    if((((Q0 *)qptr(queue-1))->Qlen)==q_max[queue]) returning_value=(t?0:1);
    else returning_value=(t?q_max[queue]-(((Q0 *)qptr(queue-1))->Qlen):0);
    break;
  case EMPTY:
    queue=node->lft->val(); if(!queue) returning_value=0;
    if((((Q0 *)qptr(queue-1))->Qlen)==0) returning_value=(t?0:1);
    else returning_value=(t?(((Q0 *)qptr(queue-1))->Qlen):0);
    break;
  case NFULL:
    queue=node->lft->val(); if(!queue) returning_value=0;
    if((((Q0 *)qptr(queue-1))->Qlen)==q_max[queue]) returning_value=(t?1:0);
    else returning_value=(t?0:q_max[queue]-(((Q0 *)qptr(queue-1))->Qlen));
    break;
  case NEMPTY:
    queue=node->lft->val(); if(!queue) returning_value=0;
    if((((Q0 *)qptr(queue-1))->Qlen)==0) returning_value=(t?1:0);
    else returning_value=(t?0:(((Q0 *)qptr(queue-1))->Qlen));
    break;
  case 's':
    queue=node->lft->val();
    if(!queue) return 0;
    returning_value=q_max[queue]-(((Q0 *)qptr(queue-1))->Qlen);
    if(returning_value<0) returning_value=0; /* Can occur. Seems ok. */
    break;     
  case 'r':
  case 'R':
    queue=node->lft->val(); if(!queue) return 0;
    if(node->rgt->lft->ntyp==NAME){ /* untagged receive */
      returning_value=(((Q0 *)qptr(queue-1))->Qlen); tag=-1;
      if(t){
	returning_value=returning_value?0:1;
      } else{
	returning_value=returning_value;
      }
    } else { /* tagged receive */
      tag=node->rgt->lft->val();
      if(t){
	for(returning_value=0; returning_value<(((Q0 *)qptr(queue-1))->Qlen); returning_value++){
	  //printf("Q[%d]=%d\n",returning_value,((Q1*)qptr(queue-1))->contents[returning_value].fld0);
	  if( (((Q0*)qptr(queue-1))->contents[returning_value].fld0)==tag) break;
	}
	if((((Q0 *)qptr(queue-1))->Qlen)==returning_value) returning_value++;
      } else{
	for(returning_value=0; returning_value<(((Q0 *)qptr(queue-1))->Qlen); returning_value++){
	  //printf("Q[%d]=%d\n",returning_value,((Q1*)qptr(queue-1))->contents[returning_value].fld0);
	  if( (((Q0*)qptr(queue-1))->contents[returning_value].fld0)!=tag) break;
	}
      }
    }
    break; 

  case 'c': returning_value=steps_until(node->lft,t); break;
  case  ELSE: returning_value=0; break;
  case '?':
    returning_value=MY_MIN(steps_until(node->lft,t)+steps_until(node->lft->lft,t),steps_until(node->lft,!t)+steps_until(node->lft->rgt,t));
    break;
  case ASGN: returning_value=0; break;
  case PRINT: returning_value=0; break;
  case NAME: returning_value=MY_XOR(node->val(),t)?1:0; break;

    /* Hardcode for invariant violation in the elevator protocol*/
    if(!MY_XOR(node->val(),t)){
      returning_value=0;
      //printf("variable %d is set\n",node);
    } else {
      //printf("variable %d is NOT set\n",node);
      if(node==&Lextok_Wood[37]){ /*elevator_opened */
	//printf("variable is elevator_opened\n");
	if(t)
	  returning_value=1+distances[2][inv_mapping[2][((P0 *)pptr(3))->_p]][inv_mapping[2][25]];
	else
	  returning_value=1+distances[2][inv_mapping[2][((P0 *)pptr(3))->_p]][inv_mapping[2][22]];
	
      } else if(node==&Lextok_Wood[36]){ /* elevator_stopped */
	//printf("variable is elevator_stopped\n");
	if(t)
	  returning_value=1+MY_MIN(
            distances[0][inv_mapping[0][((P0 *)pptr(2))->_p]][inv_mapping[0][13]],
	    MY_MIN(distances[0][inv_mapping[0][((P0 *)pptr(2))->_p]][inv_mapping[0][21]],
	    distances[2][inv_mapping[2][((P0 *)pptr(3))->_p]][inv_mapping[2][28]]));
	else
	  returning_value=1+distances[2][inv_mapping[2][((P0 *)pptr(3))->_p]][inv_mapping[2][33]];
      }
      else{
	printf("Error. Undef. variable!!!\n");
      }
    }
    //printf("H is %d\n",returning_value);
    break;
	
  case   'p': returning_value=0; break;
  case   'q': returning_value=0; break;
  case ASSERT: returning_value=steps_until(node->lft,t); break;
  case '.': returning_value=0; break;
  case BREAK: returning_value=0; break;
  case GOTO: returning_value=0; break;
  case '@': returning_value=0; break; /* FSM i in state j */

  case FSM:
    this_p=pptr((int)node->lft);
    returning_value=steps_until(node->rgt,t);
    //printf("\tFor fsm%d r is %d\n",(int)node->lft,returning_value);
    break;
  case STATE:
    returning_value=distances[((P0 *)this_p)->_t][inv_mapping[((P0 *)this_p)->_t][((P0 *)this_p)->_p]][inv_mapping[((P0 *)this_p)->_t][(int)(node->lft)]];
    //printf("Distance between %d[%d] and %d[%d] is %d\n",((P0 *)this_p)->_p,inv_mapping[((P0 *)this_p)->_t][((P0 *)this_p)->_p],(int)(node->lft),inv_mapping[((P0 *)this_p)->_t][(int)(node->lft)],returning_value);
    break;

  default:
#ifdef DEBUG
      printf("Warning: while computing heuristic, bad node type %d(%c)\n",node->ntyp,node->ntyp);
#endif // DEBUG
      returning_value=0;
  }
  if(returning_value<0){
    printf("Error: steps until returning negative value. ntyp=%d(%c)\n",node->ntyp,node->ntyp);
    bug(); exit(0);
  }
  if (returning_value>maxh) returning_value=maxh;
  return returning_value;
}

/***** END OF STEPS_UNTIL() *****/


/***** OTHER THINGS *****/

void print_heuristics(void)
{
  printf("Possible Heuristic Functions.\n");
  printf("\tHeuristics for simulation\n");
  printf("\t%c: guided simulation (use trail file %s.trail).\n",TRAIL_FILE,Source);
  printf("\t%c: interactive search.\n",INTERACTIVE);
  printf("\tHeuristics for searching unknown error states\n");
  printf("\t%c: blind heuristic (h is always 0) for a breadth-first search.\n",BLIND);
  printf("\t%c: number of enabled transitions (only for deadlock detection).\n",ENABLED_TRANSITIONS);
  printf("\t%c: number of non-blocked processes (only for deadlock detection).\n",ACTIVE_PROCESSES);
  printf("\t%c: Hf (See documentation. Only for checking safety properties).\n",FORMULA_BASED);
  printf("\t%c: thread interleaving.\n",INTERLEAVING);
  printf("\t%c: distance to endstate in claim.\n",ENDCLAIM);
  printf("\t%c: random value.\n",RANDOMH);
  printf("\tHeuristics for a searching for a known error state\n");
  printf("\t%c: hamming distance (requires error trail).\n",HAMMING_DISTANCE);
  printf("\t%c: sum of local distances in fsm (requires error trail).\n",STATE_BASED);
  printf("\t%c: fsm under symmetry in O(|[e]|) (requires error trail).\n",SYMMETRY_FSM1);
  printf("\t%c: fsm under symmetry in O(n^3) (requires error trail).\n",SYMMETRY_FSM3);
  printf("\t%c: fsm under symmetry in O(n^2) (less informed, requires error trail).\n",SYMMETRY_FSM2);
  printf("\tDefault value is %c\n",DEFAULT_HEURISTIC);
}

void print_dangers(void){
  printf("User defined dangers (for deadlock detection):\n");
  printf("\t0: no danger\n");
  printf("\t1: dangerous states are those marked with label 'danger' in the model\n");
  printf("\t2: receive operations are dangerous transitions\n");
  printf("\t4: send operations are dangerous transitions\n");
  printf("\t8: conditions are dangerous transitions\n");
  printf("\tThe last three can be combined\n");
  printf("\tFor example: 2+4+8=14 means that receives, sends and conditions are dangerous\n");
}

void Protocol_Heuristic::print_range(void){
  printf("[%d..%d]",range_min,range_max);
}

/***** END OF OTHER THINGS *****/


/***** ALL AS FORMULA *****/

int Protocol_Heuristic::is_dangerous(Trans *t){
  /* Returns 1 if the transitions is dangerous for deadlock detection. */
  int op_typ;
  int dangerous=0;
  
  if(!t->lextok_tree){
#ifdef DEBUG
    printf("Warning! No lextok tree for transition %d.\n",t->t_id);
#endif //
    return 0;
  }
  op_typ=t->lextok_tree->ntyp;
  if(Selected_Goal==DEADLOCK || Selected_Goal==SIMPLESAFETY)
    dangerous=dangerous||(
			  (READ_IS_DANGER && op_typ=='r') /* Receive operations */
			  ||(SEND_IS_DANGER && op_typ=='s') /* Send operations */
			  ||(CONDITION_IS_DANGER && op_typ=='c') /* Conditions */
			  );
  if(Selected_Goal==ASSERTION_VIOLATION || Selected_Goal==SIMPLESAFETY)
    dangerous=dangerous||(op_typ==ASSERT); /* Assertions */
  return dangerous;
}

int Protocol_Heuristic::dangerous_process(int process_type){
  /* Returns 1 if the process type is dangerous for deadlock detection. */
#ifdef VERI
  if(process_type==VERI) return 0;
#endif //
  return process_type<_NP_; /* Is _NP_-1 dangerous? */
}

HSF_Lextok *Protocol_Heuristic::new_formula(HSF_Lextok *lft, unsigned short ntyp,HSF_Lextok *rgt){
  HSF_Lextok *f;

  f=new HSF_Lextok;
  f->ntyp=ntyp;
  f->lft=lft;
  f->rgt=rgt;
  return f;
} 

void Protocol_Heuristic::construct_mapping_and_formula(int p,int node){
  Trans *t;
  int dangerous_state,assertion_state;
  HSF_Lextok *state_formula;

  //printf("DFS-Node %d\n",node);
  visited[node]=1;
  inv_mapping[p][node]=nproctype_states[p];
  mapping[p][nproctype_states[p]++]=node;
  
  dangerous_state=1; assertion_state=0; /* a state is at first dangerous */
  for(t=trans[p][node];t;t=t->nxt){
    if(!is_dangerous(t)) dangerous_state=0;
    if(t->lextok_tree && t->lextok_tree->ntyp==ASSERT) assertion_state=1;
#ifdef VERI
    if(accpstate[VERI][t->st]) error_formula=t->lextok_tree;
#endif //
    if(!visited[t->st]) construct_mapping_and_formula(p,t->st);
  }


  if(assertion_state && (Selected_Goal==ASSERTION_VIOLATION || Selected_Goal==SIMPLESAFETY)){
    state_formula=(HSF_Lextok*)0;
    for(t=trans[p][node]; t&&(t->lextok_tree->ntyp==ASSERT); t=t->nxt){
      if(!state_formula) state_formula=t->lextok_tree->lft;
      else state_formula=new_formula(state_formula,AND,t->lextok_tree->lft);
    }
    if(state_formula){
      state_formula=new_formula(state_formula,'!',(HSF_Lextok*)0); /* f=dangerous(node) */
      state_formula=new_formula(new_formula((HSF_Lextok*)node,STATE,(HSF_Lextok *)0),AND,state_formula);
    }
    else
      state_formula=new_formula((HSF_Lextok*)node,STATE,(HSF_Lextok *)0);
    if(assertion_formula_fsm[p])
      assertion_formula_fsm[p]=new_formula(assertion_formula_fsm[p],OR,state_formula);
    else
      assertion_formula_fsm[p]=state_formula;    
  }

  if(!USER_DEFINED_DANGER){
    dangstate[p][node]=dangerous_state;
  }

  /* if state is dangerous construct... */
  if(dangstate[p][node] && (Selected_Goal==DEADLOCK || Selected_Goal==SIMPLESAFETY)){
    state_formula=(HSF_Lextok*)0;
    for(t=trans[p][node];t;t=t->nxt){
      if(!state_formula) state_formula=t->lextok_tree;
      else state_formula=new_formula(state_formula,OR,t->lextok_tree);
      }
    if(state_formula){
      state_formula=new_formula(state_formula,'!',(HSF_Lextok*)0); /* f=dangerous(node) */
      state_formula=new_formula(new_formula((HSF_Lextok*)node,STATE,(HSF_Lextok *)0),AND,state_formula);
    }
    else
      state_formula=new_formula((HSF_Lextok*)node,STATE,(HSF_Lextok *)0);
    if(deadlock_formula_fsm[p])
      deadlock_formula_fsm[p]=new_formula(deadlock_formula_fsm[p],OR,state_formula);
    else
      deadlock_formula_fsm[p]=state_formula;
  }
}

void Protocol_Heuristic::build_initial_dist_table(int p,int node){
  Trans *t;
  //printf("BT-Node %d\n",node);
  
  visited[node]=1;
  for(t=trans[p][mapping[p][node]];t;t=t->nxt){
    //printf("BTsucc-node %d\n",inv_mapping[p][t->st]);      
    if(t->st!=mapping[p][node]) distances[p][node][inv_mapping[p][t->st]] = 1;
    if(!visited[inv_mapping[p][t->st]]){
      build_initial_dist_table(p,inv_mapping[p][t->st]);
    }
  }
}

void Protocol_Heuristic::init_formula(void){
  int i,j,k,p;
  Trans *t;
  
  for(p=0; p<_NP_; p++){
    deadlock_formula_fsm[p]=(HSF_Lextok*)0;
    assertion_formula_fsm[p]=(HSF_Lextok*)0;
  }

  for(p=0; p<_NP_ /*&& dangerous_process(p)*/; p++){
    /* Construct Mapping Functions and List of Dangerous States */
#ifdef DEBUG
    printf("Proctype %d: %s\n",p,procname[p]);
#endif //
    visited=new int[nstates_proc[p]];
    mapping[p]=new int[nstates_proc[p]];
    inv_mapping[p]=new int[nstates_proc[p]];
    deadlock_formula_fsm[p]=(HSF_Lextok*)0;
    assertion_formula_fsm[p]=(HSF_Lextok*)0;
    for(i=0; i<nstates_proc[p]; i++) visited[i]=0;
    nproctype_states[p]=0;
    construct_mapping_and_formula(p,start_proc[p]);
    
    /* Allocate Tables for Floyd-Warshall algorithm */
    distances[p]=new int*[nproctype_states[p]];
    new_distances=new int*[nproctype_states[p]];
    for(i=0;i<nproctype_states[p];i++){
      distances[p][i] = new int[nproctype_states[p]];
      new_distances[i] = new int[nproctype_states[p]];
      for (j=0;j<nproctype_states[p];j++)
	distances[p][i][j] = nproctype_states[p]+1;
      distances[p][i][i] = 0;
      }
    
    /* Prepare Table for Floyd-Warshall algorithm */
    for(i=0; i<nproctype_states[p]; i++) visited[i]=0;
    build_initial_dist_table(p,0);
    
      /* Floyd-Warshall algorithm */  
    for (k=0;k<nproctype_states[p];k++) {
      for (i=0;i<nproctype_states[p];i++) {
	for (j=0;j<nproctype_states[p];j++){
	  if (distances[p][i][j] < distances[p][i][k] + distances[p][k][j])
	    new_distances[i][j] = distances[p][i][j];
	  else
	    new_distances[i][j] = distances[p][i][k] + distances[p][k][j];
	}
      }
      distances[p] = new_distances;
    }
    
    /* Print Dist Table */
#ifdef DEBUG
    printf("\tDistances Table for FSM%d:\n",p);
    printf("\t[%2.d]",0);
    for (i=0;i<nproctype_states[p];i++) 
      printf("[%2.d]",mapping[p][i]);
    printf("\n");
    for (i=0;i<nproctype_states[p];i++) {
      printf("\t[%2.d]",mapping[p][i]);
      for (j=0;j<nproctype_states[p];j++)
	printf("(%2.d)",distances[p][i][j]);
      printf("\n");
    }
    /* Print error formula */
    if(Selected_Goal==SIMPLESAFETY || Selected_Goal==DEADLOCK){
      printf("Deadlock formula for FSM%d is:\n",p);
      print_formula(deadlock_formula_fsm[p],0,0,0);
      printf("\n");
    }
    if(Selected_Goal==SIMPLESAFETY || Selected_Goal==ASSERTION_VIOLATION){
      printf("Assertion formula for FSM%d is:\n",p);
      print_formula(assertion_formula_fsm[p],0,0,0);
      printf("\n");
    }
#endif // DEBUG
  }
}
  
void Protocol_Heuristic::print_formula(HSF_Lextok *node,int d, int with_values, int t){
  /* now MUST point to the actual state */
  /* this_p MUST point to the actual process */
  int i,v;
  
  if(!node) printf("false");
  else{
  for(i=0; i<(d-1); i++) printf("    ");
  if(d!=0) printf("|-> ");
  if(with_values){
    v=steps_until(node, t);
    printf("[h=%d] ",v);
  }
  switch (node->ntyp) {
  case CONST: printf("%d",node->val()); break;

  case '!': printf("!"); printf("\n"); print_formula(node->lft,d+1,with_values,!t); break;
  case UMIN: printf("-"); print_formula(node->lft,0,with_values,t); break;
  case '~': printf("~"); print_formula(node->lft,0,with_values,t); break;
    
  case '/': print_formula(node->lft,d,with_values,t); printf("/"); print_formula(node->rgt,d,with_values,t); break;
  case '*': print_formula(node->lft,d,with_values,t); printf("*"); print_formula(node->rgt,d,with_values,t); break;
  case '-': print_formula(node->lft,d,with_values,t); printf("-"); print_formula(node->rgt,d,with_values,t); break;
  case '+':
    printf("+"); printf("\n");
    print_formula(node->rgt,d+1,with_values,t); printf("\n");
    print_formula(node->lft,d+1,with_values,t); break;
  case '%':
    printf("%"); printf("\n");
    print_formula(node->rgt,d+1,with_values,t); printf("\n");
    print_formula(node->lft,d+1,with_values,t); break;
  case '&': print_formula(node->lft,d,with_values,t); printf("&"); print_formula(node->rgt,d,with_values,t); break;
  case '^': print_formula(node->lft,d,with_values,t); printf("^"); print_formula(node->rgt,d,with_values,t); break;
  case '|': print_formula(node->lft,d,with_values,t); printf("|"); print_formula(node->rgt,d,with_values,t); break;
  case LT: print_formula(node->lft,d,with_values,t); printf("<"); print_formula(node->rgt,d,with_values,t); break;
  case GT: print_formula(node->lft,d,with_values,t); printf(">"); print_formula(node->rgt,d,with_values,t); break;
  case LE: print_formula(node->lft,d,with_values,t); printf("<="); print_formula(node->rgt,d,with_values,t); break;
  case GE: print_formula(node->lft,d,with_values,t); printf(">="); print_formula(node->rgt,d,with_values,t); break;
  case NE: print_formula(node->lft,d,with_values,t); printf("!="); print_formula(node->rgt,d,with_values,t); break;
  case EQ:
    printf("=="); printf("\n");
    print_formula(node->rgt,d+1,with_values,t); printf("\n");
    print_formula(node->lft,d+1,with_values,t); break;
  case OR:
    printf("OR (%d)",t); printf("\n");
    print_formula(node->lft,d+1,with_values,t); printf("\n");
    print_formula(node->rgt,d+1,with_values,t); break;
  case AND: 
    printf("AND"); printf("\n");
    print_formula(node->lft,d+1,with_values,t); printf("\n");
    print_formula(node->rgt,d+1,with_values,t); break;
  case LSHIFT: print_formula(node->lft,d,with_values,t); printf("<<"); print_formula(node->rgt,d,with_values,t); break;
  case RSHIFT: print_formula(node->lft,d,with_values,t); printf(">>"); print_formula(node->rgt,d,with_values,t); break;
    
  case TIMEOUT: printf("timeout"); break;
  case RUN: printf("run"); break;
  case ENABLED:printf("enabled"); break;
  case NONPROGRESS:printf("non_progress"); break;
  case PC_VAL:printf("pc_val"); break;
    
  case LEN: printf("len(");print_formula(node->lft,d,0,t);printf(")"); break;
  case FULL: printf("full(");print_formula(node->lft,d,0,t);printf(")"); break;
  case EMPTY: printf("empty(");print_formula(node->lft,d,0,t);printf(")"); break;
  case NFULL: printf("!full(");print_formula(node->lft,d,0,t);printf(")"); break;
  case NEMPTY: printf("!empty(");print_formula(node->lft,d,0,t);printf(")"); break;

  case 's': printf("queue"); printf("!"); print_formula(node->rgt,0,0,t); break;
  case 'r': printf("queue"); printf("?"); print_formula(node->rgt,0,0,t); break;
  case 'R': printf("queue"); printf("?"); print_formula(node->rgt,0,0,t); break;

  case 'c': print_formula(node->lft,d,with_values,t); break;
  case  ELSE: break;
  case '?': print_formula(node->lft,d,0,t); printf("?"); print_formula(node->rgt,d,0,t); break;
  case ASGN: break;
  case PRINT: break;
  case NAME: printf("var"); break;
  case   'p': break;
  case   'q': break;
  case ASSERT: print_formula(node->lft,d,0,t); break;
  case '.': print_formula(node->lft,d,0,t); printf("."); print_formula(node->rgt,d,0,t); break;
  case BREAK:  break;
  case GOTO: break;
  case '@': break;

  case ',': printf("tag"); break;

  case FSM: printf("FSM%d\n",(int)node->lft); print_formula(node->rgt,d+1,with_values,t); break;
  case STATE: printf("fsm-state==%d",(int)node->lft); break;

  default: break;
    //printf("Warning: while printing formula, bad node type\n");
  }
  }
}

void Protocol_Heuristic::construct_global_formula(State *S){
  int fsm,i;
  HSF_Lextok *fsm_formula;

  if(Selected_Goal==SIMPLESAFETY || Selected_Goal==DEADLOCK){
    /* Construct formula for deadlocks */
    deadlock_formula=(HSF_Lextok*)0;
    for(i=0; i<now->_nr_pr; i++){
      fsm=((P0 *)(((uchar *)now)+proc_offset[i]))->_t;
      if(deadlock_formula_fsm[fsm])
	fsm_formula=new_formula((HSF_Lextok *)i,FSM,deadlock_formula_fsm[fsm]);
      else
	fsm_formula=(HSF_Lextok *)0;
      if(!deadlock_formula) deadlock_formula=fsm_formula;
      else if(fsm_formula)
	deadlock_formula=new_formula(deadlock_formula,AND,fsm_formula);
    }
  }

  if(Selected_Goal==SIMPLESAFETY || Selected_Goal==ASSERTION_VIOLATION){
    /* Construct formula for assertions */
    assertion_formula=(HSF_Lextok*)0;
    for(i=0; i<now->_nr_pr; i++){
      fsm=((P0 *)(((uchar *)now)+proc_offset[i]))->_t;
      if(assertion_formula_fsm[fsm])
	fsm_formula=new_formula((HSF_Lextok *)i,FSM,assertion_formula_fsm[fsm]);
      else
	fsm_formula=(HSF_Lextok *)0;
      if(!assertion_formula) assertion_formula=fsm_formula;
      else if(fsm_formula)
	assertion_formula=new_formula(assertion_formula,AND,fsm_formula);
    }
  }

  /* Construct error formula */
  if(Selected_Goal==LTL){
    error_formula;
#ifdef VERI
    error_formula=trans[VERI][start_claim]->lextok_tree;
#endif //
  }
  else if(Selected_Goal==DEADLOCK)
    error_formula=deadlock_formula;
  else if(Selected_Goal==ASSERTION_VIOLATION)
    error_formula=assertion_formula;
  else if(Selected_Goal==SIMPLESAFETY){
    error_formula=assertion_formula;
    if(!error_formula)
      error_formula=deadlock_formula;
    else if(deadlock_formula)
      error_formula=new_formula(error_formula,OR,deadlock_formula);
  }
}

int Protocol_Heuristic::formula_based_h(State *S){
  PackedState *old_now;
  int h;

  /* If it it is not a real state, but a rendezvous try, return h(pred) */
  if(S->ps->boq!=-1)  return S->pred->h;

  old_now=now;
  now=S->ps;

  if((old_nr_pr)!=S->ps->_nr_pr){
#ifdef DEBUG
      printf("Constructing Global Formula...\n");
#endif //
      construct_global_formula(S);
#ifdef DEBUG
      printf("F ="); print_formula(error_formula,0,0,1); printf("\n");
#endif // DEBUG
      old_nr_pr=S->ps->_nr_pr;
  }
  if(error_formula){
#ifdef DEBUG
    printf("Printing formula...\n");
    print_formula(error_formula,0,1,1); printf("\n");
    printf("Computing heuristic value...\n");
#endif // DEBUG
    h=steps_until(error_formula,1);
  }
  else
    h=0;

  now=old_now;
  return h;
}

/***** END ALL AS FORMULA *****/


/***** BEGIN ENDCLAIM HEURISTIC *****/

int Protocol_Heuristic::end_claim(State *S){
  int h;

#ifdef VERI
  h=distances[VERI][inv_mapping[VERI][((P0 *)hsf_pptr(S->ps,0))->_p]][inv_mapping[VERI][endclaim]];
#endif // VERI

  return h;
}

/***** END OF ENDCLAIM HEURISTIC *****/



/**** BEGIN OF STATE BASED HEURISTIC *****/

void Protocol_Heuristic::set_goal_state(State *s){
  goal_state=new State;
  *goal_state=*s;
  goal_state->ps=new PackedState;
  memcpy(goal_state->ps,s->ps,s->ps->_vsz);
}

int Protocol_Heuristic::state_based_h(State *S){
  unsigned int i,t,u,v;
  int h;

  h=0;
  if(!goal_state){
    printf("Error! Goal state not defined.\n");
    exit(0);
  }
  for(i=0; i<S->ps->_nr_pr; i++){
#ifdef VERI
    if (i==VERI) continue;
#endif //

#if 0 /* giop equivalent seeds */
    if(i!=3) continue;

#elif 0 /* elevator equivalent seeds */
    if(i!=1 && i!=4 && i!=5 && i!=6) continue;
#endif //

    t=(int)((P0 *)hsf_pptr(S->ps,i))->_t;
    u=(int)((P0 *)hsf_pptr(S->ps,i))->_p; u=inv_mapping[t][u];
    v=((P0 *)hsf_pptr(goal_state->ps,i))->_p; v=inv_mapping[t][v];
    h+=distances[t][u][v];
    //printf("D_%d(%d,%d) = %d\n",i,u,v,distances[t][u][v]);
  }
  //printf("=============\nTOTAL = %d\n",h);
  if(h>maxh) return maxh;
  return h;
}

int min_symmetric_h; 

int Protocol_Heuristic::symmetry_fsm1(State *S){
  unsigned int i,t,u,v;
  int h;

  h=0;
  if(!goal_state){
    printf("Error! Goal state not defined.\n");
    exit(0);
  }
  /*#ifdef SYMMETRY
    min_symmetric_h=state_based_h(S);*/
  //#ifndef SYMMOD
#ifdef SYMMETRY
#if 0 /* Antes */
  full_zeta(S->ps);
#else /* Ahora */
  min_symmetric_h=maxh;
  BucketType* my_bucket;
  for(int i=0; i<ErrorOrbit->max; i++){
    my_bucket=ErrorOrbit->bucket[i];
    while(my_bucket){

      int tmp_h=0;
      for(int i=0; i<S->ps->_nr_pr; i++){
	t=(int)((P0 *)hsf_pptr(S->ps,i))->_t;
	u=(int)((P0 *)hsf_pptr(S->ps,i))->_p; u=inv_mapping[t][u];
	v=((P0 *)hsf_pptr(my_bucket->the_state->ps,i))->_p; v=inv_mapping[t][v];
	tmp_h+=distances[t][u][v];
	//printf("D_%d(%d,%d) = %d\n",i,u,v,distances[t][u][v]);
      }
      if(tmp_h<min_symmetric_h) min_symmetric_h=tmp_h;
      
      my_bucket=my_bucket->link;
    }
  }

  //#endif //

  //#endif //
  h=min_symmetric_h;

  //int h3;
  //h3=symmetry_fsm3(S);
  //if(h==h3) printf("Coincide!!!!! h1 = %d <> %d = h3\n",h,h3); else printf("Gran pufo!!!  h1 = %d <> %d = h3\n",h,h3);

#endif //
#endif //
  //printf("=============\nTOTAL = %d\n",h);
  if(S->g==0) return 0;
  if(h>maxh) return maxh;
  return h;
}

int Protocol_Heuristic::symmetry_fsm2(State *S){
  unsigned int i,j,t,u,v;
  int h,min;

  h=0;
  if(!goal_state){
    printf("Error! Goal state not defined.\n");
    exit(0);
  }
#ifndef SYMMOD
  for(i=1; i<S->ps->_nr_pr; i++){ /* 1=do not use init. */
#else
  for(i=0; i<S->ps->_nr_pr; i++){ /* 1=do not use init. */
#endif //
    t=(int)((P0 *)hsf_pptr(S->ps,i))->_t;
    u=(int)((P0 *)hsf_pptr(S->ps,i))->_p; u=inv_mapping[t][u];
    min=maxh;

#ifndef SYMMOD
    for(j=1; j<S->ps->_nr_pr; j++){ /* 1=do not use init. */
#else
    for(j=0; j<S->ps->_nr_pr; j++){ /* 1=do not use init. */
#endif //
      //printf("(%d,%d)",i,j);
      v=((P0 *)hsf_pptr(goal_state->ps,j))->_p; v=inv_mapping[t][v];
      if(min>distances[t][u][v]) min=distances[t][u][v];
      //printf("\t J=%d, d=%d\n",j,distances[t][u][v]);
    }
    //printf("\n");
    h+=min;
    //printf("D_%d(%d,%d) = %d\n",i,u,v,distances[t][u][v]);
  }
    //printf("=============\nTOTAL = %d\n",h);
  if(h>maxh) return maxh;
  return h;
}


#if 1
int ONE_MAX;          /* number of nodes */
int MAX_NODES;  /* nodes in [1..n], extra-node 0 */
int MAX_COST;     /* max int */
int EXTRA_NODE; /* another extra-node */

/* memory allocation better outside procedures */

int *match; /* matching from B in A */
int *open;  /* search horizon. */
int *hash;  /* visited list. */
int *cost;  /* current priority for shortest path construction */
int *pred;  /* predecessor edges in the shortest path tree */

#define costGraph(i,j) distances[(int)((P0 *)hsf_pptr(S->ps,i))->_t][inv_mapping[(int)((P0 *)hsf_pptr(S->ps,i))->_t][(int)((P0 *)hsf_pptr(S->ps,i))->_p]][inv_mapping[(int)((P0 *)hsf_pptr(S->ps,j))->_t][(int)((P0 *)hsf_pptr(goal_state->ps,j))->_p]]

void Protocol_Heuristic:: printGraph(State *S) {
  int i,j;
  for(i=1; i<MAX_NODES; i++) {
    for(j=1; j<MAX_NODES; j++)
      printf("%d ",costGraph(i,j));
   printf("\n");
 }
}

void Protocol_Heuristic:: printMatch(State *S) {
  int i;
  for(i=1; i<MAX_NODES; i++) { 
    printf("%d:[%d,",i,open[i]);
    printf("%d,",hash[i]);
    printf("%d,",match[i]);
    printf("%d],",pred[i]);
  }
  for(i=MAX_NODES; i<2*MAX_NODES; i++) { 
    printf("%d:[%d,",i,pred[i]);
    printf("%d,",hash[i]);
    printf("%d,",match[i]);
    printf("%d],",pred[i]);
  }
  printf("EN:[%d,",i,pred[EXTRA_NODE]);
  printf("%d,",hash[EXTRA_NODE]);
  printf("%d,",match[EXTRA_NODE]);
  printf("%d],",pred[EXTRA_NODE]);
  printf("\n");
}

void Protocol_Heuristic::improve(State *S){
  int i;           /* for loops */
  int min;         /* minumum in horizon. */
  int adj,madj;
 
  pred[0] = -1;        /* sentinal node, all other preds point to it */

  /* Some initializations */ 
  for(i=1;i< MAX_NODES;i++) { 
    cost[i] = pred[i] = 0;
    open[i] = hash[i] = 1;  /* insertion */
  }
  for(i=MAX_NODES;i<2*MAX_NODES;i++) {
    hash[i] = pred[i] = open[i] = 0; 
  }
  for(i=1; i< MAX_NODES; i++) {
    if (match[i] != -1) { 
      cost[match[i]] = MAX_COST;
      /* remove all matched nodes from open and hash. */
      open[match[i]] = hash[match[i]] = pred[match[i]] = 0;
    }
  }
  open[EXTRA_NODE] = hash[EXTRA_NODE] = pred[EXTRA_NODE] = 0;
  while(1) {
    min = 1;
#ifdef DEBUG_ASSIGNMENT
    printMatch(S);
#endif //
    while(!open[min]) min++;   /* search first node in open */
    if (min > EXTRA_NODE){     /* horizon empty = no improvement */
      printf("Error! No assigment. \n");  
      exit(0);
    }
    for(i=min;i< MAX_NODES ;i++) {  /* search min in open */
      if (open[i] && (cost[min] > cost[i]))
        min = i; /* new min */
    }
#ifdef DEBUG_ASSIGNMENT
    printf("min=%d\n",min);
#endif //
    if (open[EXTRA_NODE] &&         /* minimum cost element is in B */
        (cost[min] > cost[EXTRA_NODE]))   
      min = EXTRA_NODE;

    if (min == EXTRA_NODE) {        /* improve matching */
      while(pred[pred[min]] != -1) {
#ifdef DEBUG_ASSIGNMENT
        printf("Improve Matching at %d \n",min);
#endif //
        match[pred[min]-MAX_NODES] = pred[pred[min]];
#ifdef DEBUG_ASSIGNMENT
        printf("set Matching %d to %d\n",pred[min]-MAX_NODES,pred[pred[min]]);
#endif //
        min = pred[pred[min]];
      }
      return;                       /* improved matching found */
    }
    for(i=1; i< MAX_NODES; i++) {   /* for all nodes on B */
      adj = MAX_NODES + i;          /* adj = index of i in B */
      madj = match[i];              /* next to adjacent node */
      if (madj == -1) {             /* i not matched. */ 
#ifdef DEBUG_ASSIGNMENT
        printf("%d not matched\n",i);
#endif //
        if (!hash[EXTRA_NODE]) { // not already considered
#ifdef DEBUG_ASSIGNMENT
          printf("%d not hashed\n",EXTRA_NODE);
#endif //
          cost[EXTRA_NODE] = cost[min] + costGraph(min,i);
          open[EXTRA_NODE] = hash[EXTRA_NODE] = 1;
          pred[EXTRA_NODE] = adj; pred[adj] = min;
        }
        else { // already considered
#ifdef DEBUG_ASSIGNMENT
          printf("%d hashed\n",EXTRA_NODE);
#endif //
          if(cost[min] + costGraph(min,i) < cost[EXTRA_NODE]) {
            cost[EXTRA_NODE] = cost[min] + costGraph(min,i);
            open[EXTRA_NODE] = 1;
            pred[EXTRA_NODE] = adj; pred[adj] = min;
          }
        }
#ifdef DEBUG_ASSIGNMENT
        printf("cost[%d]:=%d\n",EXTRA_NODE,cost[EXTRA_NODE]);
#endif //
      }
      else {
#ifdef DEBUG_ASSIGNMENT
        printf("%d matched\n",i);
#endif //
        if (!hash[madj]) {
#ifdef DEBUG_ASSIGNMENT
          printf("%d not hashed\n",madj);
#endif //
          cost[madj] = cost[min] + costGraph(min,i) - costGraph(madj,i);
          open[madj] = hash[madj] = 1;  
          pred[madj] = adj; pred[adj] = min; }
        else {
#ifdef DEBUG_ASSIGNMENT
          printf("%d hashed\n",madj);
#endif //
          if(cost[min]+costGraph(min,i)-costGraph(madj,i) < cost[madj]){
            cost[madj] = cost[min]+costGraph(min,i)-costGraph(madj,i);
            open[madj] = 1; pred[madj] = adj; pred[adj] = min;
          }
        }
#ifdef DEBUG_ASSIGNMENT
        printf("cost[%d]:=%d\n",madj,cost[madj]);
#endif //
      }
    }
    open[min] = 0; // delete min in open not in hash
  }
}


int Protocol_Heuristic::symmetry_fsm3(State *S){
  int sum = 0;
  int i;

  ONE_MAX=S->ps->_nr_pr-1;
  MAX_NODES=ONE_MAX+1;
  MAX_COST=maxh;
  EXTRA_NODE=2*MAX_NODES;

  match=new int[MAX_NODES];
  open=new int[EXTRA_NODE+1];
  hash=new int[EXTRA_NODE+1];
  cost=new int[EXTRA_NODE+1];
  pred=new int[EXTRA_NODE+1];


  for(i=1; i < MAX_NODES; i++) /* init of empty matching */
    match[i] = -1;

  for(i=1; i < MAX_NODES;i++) { /* n times matching augmentation */
#ifdef DEBUG_ASSIGNMENT
    printf("Iteration %d\n",i);
#endif //
    improve(S);
  }
  /* matching found */ 

  for(i=1; i< MAX_NODES; i++) { 
#ifdef DEBUG_ASSIGNMENT
    printf("(%d->%d) [%d] \n",match[i],i,costGraph(match[i],i));
#endif //
    if (match[i] == -1) { /* for all unmatched nodes */
      printf("Error! Unmatched nodes.\n"); bug(); exit(0);
    }
  }
  for(i=1; i< MAX_NODES; i++) 
    sum+=costGraph(match[i],i);  
  return sum;
}

#else
#define costGraph(i,j) distances[(int)((P0 *)hsf_pptr(S->ps,i))->_t][inv_mapping[(int)((P0 *)hsf_pptr(S->ps,i))->_t][(int)((P0 *)hsf_pptr(S->ps,i))->_p]][inv_mapping[(int)((P0 *)hsf_pptr(S->ps,j))->_t][(int)((P0 *)hsf_pptr(goal_state->ps,j))->_p]]


int Protocol_Heuristic::symmetry_fsm3(State *S){
  /* An implementation of the minimum-weight bipartite assignment problem, where the nodes in the first set A are the pc's in S and the nodes in the second set B are the pc's in the goal state. */

  int n = (S->ps->_nr_pr-1); /* Number of nodes in A (or B). */
  int sum = 0; /* The sum of the assignment = the heuristic value to realease. */
  int i; /* for loops */
  int min; /* Minumum in horizon. */
  int adj,madj;


  int *match; /* The matching (assignment) from nodes in B to nodes in A */
  int *open; /* Search horizon. */
  int *hash; /* Visited list. */
  int *cost; /* ? */
  int *pred; /* Predecessor edges in the shortest path tree */

  int MAX=maxh; /* ??? */
  int MAXG=nproctype_states[(int)((P0 *)hsf_pptr(S->ps,1))->_t]+1; /* ??? */

  match = new int[n+1]; /* I do not know why, but indexing is done from 1..n */
  hash = new int[2*n+1];
  open = new int[2*n+2]; /* Need i so many entries? &/
  cost = new int[2*n+1];
  pred = new int[2*n+1];

  printf("Starting with h3\n");
  printf("\t from ( ");
  for(i=1; i<=n; i++) printf(" %i ",(int)((P0 *)hsf_pptr(S->ps,i))->_p); printf(")");
  printf(" to ( ");
  for(i=1; i<=n; i++) printf(" %i ",(int)((P0 *)hsf_pptr(goal_state->ps,i))->_p); printf(")\n");

  for(i=1; i<=n; i++) match[i] = -1; /* Set the empty matching. */ 

  for(int j=1; j<=n; j++){ /* For each node in A (incremental algorithm) */
   
    /* Augment */
    printf("\t Matching: "); for(i=1; i<=n; i++) printf(" %d ", match[i]); printf("\n");

    pred[0] = MAX; /* ??? */
    open[n*2] = 1; /* sentinal in open: the last element? */

    /* Some initializations. */
    for(i=1;i<=n;i++) { /* on the sources(B nodes) */
      cost[i] = pred[i] = 0;
      open[i] = hash[i] = 1;
    }
    for(i;i<=(2*n);i++) { /* on the goals (A nodes) */
      cost[i] = MAXG;
      open[i] = hash[i] = pred[i] = 0;
    }


    for(i=1; i<=n; i++) {
      if (match[i] != -1) { /* for all unmatched nodes */
	cost[match[i]] = MAXG; 
	/* remove all unmatched nodes from open and hash. */
	open[match[i]] = hash[match[i]] = pred[match[i]] = 0;
      }
    }

    /* Main Loop */

    while(1) {
      min = 1;
      while(!open[min]) min++;            // search first node in open

      if (min > (2*n)){ /* horizon empty = no assignment? */
	printf("Error! No assigment while computing FSM3.\n"); bug(); exit(0);
      }

      for(i=min; i<=n; i++) { /* search min between the nodes of A in open */
	if (open[i] &&
	    (cost[min] > cost[i]))
	  min = i; /* new min */
      }

      if (open[(2*n)] &&             /* min on right hand side ??? */
	  (cost[min] > cost[(2*n)]))
	min = (2*n);

      if (min == (2*n)) {
	while(pred[pred[min]] != MAX) { /* This loops runs forever! */
	  match[pred[min]-n] = pred[pred[min]];
	  min = pred[pred[min]];
	}
	break; //return 0;
      }

      for(i=1; i<=n; i++) { /* for all nodes on B */
	adj = n + i; /* adj = index of v in hash, etc. */
	if (costGraph(min,i) == MAXG) /* no edge between min and adj */
	  continue; /* jump to next succ */
	madj = match[i];  // next to adjecent node
	if (madj == -1) { /* v not matched. */ 
	  if (!hash[(2*n)]) { // not already considered
	    cost[(2*n)] = cost[min] + costGraph(min,i);
	    open[(2*n)] = hash[(2*n)] = 1;
	    pred[(2*n)] = adj; pred[adj] = min;
	  }
	  else { // already considered
	    if(cost[min] + costGraph(min,i) < cost[(2*n)]) {
	      cost[(2*n)] = cost[min] + costGraph(min,i);
	      open[(2*n)] = 1;
	      pred[(2*n)] = adj; pred[adj] = min;
	    }
	  }
	}
	else {
	  if (!hash[madj]) {
	    cost[madj] = cost[min] + costGraph(min,i) - costGraph(madj,i);
	    open[madj] = hash[madj] = 1;  
	    pred[madj] = adj; pred[adj] = min; }
	  else {
	    if(cost[min]+costGraph(min,i)-costGraph(madj,i) < cost[madj]){
	      cost[madj] = cost[min]+costGraph(min,i)-costGraph(madj,i);
	      open[madj] = 1; pred[madj] = adj; pred[adj] = min;
	    }
	  }
	}
      }
      open[min] = 0; // delete min in open not in hash
    }
  }

  for(i=1; i<=n; i++) {
    printf("(%d->%d) ",i,match[i]);
    if (match[i] == -1) { /* for all unmatched nodes */
      printf("Error! Unmatched nodes.\n"); bug(); exit(0);
    }
  }


  for(int i=1; i<=n; i++) sum+=costGraph(match[i],i);  

  delete match; delete open; delete hash; delete cost; delete pred;

  return sum;

}
#endif //

int Protocol_Heuristic::hamming_distance(State *S)
{
  int hd,byte,bit;
  unsigned char the_byte, the_mask;

  if(!goal_state){
    printf("Error! Goal state not defined.\n");
    exit(0);
  }
  hd=0;

#if 0 /* giop */
  unsigned u,v;

    /* never claim */
    u=(int)((P0 *)hsf_pptr(S->ps,VERI))->_p;
    v=((P0 *)hsf_pptr(goal_state->ps,VERI))->_p;
      the_byte=u^v;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1);
    
    /* user[3] */
    u=(int)((P0 *)hsf_pptr(S->ps,3))->_p;
    v=((P0 *)hsf_pptr(goal_state->ps,3))->_p;
    the_byte=u^v;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1);
      return hd;

#elif 0 /* elevator */
  unsigned u,v;

    /* never claim */
    u=(int)((P0 *)hsf_pptr(S->ps,VERI))->_p;
    v=((P0 *)hsf_pptr(goal_state->ps,VERI))->_p;
    the_byte=u^v;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1);

    /* init */
    u=(int)((P0 *)hsf_pptr(S->ps,1))->_p;
    v=((P0 *)hsf_pptr(goal_state->ps,1))->_p;
    the_byte=u^v;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1);

    /* level[4] */
    u=(int)((P0 *)hsf_pptr(S->ps,4))->_p;
    v=((P0 *)hsf_pptr(goal_state->ps,4))->_p;
    the_byte=u^v;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1);

    /* elevator[5] */
    u=(int)((P0 *)hsf_pptr(S->ps,5))->_p;
    v=((P0 *)hsf_pptr(goal_state->ps,5))->_p;
    the_byte=u^v;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1);

    /* controller[6] */
    u=(int)((P0 *)hsf_pptr(S->ps,6))->_p;
    v=((P0 *)hsf_pptr(goal_state->ps,6))->_p;
    the_byte=u^v;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1);

    the_byte=((uchar)goal_state->ps->elevator_pos)^((uchar)S->ps->elevator_pos);
    hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1);

    hd+=goal_state->ps->elevator_opened!=S->ps->elevator_opened;
    hd+=goal_state->ps->elevator_tick!=S->ps->elevator_tick;
    hd+=goal_state->ps->controller_tick!=S->ps->controller_tick;
    hd+=goal_state->ps->level_requested[2]!=S->ps->level_requested[2];
    return hd;
#endif //

  for(byte=0; byte<S->ps->_vsz; byte++){
    if(1){ /* bit distance */
      the_byte=(((unsigned char *)S->ps)[byte])^(((unsigned char *)goal_state->ps)[byte]);
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1); the_byte>>1;
      hd+=(the_byte&0x1);
    } else { /* byte distance */
      if((((unsigned char *)S->ps)[byte])>=(((unsigned char *)goal_state->ps)[byte]))
	hd+=(((unsigned char *)S->ps)[byte])-(((unsigned char *)goal_state->ps)[byte]);
      else
	hd-=(((unsigned char *)S->ps)[byte])-(((unsigned char *)goal_state->ps)[byte]);
    }
  }
  if(hd>maxh) return maxh;
  return hd;
}


/***** END OF STATE BASED HEURISTICS *****/


/***** BEGIN OF THREAD INTERLEAVING HEURISTIC *****/

int Protocol_Heuristic::thread_interleaving(State *S){
  State *state;
  int h,history_length;

  h=0;
  if(!S->pred) return 0;
  state=S->pred;
  for(int i=0; i<Selected_History_Length && state && state->pred; i++){
    if(state->move.pr==S->move.pr){ /* Just executed in history */
      h+=(Selected_History_Length-i); /* *S->ps->_nr_pr; */
    }
    state=state->pred;
  }
  return h;
}

/***** END OF THREAD INTERLEAVING HEURISTIC *****/

#endif // _HEURISTICS_
