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

/* Includes */
#include <global.h>
#include "hashtable.h"
int Selected_Snapshot;
#define DEFAULT_SNAPSHOT 100000

class Search{
public:
  Protocol* proto; /* The procol to analyze. */
  int total; /* total number of nodes generated */ 
  int hash; /* total number of nodes hashed */
  int pruned;  /* total number of nodes pruned */
  int expanded; /* total number of nodes expanded  */
  int generated; /* total number of nodes generated (this iteration) */
  int reopened;  /* number of open or closed states a shorter path was found to */
  int memory; /* total number of nodes in memory */
  int reopenings; /* number of reopenings. */
  int open_size; int max_open_size; int stack_height; int max_stack_height; int closed_size;
  int matched; /* total number of duplicates */
  int sol_depth; /* length of the solution found. */
  int sol_depthfound; /* depth at wich the cycle begins. */
  int depth_reached; /* Maximal depth reached. */
  State** sol_ind; /* maintain gener. sequences in backtrack. */
  State S;  /* used as the initial state. */
  HashTable *ht; /* Set of visited states. */

  Search(){};
  virtual ~Search(){};
  void init(Protocol* _proto); /* Instantiates and inits the protocol. */
  void build_solution_path(State *index);
  virtual void print_name() {};
  int virtual search() {};
  int virtual search(int bound) {};
  void statistics();
  void statistics(int thresh);
  void snapshot();
  virtual void print_solution(); 
  virtual void print_trail(); 
  void filter_trail();
  void on_stack(State *S);
  void out_stack(State *S);
  int is_on_stack(State *S);
};

#endif // /* _SEARCH_H_ */
