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

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

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

/*#define DEBUG_DFS*/

class Dfs2 : public Search{
public:
#ifdef BITSTATE
  BitStateHashTable *ht;
#endif //
  int bound_depth; /* Bound depth. States beyond the depth are not explored. */
  /*HashTable* ht;   /* Set of visited states */
  int maxf;            /* Maximum value for f. */
  /* The folowing variables are used in function DFSsearch. Declared here for efficiency. */
  int rval;            /* Returning value. */
  StateItem *aux_item, *newStateList;
  State *newState; /* Successor of state. */
  State *found,*current_error_state;
  int solution_depth,admissible;
  short tt; unsigned char ot;

  Dfs2 (int hash_size, int _maxf, int _admissible): Search() {
#ifndef BITSTATE
    ht = new HashTable(1<<hash_size); /* Instantiate hash table. */
#else
    ht = new BitStateHashTable(hash_size); /* Instantiate bitstate hash table. */
#endif //
    maxf=_maxf; /* Set maximal value for f. */
    admissible=_admissible;
  }

  int search(int bound) {
    sol_depth=-1; /* No solution found. */
    bound_depth=bound; /* Set bound depth. */
    if (Selected_Heuristic==BLIND) 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) && proto->goal(&S,1)){
      /* In some cases the initial state may be a goal state. */
      build_solution_path(&S);
      return S.g;
    }
    ht->insert(&S); /* Insert initial state in hash table. */
    memory=1; generated=1; expanded=0; matched=0; open_size=max_open_size=0; /* Init statistics. */  
    solution_depth=-1;
    solution_depth=DFSsearch(&S); /* Start recursive search */
    if(admissible && current_error_state){
      build_solution_path(current_error_state);
      solution_depth=current_error_state->g;
    }
    return solution_depth;
  }

  int DFSsearch(State* state) { /* Recursive search function. */
    short process;
    Trans *transition;

    state->in_open(); /* Mark state as on dfs1 stack. */
    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--;
      return -1; /* If depth bound is reached return -1 */
    }

    process=state->ps->_nr_pr-1;
    now=state->ps;
    tt=(short) ((P0 *)pptr(process))->_p; /* Get local state of process */
    ot=(unsigned char) ((P0 *)pptr(process))->_t; /* Get type of process */
    transition=trans[ot][tt];
    aux_item=proto->expand2(state,&process,&transition); expanded++; /* Generate 1st state */
    if(aux_item)
      newState=aux_item->the_state;
    else
      newState=(State *)0;
    delete aux_item;

    if(!newState && (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 a goal state. */
      if(proto->goal(state,1)){
	if(!admissible){
	  build_solution_path(state);
	  return state->g;
	} else{
	  current_error_state=state;
	  bound_depth=state->g;
	}
      }
    }

    while(newState) { /* For all successors... */

      found = ht->search(newState);

      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). */
	if(!admissible){
	  build_solution_path(newState);
	  return newState->g;
	} else{
	  current_error_state=newState;
	  bound_depth=newState->g;
	  state->out_open();
	  open_size--;
	  return -1;
	}
      }
      
      generated++;               

#ifndef BITSTATE
      if(found && !admissible){ /* Duplicate found. */
#else
      if(found){ /* Duplicate found. */
#endif //
#ifdef DEBUG
	printf("Duplicate found at depth %d\n",found->g);
#endif //
	matched++;
	delete newState;
	open_size--;
      } else if(!found){ /* No duplicate found. */
	ht->insert(newState); memory++; /* Insert into visited list. */
	open_size++; if(open_size>max_open_size) max_open_size=open_size;
	if(memory%Selected_Snapshot==0){
	  closed_size=memory-open_size;
	  snapshot(); /* snapshot. */
	}
	rval= DFSsearch(newState);
	if(rval!=-1){
	  state->out_open();
	  open_size--;
	  return rval;
	}
      }
#ifndef BITSTATE
      else{
#ifdef DEBUG
	printf("Duplicate found at depth %d\n",found->g);
#endif //
	matched++;
	if(found->g > newState->g) { /* Found and Admissible Search and best path: reopen */
	  open_size++; if(open_size>max_open_size) max_open_size=open_size; 
	  found->g=newState->g; found->pred=newState->pred; found->move=newState->move;
	  delete newState;
	  rval= DFSsearch(found);
	  if(rval!=-1){
	    state->out_open();
	    open_size--;
	    return rval;
	  }
	} else {
	   delete newState; open_size--;
	}
      }
#endif //

      aux_item=proto->expand2(state,&process,&transition); /* Generate next state */
      if(aux_item)
	newState=aux_item->the_state;
      else
	newState=(State *)0;
      delete aux_item;

    }
    state->out_open(); open_size--;
    return -1;
  }

  void reorder(StateItem *list){
    StateItem *item_i,*item_j,*next,*prev,*aux;
    State *aux_state;
    int i,j;

    /* Bubble sort: O(n^2)! */
    for(item_i=list; item_i->next; item_i=item_i->next){
      for(aux=list,i=0; aux; aux=aux->next) i++;
      for(item_j=item_i->next; item_j; item_j=item_j->next){
	if(item_j->the_state->h<item_i->the_state->h){
	  aux_state=item_i->the_state;
	  item_i->the_state=item_j->the_state;
	  item_j->the_state=aux_state;
	}
      }
    }

  }

  void print_name() {
    /* Auxiliary function used in main programm for visualizing the algorithm's name*/
    if(Selected_Heuristic!=BLIND && Selected_Heuristic!=TRAIL_FILE && Selected_Heuristic!=INTERACTIVE) printf("Hill Climbing");
    else printf("Depth-First Search (expands only next successor)");
  }
};


#endif // _DFS2_
