/* 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 _SEARCH_C_
#define _SEARCH_C_

void Search::init(Protocol* _proto) {
  /* Generates the initial state and initis the statistics. */
  expanded = generated = pruned = reopened = total = hash = depth_reached = 0;
  sol_depth=sol_depthfound=-1;
  this->proto = _proto;
  this->proto->initial_state(&S); /* Generate initial state. */
  S.pred = (State *)0;
}
  
void Search::build_solution_path(State *goal_state) {
  /* Builds a path from initial state to the given state and
     sets sol_depth as the length of the solution.
     sol_ind[sol_depth]=initial_state --..--> sol_ind[0]=goal_state */
  State *state;
  int i;

  sol_ind=new State*[goal_state->g+1]; /* Allocate solution path. */
  i=0;
  for(state=goal_state; state; state=state->pred){
    //printf("sol[%d] at depth %d\n",i,state->g);
    if(i!=goal_state->g-state->g) printf("JUMP!!!!!!\n");
    sol_ind[i++]=state;
  }
  i--;
  if(i!=goal_state->g){ printf("Error! Path length (%d) different from error state depth (%d).\n",i,goal_state->g); bug(); exit(0); }
  sol_depth=i;
}

void Search::statistics() {
  /* Used to print out the information collected in the search. */
  printf("\tState-vector %d bytes, depth reached %d, errors: %d\n",hmax,depth_reached,sol_depth!=-1); 
  printf("\t%9d states, stored\n",memory);
  printf("\t%9d states, matched\n",matched);
  printf("\t%9d transitions (transitions performed)\n",generated);
  printf("\t%9d atomic steps\n",proto->atomic_transitions);
  printf("\t%9d states, expanded\n",expanded);
  printf("\t%9d states, reopened\n",reopenings);
  printf("\tRange of heuristic was: "); proto->My_Heuristic->print_range(); printf("\n");
#ifndef NOREDUCE
  printf("\n");
  po_statistics();
  printf("\n");
#endif //
  printf("\tMemory Statistics:\n");
  if(((int)sbrk(0)-old_brk)>(10*1024*1024))
    printf("\t\tEstimated maximum peak of memory: %d MB\n",((int)sbrk(0)-old_brk)/(1024*1024));
  else
    printf("\t\tEstimated maximum peak of memory: %d KB\n",((int)sbrk(0)-old_brk)/(1024));
  printf("\t\t              Maximum state size: %d bytes\n",hmax+sizeof(State));
  if(Selected_Algorithm==GENETIC) return;
#ifndef BITSTATE
  if(((hmax+sizeof(State))*memory)>(10*1024*1024))
    printf("\t\t     Estimated memory for states: %d MB (hashtable=%d MB)\n",((hmax+sizeof(State))*memory)/(1024*1024),(int)ht->msize/(1024*1024));
  else
    printf("\t\t     Estimated memory for states: %d KB (hashtable=%d KB)\n",((hmax+sizeof(State))*memory)/(1024),(int)ht->msize/1024);
#else
  if((Selected_Bit_Array_Size-3)>23)
    printf("\t\t          Size of bitstate table: %d MB\n",1<<(Selected_Bit_Array_Size-23));
  else
    printf("\t\t          Size of bitstate table: %d KB\n",1<<(Selected_Bit_Array_Size-13));
#endif //

  if(((hmax+sizeof(State))*max_open_size)>(10*1024*1024))
    printf("\t\t  Estimated maximum size of open: %d states (%d MB)\n",max_open_size,((hmax+sizeof(State))*max_open_size)/(1024*1024));
  else
    printf("\t\t  Estimated maximum size of open: %d states (%d KB)\n",max_open_size,((hmax+sizeof(State))*max_open_size)/(1024));
  printf("\t\t            Maximum stack height: %d\n",max_stack_height);
  

#ifndef BITSTATE
  printf("\t\t          Estimated memory/state: %d bytes\n",((int)sbrk(0)-old_brk)/memory);
  if((((int)sbrk(0)-old_brk)-(memory*(hmax+sizeof(State))))>(10*1024*1024)){
    printf("\t\t              Estimated overhead: %d MB\n",(((int)sbrk(0)-old_brk)-(memory*(hmax)))/(1024*1024));
  }
  else{
    printf("\t\t              Estimated overhead: %d KB\n",(((int)sbrk(0)-old_brk)-(memory*(hmax)))/(1024));
  }

#else
  if((((int)sbrk(0)-old_brk)-(1<<(Selected_Bit_Array_Size-3)))>(10*1024*1024))
    printf("\t\t              Estimated overhead: %d MB\n",(((int)sbrk(0)-old_brk)-(1<<(Selected_Bit_Array_Size-3)))/(1024*1024));
  else
    printf("\t\t              Estimated overhead: %d KB\n",(((int)sbrk(0)-old_brk)-(1<<(Selected_Bit_Array_Size-3)))/(1024));
#endif //
}

void Search::statistics(int thresh) {
  /* Used to print out the information collected in the search by IDA*. */
  printf("thresh= %5d; ",thresh);
  snapshot();
  /*printf("  %9d ",memory);
  printf("  %9d ",expanded);
  printf("  %9d    ",generated);
  proto->My_Heuristic->print_range();
  if(((int)sbrk(0)-old_brk)>1024)
    printf("\t %9d Mb",((int)sbrk(0)-old_brk)/(1024*1024));
  else
    printf("\t 9%d Kb",((int)sbrk(0)-old_brk)/(1024));
    printf("\n");*/
}

void Search::snapshot(){
  /* Used to print out search progress, similar to spin's snapshot. */
  printf("depth= %5d; stored= %7g;  |open|= %3d MB; |closed|= %3d MB; |total|= %3d MB; |over|= %3d MB\n",depth_reached, (double)memory, (open_size*(hmax+sizeof(State)))/(1024*1024),(closed_size*(hmax+sizeof(State)))/(1024*1024), ((int)sbrk(0)-old_brk)/(1024*1024), (((int)sbrk(0)-old_brk)-((memory)*(hmax+sizeof(State))))/(1024*1024));
  printf("\t\t\t\t|max_open|= %d (%d KB)\n",max_open_size,(max_open_size*(hmax+sizeof(State)))/(1024));
  //printf("stack=%d, open=%d; closed=%d, memory=%d\n",stack_height,open_size,closed_size,memory);
}

void Search::print_solution() {
  /* Used to output the solution.  */
  if(sol_depth!=-1){ /* Check if a solution was really found. */
    for(int i=sol_depth; i>=0; i--) {
      if(!sol_ind[i]){ printf("Error! Missing state in solution.\n"); bug(); exit(0); }
      if(sol_ind[i]->g==sol_depthfound) printf("\t\t--- begin of cycle ---\n");
      proto->print_step(sol_ind[i]); 
    }
  }
  else printf("There is no solution\n"); 
}

void Search::print_trail() {
  /* Prepare trail in spin's format and write it */
  int depthfound_aux;

  if(!sol_ind){
    printf("Error! Trail not avaliable.\n"); bug(); exit(0);
  }

  depth=0; /* Global variable of spin code for writing the trail */
  depthfound=sol_depthfound;
  if (sol_depth) {
    trail= new Trail[sol_depth+3]; /* Alloc memory for trail. */
    for(int i=sol_depth; i>=0; i--) {
      proto->add_to_trail(sol_ind[i]); 
    }
    putrail();
  }
}

void Search::filter_trail(){
  if(!sol_ind){
    printf("Error! Trail not avaliable.\n"); bug(); exit(0);
  }
#ifndef NOREDUCE
  sol_ind=eliminate_irrelevant_trans(sol_ind,&sol_depth);
#endif //
}

#endif // /* _SEARCH_C_ */
