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

#define DEBUG_RESPONSE 0

#include "search.h"
#include "hashtable.h"

class Response : public Search {
public:
  HashTable *ht;
  PrioQueue *pq;
  int wg, wh, maxf, size;
  int bound_depth;
  int cycle_length;
  State *seed,*aux_state;

  Response (int hash_size,int _maxf,int _wg,int _wh) : Search(){
    size=1<<hash_size;
    maxf=_maxf;
    ht=new HashTable(1<<hash_size);
    pq=new PrioQueue(maxf);
    wg=_wg;
    wh=_wh;
  }

  int search(int bound){
    State *state; /* State to be expaned. */
    State *found; /* State in hash table. */
    State *newState; /* Successor of state. */
    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==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; /* 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();

    bound_depth=bound;

    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) {
	return -1;
      }
      state = pq->open[pq->bestf]->the_state;  /* state is the best state in the open set */

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

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

      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. */
#ifdef DEBUG
	printf("Endstate found.\n");
#endif //
	if(proto->goal(state,1)){
	  build_solution_path(state);
	  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 soon 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) {
	  found=newState;
	  ht->insert(found); memory++; /* Insert into visited list. */  
	  if(memory%100000==0) snapshot(); /* snapshot. */
	  if(memory==size) {
	    printf("Warning: Hashtable exceeds predefined size.\n");
	    snapshot();
	  }	  
#ifdef VERI
	  if(accpstate[VERI][((P0 *)hsf_pptr(found->ps,0))->_p]){
	    /* Never claim in accepting state? */
#ifdef DEBUG_RESPONSE
	    printf("Accepting state found at depth %d (claim in state %d) by 1st Search\n",found->g,((P0 *)hsf_pptr(found->ps,0))->_p);
	    printf("\tStarting 2nd nested search...\n");
#endif //
	    if(Dfs(found)!=-1){
	      return newState->g;
	    }
	    else{
#ifdef DEBUG_RESPONSE
	      printf("\tno cycle found.\n");
#endif //
	    }
	    newStateList=(StateItem *)0;
	  } else {
	    pq->insert(found,wg * found->g + wh * found->h); /* Insert into open list. */
	  }
#endif //
	}
	else { /* If newstate is a duplicate */
	  matched++;
#ifdef DEBUG
	  printf("Successor is a duplicate state (prev. depth: %d).\n",found->g);
#endif //
 	  if (found->g > newState->g) {
	    pq->change(found,wg * found->g + wh * found->h, wg * newState->g + wh * newState->h);
	    found->in_open();
	    found->g=newState->g;
	    found->h=newState->h;
	    found->pred=newState->pred;
	  }
 	  delete newState;
	}
      }
      pq->close(state,wg * state->g + wh * state->h); /* Delete state from open set */
      state->out_open();
    }
  }

  int Dfs(State *state) {
    StateItem *newStateList,*aux_item;
    State* found;
    State* newState;
    int rval;

    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 */

    //on_stack(state); /* Mark state as on dfs1 stack. */
    unflag(state); /* Mark state as not visited in the 2nd search */

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

#ifdef VERI
    if(!newStateList && accpstate[VERI][((P0 *)hsf_pptr(state->ps,0))->_p]){
	  printf("\tpossible acceptance cycle in dfs1 (at depth %d, endstate)\n",state->g);
    }
#endif //


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

      if(found){ /* Duplicate found. */
	matched++;
	if (1 /*is_on_stack(found)*/){
	  sol_depthfound=found->g+1;
	  sol_depth=-1; cycle_length=0;
	  sol_ind=new State*[newState->g+1];
	  for(aux_state=newState; aux_state!=found; aux_state=aux_state->pred){
	    sol_ind[++sol_depth]=aux_state;
	    cycle_length++;
	  }
	  for(aux_state=found; aux_state; aux_state=aux_state->pred)
	    sol_ind[++sol_depth]=aux_state;
	  printf("\tacceptance cycle in dfs1 (at depth %d, length %d)\n",found->g,cycle_length);
	  return sol_depth;
	}
	delete newState;
	continue;
      }
      else { /* No duplicate found. */
	if (proto->goal(newState,1)) {
	  /* Check if claim violated. */
	  build_solution_path(newState);
	  return newState->g;
	}
	ht->insert(newState); memory++; /* Insert into visited list. */
	if(memory%100000==0) snapshot(); /* snapshot. */
	rval = Dfs(newState);
	if (rval != -1) return rval;
      }
    }
    //out_stack(state);
    return -1;
  }

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

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

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

  void print_name(){
    printf("Response AStar + Dfs");
  }

};

#endif //
