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

/* Includes */
#include <universal_hashing_class.h> /* Hashing functions. */
Hash_Function *the_hash_function;
#include <pan.c> /* Spin code. */
#include <compression.h>
#include <compression.c>

class Protocol;


typedef Trail Move_Type;

class BitState;

class State {
 public:
  PackedState *ps;   /* State description (spin's format, defined in pan.h) */
  unsigned int g;             /* Distance from initial state. */
  unsigned short h;           /* Heuristic distance from goal state. */
  Move_Type move;    /* Move performed (alias for struct Trail, defined in pan.c). */
  State *pred;       /* Predecessor in solution. */
#ifdef VERI
  State *cycle_pred; /* Predecessor in 2nd search. */
#endif //

  State(){
    this->h=0;
    this->ps=(PackedState *)0;
    this->pred=(State *)0;
  }

  State& operator=(State& s){
    /* Copy state description. Warning: s.ps->_vsz bytes will copied. */
    if(!(this->ps)) this->ps=new PackedState;
    memcpy((void *)this->ps,(void *)s.ps,s.ps->_vsz);
    this->g=s.g;
    this->h=s.h;
    this->move=s.move;
    this->pred=s.pred;
    return *this;
  }

  State& operator=(BitState& s);

  ~State(){
    //printf("Deleting at depth %d\n", this->g);
    if(this->pred && !(this->pred->ps)){ /* Pred is a movement, not a state */
      delete this->pred;
    }
    if(this->ps){
      //printf("\twith ps\n");
      delete(this->ps);
    }
  }

  void compress(){
    PackedState *comp_ps;
    switch(Selected_Compression){
    case NO_COMPRESSION: break;
    case BYTE_MASKING_COMPRESSION:
      byte_masking(&comp_ps,this->ps->_vsz);
      delete this->ps;
      this->ps=(PackedState*) new unsigned char[comp_ps->_vsz];
      memcpy((void *)this->ps,(void *)comp_ps,comp_ps->_vsz);
      delete comp_ps;
      break;
    case TEST_COMPRESSION:
      delete this->ps;
      this->ps=(PackedState*) new unsigned char[sizeof(PackedState)-VECTORSZ];
      this->ps->_vsz=sizeof(PackedState)-VECTORSZ;
      break;
    default: printf("Error! Undefined compression technique %d.\n",Selected_Compression); exit (0);
    }
  }

  void compress_in(PackedState **comp_ps){
    switch(Selected_Compression){
    case NO_COMPRESSION: break;
    case BYTE_MASKING_COMPRESSION:
      byte_masking(comp_ps,this->ps->_vsz);
      break;
    case TEST_COMPRESSION:
      *comp_ps=(PackedState*) new unsigned char[sizeof(PackedState)-VECTORSZ];
      (*comp_ps)->_vsz=sizeof(PackedState)-VECTORSZ;
      break;
    default: printf("Error! Undefined compression technique %d.\n",Selected_Compression); exit (0);
    }
  }

  void uncompress(){
    switch(Selected_Compression){
    case NO_COMPRESSION: break;
    default: printf("Error! Undefined compression technique %d.\n",Selected_Compression); exit (0);
    }
  }

  void byte_masking(PackedState **comp_ps, int n){
    char *v;
    char *vv = (char*)this->ps;
    int i,j;

    *comp_ps=(PackedState*) new unsigned char[n];
    v=(char *)*comp_ps;
    for (i = 0, j=0; i < n; i++)
      if (!Mask[i]){
	v[j] =vv[i];
	j++;
      }
    //for (i = 0; i < WS-1; i++) /* Is this necessary??? */
    //  v[j+i] = 0;

    (*comp_ps)->_vsz=j;
    /* Reallocates the state for using only the necessary size. */ 
    
    v=(char *)*comp_ps;
    *comp_ps=(PackedState*) new unsigned char[((PackedState *)v)->_vsz];
    memcpy((void *)*comp_ps,(void *)v,((PackedState *)v)->_vsz);
    delete v;
  }

  void shrink(){
    /* Reallocates the state for using only the necessary size. */ 
    PackedState *aux_ps;
    
    aux_ps=this->ps;
    this->ps=(PackedState*) new unsigned char[aux_ps->_vsz];
    memcpy((void *)this->ps,(void *)aux_ps,aux_ps->_vsz);
    delete aux_ps;
  }

  void unshrink(){
    /* Reallocates the the state for using the fixed state vector size. */
    PackedState *aux_ps;
    
    aux_ps=this->ps;
    this->ps=new PackedState;
    memset((void *)this->ps,0,sizeof(PackedState));
    memcpy((void *)this->ps,(void *)aux_ps,aux_ps->_vsz);
    delete aux_ps;
  }

  void in_open(){ /* Mark taht the state is in the open set */
    move.o_tt|=1;  /* Warning: using a field with other use */
  }

  void out_open(){ /* Marks state as not open set */
    move.o_tt&=~1; /* Warning: using a field with other use */
    compress();
#ifdef BITSTATE
    delete this->ps;
#endif //
    if(is_in_open()) printf("ERROR!!!");
  }

  int is_in_open(){ /* Is the state in the open set? */
    return move.o_tt&1; /* Warning: using a field with other use */
  }

};

/* Some things for bitstate compression. */

typedef struct BitStateMove{
  unsigned char pr;
  short st;
  Trans *o_t;
}BitStateMove;  

class BitState {
 public:
  BitStateMove move;
  int pred;
  
  PackedState& operator=(State& s){
    this->move.pr=s.move.pr;
    this->move.st=s.move.st;
    this->move.o_t=s.move.o_t;
    this->pred=(int)s.pred;
  }
};

class StateItem{
  /* This class is mainly used for implementing the set of successsors of a state. */
 public:
  State *the_state;
  StateItem *prev;
  StateItem *next;
  StateItem(){
    the_state=(State *)0;
    next=(StateItem *)0;
    prev=(StateItem *)0;
  }
};

#endif // _GLOBAL_
