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

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

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

#include "prioqueue.h"

/*#define DEBUG_ASTAR*/

class AStar : public Search{
 public:
#ifdef BITSTATE
  /* Bitstate table instead of hashtable */
  BitStateHashTable* ht;
#endif // BITSTATE
  PrioQueue *pq; /* set of open states (states to be expanded) */
  unsigned int wg, wh, maxf, size;

  AStar(unsigned int hash_size,unsigned int _maxf,unsigned int _wg,unsigned int _wh) : Search(){
    size=1<<hash_size;
    maxf=_maxf;

#ifndef BITSTATE
    ht=new HashTable(1<<hash_size);
#else /* Bitstate table instead of hashtable */
    ht = new BitStateHashTable(hash_size);
#endif //

    pq=new PrioQueue(maxf);
    wg=_wg;
    wh=_wh;
  }

  ~AStar(){
    /*delete ht;*/
    delete pq;
  }

  int search(int bound) {
    State *state; /* State to be expaned. */
    State *newState; /* Successor of state. */
    State *found; /* State in hash table. */
    StateItem* newStateList,*aux_item; /* Successors list and auxiliar item. */
    int f;

    sol_depth=-1; /* No solution found. */
    state=&S; /* Make state point to initial state S. */
    if (Selected_Heuristic==BLIND || Selected_Heuristic==TRAIL_FILE || Selected_Heuristic==INTERACTIVE) S.h=0; /* If not heuristic defined set h value to zero. */
    S.pred=(State*)0; /* Initial state has no predecessor. */
    if( (Selected_Goal==GIVEN_STATE || Selected_Goal==ORBIT ||  Selected_Goal==LTL) && (state!=&S) && proto->goal(state,1) ){
      /* In some cases the initial state may be a goal state. */
      build_solution_path(state);
      return state->g;
    }
    ht->insert(state); /* Insert initial state in hash table. */
    memory=1; generated=1; expanded=0; matched=0; reopenings=0; /* Init statistics. */
    pq->bestf = wg * S.g + wh * S.h; /* Set best f value in open set. */
    pq->insert(state, wg*state->g + wh*state->h);  /* Insert initial state in open set. */     
    state->in_open();
    int maxi = pq->bestf;
    while(1) { /* Expand until goal found or hash table full */
      while((!pq->open[pq->bestf]) && (pq->bestf != maxf)) { /* find best node on open lists. */
	pq->bestf++;
	if(pq->bestf > maxi){
	  maxi = pq->bestf;
	}
      }
      if (pq->bestf == maxf) {
	open_size=pq->size;
	return -1;
      }
      state = pq->open[pq->bestf]->the_state;  /* state is the best state in the open set */
      if(!state->is_in_open()){
	printf("Error! Closing closed state.\n");
	bug();
	exit(0);
      }

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

      newStateList = proto->expand(state,1,bound); expanded++; /* Expand state */
    
      if(!newStateList && (Selected_Goal==DEADLOCK || Selected_Goal==SIMPLESAFETY || Selected_Goal==VALID_ENDSTATE || Selected_Goal==GIVEN_STATE || Selected_Goal==ORBIT)){
	/* If state is an endstate and we are checking for deadlocks or valid endstates,
	   then check if state is an goal state. */
#ifdef DEBUG
	printf("Endstate found.\n");
#endif //
	if(proto->goal(state,1)){
	  build_solution_path(state);
	  open_size=pq->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++;

	found = ht->search(newState); /* See if newState has already been visited */

	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;
	}

	if (!found) {
	  /* If newState is not a duplicate */
#ifdef DEBUG
	  printf("Successor is a new state.\n");
#endif //
	  found=newState;
	  pq->insert(found,wg * found->g + wh * found->h); /* Insert into open list. */
	  found->in_open();
	  ht->insert(found); memory++; /* Insert into visited list. */
	  open_size=pq->size; if(open_size>max_open_size) max_open_size=open_size;
	  if(memory%Selected_Snapshot==0) {
	    closed_size=memory-open_size;
	    snapshot();
	  } /* snapshot. */
	  if(memory==size) {
	    printf("Warning: Hashtable exceeds predefined size.\n");
	    snapshot();
	  }

	}
	else { /* If newstate is a duplicate */
	  matched++;
#ifdef DEBUG
	  printf("Successor is a duplicate state (prev. depth: %d).\n",found->g);
#endif //
#ifndef BITSTATE
 	  if (found->g > newState->g && (wg!=0 || found->is_in_open()) ) {
	    /* Reopening only if A*. In addition open states reached through better paths are updated.*/
	    if(found->is_in_open())
	      pq->change(found,wg * found->g + wh * found->h, wg * newState->g + wh * newState->h);
	    if(Selected_Compression!=NO_COMPRESSION && !found->is_in_open()){
	      /* Uncompress found */
	      delete(found->ps);
	      found->ps=(PackedState*) new unsigned char[newState->ps->_vsz];
	      memcpy((void*)found->ps, (void *)newState->ps, newState->ps->_vsz);
	    }
	    if(!found->is_in_open()){
	      pq->insert(found, wg*newState->g + wh*newState->h);
	      reopenings++;
	    }
	    found->g=newState->g;
	    found->h=newState->h;
	    if(!found->pred->ps) delete found->pred; /* Delete old moves */
	    found->pred=newState->pred;	    
	    newState->pred=(State *)0; /* Avoid deleting moves. */
	    found->move=newState->move;	
	    found->in_open();
	  }
#endif //
 	  delete newState;
	}
      }
      pq->close(state,wg * state->g + wh * state->h); /* Delete state from open set */
      open_size=pq->size; if(open_size>max_open_size) max_open_size=open_size;
      state->out_open();
    }
  }

  void print_name() {
    /* Auxiliary function used in main programm for visualizing the algorithm's name*/
    if(Selected_Heuristic==BLIND || wh==0){
      printf("Breadth-First Search");
    } else if(wg==0){
      printf("Best-First Search");
    } else printf("A*");
  }

};

#endif //
