/*
Copyright (c) 2002-2010, Dirk Krause
All rights reserved.

Redistribution and use in source and binary forms,
with or without modification, are permitted provided
that the following conditions are met:

* Redistributions of source code must retain the above
  copyright notice, this list of conditions and the
  following disclaimer.
* Redistributions in binary form must reproduce the above 
  opyright notice, this list of conditions and the following
  disclaimer in the documentation and/or other materials
  provided with the distribution.
* Neither the name of the Dirk Krause nor the names of
  contributors may be used to endorse or promote
  products derived from this software without specific
  prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND
CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED.
IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
DAMAGE.
*/



/**	@file	reducau.c	The reducau module of the genau program.

This module contains functions to create a reduced state machine.
*/



#include <genau.h>
#include <dkmem.h>
#include <dkbf.h>
#include <dksto.h>
#include <dkapp.h>
#include <dklogc.h>


#line 54 "reducau.ctr"




/**	Pointer to bit field.
*/
typedef dk_bitfield_t *DKBFPTR;



/**	Half bit matrix.
*/
typedef struct {
  DKBFPTR  *array;	/**< Data. */
  unsigned  number;	/**< Side length. */
} half_bit_matrix_t ;



/**	Delete half bit matrix, release memory.
	@param	hbm	Matrix.
*/
static
void
hbm_delete DK_P1(half_bit_matrix_t *, hbm)
{
  DKBFPTR *ptr;
  unsigned i;
  if(hbm) {
    if(hbm->array) {
      ptr = hbm->array;
      for(i = 0; i < hbm->number; i++)
      {
	if(*ptr) {
	  dkbf_close(*ptr);
	  *ptr = NULL;
	}
	ptr++;
      }
    }
    hbm->array = NULL;
    hbm->number = 0;
    dk_delete(hbm);
  }
}



/**	Create new half bit matrix.
	@param	sz	Number of rows, equal to number of columns.
	@return	Pointer to matrix on success, NULL on error.
*/
static
half_bit_matrix_t *
hbm_new DK_P1(unsigned, sz)
{
  half_bit_matrix_t *back = NULL;
  DKBFPTR *ptr;
  int ok;
  unsigned i, j;
  if(sz) {
    back = dk_new(half_bit_matrix_t,1);
    if(back) {
      ok = 1;
      back->array = NULL; back->number = 0;
      back->array = dk_new(DKBFPTR,sz);
      if(back->array) {
	ptr = back->array;
	for(i = 0; i < sz; i++) {
	  *(ptr++) = NULL;
	}
	ptr = back->array; j = 0;
	for(i = 0; i < sz; i++) {
	  j++;
	  *ptr = dkbf_open(j);
	  if(!(*ptr)) { ok = 0; }
	  ptr++;
	}
      } else {
	ok = 0;
      }
      if(ok) {
	back->number = sz;
      } else {
	hbm_delete(back);
	back = NULL;
      }
    }
  }
  return back;
}



/**	Set value in half bit matrix.
	@param	hbm	Matrix.
	@param	r	Row index.
	@param	c	Column index.
	@param	v	Value to set.
*/
static
void
hbm_set DK_P4(half_bit_matrix_t *, hbm, unsigned, r, unsigned, c, int, v)
{
  if(hbm) {
    if((r < hbm->number) && (c < hbm->number)) {
      if(c > r) {
	hbm_set(hbm,c,r,v);
      } else {
	
	dkbf_set((hbm->array)[r],c,v);
      }
    }
  } 
}



/**	Get value from half bit matrix.
	@param	hbm	Matrix.
	@param	r	Row index.
	@param	c	Column index.
	@return	Bit value.
*/
static
int
hbm_get DK_P3(half_bit_matrix_t *, hbm, unsigned, r, unsigned, c)
{
  int back = 0;
  if(hbm) {
    if((r < hbm->number) && (c < hbm->number)) {
      if(c > r) {
	back = hbm_get(hbm,c,r);
      } else {
	back = dkbf_get((hbm->array)[r],c);
      }
    }
  } 
  return back;
}



/**	Pointer to one unsigned int row.
*/
typedef unsigned *UNSIGNEDPTR;



/**	Unsigned in matrix.
*/
typedef struct {
  UNSIGNEDPTR *array;	/**< Matrix data. */
  unsigned rows;	/**< Number of rows. */
  unsigned columns;	/**< Number of columns. */
} unsigned_matrix_t;



/**	Delete unsigned int matrix, release memory.
	@param	m	Matrix.
*/
static
void
um_delete DK_P1(unsigned_matrix_t *, m)
{
  UNSIGNEDPTR *ptr;
  unsigned i;
  if(m) {
    if(m->array) {
      ptr = m->array;
      for(i = 0; i < m->rows; i++) {
	if(*ptr) {
	  dk_delete(*ptr);
	}
	*(ptr++) = NULL;;
      }
    }
    m->array = NULL; m->rows = 0; m->columns = 0;
    dk_delete(m);
  }
}



/**	Reset all entries in an unsigned int matrix.
	@param	m	Matrix.
*/
static
void
um_reset DK_P1(unsigned_matrix_t *, m)
{
  UNSIGNEDPTR *ptr;
  unsigned *uptr;
  unsigned i, j;
  if(m) {
    ptr = m->array;
    for(i = 0; i < m->rows; i++) {
      uptr = *ptr;
      for(j = 0; j < m->columns; j++) {
	*(uptr++) = 0;
      }
      ptr++;
    }
  }
}



/**	Set value in unsigned int matrix.
	@param	m	Matrix.
	@param	r	Row index.
	@param	c	Column index.
	@param	v	Value to set.
*/
static
void
um_set DK_P4(unsigned_matrix_t *, m, unsigned, r, unsigned, c, unsigned, v)
{
  if(m) {
    if(r < m->rows) {
    if(c < m->columns) {
      ((m->array)[r])[c] = v;
    }
    }
  }
}



/**	Retrieve value from unsigned int matrix.
	@param	m	Matrix.
	@param	r	Row Index.
	@param	c	Column index.
	@return	Value at the specified position.
*/
static
unsigned
um_get DK_P3(unsigned_matrix_t *, m, unsigned, r, unsigned, c)
{
  unsigned back = 0;
  if(m) {
    if(r < m->rows) {
    if(c < m->columns) {
      back = ((m->array)[r])[c];
    }
    }
  }
  return back;
}



/**	Create new matrix of unsigned int values.
	@param	rows	Number of rows.
	@param	columns	Number of columns.
	@return	Pointer to matrix on success, NULL on error.
*/
static
unsigned_matrix_t *
um_new DK_P2(unsigned, rows, unsigned, columns)
{
  unsigned_matrix_t *back = NULL;
  UNSIGNEDPTR *ptr;
  unsigned i;
  int ok;
  if(rows && columns) {
  back = dk_new(unsigned_matrix_t,1);
  if(back) {
    back->array = NULL; back->rows = rows;
    back->columns = columns;
    back->array = dk_new(UNSIGNEDPTR,rows);
    if(back->array) {
      ok = 1;
      ptr = back->array;
      for(i = 0; i < rows; i++) {
	*ptr = dk_new(unsigned,columns);
	if(!(*ptr)) ok = 0;
	ptr++;
      }
      if(ok) {
	um_reset(back);
      } else {
	um_delete(back);
	back = NULL;
      }
    } else {
      dk_delete(back);
      back = NULL;
    }
  }
  }
  return back;
}



/**	Pointer to state type.
*/
typedef au_state_t *STATEPTR;

/**	Pointer to input type.
*/
typedef au_input_t *INPUTPTR;

/**	Pointer to output type.
*/
typedef au_output_t *OUTPUTPTR;



/**	Put unsigned value to buffer.
	@param	b	Result buffer.
	@param	i	Number to print to buffer.
	@param	m	Maximum number (used to find the length).
*/
static
void
put_unsigned_to_buffer DK_P3(char *, b, unsigned, i, unsigned, m)
{
  size_t sz;
  char format[16];
  
  sprintf(b, "%u", m);
  sz = strlen(b);
  sprintf(format, "%%%uu", (unsigned)sz);
  
  sprintf(b, format, i);
  
}



/**	String: Space.
*/
static char str_space[] = { " " };



int
reduce_automata DK_P2(automata_t *, a, dk_app_t *, app)
{
  int back = 0;
  au_state_t *st, **states;
  au_input_t *in, **inputs;
  au_output_t *out, **outputs;
  au_state_transition_t *tr, *tr1, *tr2;
  unsigned passno;
  unsigned number_of_states;
  unsigned number_of_inputs;
  unsigned number_of_outputs;
  unsigned_matrix_t *um;
  half_bit_matrix_t *hbm;
  unsigned i, j, k, l, m;
  int found_a_change;
  char b1[16], b2[16], b3[16], *errmsgs[16], **allstrings;
  
  /* progress 10 : starting state reduction */
  allstrings = genau_progress();
  if(allstrings) {			
    errmsgs[0] = allstrings[10];	
    dkapp_log_msg(app, DK_LOG_LEVEL_PROGRESS, errmsgs, 1);
  } 
  if(a && app) {
    /*
      enumerate states, inputs, outputs
    */
    number_of_states = 0;
    number_of_inputs = 0;
    number_of_outputs = 0;
    dksto_it_reset(a->stit);
    while((st = (au_state_t *)dksto_it_next(a->stit)) != NULL) {
      st->rednum = number_of_states++;
    }
    dksto_it_reset(a->init);
    while((in = (au_input_t *)dksto_it_next(a->init)) != NULL) {
      in->rednum = number_of_inputs++;
    }
    dksto_it_reset(a->outit);
    while((out = (au_output_t *)dksto_it_next(a->outit)) != NULL) {
      out->rednum = number_of_outputs++;
    }
    if(number_of_states && number_of_inputs && number_of_outputs) {
      states = NULL; inputs = NULL; outputs = NULL;
      states = dk_new(STATEPTR,number_of_states);
      inputs = dk_new(INPUTPTR,number_of_inputs);
      outputs = dk_new(OUTPUTPTR,number_of_outputs);
      if(states && inputs && outputs) {
        dksto_it_reset(a->stit);
        while((st = (au_state_t *)dksto_it_next(a->stit)) != NULL) {
	  states[st->rednum] = st;
        }
        dksto_it_reset(a->init);
        while((in = (au_input_t *)dksto_it_next(a->init)) != NULL) {
	  inputs[in->rednum] = in;
        }
        dksto_it_reset(a->outit);
        while((out = (au_output_t *)dksto_it_next(a->outit)) != NULL) {
	  outputs[out->rednum] = out;
        }
	hbm = hbm_new(number_of_states);
	if(hbm) {
	  um = um_new(number_of_states,number_of_inputs);
	  if(um) {
	    back = 1;
	    /*
	      build output matrix
	    */
	    /* progress 11 : building output lookup table */
	    allstrings = genau_progress();
	    if(allstrings) {
	      errmsgs[0] = allstrings[11];
	      dkapp_log_msg(app, DK_LOG_LEVEL_PROGRESS, errmsgs, 1);
	    } 
	    for(i = 0; i < number_of_states; i++) {
	      st = states[i];
	      for(j = 0; j < number_of_inputs; j++) {
		
		in = inputs[j];
		tr = NULL;
		tr = dksto_it_find_like(st->trit, in->name, 2);
		if(!tr) {
		  tr1 = dksto_it_find_like(a->asttrit, in->name, 2);
		  tr2 = dksto_it_find_like(st->trit, "*", 2);
		  if(tr1) {
		    if(tr2) {
		      if((tr1->lineno) < (tr2->lineno)) {
			tr = tr1;
		      } else {
			tr = tr2;
		      }
		    } else {
		      tr = tr1;
		    }
		  } else {
		    if(tr2) {
		      tr = tr2;
		    }
		  }
		}
		if(!tr) {
		  tr = a->general_rule;
		}
		k = 0;
		if(a->def_output) { k = (a->def_output)->rednum; }
		if(tr) {
		  if(tr->output_data) {
		    k = (tr->output_data)->rednum;
		  }
		} 
		
		um_set(um,i,j,k);
	      }
	    }
	    /*
	      transfer output matrix to incompatibility matrix
	    */
	    /* progress 12 : processing output lookup table */
	    allstrings = genau_progress();
	    if(allstrings) {
	      errmsgs[0] = allstrings[12];
	      dkapp_log_msg(app, DK_LOG_LEVEL_PROGRESS, errmsgs, 1);
	    } 
	    for(i = 0; i < number_of_states; i++) {		/* first state */
	      for(j = 0; j < i; j++) {				/* second state */
		if(i != j) {
		  /* progress 13 : checking state compatibility */
		  allstrings = genau_progress();
		  if(allstrings) {
                    put_unsigned_to_buffer(b1, i, number_of_states);
		    put_unsigned_to_buffer(b2, j, number_of_states);
		    errmsgs[0] = allstrings[13];
		    errmsgs[1] = str_space;
		    errmsgs[2] = b1;
		    errmsgs[3] = str_space;
		    errmsgs[4] = b2;
		    dkapp_log_msg(app, DK_LOG_LEVEL_PROGRESS, errmsgs, 5);
		  } 
		  k = 0;
		  while(k < number_of_inputs) {			/* input */
		    l = um_get(um,i,k);
		    m = um_get(um,j,k);
		    
		    
		    if(l != m) {
                      hbm_set(hbm,i,j,1);
		      
		      
		      k = number_of_inputs;
		    } else {
		      k++;
		    }
		  }
		}
	      }
	    }
	    um_reset(um);
	    /*
	      build next state matrix
	    */
	    /* progress 14 : building next-state lookup table */
	    allstrings = genau_progress();
	    if(allstrings) {
	      errmsgs[0] = allstrings[14];
	      dkapp_log_msg(app, DK_LOG_LEVEL_PROGRESS, errmsgs, 1);
	    } 
	    for(i = 0; i < number_of_states; i++) {
	      st = states[i];
	      for(j = 0; j < number_of_inputs; j++) {
		
		in = inputs[j];
		tr = NULL;
		tr = dksto_it_find_like(st->trit, in->name, 2);
		if(!tr) {
		  tr1 = dksto_it_find_like(a->asttrit, in->name, 2);
		  tr2 = dksto_it_find_like(st->trit, "*", 2);
		  if(tr1) {
		    if(tr2) {
		      if((tr1->lineno) < (tr2->lineno)) {
			tr = tr1;
		      } else {
			tr = tr2;
		      }
		    } else {
		      tr = tr1;
		    }
		  } else {
		    if(tr2) {
		      tr = tr2;
		    }
		  }
		}
		if(!tr) {
		  tr = a->general_rule;
		}
		k = i;
		if(tr) { if(tr->next_data) { k = (tr->next_data)->rednum; } }
		
		
		um_set(um,i,j,k);
	      }
	    }
	    /*
	      expand incompatibility matrix using new state matrix
	    */
	    /* progress 15 : processing next-state lookup table */
	    allstrings = genau_progress();
	    if(allstrings) {
	      errmsgs[0] = allstrings[15];
	      dkapp_log_msg(app, DK_LOG_LEVEL_PROGRESS, errmsgs, 1);
	    } 
	    passno = 0;
	    do {
	      passno++;
	      
	      found_a_change = 0;
	      for(i = 0; i < number_of_states; i++) {
		for(j = 0; j < i; j++) {
		  if(i != j) {
		    if(!hbm_get(hbm,i,j)) {
		      allstrings = genau_progress();
		      if(allstrings) {
			put_unsigned_to_buffer(b1, passno, number_of_states);
			put_unsigned_to_buffer(b2, i, number_of_states);
			put_unsigned_to_buffer(b3, j, number_of_states);
			errmsgs[0] = allstrings[16];
			errmsgs[1] = str_space;
			errmsgs[2] = b1;
			errmsgs[3] = str_space;
			errmsgs[4] = allstrings[17];
			errmsgs[5] = str_space;
			errmsgs[6] = b2;
			errmsgs[7] = str_space;
			errmsgs[8] = b3;
			dkapp_log_msg(app, DK_LOG_LEVEL_PROGRESS, errmsgs, 9);
		      } 
		      
		      k = 0;
		      while(k < number_of_inputs) {
			l = um_get(um,i,k);
			m = um_get(um,j,k);
			
			
			if(hbm_get(hbm,l,m)) {
			  
			  k = number_of_inputs;
			  found_a_change = 1;
			  hbm_set(hbm,i,j,1);
			} else {
			  k++;
			}
		      }
		    }
		  }
		}
	      }
	    } while(found_a_change);
	    /*
	      group compatible states
	    */
	    /* progress 16 : grouping compatible states */
	    allstrings = genau_progress();
	    if(allstrings) {
	      errmsgs[0] = allstrings[19];
	      dkapp_log_msg(app, DK_LOG_LEVEL_PROGRESS, errmsgs, 1);
	    } 
	    if(a->initial_state) {
	      st = a->initial_state;
	      i  = st->rednum;
	      for(j = 0; j < number_of_states; j++) {
		if(i != j) {
		  if(!hbm_get(hbm,i,j)) {
		    states[j]->compat = st;
		  }
		}
	      }
	    }
	    for(i = 0; i < number_of_states; i++) {
	      st = states[i];
	      if(!(st->compat)) {
#ifdef FIRST_VERSION
		for(j = 0; j < i; j++)
#else
		for(j = (i + 1); j < number_of_states; j++)
#endif
		{
		  if(i != j) {
		    if(!(states[j])->compat) {
#ifdef FIRST_VERSION
		      if(!hbm_get(hbm,i,j))
#else
		      if(!hbm_get(hbm,j,i))
#endif
		      {
			(states[j])->compat = st;
		      }
		    }
		  }
		}
	      }
	    }
	    /* progress 17 : state reduction finished */
	    allstrings = genau_progress();
	    if(allstrings) {
	      errmsgs[0] = allstrings[18];
	      dkapp_log_msg(app, DK_LOG_LEVEL_PROGRESS, errmsgs, 1);
	    } 
	    um_delete(um);
	  }
	  hbm_delete(hbm);
	}
      }
      if(outputs) { dk_delete(outputs); }
      if(inputs)  { dk_delete(inputs); }
      if(states)  { dk_delete(states); }
    }
  } 
  return back;
}