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

// -----------------------------------
#include "Search.h"
#include "HashTable.h"
#include "PrioQueue.h"

template<class Automaton>
class NestedAStar : public Search<Automaton> {

public:
  HashTable ht;
  PrioQueue pq;

  NestedAStar(Automaton* aT,int max,int maxf, 
	       int applicability,int heuristic,int wg,int wh) : 
    Search<Automaton>(aT,max,maxf,maxmove,applicability,heuristic,wg,wh), 
    ht(max), pq(max,maxf) {
  }

  ~NestedAStar(){
    ht.~HashTable();
    pq.~PrioQueue();
  }

  search(int bound) {
    State *index;
    State *found;
    State *newState;
    StateItem* newStateList,*aux_item;
    int newindex;
    int hashval;                                 
    int f,flag;

    ht.init(); pq.init();
    
    pq.bestf = wh * S.h; expanded=0;       // compute F value of initial state 
    expanded=sol_depth= 0;    
    if (!heuristic) S.h = 0;
    index=new State;
    *index=S;
    ht.insert(index); memory=1;    
    f = wg * index->g + wh * index->h;       // compute f value 
    pq.insert(index,f);      
    aT->dfa();

    // ------------------------- run -------------------------------
    int maxi = pq.bestf;

    while (1) {    // expand until goal found or hash table full
      flag = 0;
      while ((!pq.open[pq.bestf]) && (pq.bestf != maxf)) {
	pq.bestf++;                            // find best node on open lists
	if (pq.bestf > maxi) {
	  //cout << maxi << ":" << expanded << endl;
	  maxi = pq.bestf;
	}
      }
      if (pq.bestf == maxf || pq.bestf==bound) {
	//cout << "e:" << expanded << endl;
	//delete newState; ???
	return -1;
      }
      index = pq.open[pq.bestf]->the_state;  // new best state on open list 
      found = 0;

      newStateList = ot->expand(index); expanded++;  
 
      while(newStateList){
	newState=newStateList->the_state;
	aux_item=newStateList;
	newStateList=newStateList->next;
	delete aux_item;
	generated++;                                  // count nodes generated 

	if (ot->goal(newState)) {
	  printf("\tacceptance cycle (of length %d)\n",newState->g);
	  //build_rek_path(newState,sol_depth,sol_move); // sol_depth--;
	  return newState->g;
	}

	if (!heuristic) newState->h = 0;

	found = ht.search(*(newState->ps)); // target loc.
       
	if (!found) {
	  found=newState;
	  f = wg * found->g + wh * found->h;
	  pq.insert(found,f);           // insert into open list
	  ht.insert(found); memory++;     // insert into hash list
	}
	else {
	  if (found->g > newState->g) {    
	    f = wg * found->g + wh * found->h; 
	    pq.close(found,f);                  // remove node from open
	    found=newState;
	    f = wg * found->g + wh * found->h; 
	    pq.insert(found,f);                 // insert into open list 
	    ht.insert(found);                   // insert into hash table
	    reopened++;         // keep track of how many times this happens
	  }
	  delete newState;
	}
      }
      f = wg * index->g + wh * index->h;     // compute f value
      pq.close(index,f);                     // move best state to closed list
    }
  }

  print_name() { cout << "NestedA* with Dynamic State Allocation"; }

};

#endif //


