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

#define DEBUG_NDFS

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

class Ndfs : public Search {
public:
  int bound_depth; /* Bound depth. States beyond the depth are not explored. */
  int cycle_length;
  State *seed,*aux_state;
  /* The folowing variables are used in function DFSsearch. Declared here for efficiency. */
  int rval; /* Returning value. */
  StateItem* aux_item;
  State* found;
  int maxf; /* Maximum value for f. */
  int improved; /* Normal or Improved NDFS? */
  SCC *My_SCC; /* SCC classificator */

  Ndfs (int hash_size, int _maxf, int _improved): 
    Search() {
    ht = new HashTable(1<<hash_size); /* Instantiate hash table. */
    maxf=_maxf; /* Set maximal value for f. */
    improved=_improved;
  }

  int search(int bound) {
    sol_depth=-1; /* No solution found. */
    bound_depth=bound; /* Set bound depth. */
    if (!Selected_Heuristic) S.h=0; /* If not heuristic defined set h value to zero. */
    S.pred=(State *)0; /* Initial state has no predecessor. */
    if( (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=1;/* Init statistics. */ 
    if(improved){
      My_SCC=new SCC;
#ifdef VERI
      My_SCC->Classify_SCC(VERI);
#endif //
    }
    return Dfs1(&S);
  }


  int Dfs1(State* state){ 
    State* newState = (State *)0; /* Successor of state. */
    StateItem* newStateList; /* Successors list and auxiliar item. */

    stack_height++;
    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--; stack_height--;
      return -1; /* If depth bound is reached return -1 */
    }

    state->in_open(); /* 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 */
    for(aux_item=newStateList; aux_item; aux_item=aux_item->next)
      open_size++;
    if(open_size>max_open_size) max_open_size=open_size;
    
    if(Selected_Heuristic!=BLIND && Selected_Heuristic!=TRAIL_FILE && Selected_Heuristic!=INTERACTIVE && newStateList) reorder(newStateList); /* Move ordering if heuristic defined */

#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++;
#ifdef VERI
	if (improved && found->is_in_open() && My_SCC->f_scc(My_SCC->scc[neverstate(found->ps)])){
	  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);
	  state->out_open(); open_size--;
	  return sol_depth;
	}
#endif // VERI
	delete newState; open_size--;
	continue;
      }
      else { /* No duplicate found. */
#ifdef VERI
	if ((Selected_Goal==LTL) && proto->goal(newState,1)) {
	  /* Check if claim violated. */
	  build_solution_path(newState);
	  state->out_open(); open_size--;
	  return newState->g;
	}
#endif //
	ht->insert(newState); memory++; /* Insert into visited list. */
	if(memory%Selected_Snapshot==0){
	  closed_size=memory-stack_height;
	  snapshot(); /* snapshot. */
	}
	rval = Dfs1(newState);
	if (rval != -1){
	  state->out_open(); open_size--;
	  return rval;
	}
      }
    }
    /* Start 2nd dfs in postorder. */
#ifdef VERI
    if(((!improved) && accpstate[VERI][((P0 *)hsf_pptr(state->ps,0))->_p])
       || (improved && accpstate[VERI][((P0 *)hsf_pptr(state->ps,0))->_p] && My_SCC->p_scc(My_SCC->scc[neverstate(state->ps)]))){
      /* Never claim in accepting state? */
      seed=state;
      rval=Dfs2(state);
      if(rval!=-1){
	state->out_open(); //open_size--;
	return rval;
      }
    }
#endif //
    state->out_open(); open_size--; stack_height--;
    return -1;
  }

#ifdef VERI
  int Dfs2(State* state) { 
    State* newState = (State *)0;
    StateItem *newStateList = (StateItem*) 0;

    flag(state); /* mark state as visited in dfs. */
    stack_height++;
    if(state->g==bound_depth){
      printf("Warning: max search depth too small\n");
      open_size--; stack_height--;
      return -1; /* If depth bound is reached return -1 */
    }

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

    for(aux_item=newStateList; aux_item; aux_item=aux_item->next)
      open_size++;
    if(open_size>max_open_size) max_open_size=open_size;

    if(Selected_Heuristic!=BLIND && Selected_Heuristic!=TRAIL_FILE && Selected_Heuristic!=INTERACTIVE && newStateList) reorder(newStateList); /* Move ordering if heuristic defined */

    while(newStateList) {
      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){ printf("Error! Found new state in 2nd Dfs.\n"); bug(); exit(0); }

      /* Set pred in 2nd search. */
      for(aux_state=newState; aux_state!=state; aux_state=aux_state->pred)
	aux_state->cycle_pred=aux_state->pred;
      if( (found->is_in_open()) ){
	if(Selected_Goal!=LTL){
	  delete newState;
	  open_size--;
	  continue;
	}
	sol_depthfound=found->g+1;
	sol_depth=-1;
	cycle_length=0;
	sol_ind=new State*[maxf*2]; /* Allocate solution path. */
	/* Construct cycle. 1st part: found..seed */
	for(aux_state=newState; aux_state!=seed; aux_state=aux_state->cycle_pred){
	  sol_ind[++sol_depth]=aux_state;
	  cycle_length++;
	}
	/* Construct cycle. 1st part: seed..found */
	for(aux_state; aux_state!=found; aux_state=aux_state->pred){
	  sol_ind[++sol_depth]=aux_state;
	  cycle_length++;
	}
	/* Construct path to cycle: found..root. */
	for(aux_state; aux_state && (aux_state->g>0); aux_state=aux_state->pred){
	  sol_ind[++sol_depth]=aux_state;
	}
	printf("\tacceptance cycle in dfs2 (at depth %d, length %d)\n",found->g,cycle_length);
	return sol_depth;
      }
      delete newState; open_size--;
      if(!flagged(found) &&
	 !(improved && (My_SCC->scc[neverstate(found->ps)]!=My_SCC->scc[neverstate(state->ps)]) )){
	rval=Dfs2(found);
	if(rval!=-1){
	  return rval;
	}
      }
    }
    open_size--; stack_height--;
    return -1;
  }
#endif //

  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 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() {
    if(improved) printf("Improved ");
    printf("Nested Depth First Search");
  }
 
  
};


#endif // _NDFS_
