#ifndef _PARTIAL_ORDER_C_
#define _PARTIAL_ORDER_C_

#ifndef NOREDUCE

void init_po(void){
  switch(Selected_C3){
  case C3LIVENESSSTACK:
  case C3LIVENESSDUPLICATE:
  case C3SAFETYSTACK:
  case C3SAFETYDUPLICATE:
  case C3QUEUE:
    break;
  case C3STATIC:
    init_static_po();
    break;
  }
}

StateItem* reduce(State *s, StateItem *successors){
  /* Reduces a set of successors. Maybe not the very efficient but clean. */

  short selected;
  StateItem *aux_item, *succ, *last;
  int found;

  if(Selected_C3==0) {full_expansions++; return successors;}
#ifdef DEBUGPO
  printf("Trying to reduce...\n");
#endif //
  if(!successors) return successors;
  selected=ample(s,successors);
  if(selected==-1){
#ifdef DEBUGPO
    printf("\tNo reduction possible.\n");
#endif //
    full_expansions++;
    return successors; /* No reduction possible */
  }
  reductions++;
#ifdef DEBUGPO
  printf("\tReduction possible. Selected process is %d\n",selected);
#endif //
  /* Remove all successors not corresponding to a transition of the selected process. */
  found=0;
  last=succ=successors;

  while(succ){
    if((!found) && (succ->the_state->move.pr==selected)){
      successors=succ;
      found=1;
      last=succ;
      succ->prev=(StateItem*)0;
      succ=succ->next;
    } else if(found && (succ->the_state->move.pr==selected)){
      last=succ;
      succ=succ->next;
    } else if(succ->the_state->move.pr!=selected){
      aux_item=succ->next;
      last->next=succ->next;
      delete succ->the_state->ps; succ->the_state->ps=(PackedState *)0;
      delete succ->the_state;
      delete succ;
      succ=aux_item;
    }
  }

  if(!found){
    printf("Error! No successors corresponding to the selected process found.\n");
    bug();
    exit(0);
  }
  last->next=(StateItem*)0;

  return successors;
}


short ample(State *s, StateItem *successors){
  /* Returns the pid of the process which transitions can be selected as ample set for the given state. If the state must be fully expanded -1 is returned. */

  short pid;
  short best_ample=-1;

  for(pid=s->ps->_nr_pr-1; pid>=BASE; pid-=1){ /* For all processes... */
#ifdef DEBUGPO
    printf("\tChecking conditions for process %d\n",pid);
#endif //
    if( check_C1_C2(s,pid) && check_C0_C3(s,pid,successors) ){
     if (!Selected_Ample_Heuristic) return pid; /* Transitions of pid is a valid ample set. */
     else if (Selected_Ample_Heuristic && best_ample==-1) best_ample=pid;
     else if (eval_ample(pid,successors)<eval_ample(best_ample,successors)){
       //printf("Found a better candidate!\n");
       best_ample=pid;
     }
    }
  }
  return best_ample; /* State s must be fully expanded. */
}

int check_C1_C2(State *s, short pid){
  /* Checks condition C1 (independence) and condition C2 (invisibility).
     Following Spin's implementation of (conditional) safe transitions. */

  short tt;
  unsigned char ot;
  Trans *t;
  int hold;

#ifdef DEBUGPO
  printf("\t\tChecking conditions C1&C2...\n");
#endif //
  now=s->ps;
  this_p=pptr(pid);
  tt=(short) (((P0 *)this_p)->_p);
  ot=(short) (((P0 *)this_p)->_t);
  t=trans[ot][tt];
  if((t->atom&8)){
    /* Transition(s???) do only local references.*/
    if(t->qu[0]==0) /* Transitions are unconditionally safe. */
      return 1;
    else{
      hold=q_cond(pid,t); /* return "Transitions of pid conditional safe". */
      C1C2_fail+=(hold==0);
      return hold;
    }
  }
  C1C2_fail++;
#ifdef DEBUGPO
  printf("\t\tConditions C1&C2 do NOT hold.\n");
#endif //
  return 0;
}

int check_C0_C3(State *s, short pid, StateItem* successors){
  /* Checks condition C0 (emptiness) and condition C3 (cycle).
     Successors is considered to be ordered by the corresponding process. */
 
  StateItem *succ;
  State *found;

#ifdef DEBUGPO
  printf("\t\tChecking conditions C0&C3...\n");
#endif //

  for(succ=successors; succ && (succ->the_state->move.pr>pid); succ=succ->next);
#ifdef DEBUGPO
  if(succ && (succ->the_state->move.pr==pid)) printf("\t\tCondition C0 holds.\n");
#endif //
  if((!succ) || (succ->the_state->move.pr<pid)){
    /* C0: No successors corresponding to pid. */
#ifdef DEBUGPO
    printf("\t\tCondition C0 does NOT hold.\n");
#endif //
    C0_fails++;
    return 0;
  }

  /* Check C3 in its different variants. */
  if(Selected_C3==C3IGNORE) return 1;
  for(succ; succ && (succ->the_state->move.pr==pid); succ=succ->next){
    /* For all enabled transitions of pid...*/
    switch(Selected_C3){
    case C3LIVENESSSTACK:
      found=Algo->ht->search(succ->the_state);
      if(found && found->is_in_open()){
#ifdef DEBUGPO
	printf("\t\tCondition C3 does NOT hold.\n");
#endif //
	C3_fails++;
	return 0;
      }
      break;
    case C3LIVENESSDUPLICATE:
      found=Algo->ht->search(succ->the_state);
      if(found){
#ifdef DEBUGPO
	printf("\tCondition C3 does NOT hold.\n");
#endif //
	C3_fails++;
	return 0;
      }
      break;
    case C3SAFETYSTACK:
      found=Algo->ht->search(succ->the_state);
      if((!found) || !found->is_in_open()) return 1;
      break;
    case C3SAFETYDUPLICATE:
      found=Algo->ht->search(succ->the_state);
      if(!found) return 1;
      break;
    case C3QUEUE:
      found=Algo->ht->search(succ->the_state);
      if(!found || (found && found->is_in_open())) return 1;
      break;
    case C3STATIC:
      if(sticky((succ->the_state->move.o_t))){
	C3_fails++;
	return 0;
      }
      break;
    }
  }
#ifdef DEBUGPO
  if (Selected_C3==C3SAFETYSTACK || Selected_C3==C3SAFETYDUPLICATE || Selected_C3==C3QUEUE)
    printf("\t\tCondition C3 does NOT hold.\n");
#endif //
  if (Selected_C3==C3SAFETYSTACK || Selected_C3==C3SAFETYDUPLICATE || Selected_C3==C3QUEUE){
    C3_fails++;
    return 0;
  } else return 1;
}

int eval_ample(short pid, StateItem* successors){
  StateItem *succ;
  int val,aux_val;

  for(succ=successors; succ && (succ->the_state->move.pr!=pid); succ=succ->next);
  switch(Selected_Ample_Heuristic){
  case AMPLEH_SUCCS:
    for(succ=successors; succ && (succ->the_state->move.pr==pid); succ=succ->next)
      val++;
    break;
  case AMPLEH_BEST:
    val=successors->the_state->h;
    for(succ=successors; succ && (succ->the_state->move.pr==pid); succ=succ->next)
      if(succ->the_state->h<val) val=succ->the_state->h;
    break;
  case AMPLEH_MEAN:
    val=aux_val=0;
    for(succ=successors; succ && (succ->the_state->move.pr==pid); succ=succ->next)
      val+=succ->the_state->h<val; aux_val++;
    break;
    val=(int) (val/aux_val);
  }   
  return val;
}

void print_C3_conditions(){
  printf("Available C3 conditions are:\n");
  printf("\t%d: no transitions in ample leads to stack\n",C3LIVENESSSTACK);
  printf("\t%d: no transitions in ample leads to a duplicate\n",C3LIVENESSDUPLICATE);
  printf("\t%d: at least one transition do not lead to stack\n",C3SAFETYSTACK);
  printf("\t%d: at least one transition do not lead to a duplicate\n",C3SAFETYDUPLICATE);
  printf("\t%d: at least one transition do not lead to a duplicate or to a duplicate in the queue\n",C3QUEUE);
  printf("\t%d: no sticky transitions in ample\n",C3STATIC);
  printf("\t%d: ignore cycle proviso\n",C3IGNORE);
}

void print_ampleh(){
  printf("Available ample set selection heuristics are:\n");
  printf("\t%d: first candidate found\n",AMPLEH_NONE);
  printf("\t%d: ample set with best successors\n",AMPLEH_BEST);
  printf("\t%d: ample set with best mean of successors\n",AMPLEH_MEAN);
  printf("\t%d: ample set with less successors\n",AMPLEH_SUCCS);
}

void po_statistics(){
  printf("\tPartial Order Reduction Statistics:\n");
  printf("\t\treductions: %d\n",reductions);
  printf("\t\tfull expansions: %d\n",full_expansions);
  printf("\t\tample set refuted by conditions C1C2: %d\n",C1C2_fail);
  printf("\t\tample set refuted by condition    C0: %d\n",C0_fails);
  printf("\t\tample set refuted by condition    C3: %d\n",C3_fails);
}

/****** STATIC REDUCTION THINGS *****/

typedef struct arcs{
  Trans *t;
  struct arcs *next;
} arc;

typedef struct cycle{
  arc *start;
  struct cycle *next;
} cycle;

unsigned char *nodes; /* bit 1=visited, bit 2=on_stack */
cycle *cycles[_NP_];
Trans **arcs_stack;
int arcs_top;

void identify_cycles_p(int proctype, int node){
  arc *aux_arc;
  cycle *aux_cycle;
  int i;
  Trans *t;

  nodes[node]|=3; /* visited and on stack */
  for(t=trans[proctype][node]; t; t=t->nxt){
    if(nodes[t->st]&2){ /* if node on stack.. */
      arcs_stack[arcs_top]=t;
      arcs_top++;
      aux_cycle=new cycle; aux_cycle->start=(arc *)0;
      for(i=0; i<arcs_top && (t->st!=arcs_stack[i]->st); i++);
      for(i; i<arcs_top; i++){
	aux_arc=new arc; aux_arc->t=t; aux_arc->next=aux_cycle->start;
	aux_cycle->start=aux_arc;
      }
      aux_cycle->next=cycles[proctype];
      cycles[proctype]=aux_cycle;
#ifdef DEBUGPO
      printf("\tCycle found: ");
      for(aux_arc=aux_cycle->start; aux_arc; aux_arc=aux_arc->next)
	printf("t%d ",aux_arc->t);
      printf("\n");
#endif //
    } else{ /* Visit also already visited states! */
      arcs_stack[arcs_top]=t;
      arcs_top++;
      identify_cycles_p(proctype,t->st);
    }
    arcs_top--;
  }
  nodes[node]&=~2; /* out of stack */
}

void identify_cycles(void){
  int i,j;
  
  for(i=0; i<_NP_; i++){
    nodes=new unsigned char[nstates_proc[i]];
    for(j=0; j<nstates_proc[i]; j++) nodes[i]=0;
    arcs_stack=new Trans*[nstates_proc[i]];
    arcs_top=0;
#ifdef DEBUGPO
    printf("Looking for cycles in proctype %d...\n",i);
#endif //
    identify_cycles_p(i,start_proc[i]);
  }
}

void select_sticky_transitions(void){
  cycle *aux_cycle;
  arc *aux_arc;
  int i;

  for(i=0; i<_NP_; i++)
    for(aux_cycle=cycles[i]; aux_cycle; aux_cycle=aux_cycle->next){
      //printf("Selecting trans for cycle...\n");
      for(aux_arc=aux_cycle->start; aux_arc; aux_arc=aux_arc->next){
	if(aux_arc->t->qu[0]!=0){ /* Transitions are not conditionally safe. */
	  //printf("\tMarking unsafe t%d as sticky\n",aux_cycle->start->t->t_id);
	  aux_arc->t->atom|=1; break;
	}	
      }
      if(!aux_arc){
	//printf("\tMarking safe t%d as sticky\n",aux_cycle->start->t->t_id);
	aux_cycle->start->t->atom|=1; /* If no t was warked as sticky...*/
      }
    }
}

int sticky(Trans *t){
  return t->atom&1;
}

void init_static_po(void){
  identify_cycles();
  select_sticky_transitions();
}

/****** END STATIC REDUCTION THINGS *****/

int is_used_in(void *var, HSF_Lextok *node){
  /* The address of a bit cannot be accesses and is marked with 0. */
  if(!node) return 0;
  if(node->ntyp==NAME && node->var()==var){
    /* The address of a bit cannot be accesses and is marked with 0. */
    printf("\t\t\t modified variable is %d and used is %d\n",var,node->var());
    return 1;
  }
  else return (is_used_in(var,node->lft) || is_used_in(var,node->rgt));
}

int relevant(State *s1, State *s2){
  Trans *trans1, *trans2;
  void *variable_modified;
  int q1,q2;

  trans1=s1->move.o_t;
  trans2=s2->move.o_t;
  //if(s2->ps) now=s2->ps;
  //now=s1->ps;

  if(trans1->atom&2){
    printf("t1 is atomic!\n");
    return 1;
  }

  /* Is trans2 dependent from trans1? */
  printf("\tChecking dependency...\n");
  printf("\t\tT1: proc %d (%s) (%d--%d-->%d): %s\n",s1->move.pr,procname[((P0*)hsf_pptr(now,s1->move.pr))->_t],s1->move.st, s1->move.o_t->t_id,s1->move.o_t->st, s1->move.o_t->tp);
  printf("\t\tT2: proc %d (%s) (%d--%d-->%d): %s\n",s2->move.pr,procname[((P0*)hsf_pptr(now,s2->move.pr))->_t],s2->move.st, s2->move.o_t->t_id,s2->move.o_t->st, s2->move.o_t->tp);
/* Belong to the same process... */
  if (s1->move.pr==s2->move.pr){
    printf("\t\t t1 Belongs to the same process!\n");
    return 1;
  }
  
  /* Can trans1 enable trans2? */
  //printf("\tChecking enabledness...\n");
  /* Share a variable and one writes? */
  printf("t1 global?=%d, t2 global?=%d\n",!(trans1->atom&8),!(trans2->atom&8));
  if((!(trans1->atom&8) && !(trans2->atom&8)) && trans1->lextok_tree->ntyp==ASGN){
    this_p=pptr(s1->move.pr);
    variable_modified=trans1->lextok_tree->lft->var();
    this_p=pptr(s2->move.pr);
    if (is_used_in(variable_modified,trans2->lextok_tree)){
      printf("\t\t t1 and t2 share a variable and t1 writes.\n");
      return 1;
    }
  }
  if((!(trans1->atom&8) && !(trans2->atom&8)) && trans2->lextok_tree->ntyp==ASGN){
    this_p=pptr(s2->move.pr);
    variable_modified=trans2->lextok_tree->lft->var();
    this_p=pptr(s1->move.pr);
    if (is_used_in(variable_modified,trans1->lextok_tree)){
      printf("\t\t t1 and t2 share a variable and t2 writes.\n");
      return 1;
    }
  }
  /* Share a queue? */
  if( (trans1->lextok_tree->ntyp=='r' || trans1->lextok_tree->ntyp=='R' || trans1->lextok_tree->ntyp=='s') &&
      (trans2->lextok_tree->ntyp=='r' || trans2->lextok_tree->ntyp=='R' || trans2->lextok_tree->ntyp=='s') ){

    this_p=pptr(s1->move.pr);
    q1=trans1->lextok_tree->lft->val();

    this_p=pptr(s2->move.pr);
    q2=trans2->lextok_tree->lft->val();

    //printf("\t\t Q1 is %d and Q2 is %d\n",q1,q2);
    if(q1==q2) {
      printf("\t\t t1 can enable t2 (share a queue)!\n");
      return 1;
    }
  }

  /* Is trans1 visible? */
  //printf("\tChecking visibility...\n");
  if(visible(trans1)) { 
    printf("\t\t t1 is visible!\n");
    return 1;
  }
  return 0;
}

int visible(Trans* t){
  if(!(t->atom&8)) { /* Transition uses global variables? */
    printf("\t\t t1 is visible (global)!\n");
    return 1;
  }
  return 0;
  //if(trans1->lextok_tree->ntyp!=ASGN) return 0;
  //this_p=pptr(s1->move.pr);
  //variable_modified=trans1->lextok_tree->lft->var();
#ifdef VERI
  //if(is_used_in(variable_modified,trans[VERI][start_claim]->lextok_tree)){
  //printf("\t\t t1 is visible!\n");return 1;
  // return 1;
  //}
#endif //
}

State** eliminate_irrelevant_trans(State **trail, int *length){
  unsigned char* irrelevant;
  int i,j,new_length;
  State **new_trail;
  
  //printf("Checking for irrelevant transitions...\n");
  new_length=*length;
  printf("\tOld length is %d\n",new_length);
  irrelevant=new unsigned char[*length];
  for(i=0; i<=*length; i++){
    if(trail[i]->move.pr==0) /* init transition */
       irrelevant[i]=0;
    else
       irrelevant[i]=1;
  }
  irrelevant[0]=0;
  now=trail[0]->ps;
  irrelevant[(*length)-1]=0;
  
  for(i=0; i<(*length-1); i++){
    /* TO BE CHANGED!!!*/
#ifdef VERI
    //if(trail[i]->move.pr==VERI && irrelevant[i-1]){ new_length--; irrelevant[i-1]=0; continue;}
    //if(trail[i]->move.pr==VERI && !irrelevant[i-1]){ irrelevant[i]=0; continue; }
#endif //
    if(irrelevant[i]) {printf("TRANSITION t%d IS NOT RELEVANT!\n",i); new_length--; continue;}
    for(j=i+1; j<*length; j++){
      if(!irrelevant[j]){
	//printf("t%d already marked as relevant\n",j);
	continue;
      }
      printf("Checking irrelevance of t%d(id=%d) with respect to t%d(id=%d)\n",trail[j]->g,trail[j]->move.o_t->t_id,trail[i]->g,trail[i]->move.o_t->t_id);
      if(relevant(trail[j],trail[i])){
	irrelevant[j]=0;
      }
    }
  }
  if(irrelevant[i]) new_length--;
  printf("\tEliminating irrelevant transitions...\n");
  printf("\tNew length is %d\n",new_length);
  new_trail=new State*[new_length+1];
  j=0;
  for(i=0; i<*length; i++){
    if(!irrelevant[i]){
      new_trail[j]=trail[i];
      if(!new_trail){ printf("Error! Void transition in reordered trail.\n"); bug(); exit(0);}
      j++;
    } else{
      printf("\t Ignored transition: Depth %d: %s[%d] (%s)\n",trail[i]->g,procname[((P0 *)pptr(trail[i]->move.pr))->_t],trail[i]->move.pr,trail[i]->move.o_t->tp);
      }
  }
  new_trail[j]=trail[i];  /* The last one is the start state */
  if(j!=new_length){ printf("Error! Missing transitions in reordered trail (added=%d).\n",j); bug();}
  *length=new_length;
  return new_trail;
}

#endif // NOREDUCE  

#endif // _PARTIAL_ORDER_C_
