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

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

#ifndef BITSTATE
#include "hashtable.h"
#else
#include "bitstate_hashtable.h"
#endif //

class IDAStar : public Search{

private:
#ifdef BITSTATE
  /* Bitstate table instead of hashtable */
  BitStateHashTable* ht;
#endif // BITSTATE
  int 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:
  
  IDAStar (int _cachemax, int hash_size, int _maxf, int _wg, int _wh): Search() {
    cachemax=1<<_cachemax;
#ifndef BITSTATE
    ht = new HashTable(1<<hash_size);
#else /* Bitstate table instead of hashtable */
    ht = new BitStateHashTable(1<<hash_size);
#endif //
    maxf=_maxf; wg=_wg; wh=_wh;
  }

  int search(int bound) {
    int thresh = wh*S.h;
    long total_expanded, total_generated, max_memory;

    bound_depth=bound;
    total_expanded = total_generated = max_memory =max_open_size = 0; /* Init global statistics. */
    //printf("\n threshold    stored     expanded   generated    range\n");
    //printf("===========|===========|===========|===========|===========|\n");

    while (thresh < bound){
      ht->init(); 
      //ht->insert(&S); /* Insert initial state in hash table. */
      fstar = maxf;
      stack_height = memory = generated =1; 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. */
      if(max_memory<memory) max_memory=memory;
      statistics(thresh);
      if (sol_depth!=-1){
	generated=total_generated, expanded=total_expanded; memory=max_memory;
	return sol_depth;
      }
      if(fstar==maxf) break;
      thresh = fstar;     
    }
    generated=total_generated, expanded=total_expanded; memory=max_memory;
    return -1;
  }

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

    stack_height++;
    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){
      state->out_open();
      open_size--; stack_height--;
      return -1; /* If depth bound is reached return -1 */
    }

#ifndef BITSTATE
    state->in_open();
#endif //

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

    for(aux_item=newStateList; aux_item; aux_item=aux_item->next)
      open_size++;
    if(open_size>max_open_size) max_open_size=open_size;

    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);
#ifndef BITSTATE
	state->out_open();
#endif //
	open_size--;
	return state->g;	
      }
    }

    while(newStateList) { /* For all successors... */
      newState = newStateList->the_state; /* newState is the first successor */
      aux_item = newStateList;
      newStateList = newStateList->next;
      delete aux_item; /* Delete item in list */
      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);
#ifndef BITSTATE
	state->out_open();
	open_size--;
#endif //
	return newState->g;
      }

      found = ht->search(newState);
      f = wh*newState->h + newState->g;
 
      if (found) {
	matched++;
#ifdef BITSTATE
	open_size--;
	delete newState;
	continue;
#else
	if (wh*found->h + found->g <= f){
	  open_size--;
	  delete newState;
	  continue;
	}
/*        	if (wh*found->h + found->g == f) {  */
/*        	  if( found->pred && (found->pred->move.o_t == newState->pred->move.o_t) ) { */
/* 	    if (f > thresh) { */
/* 	      if (f < fstar)   */
/* 		fstar = f; */
/* 	      continue; */
/* 	    } */
/* 	    rval = IDAsearch(thresh,found); */
/* 	    if (rval != -1) return rval; */
/* 	  } */
/* 	  continue; */
/* 	} */
	found->h = newState->h; 
	found->g = newState->g;
	found->pred = newState->pred;
	delete newState;
#endif // /* BITSTATE */
      } else {
	found=newState;
	if (memory < cachemax) {
	  newState=(State *)0; /* To avoid the state to be deleted. */
	  ht->insert(found); memory++;
	  if(memory%Selected_Snapshot==0){
	    closed_size=memory-stack_height;
	    snapshot(); /* snapshot. */
	  }
	}
	else {
	  if (memory == cachemax) {
	    printf("Warning! Transposition Table full.\n");
	    if(memory%Selected_Snapshot==0){
	      closed_size=memory-stack_height;
	      snapshot(); /* snapshot. */
	    }
	  }
	}
      }
      if (f > thresh) { /* f value exceeds thresh. */
	if (f < fstar) /* min for horizon nodes. */
	  fstar = f;
	continue;
      }
      rval = IDAsearch(thresh,found);
      if(memory >= cachemax)
        delete newState; /* Delete from search stack if not in transposition table. */
      if (rval != -1){
#ifndef BITSTATE
	state->out_open();
#endif //
	open_size--;
	return rval;
      }
    }
    //delete newState;
#ifndef BITSTATE
    state->out_open();
#endif //
    open_size--; stack_height--;
    return -1;
  }

  void print_name() {
#ifndef BITSTATE
    printf("IDA* using transposition table");
#else
    printf("Bitstate IDA* using transposition table");
#endif //
  }

};


#endif // _IDASTAR_
