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

void print_compressions(){
  printf("Available Algorithms are:\n");
  printf("\t%c: No compression\n",NO_COMPRESSION);
  printf("\t%c: Byte masking compression\n",BYTE_MASKING_COMPRESSION);
}

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

void init_byte_masking(){
  int i;

  Mask[0] = Mask[1] = 1;	/* _nr_pr, _nr_qs */
  if (!a_cycles)
    {	i = &(now->_a_t) - (uchar *) &now;
    Mask[i] = 1; /* _a_t */
    }
#ifndef NOFAIR
  if (!fairness)
    {	int j = 0;
    i = &(now->_cnt[0]) - (uchar *) &now;
    while (j++ < NFAIR)
      Mask[i++] = 1; /* _cnt[] */
    }
#endif //
}

#endif //
