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

/* Includes */
#include <stdio.h>                                 
/*#include <stdlib.h>*/
#include <global.h>


struct BucketType;

typedef struct BucketType{
  State *the_state;
  struct BucketType *link;
  ~BucketType(){delete the_state;};
}BucketType;

class HashTable {
 public:
  BucketType** bucket; /* Pointer to first element in table with given hash value. */
  int max; /* Number of entries in hash table. */
  double msize;
  
  HashTable(int m);
  void clean(); 
  void init(); 
  ~HashTable();
  int hash(PackedState& ps);
  State* search(State *ps); /* Search a state with given state vector. */
  void remove(State *S); /* Remove a given state. */
  void insert(State *S); /* Insert a given state. */
  State* search(PackedState& ps, int hashval); /* Search a state with given state vector in given entry. */
  void insert(State *S, int hashval); /* Insert a given state in given entry. */
};


HashTable::HashTable(int m): max(m) {
  bucket = new BucketType*[max]; /* Alloc entries. */
  for(int i=0; i<max; i++) bucket[i]=(BucketType *)0; /* Make sure pointers are nill */
  msize=max*sizeof(BucketType*);
}

void HashTable::clean() { /* REMOVES ONLY THE ENTRIES, NOT THE STATES */ 
  BucketType* old_bucket;
  for(int i=0; i<max; i++){
    while(bucket[i]){ /* Remove each bucket list. */
      old_bucket=bucket[i];
      bucket[i]=bucket[i]->link;
      old_bucket->the_state=(State*)0; /* To avoid removing of state */
      delete old_bucket;
    }
    bucket[i]=(BucketType *)0; /* Make sure pointers are nill */
  }
  msize=max*sizeof(BucketType*);
}

void HashTable::init() { 
  BucketType* old_bucket;
  for(int i=0; i<max; i++){
    while(bucket[i]){ /* Remove each bucket list. */
      old_bucket=bucket[i];
      bucket[i]=bucket[i]->link;
      delete old_bucket;
    }
    bucket[i]=(BucketType *)0; /* Make sure pointers are nill */
  }
  msize=max*sizeof(BucketType*);
}

HashTable::~HashTable() {
  BucketType* old_bucket;
  for(int i=0; i<max; i++){
    while(bucket[i]){ /* Remove each bucket list. */
      old_bucket=bucket[i];
      bucket[i]=bucket[i]->link;
      delete old_bucket;
    }
    bucket[i]=(BucketType *)0; /* Make sure pointers are nill */
  }
  delete bucket; /* Free bucket list. */
  msize=0;
}

int HashTable::hash(PackedState& ps) {
  int h;
  h=PackedState::hash(ps,max); /* Hash function defined in hsf-pan.h */
  if(h<0){ printf("Error! hashvalue negative.\n"); bug(); exit(0);}
  return h;
}      

State *HashTable::search(State *S) {
  /* Search takes an UNCOMPRESSED  state and its hash value, and returns
     the index in the hash table where it is located. 
     Collisions are handled by searching down the linked chain of 
     the bucket. If the state is not in the table, it returns a nill pointer. */
  int hashval;
  BucketType *my_bucket;
  PackedState *comp_ps;
  PackedState *ps=S->ps;

  /* If compression is used this searches only in open */
  hashval=this->hash(*ps);
  for(my_bucket  = bucket[hashval]; my_bucket; my_bucket=my_bucket->link) {
    if (((!Selected_Compression) || my_bucket->the_state->is_in_open()) && PackedState::equal(*ps,*(my_bucket->the_state->ps)))
      return my_bucket->the_state; /* State found */
  }
  /* If compression is used we have to look for the state in closed too */
  if(Selected_Compression!=NO_COMPRESSION){
    S->compress_in(&comp_ps);
    for(my_bucket  = bucket[hashval]; my_bucket; my_bucket=my_bucket->link) {
      if ((!my_bucket->the_state->is_in_open()) && PackedState::equal(*comp_ps,*(my_bucket->the_state->ps))){
	delete comp_ps;
	return my_bucket->the_state; /* State found */
      }
    }
    delete comp_ps;
  }
  return (State *)0; /* State not found. */
}

void HashTable::remove (State *S) {
  /* remove assumes that the state is in closed. */
  int hashval;
  BucketType *my_bucket;
  BucketType *prev_bucket;

  msize-=sizeof(BucketType*)+sizeof(State)+S->ps->_vsz;
  hashval=this->hash(*(S->ps)); /* incorrect with compression!!! */
  prev_bucket=bucket[hashval];
  for(my_bucket=bucket[hashval]; my_bucket; my_bucket=my_bucket->link) {
    if (PackedState::equal(*(S->ps),*(my_bucket->the_state->ps))){
      if(my_bucket==bucket[hashval]){ /* If first state... */
	delete bucket[hashval];
	bucket[hashval]=(my_bucket->link)?(my_bucket->link):(BucketType *)0;
      }else if(!my_bucket->link){ /* If last state... */
	delete my_bucket;
	prev_bucket->link=(BucketType *)0;
      } else{
	prev_bucket->link=my_bucket->link;
	delete my_bucket;
      }
      return;
    }
    prev_bucket=my_bucket;
  }
  printf("Error! Trying to delete from hash table a non existing state.\n");
  bug(); exit(0); /* It is an error trying to delete a non existing state. */
}

void HashTable::insert (State *S) {
  /* For compression it assumes that states are first inserted in the open set. */
  int hashval;
  BucketType *my_bucket;
  
  hashval=this->hash(*(S->ps));
  my_bucket=new BucketType;
  my_bucket->the_state=S;
  my_bucket->link=bucket[hashval];
  bucket[hashval] = my_bucket;
  msize+=sizeof(BucketType*)+sizeof(State)+S->ps->_vsz;
}

/* The following methods are no more used. */

State *HashTable::search (PackedState& ps, int hashval) {
  BucketType *my_bucket;

  for(my_bucket  = bucket[hashval]; my_bucket; my_bucket=my_bucket->link) {
    if (PackedState::equal(ps,*(my_bucket->the_state->ps)))
      return my_bucket->the_state; /* State found. */
  }
  return (State *)0; /* State not found. */
}

void HashTable::insert (State *S, int hashval) {
  BucketType *my_bucket;

  my_bucket=new BucketType;
  my_bucket->the_state=S;
  my_bucket->link=bucket[hashval];
  bucket[hashval] = my_bucket;
}

#endif //
