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

/* Includes */
#include "search.h"
#include "hashtable.h"
#include "bitstate_hashtable.h"

class HybridIDAStar : public Search{
  BitStateHashTable* bst;
  HashTable* tt;
  int cachemax;
  int wg,wh,maxf;
  int f;
  int fstar, bound_depth;
  int bit_array_size;
  /* The folowing variables are used in function DFSsearch. Declared here for efficiency. */
  StateItem* aux_item;
  int rval;

public:
  
  HybridIDAStar (int _cachemax, int _bit_array_size, int hash_size,int _maxf,int _wg, int _wh): 
    Search() {
    cachemax=_cachemax;
    tt = new HashTable(hash_size);
    bst = new BitStateHashTable(_bit_array_size);
    bit_array_size=1<<_bit_array_size;
    maxf=_maxf; wg=_wg; wh=_wh;
  }

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


  IDAsearch(int thresh, State* state) { /* Recursive search function. */
    StateItem *newStateList = (StateItem*) 0;  
    State* found;
    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==SAFETY || 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) && (!found || (found && Selected_Goal==ASSERTION_VIOLATION)) && 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 = tt->search(*(newState->ps));
      f = wh*newState->h + newState->g;
       
      if (found) {
	matched++;
	if (wh*found->h + found->g < f)
	  continue; 
	if (wh*found->h + found->g == f) { 
	  if( found->pred && (found->pred->move.o_t == newState->pred->move.o_t) ) {
	    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;
	  }
	  continue;
	}
	found->h = newState->h; 
	found->g = newState->g;
      }
      else {
	if (memory < cachemax) {
	  found = newState;
	  newState=(State *)0;
	  tt->insert(found); memory++;
	  if(memory%100000==0) snapshot(); /* snapshot. */
	}
	else {
	  found = newState;
	  if (memory == cachemax) {
	    printf("Warning! Transposition Table full.\n");
	    memory++;
	    if(memory%100000==0) snapshot(); /* snapshot. */
	  }
	}
      }
      if (f > thresh) { /* f value exceeds thresh. */
	if (f < fstar)  /* min for horizon nodes. */
	  fstar = f;
	continue;
      }
      int rval = IDAsearch(thresh,found);
      if (rval != -1) return rval;
    }  
    delete newState;
    return -1;
  }

  bitstate(int thresh, State* state) { 
    StateItem* newStateList;
    State* found;
    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==SAFETY || 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) && (!found || (found && Selected_Goal==ASSERTION_VIOLATION)) && 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 = tt->search(*(newState->ps));
      f = wh*newState->h + newState->g;

      if (found) {
	matched++;
	if (found->h < f || (found->h == f && ( found->pred && (found->pred->move.o_t == newState->pred->move.o_t) ))){
	  continue;
	}
      }
      else {
	found = bst->search(newState->ps);
	if (found) continue;      
	found = newState;
	f = wh*found->h + found->g;
      }

      if (memory < bit_array_size) {
	bst->insert(newState); memory++;
	if(memory%100000==0) snapshot(); /* snapshot. */
      }
      else {
	if (memory == bit_array_size) {
	  printf("Bit State Table full: %d\n",bit_array_size);
	  memory++;
	}
      }
      if (f > thresh) { /* f value exceeds thresh. */
	if (f < fstar)  /* min for horizon nodes. */
	  fstar = f;
	continue;
      }
      int rval = bitstate(thresh,found);
      if (rval != -1) return rval;
    }  
    delete newState;
    return -1;
  }

  void print_name() { printf("Hybrid IDA* wit transposition table (when full -> bitstate)"); }
};


#endif //
