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

/* Includes */
#include "search.h"
#include "bitstate_hashtable.h"
#ifdef DEBUG_HASHING
#include "universal_hashing_class.h"
#include "hashtable.h"
#endif //

class BitStateIDAStar : public Search{
  BitStateHashTable* ht;
  long cachemax;
  int wg,wh,maxf;
  int bound_depth;
  int fstar;
  /* The folowing variables are used in function DFSsearch. Declared here for efficiency. */
  StateItem* aux_item;
  State* found;
  int rval;

public:
  BitStateIDAStar (int _cachemax,int _maxf,  int _wg, int _wh): Search() {
    cachemax=(1<<_cachemax);
    ht = new BitStateHashTable(_cachemax);
    maxf=_maxf; wg=_wg; wh=_wh;
  }

  int search(int bound) {
    int thresh = wh*S.h;
    long total_expanded, total_generated, total_memory;
    
    bound_depth=bound;
    total_expanded = total_generated = total_memory = 0; /* Init global statistics. */

    for(int r=0; r < Supertraces; r++) {
      //printf("RUN %d\n",r+1);
      //the_hash_function->rand();
      HASH_NR++;
      total = expanded = pruned = generated = memory = 0;  
      thresh = wh*S.h;
      printf("\n threshold    stored     expanded   generated    range\n");
      printf("===========|===========|===========|===========|===========|\n");
      while (thresh < bound)  {  /* dfs iterations until solution is found. */
	ht->init();  
	fstar = maxf;
	memory = generated = expanded = matched = 0; /* Init partial statistics. */
	sol_depth = IDAsearch(thresh,&S);
	total_expanded+=expanded; /* keep track of total expanded nodes per problem. */
	total_generated+=generated; /* keep track of total generated nodes per problem. */
	total_memory+=memory;
	statistics(thresh);
	if (sol_depth!=-1) {
	  generated=total_generated, expanded=total_expanded;/* memory=total_memory;*/
	  return sol_depth;
	}
	thresh = fstar;     
      }   
    }
    generated=total_generated, expanded=total_expanded;/* memory=total_memory;*/
    return -1;
  }


  int IDAsearch(int thresh, State* state) { /* Recursive search function. */
    StateItem* newStateList = (StateItem*)0;
    State* newState = (State *)0;
    int f;

    if(depth_reached<bound_depth && state->g>=bound_depth)
      printf("Warning: max search depth too small\n");
    if(state->g > depth_reached)
      depth_reached=state->g;
    if(state->g>=bound_depth)
      return -1; /* If depth bound is reached return -1 */

    newStateList = proto->expand(state); expanded++; /* Expand state */      

    if(!newStateList && (Selected_Goal==DEADLOCK || Selected_Goal==SIMPLESAFETY || Selected_Goal==VALID_ENDSTATE)){
      /* If state is an endstate and we are checking for deadlocks or valid endstates,
	 then check if state is an goal state. */
      if(proto->goal(state,1)){
	build_solution_path(state);
	return state->g;	
      }
    }

    while(newStateList) {
      delete newState;
      newState = newStateList->the_state;
      aux_item = newStateList;
      newStateList = newStateList->next;
      delete aux_item;
      generated++;                      

      if( (Selected_Goal!=DEADLOCK && Selected_Goal!=VALID_ENDSTATE) && proto->goal(newState,1) ){
	/* Check for errors, but not in the case of deadlocks and valid endstates */
	/* Also a duplicate could be an error (only by checking assertions violations). */
	build_solution_path(newState);
	return newState->g;
      }

      found = ht->search(newState);

      if (found){ matched++; continue;}
      found = newState;

      if (memory < cachemax) {
	ht->insert(found); memory++;
	if(memory%100000==0) snapshot(); /* snapshot. */
      } else {
	if (memory == cachemax) {
	  printf("Transposition Table full: %d states\n",cachemax);
	  memory++;
	  if(memory%100000==0) snapshot(); /* snapshot. */
	}
      }
      f = wh*found->h + found->g;
      if (f > thresh) { /* f value exceeds thresh. */
	if (f < fstar)  /* min for horizon nodes. */
	  fstar = f;
	continue;
      }
      rval = IDAsearch(thresh,found);
      if (rval != -1) return rval;
    }  
    delete newState;
    return -1;
  }

  void print_name() {
    printf("Bitstate IDA* using transposition table");
  }

};


#endif // _BITSTATE_IDASTAR_
