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

  FileName    [ltlAutomaton.c]

  PackageName [ltl]

  Synopsis    [Translate LTL formula to the Buechi Automaton.]

  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: ltlAutomaton.c,v 1.34 2005/04/28 08:47:15 bli Exp $";

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

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

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

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

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

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

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

static int HasToBeStored(LtlTableau_t *tableau, int index);
static int Contradiction(LtlTableau_t *tableau, int index, LtlSet_t *ToCover, LtlSet_t *Current, LtlSet_t *Covered);
static int Redundant(LtlTableau_t *tableau, int index, LtlSet_t *ToCover, LtlSet_t *Current, LtlSet_t *Covered);
static int SI(LtlTableau_t *tableau, int index, LtlSet_t *A);
static void AutomatonComputeFair(LtlTableau_t *tableau, LtlSet_t *r, vertex_t *vtx1);
static int AutomatonCreateFairList(LtlTableau_t *tableau, Ltl_Automaton_t *aut);
static void AutomatonAssignNext(LtlTableau_t *tableau, LtlSet_t * toCover, LtlSet_t * s);
static LtlSet_t * AutomatonSetCreate(LtlTableau_t *tableau, Ctlsp_Formula_t *F);
static lsList AutomatonBuildCover(LtlTableau_t *tableau, LtlSet_t *ToCover);
static void AutomatonBuildCover_Aux(LtlTableau_t *tableau, LtlSet_t *pToCover, LtlSet_t *pCurrent, LtlSet_t *pCovered, lsList Cover);

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

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

  Synopsis    [Allocate the automaton data structure.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ltl_Automaton_t *
Ltl_AutomatonCreate(void)
{
  Ltl_Automaton_t *aut = ALLOC(Ltl_Automaton_t, 1);  
  (void)memset((void *)aut, 0, sizeof(Ltl_Automaton_t));
  
  aut->name = 0;
  aut->SCC = (st_table *)0;
  aut->G = g_alloc();
  /* table of the initial states */
  aut->Init = st_init_table(st_ptrcmp, st_ptrhash);  
  /* these states can be either in or outside the "FairSet" */
  aut->dontcare = st_init_table(st_ptrcmp, st_ptrhash); 
  /* list of FairSets (each FairSet is a table of states) */
  aut->Fair = lsCreate();  
  aut->node_idx = 1;
  
  return aut;
}

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

  Synopsis    [Free the automaton data structure.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Ltl_AutomatonFree(gGeneric g)
{
  st_table *tbl;
  st_generator *stgen;
  int i, n;
  Ltl_Automaton_t *aut = (Ltl_Automaton_t *) g;

  if (aut->name)  FREE(aut->name);

  g_free(aut->G, (void (*)(gGeneric))0, Ltl_AutomatonNodeFree,
	 (void (*)(gGeneric))0);

  st_free_table(aut->Init);
  st_free_table(aut->dontcare);
  
  while (lsDelBegin(aut->Fair, &tbl) != LS_NOMORE) {
      st_free_table(tbl);
  }
  lsDestroy(aut->Fair, (void (*)(lsGeneric)) NULL);

  if (aut->labelTable) {
      n = array_n(aut->labelTable);
      for (i=0; i<n; i++) 
          Ctlsp_FormulaFree(array_fetch(Ctlsp_Formula_t *, 
                                        aut->labelTable, i));
      array_free(aut->labelTable);
      array_free(aut->labelTableNegate);
  }

  /* free the partition/quotient */
  if (aut->SCC) {
    /* for a Buechi automaton, this is a st_table of st_table of vertices;
     * otherwise, this is a st_table of vertices */
    if (aut->isQuotientGraph == 0) {
      st_foreach_item(aut->SCC, stgen, &tbl, NIL(char *)) {
	st_free_table(tbl);
      }
    }
    st_free_table(aut->SCC);
  }

  if (aut->Q)
      Ltl_AutomatonFree((gGeneric) aut->Q);

  FREE(aut);
}
	
/**Function********************************************************************

  Synopsis    [Allocate the automaton node data structure.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ltl_AutomatonNode_t *
Ltl_AutomatonNodeCreate(Ltl_Automaton_t *aut)
{
  Ltl_AutomatonNode_t *node = ALLOC(Ltl_AutomatonNode_t, 1);
  (void)memset((void *)node, 0, sizeof(Ltl_AutomatonNode_t));

  node->index = aut->node_idx++;
  node->Labels = NIL(LtlSet_t);
  node->CoverSet = NIL(LtlSet_t);
  node->Class = (st_table *)0;        /* used in Quotient graph */
      
  return node;
}

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

  Synopsis    [Free the automaton node data structure.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Ltl_AutomatonNodeFree(gGeneric g)
{
  Ltl_AutomatonNode_t *node = (Ltl_AutomatonNode_t *) g;
  if (node->Labels)
    LtlSetFree(node->Labels);
  if (node->CoverSet)
    LtlSetFree(node->CoverSet);
  /*  if (node->Class)
        st_free_table(node->Class);*/
  
  FREE(node);
}

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

  Synopsis    [Print the automaton node.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Ltl_AutomatonNodePrint(
  Ltl_Automaton_t *aut,
  Ltl_AutomatonNode_t *node)
{
  st_generator *stgen;
  vertex_t *vtx;
  Ltl_AutomatonNode_t *state;
  Ctlsp_Formula_t *F;
  int first, i, n;
  
  /* index (required) */
  fprintf(vis_stdout, "n%d: ", node->index);
  
  /* 1. cover (set of formulae) ? */
  if (aut->tableau && node->CoverSet) 
    LtlSetPrint(aut->tableau, node->CoverSet);
  
  /* 2. label ? */
  if (node->Labels) {
    fprintf(vis_stdout, " label: {");
    first = 1; n = array_n(aut->labelTable);
    for (i=0; i<n; i++) {
      if (LtlSetGetElt(node->Labels, i)) {
	if (!first)	  fprintf(vis_stdout, ",");
	else       	  first = 0;
	F = array_fetch(Ctlsp_Formula_t *, aut->labelTable, i);
	Ctlsp_FormulaPrint(vis_stdout, F);
      }
    }
    fprintf(vis_stdout, "}");
  }

  /* 3. Class ? (for quotient graph node) */
  if (node->Class) {
    fprintf(vis_stdout, "scc{");
    st_foreach_item(node->Class, stgen, &vtx, NIL(char *)) {
      state = (Ltl_AutomatonNode_t *)vtx->user_data;
      fprintf(vis_stdout, "n%d ", state->index);
    }
    fprintf(vis_stdout, "}");
  }
  
  fprintf(vis_stdout, "\n");
}

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

  Synopsis    [Print the automaton.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Ltl_AutomatonPrint(
  Ltl_Automaton_t *aut,
  int verbosity)
{
  edge_t   *edge;
  vertex_t *vtx1, *vtx2;           
  Ltl_AutomatonNode_t *node, *node2;
  lsGen     gen;
  lsGeneric data;

  st_table  *tbl;
  st_generator *stgen;

  int n_states = 0;
  int n_trans = 0;
  int n_fairsets = 0;
  int n_init = 0;
  int strength;
  
  /* name ? */
  if (verbosity)
    fprintf(vis_stdout, "Automaton:\n");

  if (verbosity > 1) {
    fprintf(vis_stdout, "-----------------------------------------------\n");
    if (aut->name)
      fprintf(vis_stdout, "Name: %s \n", aut->name);
    fprintf(vis_stdout, "-----------------------------------------------\n");
    
    /* negation normal form ?*/
    if(aut->tableau)
      Ctlsp_FormulaPrint(vis_stdout, aut->tableau->F);
    
    /* States & Labels */
    fprintf(vis_stdout, "\nStates: \n");
    foreach_vertex( aut->G, gen, vtx1) {
      node = (Ltl_AutomatonNode_t *) vtx1->user_data;
      Ltl_AutomatonNodePrint(aut, node);
    }
    
    /* Init States ? */
    fprintf(vis_stdout, "Arcs: \n");  
    st_foreach_item(aut->Init, stgen,  &vtx1, NIL(char *)) {
      node = (Ltl_AutomatonNode_t *) vtx1->user_data;
      fprintf(vis_stdout, "-> n%d\n", node->index);
    }
    
    /* Edges */
    foreach_edge(aut->G, gen, edge) {
      vtx1 = g_e_source(edge);
      vtx2 = g_e_dest(edge);
      node = (Ltl_AutomatonNode_t *) vtx1->user_data;
      node2 = (Ltl_AutomatonNode_t *) vtx2->user_data;
	  
      if (node)
	fprintf(vis_stdout, "   n%d -> ", node->index);
      if (node2)
	fprintf(vis_stdout, "n%d\n", node2->index);
    }

    /* Sets of Fair Sets */
    fprintf(vis_stdout, "Fair Sets: \n");  
    lsForEachItem (aut->Fair, gen, data) {
      tbl = (st_table *) data;
      fprintf(vis_stdout, "{ ");
      st_foreach_item(tbl, stgen,  &vtx1, NIL(char *)) {
	node = (Ltl_AutomatonNode_t *) vtx1->user_data;
	fprintf(vis_stdout, "n%d ", node->index);
      }
      fprintf(vis_stdout, " }\n");
    }
    
#ifdef DEBUG_LTLMC      
    /* Dontcare states */
    fprintf(vis_stdout, "Dontcare States: \n{");
    if (aut->dontcare) {
      st_foreach_item(aut->dontcare, stgen, &vtx1, NIL(char *)) {
	node = (Ltl_AutomatonNode_t *) vtx1->user_data;
	fprintf(vis_stdout, "n%d ", node->index);
      }
    }
    fprintf(vis_stdout, " }\n");
#endif
  
    fprintf(vis_stdout, "End\n");
  }
  
  /* Get the strength (2, 1, 0) */
  n_states = lsLength(g_get_vertices(aut->G));
  n_init = st_count(aut->Init);
  n_trans = lsLength(g_get_edges(aut->G));
  n_fairsets = lsLength(aut->Fair);
  strength = Ltl_AutomatonGetStrength(aut);

  if (verbosity) 
    fprintf(vis_stdout, "Stats: %d states, %d trans, %d fair sets, %d init states, %s\n", n_states, n_trans, n_fairsets, n_init, (strength==2)? "strong":((strength==1)?"weak":"terminal") );

}


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

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

  Synopsis    [Generate the Buechi automaton from the formula.]

  Description [Before calling this function, 'tableau' should contains:
   1) LTL Formula (NNF) and its negation in a DAG (or UniqueTable)
   2) alpha-beta Table (tableau-rule expansion of each sub-formulae )
   3) Until formulae list.]

  SideEffects [The returned automaton should be freed by the caller.]

  SeeAlso     []

******************************************************************************/
Ltl_Automaton_t *
LtlAutomatonGeneration(
  LtlTableau_t *tableau)
{
  LtlSet_t *toCover, *s, *r, *rprime; /* terms (set) */
  lsList Cover;                       /* current list of terms (cover) */
  lsList U = lsCreate();              /* a list of terms <to be processed>*/
  lsList Q = lsCreate();              /* unique table for terms <processed> */
  st_table  *Set2Vtx = st_init_table(st_ptrcmp, st_ptrhash);
  vertex_t *vtx1, *vtx2;              /* vertex in graph, related to node */
  Ltl_Automaton_t *A = Ltl_AutomatonCreate();
  Ltl_AutomatonNode_t *node;
  Ctlsp_Formula_t *F;
  int i;

  A->tableau = tableau;
  
  /* Compute Cover( {F} ), the init states, and U */
  toCover = AutomatonSetCreate(tableau, tableau->F); 
  Cover = AutomatonBuildCover(tableau, toCover);     
  while (lsDelBegin(Cover, &r) != LS_NOMORE) {
#ifdef DEBUG_LTLMC
    if (tableau->verbosity >=2) {
      fprintf(vis_stdout, "**** term: ");
      LtlSetPrintIndex(tableau->abIndex, r);
      fprintf(vis_stdout, "**** n%d added! \n", A->node_idx);
    }
#endif
    lsNewEnd(U, (lsGeneric) r, (lsHandle *) 0);
    lsNewEnd(Q, (lsGeneric) r, (lsHandle *) 0);
    /* Build the initial states of the Buechi automaton 
     * add a new node in G
     */
    node = Ltl_AutomatonNodeCreate(A);
    node->Labels = LtlSetToLabelSet(tableau, r);
    node->CoverSet = LtlSetCopy(r); 
    vtx1 = g_add_vertex(A->G);
    vtx1->user_data = (gGeneric) node;
    /* add into A->Init */
    st_insert(A->Init, vtx1,  vtx1);
    /* put this node to proper Fair sets */
    AutomatonComputeFair(tableau, r, vtx1);
    /* add into the (Set, Vtx) unique table */
    st_insert(Set2Vtx, r,  vtx1);
  }
  lsDestroy(Cover, (void (*)(lsGeneric))0);

  /* Each time, remove one set 's' from the to-be-processed list 'U' */
  while (lsDelBegin(U, &s) == LS_OK) {
    /* Put all the next (state) formulae into toCover */
    AutomatonAssignNext(tableau, toCover, s);
#ifdef DEBUG_LTLMC
    if (tableau->verbosity >= 2) {
      fprintf(vis_stdout, "\n** AssignNext Of:");
      LtlSetPrintIndex(tableau->abIndex, s);
      fprintf(vis_stdout, "** ==>           ");
      LtlSetPrintIndex(tableau->abIndex, toCover);
    }
#endif
    /* Build the cover for next state */
    Cover = AutomatonBuildCover(tableau, toCover);
    while (lsDelBegin(Cover, &r) == LS_OK) {
      /* Get the existing identical copy of r from Q (if exist) */
      rprime = LtlSetIsInList(r, Q);
#ifdef DEBUG_LTLMC	  
      if (tableau->verbosity >=2 ) {
	fprintf(vis_stdout, "** term: ");
	LtlSetPrintIndex(tableau->abIndex, r);
      }
#endif
      /* If the next state exists, simply add the new edge; Otherwise,
	 create the next state, and add the new edge */
      if (rprime) {
	/* both s and r' are already in G */
	st_lookup(Set2Vtx,  rprime,  &vtx1);
	assert(vtx1 != NIL(vertex_t));
	st_lookup(Set2Vtx, s,  &vtx2); 
	assert(vtx2 != NIL(vertex_t));
	/* add edge(s, r') */
	g_add_edge(vtx2, vtx1);	      
	LtlSetFree(r);
      }else {
#ifdef DEBUG_LTLMC	      
	if (tableau->verbosity >=2 ) {
	  fprintf(vis_stdout, "** n%d added!\n", A->node_idx);
	}
#endif
	/* add a new state in G */
	node = Ltl_AutomatonNodeCreate(A);
	node->Labels = LtlSetToLabelSet(tableau, r);
	node->CoverSet = LtlSetCopy(r); 
	vtx1 = g_add_vertex(A->G);  
	vtx1->user_data = (gGeneric) node;
	/* add edge(s, r) */
	st_lookup(Set2Vtx,  s,  &vtx2);
	assert(vtx2 != NIL(vertex_t));     
	g_add_edge(vtx2, vtx1); 
	/* put the new state to the proper Fair Sets */
	AutomatonComputeFair(tableau, r, vtx1);
	/* add r in the (Set, Vtx) unique table */
	st_insert(Set2Vtx,  r,  vtx1);	      
	lsNewEnd(Q, (lsGeneric) r, (lsHandle *) 0);
	lsNewEnd(U, (lsGeneric) r, (lsHandle *) 0);
      }
    }
      
    lsDestroy(Cover, (void (*)(lsGeneric))0);
  }

  /* Convert fair sets of the tableau into fair sets of the automaton:
   * if there is an empty fairset, create an empty automaton and return;
   * otherwise, keep going ...
   */
  if (AutomatonCreateFairList(tableau, A) == 0) {
    st_table *tbl;
    while (lsDelBegin(A->Fair, &tbl) != LS_NOMORE) {
      st_free_table(tbl);
    }
    g_free(A->G, (void (*)(gGeneric))0, Ltl_AutomatonNodeFree,
	   (void (*)(gGeneric))0);
    A->G = g_alloc();
    st_free_table(A->Init);
    A->Init = st_init_table(st_ptrcmp, st_ptrhash);
  }

  /* Copy the lable table of the tableau into the automaton 
   * Note that the new one shares nothing with the one in the tableau 
   */
  A->labelTable = array_alloc(Ctlsp_Formula_t *, tableau->labelIndex);
  for (i=0; i<tableau->labelIndex; i++) {
    F = Ctlsp_LtlFormulaNegationNormalForm(tableau->labelTable[i]);
    array_insert(Ctlsp_Formula_t *, A->labelTable, i, F);
  }
  A->labelTableNegate = array_dup(tableau->labelTableNegate);
  
  /* Free all the sets in the list 
   * toCover/U  should be empty sets, while Q contains all the processed set 
   */
  LtlSetFree(toCover);         
  lsDestroy(U, (void (*)(lsGeneric)) 0);    
  lsDestroy(Q, (void (*)(lsGeneric))LtlSetFree);    
  st_free_table(Set2Vtx);

#ifdef DEBUG_LTLMC  
  /* sanity check */
  g_check(A->G);
#endif
  
  return A;
}


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

  Synopsis    [Return 1 if the given set belongs to a fair set.]

  Description [It is used in Boolean minimization. It might prevent
  over-simplification.]

  SideEffects []

******************************************************************************/
int 
LtlAutomatonSetIsFair(
  LtlTableau_t *tableau,
  LtlSet_t *r)
{
#if 0
  st_table *uniqueTable = tableau->untilUniqueTable;
  char *key, *value;
  st_generator *gen;
  int flag = 0;
#endif

  /* this is the same as "Wring" */
  return 0;  

#if 0  
  st_foreach_item(uniqueTable, gen, &key, &value) {
    Ctlsp_Formula_t *F = (Ctlsp_Formula_t *) key;
    Ctlsp_Formula_t *right = Ctlsp_FormulaReadRightChild(F);
    int F_ab_idx = Ctlsp_FormulaReadABIndex(F);
    int right_ab_idx = Ctlsp_FormulaReadABIndex(right);
      
    if ( SI(tableau, right_ab_idx, r) ||
	 !(SI(tableau, F_ab_idx, r)) ) {
      /* set 'r' belongs to one fair set */
      flag = 1;
      st_free_gen(gen);
      break;
    }
  }
  return flag;
#endif
}


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

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

  Synopsis    [Return 1 iff the elementary formula need to be stored.]

  Description [The formula is represented by its index in the abTable]

  SideEffects []

******************************************************************************/
static int
HasToBeStored(
  LtlTableau_t *tableau,
  int index)
{
  int result = 1;
  Ctlsp_Formula_t *F;
  Ctlsp_FormulaType F_type;
  
  F = tableau->abTable[index].F;
  
  switch(tableau->algorithm) {
  case Ltl2Aut_GPVW_c:
    result = 1;
    break;
  case Ltl2Aut_GPVWplus_c:
    /* T iff 'u' is an until formula or 'u' is the right hand of an until */
    F_type = Ctlsp_FormulaReadType(F);
    result = (F_type == Ctlsp_U_c || Ctlsp_FormulaReadRhs(F) == 1);
    break;
  case Ltl2Aut_LTL2AUT_c:  
  case Ltl2Aut_WRING_c:   
    result = 0;
    break;
  }
#ifdef DEBUG_LTLMC
  if (tableau->verbosity >2)
    fprintf(vis_stdout, "...HasToBeStored=%d\n", result);
#endif
  
  return result;
}

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

  Synopsis    [Return 1 iff there is there is a contradition so far.]

  Description [The formula is represented by its index in the abTable]

  SideEffects []

******************************************************************************/
static int
Contradiction(
  LtlTableau_t *tableau,
  int index,
  LtlSet_t *ToCover,
  LtlSet_t *Current,
  LtlSet_t *Covered)
{
  int result = 0;
  Ctlsp_Formula_t *F, *notF;
  LtlSet_t *UC;
  int notF_ab_idx;
  Ctlsp_FormulaType F_type;
  
  F = tableau->abTable[index].F;
  F_type = Ctlsp_FormulaReadType(F);
  notF = tableau->abTable[index].notF;
  notF_ab_idx = Ctlsp_FormulaReadABIndex(notF);

  
  switch(tableau->algorithm) {
  case Ltl2Aut_GPVW_c:
    /* if 'u' is False, or (!u) exists in Current */
    result = ( F_type == Ctlsp_FALSE_c ||
	       LtlSetGetElt(Current, notF_ab_idx) );
    break;
  case Ltl2Aut_GPVWplus_c:
    /* if 'u' is False, or !(u) exists in Covered */
    result = ( F_type == Ctlsp_FALSE_c ||
	       LtlSetGetElt(Covered, notF_ab_idx) );
    break;
  case Ltl2Aut_LTL2AUT_c:
  case Ltl2Aut_WRING_c:
    UC = LtlSetCopy(ToCover);
    LtlSetOR(UC, ToCover, Current);
    /* T iff (!u) \in SI(ToCover U Current) */
    result = SI(tableau, notF_ab_idx, UC);
    LtlSetFree(UC);
    break;
  }
#ifdef DEBUG_LTLMC
  if (tableau->verbosity >2)
    fprintf(vis_stdout, "...Contradiction=%d\n", result);
#endif
  
  return result;
}

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

  Synopsis    [Return 1 iff the given formula is redundant.]

  Description [The formula is represented by its index in the abTable]

  SideEffects []

******************************************************************************/
static int
Redundant(
  LtlTableau_t *tableau,
  int index,
  LtlSet_t *ToCover,
  LtlSet_t *Current,
  LtlSet_t *Covered)
{
  int result = 0;
  Ctlsp_Formula_t *F;
  LtlSet_t *UC = LtlSetCopy(ToCover);
  int Fleft_ab_idx , Fright_ab_idx;
  Ctlsp_FormulaType F_type;
  
  LtlSetOR(UC, ToCover, Current);
  
  F = tableau->abTable[index].F;
  
  F_type = Ctlsp_FormulaReadType(F);
  if (F_type == Ctlsp_U_c || F_type == Ctlsp_R_c) {
    Fleft_ab_idx = Ctlsp_FormulaReadABIndex(Ctlsp_FormulaReadLeftChild(F));
    Fright_ab_idx = Ctlsp_FormulaReadABIndex(Ctlsp_FormulaReadRightChild(F));
  } else { /* to remove uninitialized variable warnings */
    Fleft_ab_idx = 0;
    Fright_ab_idx = 0;
  }
  switch(tableau->algorithm) {
  case Ltl2Aut_GPVW_c:
    result = 0;
    break;
  case Ltl2Aut_GPVWplus_c:
    /* T iff  'u' is (n U v) and {v} is in (ToCover U Current),
     *   or   'u' is (n R v) and {n,v} is in (ToCover U Current) 
     */
    if (F_type == Ctlsp_U_c) 
      result = LtlSetGetElt(UC, Fright_ab_idx);
    else if (F_type == Ctlsp_R_c) 
      result = ( LtlSetGetElt(UC, Fleft_ab_idx) &&
		 LtlSetGetElt(UC, Fright_ab_idx) );
    else
      result = 0;
    break;
  case Ltl2Aut_LTL2AUT_c:
  case Ltl2Aut_WRING_c:
    /* T iff the following two cases are both true:
     *  (1) 'u' is in SI(ToCover U Current)
     *  (2) if 'u' is (n U v), then 'v' is in (ToCover U Current) 
     */
    result = SI(tableau, index, UC);
    if (result && F_type == Ctlsp_U_c) {
      result = SI(tableau, Fright_ab_idx, UC);
    }
    break;
  }
  LtlSetFree(UC);
#ifdef DEBUG_LTLMC  
  if (tableau->verbosity >2)
    fprintf(vis_stdout, "...Redundant=%d\n", result);
#endif
  
  return result;
}

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

  Synopsis    [Test if the given formula is synatically implied by the
  existing set (product term).]

  Description [Return 1 if the formula is implied. The formula is represented
  by its index in the abTable]

  SideEffects []

******************************************************************************/
static int
SI(
  LtlTableau_t *tableau,
  int index,
  LtlSet_t *A)
{
  int result = 0;
  Ctlsp_Formula_t *XF;
  Ctlsp_Formula_t *F = tableau->abTable[index].F;
  Ctlsp_FormulaType F_type = Ctlsp_FormulaReadType(F);
  int Fleft_ab_idx, Fright_ab_idx;
  
  if (tableau->algorithm == Ltl2Aut_GPVW_c ||
      tableau->algorithm == Ltl2Aut_GPVWplus_c) {
    result = LtlSetGetElt(A, index);
  } else {
    if (F_type == Ctlsp_AND_c || F_type == Ctlsp_OR_c ||
	F_type == Ctlsp_U_c || F_type == Ctlsp_R_c) {
      Fleft_ab_idx =
	Ctlsp_FormulaReadABIndex(Ctlsp_FormulaReadLeftChild(F));
      Fright_ab_idx =
	Ctlsp_FormulaReadABIndex(Ctlsp_FormulaReadRightChild(F));
    } else { /* to remove uninitialized variable warnings */
      Fleft_ab_idx = 0;
      Fright_ab_idx = 0;
    }
    
    switch(Ctlsp_FormulaReadType(F)) {
    case Ctlsp_FALSE_c:
      result = 0;
      break;
    case Ctlsp_TRUE_c:
      result = 1;
      break;
    case Ctlsp_X_c:
    case Ctlsp_NOT_c:
    case Ctlsp_ID_c:
      result = LtlSetGetElt(A, index);
      break;
    case Ctlsp_AND_c:
      if (Ctlsp_LtlFormulaIsPropositional(F))
	result = LtlSetGetElt(A, index);
      else {
	result = (SI(tableau, Fleft_ab_idx, A) &&
		  SI(tableau, Fright_ab_idx, A));
      }
      break;
    case Ctlsp_OR_c:
      if (Ctlsp_LtlFormulaIsPropositional(F))
	result = LtlSetGetElt(A, index);
      else {
	result = (SI(tableau, Fleft_ab_idx, A) ||
		  SI(tableau, Fright_ab_idx, A));
      }
      break;
    case Ctlsp_U_c:
      XF = LtlTableauGetUniqueXFormula(tableau, F);	  
      result = (SI(tableau, Fright_ab_idx, A) ||
		(SI(tableau, Fleft_ab_idx, A) &&
		 LtlSetGetElt(A, Ctlsp_FormulaReadABIndex(XF))));
      break;
    case Ctlsp_R_c:
      XF = LtlTableauGetUniqueXFormula(tableau, F);	  
      result = SI(tableau, Fright_ab_idx, A) &&
	(SI(tableau, Fleft_ab_idx, A) ||
	 LtlSetGetElt(A, Ctlsp_FormulaReadABIndex(XF)));
      break;
    default:
      assert(0);
    }
  }
  
#ifdef DEBUG_LTLMC
  if (tableau->verbosity > 3) {
    fprintf(vis_stdout, "...SI( %d, ", index);
    LtlSetPrintIndex(tableau->abIndex, A);
    fprintf(vis_stdout, "     )=%d\n", result);
  }
#endif
  
  return result;
}


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

  Synopsis    [Put the node into the fairset if it contains a until formula.]

  Description [Each until formula in the 'untilUnqiueTable' corresponds to
  a fair set (a set of vertices in the automaton, represented by a hash
  table. A vertex belongs to a fair set iff its cover set contains the until
  formula.]

  SideEffects []

******************************************************************************/
static void
AutomatonComputeFair(
  LtlTableau_t *tableau,
  LtlSet_t *r,
  vertex_t *vtx1)
{
  st_table *uniqueTable = tableau->untilUniqueTable;
  char *key, *value;
  st_generator *gen;

  /* Notice that each pair in 'uniqueTable' is a (Unitl formula, Fair set) */
  st_foreach_item(uniqueTable, gen, &key, &value) {
    Ctlsp_Formula_t *F = (Ctlsp_Formula_t *) key;
    Ctlsp_Formula_t *right = Ctlsp_FormulaReadRightChild(F);
    int F_ab_idx = Ctlsp_FormulaReadABIndex(F);
    int right_ab_idx = Ctlsp_FormulaReadABIndex(right);
    lsList Fair = (lsList) value;
      
    if ( SI(tableau, right_ab_idx, r) || !(SI(tableau, F_ab_idx, r)) ) {
      lsNewEnd(Fair, (lsGeneric) vtx1, (lsHandle *) 0); 
    }
  }
}

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

  Synopsis    [Convert the fair sets of the tableau into the fair set in the
  automaton.]

  Description [The fairness in the tableau is "a hash table (Until formula,
  FairVerticesList)". The fairness in the automaton should be " a list of
  hash tables" (each hash table corresponds to a fair set, and a vertex is
  in the hash table iff it's in that fair set).

  Return 0 iff there is an empty fairset (which means the language of the 
  automaton is empty no matter what);  Return 1 otherwise.]

  SideEffects []

******************************************************************************/
static int
AutomatonCreateFairList(
  LtlTableau_t *tableau,
  Ltl_Automaton_t *aut)
{
  lsList FairList = aut->Fair;
  char *key, *value;
  st_generator *gen;
  int noEmptyFairSet = 1;

  st_foreach_item(tableau->untilUniqueTable, gen, &key, &value) {
    lsList Fair = (lsList) value;

    /* translate a lsList into a st_table */
    if (lsLength(Fair) > 0) {
      lsGen lsgen;
      lsGeneric lsdata;
      st_table *tbl = st_init_table(st_ptrcmp, st_ptrhash);
      
      lsForEachItem (Fair, lsgen, lsdata) {
	st_insert(tbl, lsdata, lsdata);
      }
      lsNewEnd(FairList, (lsGeneric) tbl, (lsHandle *) 0); 
    }else 
      noEmptyFairSet = 0;

    lsDestroy(Fair, (void (*)(lsGeneric)) NULL);
  }

  return noEmptyFairSet;
}

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

  Synopsis    [Generate the next-formulae set.]
  
  Description [toCover = { u: X(u) is in s }. In other words, for each formula
  of the form X(u) in the set 's', add the subformula u into 'toCover'.]

  SideEffects ['toCover' is changed.]

******************************************************************************/
static void
AutomatonAssignNext(
  LtlTableau_t *tableau,
  LtlSet_t * toCover,
  LtlSet_t * s)
{
  int i;
  Ctlsp_FormulaType type;
  Ctlsp_Formula_t *left;
  int left_ab_idx;
      
  LtlSetClear(toCover);
  
  for (i=0; i<tableau->abIndex; i++) {
    if (LtlSetGetElt(s, i)) {
      type = Ctlsp_FormulaReadType(tableau->abTable[i].F);
      if (type == Ctlsp_X_c) {
	left = Ctlsp_FormulaReadLeftChild(tableau->abTable[i].F);
	left_ab_idx = Ctlsp_FormulaReadABIndex(left);
	LtlSetSetElt(toCover, left_ab_idx);
	
      }
    }
  }
}  


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

  Synopsis    [Create the set representation of the given formula.]

  Description [Its size will be the total number of sub-formulae in the
  tableau. Only the bit corresponding to the given formula is set.]

  SideEffects [The result should be freed by the caller.]

******************************************************************************/
static LtlSet_t *
AutomatonSetCreate(
  LtlTableau_t *tableau,
  Ctlsp_Formula_t *F)  
{
  LtlSet_t *cs = LtlSetNew(tableau->abIndex);

  if (!F)
    return cs;

  LtlSetSetElt(cs, Ctlsp_FormulaReadABIndex(F));
    
  return cs;
}

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

  Synopsis    [Build the cover for a given set 'toCover'.]

  Description [The cover is "a list of sets", where the sets are product terms
  and the list is in DNF form (union of all its product terms).]

  SideEffects [The result should be freed by the caller.]

******************************************************************************/
static lsList
AutomatonBuildCover(
  LtlTableau_t *tableau,
  LtlSet_t *ToCover)
{
  LtlSet_t *Current = LtlSetNew(tableau->abIndex);
  LtlSet_t *Covered = LtlSetNew(tableau->abIndex);
  lsList Cover = lsCreate();

  AutomatonBuildCover_Aux(tableau, ToCover, Current, Covered, Cover);
  LtlSetFree(Current);
  LtlSetFree(Covered);
  
  /* Boolean Minimization -- heuristics */
  if (tableau->booleanmin == 1) {
    if (lsLength(Cover)) {
      lsList list = Cover;
      Cover = LtlCoverPrimeAndIrredundant(tableau, Cover,
					  tableau->abTableNegate);
      lsDestroy(list, (void (*)(lsGeneric))LtlSetFree);
    }
  }
  return Cover;
}

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

  Synopsis    [Recursively construct the cover.]

  Description [the cover is updated in the parameter 'lsList Cover'. This
  function is used in AutomatonBuildCover() only.]

  SideEffects []

******************************************************************************/
static void
AutomatonBuildCover_Aux(
  LtlTableau_t *tableau,
  LtlSet_t *pToCover,
  LtlSet_t *pCurrent,
  LtlSet_t *pCovered,
  lsList Cover)
{
  LtlSet_t *ToCover = LtlSetCopy(pToCover);
  LtlSet_t *Current = LtlSetCopy(pCurrent);
  LtlSet_t *Covered = LtlSetCopy(pCovered);
  int i;

#ifdef DEBUG_LTLMC  
  if (tableau->verbosity >2 ) {
    fprintf(vis_stdout, "ToCover=");
    LtlSetPrintIndex(tableau->abIndex, ToCover);
    fprintf(vis_stdout, "Current=");
    LtlSetPrintIndex(tableau->abIndex, Current);
    fprintf(vis_stdout, "Covered=");
    LtlSetPrintIndex(tableau->abIndex, Covered);
    fflush(vis_stdout);
  }      
#endif
  
  if (LtlSetIsEmpty(ToCover)) {
#if 1
    /* chao: 7/22/2002 remove identical set in current Cover */
    if (!LtlSetIsInList(Current, Cover))
#endif
      lsNewEnd(Cover, (lsGeneric) LtlSetCopy(Current), (lsHandle *) 0);
    /* return */
  }else {
    /* select 'u' from 'ToCover' */
    for (i=0; i<tableau->abIndex; i++) {
      if (LtlSetGetElt(ToCover,i))
	break;
    }
    /* remove 'u' from 'ToCover' and add it to 'Covered' */
    LtlSetClearElt(ToCover, i);
    LtlSetSetElt(Covered, i);
    
    /* if HAS_TO_BE_STORED(u), store into 'Current' */
    if (HasToBeStored(tableau,i)) 
      LtlSetSetElt(Current, i);
    
    /* if CONTRADICTION(u, ToCover, Current, Covered), return 'Cover' */
    if (Contradiction(tableau, i, ToCover, Current, Covered)) {
      ; /* return */
    }else if (Redundant(tableau, i, ToCover, Current, Covered)) {
      AutomatonBuildCover_Aux(tableau, ToCover, Current, Covered, Cover);
      /* return */
    }else {
      if (Ctlsp_LtlFormulaIsElementary(tableau->abTable[i].F)) {
	LtlSetSetElt(Current, i);
	AutomatonBuildCover_Aux(tableau, ToCover, Current, Covered,
				Cover);
	/* return */
      }else {
	int A0B0 = tableau->abTable[i].A[0].B[0];
	int A0B1 = tableau->abTable[i].A[0].B[1];
	int A0n = tableau->abTable[i].A[0].n;
	int A1B0 = tableau->abTable[i].A[1].B[0];
	int A1B1 = tableau->abTable[i].A[1].B[1];
	int A1n = tableau->abTable[i].A[1].n;
	
	/* cover( (ToCover+alph2(u)-Current), Current, Covered, Cover) */
	if (A1B0 != -1 || A1B1!= -1 || A1n!= -1) {
	  LtlSet_t *saveToCover = LtlSetCopy(ToCover);	      
	  if (A1B0 != -1)
	    if (!LtlSetGetElt(Current, A1B0))
	      LtlSetSetElt(ToCover, A1B0);
	  if (A1B1 != -1)
	    if (!LtlSetGetElt(Current, A1B1))
	      LtlSetSetElt(ToCover, A1B1);
	  if (A1n != -1)
	    if (!LtlSetGetElt(Current, A1n))
	      LtlSetSetElt(ToCover, A1n);
	  
	  AutomatonBuildCover_Aux(tableau, ToCover, Current, Covered,
				  Cover);
	  
	  LtlSetAssign(ToCover, saveToCover);
	  LtlSetFree(saveToCover);
	}
	
	/* cover( (ToCover+alph1(u)-Current), Current, Covered, Cover) */
	if (A0B0 != -1 || A0B1!= -1 || A0n!= -1) {	      
	  if (A0B0 != -1)
	    if (!LtlSetGetElt(Current, A0B0))
	      LtlSetSetElt(ToCover, A0B0);
	  if (A0B1 != -1)
	    if (!LtlSetGetElt(Current, A0B1))
	      LtlSetSetElt(ToCover, A0B1);
	  if (A0n != -1)
	    if (!LtlSetGetElt(Current, A0n))
	      LtlSetSetElt(ToCover, A0n);
	  
	  AutomatonBuildCover_Aux(tableau, ToCover, Current, Covered,
				  Cover);
	}
	/* return */
      }
    }
  }
  
  /* Clean-Ups */
  LtlSetFree(ToCover);
  LtlSetFree(Current);
  LtlSetFree(Covered);
}