/**CFile***********************************************************************

  FileName    [ltlTableau.c]

  PackageName [ltl]

  Synopsis    [Expand the LTL Formula by applying the Tableau Rules.]

  Author      [Chao Wang<chao.wang@colorado.EDU>]

  Copyright   [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

******************************************************************************/

#include "ltlInt.h"

static char rcsid[] UNUSED = "$Id: ltlTableau.c,v 1.15 2008/04/22 21:22:33 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static void TableauClearMarks(LtlTableau_t *tableau);
static int TableauRules(LtlTableau_t *tableau, Ctlsp_Formula_t *F);
static void HashNextFormulae(LtlTableau_t *tableau, Ctlsp_Formula_t *F);
static void TableauLoadUntilSubFormulae(LtlTableau_t *tableau, Ctlsp_Formula_t *F);

/**AutomaticEnd***************************************************************/

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Generate the 'Tableau' sturcture for the LTL->AUT problem.
  It first computes the NNF of the input formula, then create the alpha/beta
  entry table for both the input formula and its negation according the
  tableau rules, and finally compute the list of 'Until formulae'.]

  SideEffects []

  SeeAlso     [LtlTableauGenerateRules]

******************************************************************************/
LtlTableau_t *
LtlTableauGenerateTableau(
  Ctlsp_Formula_t *formula)
{
  Ctlsp_Formula_t *F, *notF, *tmpF;
  LtlTableau_t   *tableau;
  int save_n;
  int i, j;

  /* compute the NNF of (formula) and (its negation) */
  F = Ctlsp_LtlFormulaNegationNormalForm(formula);
  tmpF = Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula, NIL(Ctlsp_Formula_t));
  notF = Ctlsp_LtlFormulaNegationNormalForm(tmpF);
  FREE(tmpF);

  /* Create the 'tableau' for this LTL->AUT problem */
  tableau = LtlTableauCreate();
  
  /* Hash F & notF into the unique table */
  F = Ctlsp_LtlFormulaHashIntoUniqueTable(F,tableau->formulaUniqueTable);
  notF = Ctlsp_LtlFormulaHashIntoUniqueTable(notF,tableau->formulaUniqueTable);
  tableau->F = F;
  tableau->notF = notF;

  /* tricky part:: for each U-formula/R-formula 'F', also hash 'XF' */
  TableauClearMarks(tableau);
  HashNextFormulae(tableau, F);
  
  /* Build the Alpha/Beta entry table */
  tableau->abIndex = st_count(tableau->formulaUniqueTable);
  tableau->abTable = ALLOC(LtlTableauEntry_t, tableau->abIndex);
  tableau->labelTable = ALLOC(Ctlsp_Formula_t *, tableau->abIndex);

  save_n = tableau->abIndex;
  tableau->abIndex = 0;
  TableauClearMarks(tableau);
  TableauRules(tableau,F);      /* build the Alpha-Beta table */
  TableauRules(tableau, notF);
  tableau->abIndex = save_n;

  /* compute the negation field (.notF) for each Alpha-Beta entry */
  for (i=0; i<tableau->abIndex; i++) {
    if (!tableau->abTable[i].notF) {
      Ctlsp_Formula_t *thisF = Ctlsp_FormulaCreate(Ctlsp_NOT_c,
						   tableau->abTable[i].F,
						   NIL(Ctlsp_Formula_t));
      Ctlsp_Formula_t *nnfF = Ctlsp_LtlFormulaNegationNormalForm(thisF);
      FREE(thisF);
						       
      tableau->abTable[i].notF = 
	Ctlsp_LtlFormulaHashIntoUniqueTable(nnfF, tableau->formulaUniqueTable);
      for (j=0; j<tableau->abIndex; j++) {
	if (tableau->abTable[j].F == tableau->abTable[i].notF) {
	  tableau->abTable[i].notF_idx = j;
	  tableau->abTable[j].notF_idx = i;
	  tableau->abTable[j].notF = tableau->abTable[i].F;
	  break;
	}
      }
      assert(j < tableau->abIndex);
    }
    array_insert(int, tableau->abTableNegate, i, tableau->abTable[i].notF_idx);
  }

  /* put all constant formulae (labels) into tableau->labelTable
   * includes: ID/NOT(ID) */
  j = 0;
  for (i=0; i<tableau->abIndex; i++) {
    Ctlsp_Formula_t *holdF = tableau->abTable[i].F;
    if (Ctlsp_LtlFormulaIsPropositional(holdF) &&
	Ctlsp_FormulaReadType(holdF) != Ctlsp_TRUE_c &&
	Ctlsp_FormulaReadType(holdF) != Ctlsp_FALSE_c) {
      tableau->labelTable[j] = tableau->abTable[i].F;
      Ctlsp_FormulaSetLabelIndex(tableau->abTable[i].F, j);
      j++;
    }
  }
  tableau->labelIndex = j;
  
  /* Create the Negate Method for abTable and labelTable */
  for (i=0; i<tableau->abIndex; i++) {
    array_insert(int, tableau->abTableNegate, i,
		 Ctlsp_FormulaReadABIndex(tableau->abTable[i].notF));
  }
  for (i=0; i<tableau->labelIndex; i++) {
    int idx = Ctlsp_FormulaReadABIndex(tableau->labelTable[i]);
    array_insert(int, tableau->labelTableNegate, i,
		 Ctlsp_FormulaReadLabelIndex(tableau->abTable[idx].notF));
  }
  
  /* put all the 'until sub-formulae' into tableau->untilUniqueTable */
  TableauClearMarks(tableau);
  TableauLoadUntilSubFormulae(tableau, F);
  
  return tableau;
}


/**Function********************************************************************

  Synopsis    [Allocate the data structure of tableau.]

  Description []
  
  SideEffects []

******************************************************************************/
LtlTableau_t *
LtlTableauCreate(
  void)
{
  LtlTableau_t *tableau = ALLOC(LtlTableau_t, 1);
  memset(tableau, 0, sizeof(LtlTableau_t));

  tableau->F = tableau->notF = NIL(Ctlsp_Formula_t);
  tableau->abIndex = 0;
  tableau->abTable = 0;
  tableau->abTableNegate = array_alloc(int, 0);
  tableau->labelTable = 0;
  tableau->labelTableNegate = array_alloc(int, 0);
  /* create empty hash tables */
  tableau->formulaUniqueTable = Ctlsp_LtlFormulaCreateUniqueTable();
  tableau->untilUniqueTable = Ctlsp_LtlFormulaCreateUniqueTable();
  
  return tableau;
} 


/**Function********************************************************************

  Synopsis    [Free the tableau data structure.]

  SideEffects []

  SeeAlso     [LtlTableauGenerateTableau]

******************************************************************************/
void
LtlTableauFree(
  LtlTableau_t *tableau)
{
  int i;
  char *tmpstr;
  
  /* free all the LTL formulae */
  for (i=0; i<tableau->abIndex; i++) {
    if (Ctlsp_FormulaReadType(tableau->abTable[i].F) == Ctlsp_ID_c) {
      tmpstr = Ctlsp_FormulaReadVariableName(tableau->abTable[i].F);
      FREE(tmpstr);
      tmpstr = Ctlsp_FormulaReadValueName(tableau->abTable[i].F);
      FREE(tmpstr);
    }
    FREE(tableau->abTable[i].F);
  }

  FREE(tableau->abTable);
  FREE(tableau->labelTable);
  array_free(tableau->abTableNegate);
  array_free(tableau->labelTableNegate);
  
  st_free_table(tableau->formulaUniqueTable);
  st_free_table(tableau->untilUniqueTable);

  FREE(tableau);
}


/**Function********************************************************************

  Synopsis    [Print the content of the tableau.]

  SideEffects []

  SeeAlso     [LtlTableauGenerateTableau]

******************************************************************************/
void 
LtlTableauPrint(
  FILE *fp,
  LtlTableau_t *tableau)
{
  int i;

  (void) fprintf(fp, "Tableau Rules for {");
  Ctlsp_FormulaPrint(fp,tableau->F);
  (void) fprintf(fp, "} : # of sub-formulae = %d\n", tableau->abIndex);
    
  for (i=0; i<tableau->abIndex; i++) {
    fprintf(fp, "%d   [", i);
    Ctlsp_FormulaPrint(fp, tableau->abTable[i].F);
    fprintf(fp, "]\n\t");
    fprintf(fp, "(%3d * %3d * X%3d) + (%3d * %3d * X%3d) -- notF= %3d\n",
	    tableau->abTable[i].A[0].B[0],
	    tableau->abTable[i].A[0].B[1],
	    tableau->abTable[i].A[0].n,
	    tableau->abTable[i].A[1].B[0],
	    tableau->abTable[i].A[1].B[1],
	    tableau->abTable[i].A[1].n,
	    tableau->abTable[i].notF_idx);
  }
}


/**Function********************************************************************

  Synopsis    [Return the unique formula 'X F' in the tableu by giving 'F'.]

  Description [If there does not exist, create and hash it into the unique
  table.]
  
  SideEffects []

******************************************************************************/
Ctlsp_Formula_t *
LtlTableauGetUniqueXFormula(
  LtlTableau_t *tableau,
  Ctlsp_Formula_t *F)
{
  Ctlsp_Formula_t *tmpF, *XF;
  
  tmpF = Ctlsp_FormulaCreate(Ctlsp_X_c, F, NIL(Ctlsp_Formula_t));
  XF = Ctlsp_LtlFormulaNegationNormalForm(tmpF);
  FREE(tmpF);
  XF = Ctlsp_LtlFormulaHashIntoUniqueTable(XF,tableau->formulaUniqueTable);

  return XF;
}


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Clear the marks of all the formula in the tableau.]

  Description []
  
  SideEffects []

******************************************************************************/
static void
TableauClearMarks(
  LtlTableau_t *tableau)
{
  st_table *tbl = tableau->formulaUniqueTable;
  st_generator *stgen;
  Ctlsp_Formula_t *F;

  st_foreach_item(tbl, stgen, &F, NIL(char *)) {
    Ctlsp_FormulaResetMarked(F);
  }
}


/**Function********************************************************************

  Synopsis    [Fill out the Alpha-Beta entry table recursively.]

  Description [1) assign each formula F an index and an entry;
  2) build for each formula F a expansion  ( {A0B0 ^ A0B1} + {A1B0 ^ A1B1} )]
  
  SideEffects []

******************************************************************************/
static int
TableauRules(
  LtlTableau_t *tableau,
  Ctlsp_Formula_t *F)
{
  int index;
  int A0B0=-1, A0B1=-1, A0n=-1;
  int A1B0=-1, A1B1=-1, A1n=-1;
  Ctlsp_Formula_t *XF;
  Ctlsp_Formula_t *F_left, *F_right;
  Ctlsp_FormulaType F_type;
  
  assert( F );
  
  if (Ctlsp_FormulaReadMarked(F))
    return Ctlsp_FormulaReadABIndex(F);

  Ctlsp_FormulaSetMarked(F);
  index = tableau->abIndex++;
  Ctlsp_FormulaSetABIndex(F, index);

  F_type = Ctlsp_FormulaReadType(F);
  F_left = Ctlsp_FormulaReadLeftChild(F);
  F_right = Ctlsp_FormulaReadRightChild(F);
  
  switch(F_type) {
  case Ctlsp_X_c:
    TableauRules(tableau, F_left); 
    A0n = index;
    break;
  case Ctlsp_OR_c:
    A0B0 = TableauRules(tableau, F_left);
    A1B0 = TableauRules(tableau, F_right);
    break;
  case Ctlsp_AND_c:
    A0B0 = TableauRules(tableau, F_left);
    A0B1 = TableauRules(tableau, F_right);
    break;
  case Ctlsp_U_c:
    A0B0 = TableauRules(tableau, F_left);
    A1B0 = TableauRules(tableau, F_right);
    XF = LtlTableauGetUniqueXFormula(tableau, F);
    A0n = TableauRules(tableau, XF);
    break;
  case Ctlsp_R_c:
    A0B0 = TableauRules(tableau, F_right);
    A1B0 = TableauRules(tableau, F_right);
    A1B1 = TableauRules(tableau, F_left);
    XF = LtlTableauGetUniqueXFormula(tableau, F);
    A0n = TableauRules(tableau, XF);
    break;
  default:
    break;
  }
  
  tableau->abTable[index].F = F;
  tableau->abTable[index].A[0].B[0] = A0B0;
  tableau->abTable[index].A[0].B[1] = A0B1;
  tableau->abTable[index].A[1].B[0] = A1B0;
  tableau->abTable[index].A[1].B[1] = A1B1;
  tableau->abTable[index].A[0].n = A0n;
  tableau->abTable[index].A[1].n = A1n;
  
  tableau->abTable[index].notF_idx = -1;
  tableau->abTable[index].notF = NIL(Ctlsp_Formula_t);

  return index;
}

/**Function********************************************************************

  Synopsis    [Hash the formula 'X F' and its negation in the unique tableau.]

  Description [Construct the 'X F' from the given 'F', and hash it.]
  
  SideEffects []

******************************************************************************/
static void
HashNextFormulae(
  LtlTableau_t *tableau,
  Ctlsp_Formula_t *F)
{
  Ctlsp_Formula_t *XF, *NXF, *tmpF;
  Ctlsp_FormulaType F_type = Ctlsp_FormulaReadType(F);
  Ctlsp_Formula_t *F_left = Ctlsp_FormulaReadLeftChild(F);
  Ctlsp_Formula_t *F_right = Ctlsp_FormulaReadRightChild(F);
  
  switch( F_type ) {
  case Ctlsp_X_c:
    HashNextFormulae(tableau, F_left);
    break;
  case Ctlsp_OR_c:
  case Ctlsp_AND_c:
    HashNextFormulae(tableau, F_left);
    HashNextFormulae(tableau, F_right);
    break;
  case Ctlsp_U_c:
  case Ctlsp_R_c:
    HashNextFormulae(tableau, F_left);
    HashNextFormulae(tableau, F_right);
    XF = LtlTableauGetUniqueXFormula(tableau, F);      
    tmpF = Ctlsp_FormulaCreate(Ctlsp_NOT_c, XF, NIL(Ctlsp_Formula_t));
    NXF = Ctlsp_LtlFormulaNegationNormalForm(tmpF);
    FREE(tmpF);
    Ctlsp_LtlFormulaHashIntoUniqueTable(NXF,tableau->formulaUniqueTable);
    break;
  default:
    break;
  }
}

/**Function********************************************************************

  Synopsis    [Put all the Until sub-formulae in a list.]

  Description []
  
  SideEffects []

******************************************************************************/
static void
TableauLoadUntilSubFormulae(
  LtlTableau_t *tableau,
  Ctlsp_Formula_t *F)
{
  char *list;
  st_table *uniqueTable = tableau->untilUniqueTable;
  Ctlsp_FormulaType F_type;
  
  if (!F)
    return;

  if (Ctlsp_FormulaReadMarked(F))
    return;

  
  Ctlsp_FormulaSetMarked(F);
  F_type = Ctlsp_FormulaReadType(F);
  if (F_type == Ctlsp_U_c) {
    if(!st_is_member(uniqueTable,  F)) {
      list = (char *) lsCreate();
      st_insert(uniqueTable,  F, list);
    }
    Ctlsp_FormulaSetRhs(Ctlsp_FormulaReadRightChild(F));
  }
  if (F_type != Ctlsp_ID_c) {
    TableauLoadUntilSubFormulae(tableau, Ctlsp_FormulaReadLeftChild(F));
    TableauLoadUntilSubFormulae(tableau, Ctlsp_FormulaReadRightChild(F));
  }
}