// ..
// ..

#ifndef __LTL_POST_ASTAR_H__
#define __LTL_POST_ASTAR_H__

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

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

public:
  HashTable ht;
  PrioQueue pq;
  int bound_depth;

  LtlPostAStar(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) {  
  }

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

    ht.init(); pq.init();
    bound_depth=bound;
    
    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;

      if (ot->goal(index)) {
	build_rek_path(index,sol_depth,sol_move); // sol_depth--;
	return index->g;
      }

      newStateList = ot->expand(index); expanded++;  
      unflag(index); /* Mark state as not visited in the 2nd search */
      while(newStateList){
	newState=newStateList->the_state;
	aux_item=newStateList;
	newStateList=newStateList->next;
	delete aux_item;
	generated++;                                  // count nodes generated 

	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
	  successors++;
	}
	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
	    successors++;
	  }
	  delete newState;
	}
      }
      if(successors==0){
	rval=check(index); /* check acceptance cycles and sign to father */
	if(rval!=-1) return rval;
      } else{
	set_successors(index,successors);
      }
      f = wg * index->g + wh * index->h;     // compute f value
      pq.close(index,f);                     // move best state to closed list
    }
  }

  int check(State *s){
    int rval;

#ifdef VERI
    if(accpstate[VERI][((P0 *)hsf_pptr(s->ps,0))->_p]){ // Never claim in accepting state?
      printf("Accepting state found at depth %d (claim in state %d)\n",s->g,((P0 *)hsf_pptr(s->ps,0))->_p);
      ot->My_Goal->set_goal(s);
      ot->My_Heuristic->set_goal_state(s);
      printf("\tStarting nested search...\n");
      rval=AStar2(s);
      if(rval!=-1){
	printf("\taccepting cycle found!\n");
	depthfound=s->g-1;
	return s->g;
      }
      else{
	printf("\tno cycle found.\n");
	ot->My_Goal->unset_goal();
      }
    }
#endif //
    set_successors(s->pred,successors(s->pred)-1);
    if(successors(s->pred)==0) check(s->pred);
  }

  void set_successors(State *s, int n){
    s->move.o_To=n; /* Warning: using a field with other use*/
  }

  int successors(State *s){
    return s->move.o_To; /* Warning: using a field with other use*/
  }

  int AStar2(State *s){
    StateItem 
      *newStateList = (StateItem*) 0,  
      *aux_item = (StateItem*) 0;
    State* found;
    State* newState = (State *)0;
    int rval;

    if(s->g==bound_depth) return -1;
    flag(s);
    newStateList = ot->expand(s); expanded++;  
    while(newStateList) {
      newState = newStateList->the_state;
      aux_item = newStateList;
      newStateList = newStateList->next;
      delete aux_item;
      generated++;               

      if (ot->goal(*newState)) {    
	sol_depth=0;
	build_rek_path(newState,sol_depth,sol_move);
	depthfound=newState->g; // for putrail()
	return newState->g;
      }
      
      found = ht.search(*(newState->ps)); // target loc.
      delete newState;
      if(!found){ printf("Error! Found new state in 2nd Dfs!!!\n"); exit(0); }
      if(!flagged(found)) {
	rval=AStar2(found);
	if(rval!=-1){
	  return rval;
	}
      }
    }
    return -1;
  }

  void flag(State *S){ /* Marks state as visited in the 2nd search */
    S->move.o_tt=1;  /* Warning: using a field with other use*/
  }

  void unflag(State *S){ /* Marks state as not visited in the 2nd search */
    S->move.o_tt=0; /* Warning: using a field with other use*/
  }

  int flagged(State *S){ /* Has been visited in the 2nd search? */
    return S->move.o_tt; /* Warning: using a field with other use*/
  }

  print_name() { cout << "LTL Nested A* in postorder"; }

};

#endif //
