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

#include <stdio.h>
/*#include <stdlib.h>
  #include <Debug.h>*/

struct PrioElem;

typedef struct PrioElem{
  State *the_state;
  struct PrioElem *prev;
  struct PrioElem *next;
}PrioElem;

class PrioQueue {

public:
  PrioElem** open; /* Index of first element of OPEN with given f value. */
  unsigned int bestf; /* F value of best nodes on OPEN. */
  unsigned int maxf; /* Maximal f value. */
  int size; /* Size of Priority Queue. */
  double msize; /* Size in bytes of Priority Queue. */

  PrioQueue(unsigned int _maxf);
  ~PrioQueue(); 
  void init();
  void insert (State* s, int f); /* Insert a state in the queue with given f value. */
  void close (State* s, int f); /* Remove a state from the queue with given f value. */
  void change (State*s, int oldf, int newf); /* Change priority of a state. */
};

PrioQueue::PrioQueue(unsigned int _maxf) {
  bestf=0; maxf=_maxf;
  open = new PrioElem*[maxf+1]; /* Alloc memory for queue. */
  for(int i=0;i<maxf+1;i++) open[i]=(PrioElem*)0; /* Make sure pointers are nill. */
  size=0;
  msize=(maxf+1)*sizeof(PrioElem*);
}

PrioQueue::~PrioQueue() {
  PrioElem *current;

  for(int i=0;i<(maxf+1);i++){
    if(open[i]){
      for(current=open[i]; current; current=current->next){ /* Delete each entry */
	if(current->next) /* If not last state */
	  open[i]=current;
	delete open[i];
      }
      open[i] = (PrioElem*)0; /* Make sure pointers are nill. */
    }
  }
  delete open; /* Delete queue. */
  size=0;
  msize=0;
}
 
void PrioQueue::init() {
  PrioElem *current;

  size=0;
  bestf = 0;   
  for(int i=0; i<(maxf+1); i++){
    while(open[i]){ /* Delete each entry */
      current=open[i];
      open[i]=open[i]->next;
      delete current;
    }
    open[i] = (PrioElem*)0; /* Make sure pointers are nill. */
  }
}

void PrioQueue::insert (State *index, int f) {
  PrioElem *MyPrioElem;
  
  MyPrioElem=new PrioElem; /* Create new item. */
  MyPrioElem->the_state=index; /* Set state pointer. */
  MyPrioElem->prev=(PrioElem*)0; /* No previous item. */
  if(open[f]){ /* If already a state with same f value */
    open[f]->prev = MyPrioElem; /* Next state points back to it. */
  }
  MyPrioElem->next= open[f]; /* Put at head of correct open list. */
  open[f] = MyPrioElem; /* Set head to point to new element. */
  if (f < bestf) bestf = f;
  size++;
  msize+=sizeof(PrioElem);
}

void PrioQueue::close (State *index, int f) {
  PrioElem *current;

  size--;
  msize-=sizeof(PrioElem);
  for(current=open[f]; current; current=current->next){
    if(current->the_state==index){
      if(current->prev) /* It is not the first element. */
	current->prev->next=current->next;
      else /* It is the 1st element. */
	open[f]=current->next;
      if(current->next) /* It is not the last element. */
	current->next->prev=current->prev;
      delete current;
      return;
    }
  }
  printf("Error! Trying to delete from priority queue a non existing state\n");
  printf("The state is %d (in_open=%d)\n",(int)index,index->is_in_open());
  bug();
  exit(0);
}

void PrioQueue::change (State *index, int oldf, int newf) {
  PrioElem *current;
  /* Delete state in open[oldf], */
  for(current=open[oldf]; current; current=current->next){
    if(current->the_state==index){
      if(current->prev) /* It is not the first element. */
	current->prev->next=current->next;
      else /* It is the 1st element. */
	open[oldf]=current->next;
      if(current->next) /* It is not the last element. */
	current->next->prev=current->prev;
      break;
    }
  }
  if(!current){
    printf("Error! Open state not found when changing its value.\n"); bug(); exit(0);
  }

  /* Insert current in open[newf]. */
  current->prev=(PrioElem*)0; /* No previous item. */
  if(open[newf]){ /* If already a state with same f value */
    open[newf]->prev = current; /* Next state points back to it. */
  }
  current->next= open[newf]; /* Put at head of correct open list. */
  open[newf] = current; /* Set head to point to new element. */
  if (newf < bestf) bestf = newf;

}

#endif //
