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

  FileName    [ltlCompose.c]

  PackageName [ltl]

  Synopsis    [Write the Buechi automaton into a file.]

  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: ltlCompose.c,v 1.30 2005/04/28 08:51:19 bli Exp $";

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

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

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

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

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

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

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

static void AutomatonGetInputNames(Ltl_Automaton_t *A, array_t *InputNames, array_t *Name2LabelIdx);
static int AutomatonCountSelector(Ltl_Automaton_t *A);
static int AutomatonComputeInitState(Ltl_Automaton_t *A);
/*static lsList AutomatonLabelGetCubes(Ltl_Automaton_t *A, LtlSet_t *compositeLabel, Ntk_Network_t *network);*/
static lsList GetCubes_Aux(Ltl_Automaton_t *A, int index);
static char * StringNormalize(char *inputString);
static void AutomatonVtxLabelToBlifMv(FILE *fp, Ltl_Automaton_t *A, vertex_t *vtx);
static void VtxLabelToBlifMv_Aux(FILE *fp, Ltl_Automaton_t *A, int node_idx, int index, st_table *CreatedSignals);

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

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

  Synopsis    [Translate the Automaton into Dot format.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Ltl_AutomatonToDot(
  FILE *fp,
  Ltl_Automaton_t *aut,
  int level)
{
  edge_t   *edge;
  vertex_t *vtx1, *vtx2;         
  Ltl_AutomatonNode_t *node, *node2;
  lsGen     lsgen, lsgen2;
  st_table  *FairSet;
  st_generator *stgen;
  Ctlsp_Formula_t *F;
  char *tmpString;
  int fairindex, first, i, n;
  
  /*-------------------------------------------------
   * digraph "G(F(p=1))" {
   * node [shape=ellipse];
   * size = "7.5,10"
   * center = true;
   * "title" [label="G(F(p=1))", shape=plaintext];
   *-------------------------------------------------
   */
  if (aut->name)
    tmpString = aut->name;
  else
    tmpString = "";
  
  fprintf(fp, "\ndigraph \"%s\" {\nnode [shape=ellipse];\nsize = \"7.5,10\"\ncenter = true;\n\"title\" [label=\"%s\",shape=plaintext];", tmpString, tmpString);
  
  /*-------------------------------------------------
   * "n1" [label="n1\n{p=1}\n(1)"];
   *-------------------------------------------------
   */
  foreach_vertex( aut->G, lsgen, vtx1) {
    node = (Ltl_AutomatonNode_t *)vtx1->user_data;
    fprintf(fp,"\n\"n%d\" [label=\"n%d\\n{", node->index, node->index);
    if (node->Labels) {
      first = 1; n = array_n(aut->labelTable);
      for (i=0; i<n; i++) {
	if (LtlSetGetElt(node->Labels, i)) {
	  if (!first)	  fprintf(fp, ",");
	  else       	  first = 0;
	  F = array_fetch(Ctlsp_Formula_t *, aut->labelTable, i);
	  Ctlsp_FormulaPrint(fp, F);
	}
      }
    }
    fprintf(fp, "}\\n(");
    fairindex = 1;
    lsForEachItem(aut->Fair, lsgen2, FairSet) {
      if (st_is_member(FairSet, vtx1))
	fprintf(fp, " %d ", fairindex);
      fairindex++;
    }
    fprintf(fp, ")\"];");
  }

  /*-------------------------------------------------
   * "init-n2" [style=invis]
   * "init-n2" -> "n2";
   *-------------------------------------------------
   */
  st_foreach_item(aut->Init, stgen, &vtx1, NIL(char *)) {
    node = (Ltl_AutomatonNode_t *) vtx1->user_data;
    fprintf(fp, "\n\"init-n%d\" [style=invis]", node->index);
    fprintf(fp, "\n\"init-n%d\" -> \"n%d\";", node->index, node->index);
  }


  /*-------------------------------------------------
   * "n1" -> "n1";
   *-------------------------------------------------
   */
  foreach_edge(aut->G, lsgen, 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;
    fprintf(fp, "\n\"n%d\" -> \"n%d\";", node->index, node2->index);
  }
  fprintf(fp, "\n}\n");
}


/**Function********************************************************************
   
  Synopsis    [Translate the automaton to a BlifMv file.]
  
  Description [The Hrc_Manager may or may not be provided. If not, the blifmv
  file generated is not complete (all the inputs are assummed to be boolean).
  
  Notice that the labels on each state are propositional subformulae, not
  necessarily atomic propositions.]
  
  SideEffects []
  
  SeeAlso     []

******************************************************************************/
int
Ltl_AutomatonToBlifMv(
  FILE *fp,             
  Ntk_Network_t *network,
  Ltl_Automaton_t *A)     
{
  Var_Variable_t *inputVar;
  array_t *InputNames = array_alloc(char *, 0);
  array_t *Name2LabelIdx = array_alloc(st_table *, 0);
  Ntk_Node_t *ntknode;
  char *inputName;
  st_generator *stgen;
  lsGen lsgen, lsgen2;
  int i, j, is_enum, range;
  int sel_num, sel_cnt;
  edge_t *edge;
  vertex_t *vtx, *vtx2;
  st_table *FairSet, *tmptbl;
  int InitIdx = AutomatonComputeInitState(A);
  char InitStr[10];
  int result = 1;
  array_t *labelArray;
  
  /* The initState of the automaton */
  if (InitIdx == -1) 
    sprintf(InitStr, "Init");
  else
    sprintf(InitStr, "n%d", InitIdx);
  
  if (network == NIL(Ntk_Network_t)) {
    result = 0;
    fprintf(vis_stderr, "Warning: the BlifMv output is incomplete. (The current node is empty. Read in design.)\n");
  }

  /* Retrieve all the input names on the labels; For each input, create a
   *  hash table and add all the label subformulae contains that input;
   *  Finally, calculate the size of the "selector" 
   */
  AutomatonGetInputNames(A, InputNames, Name2LabelIdx);
  sel_num = AutomatonCountSelector(A);
  fprintf(fp, "\n# Buechi automaton: %s\n\n", A->name);
  
  /*-------------------------------------------------------
   * .model Buechi$AUT
   * .root  Buechi$AUT
   *-------------------------------------------------------
   */
   fprintf(fp, ".model Buechi$AUT\n.root Buechi$AUT");
  
   /*-------------------------------------------------------
    * .inputs in1 in2 in3 ... inN 
    *-------------------------------------------------------
    */
   fprintf(fp, "\n.inputs ");
   for (i=0; i<array_n(InputNames); i++) {
     inputName = array_fetch(char *, InputNames, i);
     fprintf(fp, "%s ", inputName);
   }

   /*-------------------------------------------------------
    * .outputs fair1 fair2 fair3... fairN
    *-------------------------------------------------------
    */
   fprintf(fp, "\n.outputs ");
   if ( lsLength(A->Fair) != 0) {
     for (i=0; i<lsLength(A->Fair); i++) {
       fprintf(fp, "fair%d$AUT ", i+1);
     }
   }else
     fprintf(fp, "fair1$AUT");

   /*-------------------------------------------------------
    * .mv in1 3 RED GREEN YELLOW 
    *-------------------------------------------------------
    */
   if (network != NIL(Ntk_Network_t)) {
     for (i=0; i<array_n(InputNames); i++) {
       inputName = array_fetch(char *, InputNames, i);
       ntknode = Ntk_NetworkFindNodeByName(network, inputName);
       assert(ntknode != NIL(Ntk_Node_t));
       inputVar = Ntk_NodeReadVariable(ntknode);
       is_enum = Var_VariableTestIsEnumerative(inputVar);
       range = Var_VariableReadNumValues(inputVar);
       if (is_enum) {
	 if (range != 2) 
	   fprintf(fp, "\n.mv %s %d\n", inputName, range);
       }else {
	 fprintf(fp, "\n.mv %s %d ", inputName, range);
	 for (j=0; j<range; j++) {
	   fprintf(fp, "%s ",
		   Var_VariableReadSymbolicValueFromIndex(inputVar,j));
	 }
       }
     }
   }

   /*-------------------------------------------------------  
    * .mv stateD$AUT N Init n1 n2 n3 ... nN 
    * .mv state$AUT  N Init n1 n2 n3 ... nN
    *-------------------------------------------------------
    */
   if (InitIdx == -1) 
     fprintf(fp, "\n.mv stateD$AUT %d Init Trap ",
	     lsLength(g_get_vertices(A->G)) + 2);
   else
     fprintf(fp, "\n.mv stateD$AUT %d Trap ",
	     lsLength(g_get_vertices(A->G)) + 1);
   foreach_vertex(A->G, lsgen, vtx) {
     fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx));
   }
   if (InitIdx == -1)
     fprintf(fp, "\n.mv state$AUT %d Init Trap ",
	     lsLength(g_get_vertices(A->G)) + 2);
   else
     fprintf(fp, "\n.mv state$AUT %d Trap ",
	     lsLength(g_get_vertices(A->G)) + 1);
   foreach_vertex(A->G, lsgen, vtx) {  
     fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx));
   }

   /*-------------------------------------------------------
    * .mv selector n
    * .table selector 
    * - 
    *-------------------------------------------------------
    */
   if (sel_num > 1) 
     fprintf(fp, "\n.mv selector$AUT %d\n.table selector$AUT\n-", sel_num);

   /*-------------------------------------------------------
    * for each state label, create a signal n1_##_label$AUT (recursively)
    *-------------------------------------------------------
    */
   labelArray = array_alloc(vertex_t *, 0);
   foreach_vertex(A->G, lsgen, vtx) {
     AutomatonVtxLabelToBlifMv(fp, A, vtx);
     array_insert_last(vertex_t *, labelArray, vtx);
   }
   
   /*-------------------------------------------------------  
    * .latch stateD$AUT state$AUT
    * .reset state$AUT
    * Init (or ns) 
    *-------------------------------------------------------
    */
   fprintf(fp, "\n.latch stateD$AUT state$AUT\n.reset -> state$AUT\n%s",
	   InitStr);


   /*------------------------------------------------------
    * .table selector$AUT state$AUT n1_label$AUT n2_label... -> stateD$AUT
    * .default Trap
    * 0 1 0 0 ... n1
    * 1 0 1       n2
    * ...
    *------------------------------------------------------
    */
   if (sel_num >1)
     fprintf(fp, "\n.table selector$AUT state$AUT ");
   else
     fprintf(fp, "\n.table state$AUT ");

   arrayForEachItem(vertex_t *, labelArray, i, vtx) {
     fprintf(fp, "n%d_label$AUT ", Ltl_AutomatonVtxGetNodeIdx(vtx));
   }
   fprintf(fp, " -> stateD$AUT\n.default Trap");

   if (InitIdx == -1) {
     sel_cnt = 0;
     arrayForEachItem(vertex_t *, labelArray, i, vtx) {
       if (!st_is_member(A->Init, vtx))
	 continue;
       if (sel_num > 1) {
	 if (st_count(A->Init) == 1) 
	   fprintf(fp, "\n- Init ");
	 else
	   fprintf(fp, "\n%d Init ", sel_cnt);
       }else
	 fprintf(fp, "\nInit ");
       
       for(j=0; j<array_n(labelArray); j++)
	 fprintf(fp, "%s ", ((i==j)?"1":"-"));

       fprintf(fp, "   n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));

       if (sel_num > 1)
	 sel_cnt++;
     }
   }

   /* for each edge (n1, n2) with n2 labeled n2_label$AUT, add entry: 
    *-------------------------------------------------------     
    * selector 1 0 0  ...     n1
    * selector 0 1 0  ...     n2
    * ...
    *-------------------------------------------------------
    */
   foreach_vertex(A->G, lsgen, vtx) {
     int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx);
     int outDegree = lsLength(g_get_out_edges(vtx));
     sel_cnt = 0;
     foreach_out_edge(vtx, lsgen2, edge) {
       int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge));

       if (sel_num > 1) {
	 if (outDegree == 1) 
	   fprintf(fp, "\n- n%d ", n1);
	 else
	   fprintf(fp, "\n%d n%d ", sel_cnt, n1);
       }else {
	 fprintf(fp, "\nn%d ", n1);
       }
       
       arrayForEachItem(vertex_t *, labelArray, i, vtx2) {
	 fprintf(fp, "%s ", ((vtx2 == g_e_dest(edge))?"1":"-"));
       }
       fprintf(fp, "   n%d", n2);
	  
       if (sel_num > 1)
	 sel_cnt++;
     }
   }
   array_free(labelArray);

   /*-------------------------------------------------------  
    * .table state -> fair1
    * .default 0 
    * ------------------------------------------------------
    */
   if (lsLength(A->Fair) != 0) {
     i = 1;
     lsForEachItem(A->Fair, lsgen, FairSet) {
       int isFirst = 1;
       fprintf(fp, "\n.table state$AUT -> fair%d$AUT ", i++);
       fprintf(fp, "\n.default 0\n(");
       st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) {
	 if (isFirst)
	   isFirst = 0;
	 else
	   fprintf(fp, ",");
	 fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
       }
       fprintf(fp, ")   1");
     }
   }else {
     fprintf(fp, "\n.table state$AUT -> fair1$AUT ");
     if (InitIdx == -1)
       fprintf(fp, "\n.default 0\n!(Trap,Init)   1");
     else
       fprintf(fp, "\n.default 0\n!(Trap)   1");
   }

   /*-------------------------------------------------------  
    * .end 
    * ------------------------------------------------------
    */
   fprintf(fp, "\n.end\n");

   /* free the name array 
    */
   array_free(InputNames);
   arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) {
     st_free_table(tmptbl);
   }
   array_free(Name2LabelIdx);
 
   return result;
}

#if 0
int
Ltl_AutomatonToBlifMv_Old(
  FILE *fp,             
  Ntk_Network_t *network,
  Ltl_Automaton_t *A)     
{
  Var_Variable_t *inputVar;
  array_t *InputNames = array_alloc(char *, 0);
  array_t *Name2LabelIdx = array_alloc(st_table *, 0);
  Ntk_Node_t *ntknode;
  char *inputName;
  st_generator *stgen, *stgen2;
  lsGen lsgen, lsgen2, lsgen3;
  int i, j, is_enum, range;
  long index;
  int sel_num, sel_cnt;
  edge_t *edge;
  vertex_t *vtx;
  st_table *FairSet, *tmptbl;
  LtlSet_t *label;
  int InitIdx = AutomatonComputeInitState(A);
  char InitStr[10];
  int result = 1;

  /* The initState of the automaton */
  if (InitIdx == -1) 
    sprintf(InitStr, "Init");
  else
    sprintf(InitStr, "n%d", InitIdx);
  
  if (network == NIL(Ntk_Network_t)) {
    result = 0;
    fprintf(vis_stderr, "Warning: the BlifMv output is incomplete. (The current node is empty. Read in design.)\n");
  }

  /* Retrieve all the input names on the labels; For each input, create a
   *  hash table and add all the label subformulae contains that input;
   *  Finally, calculate the size of the "selector" 
   */
  AutomatonGetInputNames(A, InputNames, Name2LabelIdx);
  sel_num = AutomatonCountSelector(A);
  fprintf(fp, "\n# Buechi automaton: %s\n\n", A->name);
  
  /*-------------------------------------------------------
   * .model Buechi$AUT
   * .root  Buechi$AUT
   *-------------------------------------------------------
   */
   fprintf(fp, ".model Buechi$AUT\n.root Buechi$AUT");
  
   /*-------------------------------------------------------
    * .inputs in1 in2 in3 ... inN 
    *-------------------------------------------------------
    */
   fprintf(fp, "\n.inputs ");
   for (i=0; i<array_n(InputNames); i++) {
     inputName = array_fetch(char *, InputNames, i);
     fprintf(fp, "%s ", inputName);
   }

   /*-------------------------------------------------------
    * .outputs fair1 fair2 fair3... fairN
    *-------------------------------------------------------
    */
   fprintf(fp, "\n.outputs ");
   if ( lsLength(A->Fair) != 0) {
     for (i=0; i<lsLength(A->Fair); i++) {
       fprintf(fp, "fair%d$AUT ", i+1);
     }
   }else
     fprintf(fp, "fair1$AUT");

   /*-------------------------------------------------------
    * .mv in1 3 RED GREEN YELLOW 
    *-------------------------------------------------------
    */
   if (network != NIL(Ntk_Network_t)) {
     for (i=0; i<array_n(InputNames); i++) {
       inputName = array_fetch(char *, InputNames, i);
       ntknode = Ntk_NetworkFindNodeByName(network, inputName);
       assert(ntknode != NIL(Ntk_Node_t));
       inputVar = Ntk_NodeReadVariable(ntknode);
       is_enum = Var_VariableTestIsEnumerative(inputVar);
       range = Var_VariableReadNumValues(inputVar);
       if (is_enum) {
	 if (range != 2) 
	   fprintf(fp, "\n.mv %s %d\n", inputName, range);
       }else {
	 fprintf(fp, "\n.mv %s %d ", inputName, range);
	 for (j=0; j<range; j++) {
	   fprintf(fp, "%s ",
		   Var_VariableReadSymbolicValueFromIndex(inputVar,j));
	 }
       }
     }
   }

   /*-------------------------------------------------------  
    * .mv stateD$AUT N Init n1 n2 n3 ... nN 
    * .mv state$AUT  N Init n1 n2 n3 ... nN
    *-------------------------------------------------------
    */
   if (InitIdx == -1) 
     fprintf(fp, "\n.mv stateD$AUT %d Init Trap ",
	     lsLength(g_get_vertices(A->G)) + 2);
   else
     fprintf(fp, "\n.mv stateD$AUT %d Trap ",
	     lsLength(g_get_vertices(A->G)) + 1);
   foreach_vertex(A->G, lsgen, vtx) {
     fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx));
   }
   if (InitIdx == -1)
     fprintf(fp, "\n.mv state$AUT %d Init Trap ",
	     lsLength(g_get_vertices(A->G)) + 2);
   else
     fprintf(fp, "\n.mv state$AUT %d Trap ",
	     lsLength(g_get_vertices(A->G)) + 1);
   foreach_vertex(A->G, lsgen, vtx) {  
     fprintf(fp, "n%d ", Ltl_AutomatonVtxGetNodeIdx(vtx));
   }

   /*-------------------------------------------------------
    * .mv selector n
    * .table selector 
    * - 
    *-------------------------------------------------------
    */
   if (sel_num > 1) 
     fprintf(fp, "\n.mv selector$AUT %d\n.table selector$AUT\n-", sel_num);

   /*-------------------------------------------------------  
    * .latch stateD$AUT state$AUT
    * .reset state$AUT
    * Init (or ns) 
    *-------------------------------------------------------
    */
   fprintf(fp, "\n.latch stateD$AUT state$AUT\n.reset -> state$AUT\n%s",
	   InitStr);
   
   /*------------------------------------------------------
    * .table selector$AUT state$AUT in1 in2 ... inN -> stateD$AUT
    * .default Trap 
    *------------------------------------------------------
    */
   if (sel_num >1)
     fprintf(fp, "\n.table selector$AUT state$AUT ");
   else
     fprintf(fp, "\n.table state$AUT ");
   
   for (i=0; i<array_n(InputNames); i++) {
     inputName = array_fetch(char *, InputNames, i);
     fprintf(fp, "%s ", inputName);
   }
   fprintf(fp, " -> stateD$AUT\n.default Trap");
   
  
   /* for each initial state n2 with label "in1=p  !in3=q...", add entry: 
    *-------------------------------------------------------
    *  selector Init (p) -  (!(q)) ..  n2   
    *-------------------------------------------------------
    */
   if (InitIdx == -1) {
     sel_cnt = 0;
     st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) {
       int n2 = Ltl_AutomatonVtxGetNodeIdx(vtx);
       /* each 'compLabel' is a set of "propositional formulae" */
       LtlSet_t *compLabel = LtlAutomatonVertexGetLabels(vtx);
       /* each item in labelList is a set of "atomic proposition" */
       lsList labelList = AutomatonLabelGetCubes(A, compLabel, network);
       lsForEachItem(labelList, lsgen, label) {
	 if (sel_num > 1) {
	   if (st_count(A->Init) == 1) 
	     fprintf(fp, "\n- Init ");
	   else
	     fprintf(fp, "\n%d Init ", sel_cnt);
	 }else
	   fprintf(fp, "\nInit ");
	 arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) {
	   int isFirst = 1;
	   int is_universe = 1;
	   /* The value is the universe '-' iff it is not in the label */
	   if (!LtlSetIsEmpty(label)) {
	     st_foreach_item(tmptbl, stgen2, &index, NIL(char *)) {
	       if (LtlSetGetElt(label, (int) index)) {
		 is_universe = 0;
		 st_free_gen(stgen2);
		 break;
	       }
	     }
	   }
	   if (is_universe) {
	     fprintf(fp, "- ");
	     continue;
	   }
	   /* Otherwise, write the value. Note that the value should be
	    * the conjunction of the values of the atomic propositions.
	    * A * B * C = !(!A + !B +!C) 
	    */
	   fprintf(fp, "!(");
	   st_foreach_item(tmptbl, stgen2, &index, NIL(char *)) {
	     if (LtlSetGetElt(label, (int) index)) {
	       Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *,
						A->labelTable,
						(int) index);
	       if (isFirst)
		 isFirst = 0;
	       else
		 fprintf(fp, ",");
	       if (Ctlsp_FormulaReadType(F) == Ctlsp_NOT_c) {
		 F = Ctlsp_FormulaReadLeftChild(F);
	       }else {
		 fprintf(fp, "!");
	       }
	       
	       fprintf(fp, "(%s)", Ctlsp_FormulaReadValueName(F));
	     }
	   }
	   fprintf(fp, ") ");
	 }
	 fprintf(fp, "   n%d", n2);
       }
       lsDestroy(labelList, (void (*)(lsGeneric))LtlSetFree);
       
       if (sel_num > 1)
	 sel_cnt++;
     }
   }

   /* for each edge (n1, n2) with n2 labelled "in1=p !in3=q...", add entry: 
    *-------------------------------------------------------     
    * selector n1 (p) - (!(q)) ...     n2
    *-------------------------------------------------------
    */
   foreach_vertex(A->G, lsgen, vtx) {
     int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx);
     int outDegree = lsLength(g_get_out_edges(vtx));
     sel_cnt = 0;
     foreach_out_edge(vtx, lsgen2, edge) {
       int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge));
       /* 'compLabel' contains a set of "propositional formulae" */
       LtlSet_t *compLabel =   LtlAutomatonVertexGetLabels(g_e_dest(edge));
       /* each item in 'labelList' is a set of "atomic propositions" */ 
       lsList labelList = AutomatonLabelGetCubes(A, compLabel, network);
       lsForEachItem(labelList, lsgen3, label) {
	 if (sel_num > 1) {
	   if (outDegree == 1) 
	     fprintf(fp, "\n- n%d ", n1);
	   else
	     fprintf(fp, "\n%d n%d ", sel_cnt, n1);
	 }else {
	   fprintf(fp, "\nn%d ", n1);
	 }
	 arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) {
	   int isFirst = 1;
	   int is_universe = 1;
	   /* the value is universe '-' iff it is not in the label */
	   if (!LtlSetIsEmpty(label)) {
	     st_foreach_item(tmptbl,stgen2,&index, NIL(char *)){
	       if (LtlSetGetElt(label, (int) index)) {
		 is_universe = 0;
		 st_free_gen(stgen2);
		 break;
	       }
	     }
	   }
	   if (is_universe) {
	     fprintf(fp, "- ");
	     continue;
	   }
	   /* write the value as the conjunction of the values in the
	    * atomic proposition. for example, if the state is labeled
	    * 'in1={R,G,B}' and 'in1={G}', we should write as
	    * !( !(R,G,B), !(G) )
	    * Note that it's the same as {R,G,B}^{G}={G} 
	    */
	   fprintf(fp, "!(");
	   st_foreach_item(tmptbl, stgen, &index, NIL(char *)) {
	     if (LtlSetGetElt(label, (int) index)) {
	       Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *,
						A->labelTable,
						(int) index);
	       if (isFirst)
		 isFirst = 0;
	       else
		 fprintf(fp, ",");
	       if (Ctlsp_FormulaReadType(F) == Ctlsp_NOT_c) 
		 F = Ctlsp_FormulaReadLeftChild(F);
	       else 
		 fprintf(fp, "!");
	       fprintf(fp, "(%s)",	Ctlsp_FormulaReadValueName(F));
	     }
	   }
	   fprintf(fp, ") ");
	 }
	 fprintf(fp, "   n%d", n2);
       }
       lsDestroy(labelList, (void (*)(lsGeneric))LtlSetFree);
	  
       if (sel_num > 1)
	 sel_cnt++;
     }
   }
 

   /*-------------------------------------------------------  
    * .table state -> fair1
    * .default 0 
    * ------------------------------------------------------
    */
   if (lsLength(A->Fair) != 0) {
     i = 1;
     lsForEachItem(A->Fair, lsgen, FairSet) {
       int isFirst = 1;
       fprintf(fp, "\n.table state$AUT -> fair%d$AUT ", i++);
       fprintf(fp, "\n.default 0\n(");
       st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) {
	 if (isFirst)
	   isFirst = 0;
	 else
	   fprintf(fp, ",");
	 fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
       }
       fprintf(fp, ")   1");
     }
   }else {
     fprintf(fp, "\n.table state$AUT -> fair1$AUT ");
     if (InitIdx == -1)
       fprintf(fp, "\n.default 0\n!(Trap,Init)   1");
     else
       fprintf(fp, "\n.default 0\n!(Trap)   1");
   }

   /*-------------------------------------------------------  
    * .end 
    * ------------------------------------------------------
    */
   fprintf(fp, "\n.end\n");

   /* free the name array 
    */
   array_free(InputNames);
   arrayForEachItem(st_table *, Name2LabelIdx, i, tmptbl) {
     st_free_table(tmptbl);
   }
   array_free(Name2LabelIdx);
   
   return result;
}
#endif

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

  Synopsis    [Translate the automaton to Verilog file.]

  Description [The Hrc_Manager may or may not be provided. If not, the verilog
  file generated is not accurate (all the inputs are assummed to be boolean).]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Ltl_AutomatonToVerilog(
  FILE *fp,             
  Ntk_Network_t *network,
  Ltl_Automaton_t *A)     
{
  Var_Variable_t *inputVar;
  array_t *InputNames = array_alloc(char *, 0);
  array_t *Name2LabelIdx = array_alloc(st_table *, 0);
  Ntk_Node_t *ntknode;
  char *inputName, *formulaString, *normalString;
  st_generator *stgen;
  lsGen lsgen, lsgen2;
  int i, j, is_enum, range, isFirst;
  int sel_num, sel_cnt;
  edge_t *edge;
  vertex_t *vtx;
  st_table *FairSet;
  int InitIdx = AutomatonComputeInitState(A);
  char InitStr[10];
  int result = 1;
  
  /* The initState of the automaton */
  if (InitIdx == -1) 
    sprintf(InitStr, "Init");
  else
    sprintf(InitStr, "n%d", InitIdx);

  if (network == NIL(Ntk_Network_t)) {
    result = 0;
    fprintf(vis_stderr, "Warning: the Verilog output is incomplete. (The current node is empty. Read in design.)\n");
  }

  /* Retrieve all the input names of the automaton into 'InputNames', And for
   * each name, put into a hash table all the subformulae contains it 
   */
  AutomatonGetInputNames(A, InputNames, Name2LabelIdx);
  sel_num = AutomatonCountSelector(A);
  fprintf(fp, "\n// Buechi automaton: %s", A->name);
   
  /*-------------------------------------------------------
   * typedef enum {Init, trap, n1, n2, ... nN} states;
   * typedef enum {READ, GREEN, YELLOW} type_in1;
   *-------------------------------------------------------
   */    
  if (InitIdx == -1)
    fprintf(fp, "\ntypedef enum {Init,Trap");
  else
    fprintf(fp, "\ntypedef enum {Trap");
  foreach_vertex(A->G, lsgen, vtx) {
    fprintf(fp, ",n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
  }
  fprintf(fp, "} type_states;");

  if (network != NIL(Ntk_Network_t)) {
    arrayForEachItem(char *, InputNames, i, inputName) {
      /* replace illegal characters in the input name string */
      normalString = StringNormalize(inputName);
      fprintf(fp, "\n//Input name mapping:\t %s => %s;", inputName,
	      normalString);

      ntknode = Ntk_NetworkFindNodeByName(network, inputName);
      assert(ntknode != NIL(Ntk_Node_t));
      inputVar = Ntk_NodeReadVariable(ntknode);
      
      is_enum = Var_VariableTestIsEnumerative(inputVar);
      range = Var_VariableReadNumValues(inputVar);
      if (is_enum) {
	if (range>2)
	  fprintf(fp, "\ntypedef enum {0-%d}  type_%s;", 
		  range-1, normalString);
      }else {
	fprintf(fp, "\ntypedef enum {");
	isFirst = 1;
	for (j=0; j<range; j++) {
	  char *vstr =
	    Var_VariableReadSymbolicValueFromIndex(inputVar,j);
	  if (isFirst)  {
	    fprintf(fp, "%s ", vstr);
	    isFirst = 0;
	  } else 
	    fprintf(fp, ",%s ", vstr);
	}
	fprintf(fp, "}  type_%s;", normalString);
      }
      
      FREE(normalString);
    }
  }
 
  /*-------------------------------------------------------    
   * module Buechi (clock, in1, in2 ... inN, fair1, ...);
   *-------------------------------------------------------
   */
  fprintf(fp, "\n//Buechi Buechi (clock");
  for (i=0; i<array_n(InputNames); i++) {
    inputName = array_fetch(char *, InputNames, i);
    fprintf(fp, ",%s", inputName);
  }
  for (i=0; i<lsLength(A->Fair); i++) {
    fprintf(fp, ",fair%d", i+1);
  }
  fprintf(fp, ");");
  
  fprintf(fp, "\nmodule Buechi (clock");
  for (i=0; i<array_n(InputNames); i++) {
    inputName = array_fetch(char *, InputNames, i);
    normalString = StringNormalize(inputName);
    fprintf(fp, ",%s", normalString);
    FREE(normalString);
  }
  for (i=0; i<lsLength(A->Fair); i++) {
    fprintf(fp, ",fair%d", i+1);
  }
  fprintf(fp, ");");

  
  /*-------------------------------------------------------
   * input clock, in1, in2 ... inN ;
   * output fair1, fair2 ... fairN ;
   *-------------------------------------------------------
   */
  fprintf(fp, "\n\tinput clock");
  for (i=0; i<array_n(InputNames); i++) {
    inputName = array_fetch(char *, InputNames, i);
    normalString = StringNormalize(inputName);
    fprintf(fp, ", %s", normalString);
    FREE(normalString);
  }
  if (lsLength(A->Fair)>0) {
    fprintf(fp, ";\n\toutput ");
    isFirst = 1;
    for (i=0; i<lsLength(A->Fair); i++) {
      if (isFirst)  {
	fprintf(fp, "fair%d", i+1);
	isFirst = 0;
      } else {
	fprintf(fp, ",fair%d", i+1);
      }
    }
  }
  fprintf(fp, ";");

  
  /*-------------------------------------------------------
   * type_in1 wire in1;
   * type_in2 wire in2;
   * ...
   * type_states reg state;
   * wire[0:logN] sel;
   *-------------------------------------------------------
   */
  if (network != NIL(Ntk_Network_t)) {
    arrayForEachItem(char *, InputNames, i, inputName) {
      normalString = StringNormalize(inputName);

      ntknode = Ntk_NetworkFindNodeByName(network, inputName);
      assert(ntknode != NIL(Ntk_Node_t));
      inputVar = Ntk_NodeReadVariable(ntknode);
      
      is_enum = Var_VariableTestIsEnumerative(inputVar);
      range = Var_VariableReadNumValues(inputVar);
      
      if (!is_enum || range > 2)
	fprintf(fp, "\n\ttype_%s  wire  %s;", normalString,normalString);
      FREE(normalString);
    }
  }
  fprintf(fp, "\n\ttype_states reg state;");
  if (sel_num >1) {
    if (sel_num == 2)
      fprintf(fp, "\n\twire sel;");
    else
      fprintf(fp, "\n\twire [0:%d] sel;", (int)(ceil(log(sel_num)))-1);
  }
  
  /*-------------------------------------------------------
   * assign sel = $ND( {0-N} );
   * assign fair = (state==n1 || state==n2 || ... );
   *-------------------------------------------------------
   */
  fprintf(fp, "\n\tassign sel = $ND( {0-%d} );", sel_num-1 );
  i = 1;
  lsForEachItem(A->Fair, lsgen, FairSet) {
    int isFirst = 1;
    fprintf(fp, "\n\tassign fair%d = (state==", i++);
    st_foreach_item(FairSet, stgen, &vtx, NIL(char *)) {
      if (isFirst)
	isFirst = 0;
      else
	fprintf(fp, "|| state==");
      fprintf(fp, "n%d", Ltl_AutomatonVtxGetNodeIdx(vtx));
    }
    fprintf(fp, ");");
  }
  
  /*-------------------------------------------------------
   * initial state = Init;
   *-------------------------------------------------------
   */
  fprintf(fp, "\n\tinitial state = %s;", InitStr);

  /*-------------------------------------------------------
   * always @ (posedge clock) begin
   *    case (state)
   *-------------------------------------------------------
   */
  fprintf(fp, "\n\talways @ (posedge clock) begin");
  fprintf(fp, "\n\t\tcase (state)");  

  /* for each initial state n2 with label "in1=p  !in3=q...", add entry: 
   *-------------------------------------------------------
   *      Init:
   *         if( sel==0 && in1==p && !in3=q ... ) 
   *            state = n2;
   *         else if( sel==1 && ...) 
   *            state = n3;
   *         else
   *            state = Trap;
   *------------------------------------------------------
   */
  if (InitIdx == -1) {
    fprintf(fp, "\n\t\tInit:");
    sel_cnt = 0;
    st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) {
      int n2 = Ltl_AutomatonVtxGetNodeIdx(vtx);
      LtlSet_t *label = LtlAutomatonVertexGetLabels(vtx);
      
      /* universal label (no label) on n2 */
      if (LtlSetIsEmpty(label)) {
	if (st_count(A->Init) == 1 || sel_num == 0)
	  fprintf(fp,"\n\t\t\tif(1) \n\t\t\t\tstate = n%d;", n2);
	else if (sel_cnt == 0)
	  fprintf(fp,"\n\t\t\tif(sel==%d)\n\t\t\t\tstate = n%d;",
		  sel_cnt++, n2);
	else 
	  fprintf(fp, "\n\t\t\telse if(sel==%d)\n\t\t\t\tstate = n%d;",
		  sel_cnt++, n2);
      }else {
	/* there is at least one label on n2 */
	if (st_count(A->Init) == 1 || sel_num == 0)
	  fprintf(fp, "\n\t\t\tif(");
	else if (sel_cnt==0)
	  fprintf(fp, "\n\t\t\tif(sel==%d && ", sel_cnt++);
	else 
	  fprintf(fp, "\n\t\t\telse if(sel==%d && ", sel_cnt++);
	
	isFirst = 1;
	for (i=0; i<array_n(A->labelTable); i++) {
	  if (LtlSetGetElt(label, i)) {
	    Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *,
					     A->labelTable, i);
	    formulaString = Ctlsp_FormulaConvertToString(F);
	    normalString = StringNormalize(formulaString);
	    FREE(formulaString);
	    
	    if (isFirst)
	      isFirst = 0;
	    else
	      fprintf(fp, " && ");
	    
	    fprintf(fp, "%s", normalString);
	    FREE(normalString);
	  }
	}
	fprintf(fp, ")\n\t\t\t\tstate = n%d;", n2);
      }
    }      
    fprintf(fp, "\n\t\t\telse\n\t\t\t\tstate = Trap;");
  }
  
  /* for each edge (n1, n2) with n2 labelled "in1=p !in3=q...", add entry: 
   *-------------------------------------------------------     
   *      n1:
   *         if( sel==0 && in1==p && !in3=q ... ) 
   *            state = n2;
   *         else if( sel==1 && ...) 
   *            state = n3;
   *         else
   *            state = Trap;
   *-------------------------------------------------------
   */
  foreach_vertex(A->G, lsgen, vtx) {
    int n1 = Ltl_AutomatonVtxGetNodeIdx(vtx);
    int outDegree = lsLength(g_get_out_edges(vtx));
    fprintf(fp, "\n\t\tn%d:", n1);
    sel_cnt = 0;
    foreach_out_edge(vtx, lsgen2, edge) {
      int n2 = Ltl_AutomatonVtxGetNodeIdx(g_e_dest(edge));
      LtlSet_t *label =   LtlAutomatonVertexGetLabels(g_e_dest(edge));
	  
      /* universal label (no label) on n2 */
      if (LtlSetIsEmpty(label)) {
	if (outDegree == 1 || sel_num == 0)
	  fprintf(fp, "\n\t\t\tif(1) \n\t\t\t\tstate = n%d;", n2);
	else if (sel_cnt == 0)
	  fprintf(fp, "\n\t\t\tif(sel==%d) \n\t\t\t\tstate = n%d;",
		  sel_cnt++, n2);
	else 
	  fprintf(fp, "\n\t\t\telse if(sel==%d)\n\t\t\t\tstate = n%d;",
		  sel_cnt++, n2);
      }else {  
	/* at least 1 label on n2 */
	if (outDegree == 1 || sel_num == 0)
	  fprintf(fp, "\n\t\t\tif(");
	else if (sel_cnt==0)
	  fprintf(fp, "\n\t\t\tif(sel==%d && ", sel_cnt++);
	else 
	  fprintf(fp, "\n\t\t\telse if(sel==%d && ", sel_cnt++);
	
	isFirst = 1;
	for (i=0; i<array_n(A->labelTableNegate); i++) {
	  if (LtlSetGetElt(label, i)) {
	    Ctlsp_Formula_t *F = array_fetch(Ctlsp_Formula_t *,
					     A->labelTable, i);
	    formulaString = Ctlsp_FormulaConvertToString(F);
	    normalString = StringNormalize(formulaString);
	    FREE(formulaString);
	    
	    if (isFirst)  isFirst = 0;
	    else fprintf(fp, " && ");
	    
	    fprintf(fp, "%s", normalString);
	    FREE(normalString);
	  }
	}
	fprintf(fp, ")\n\t\t\t\tstate = n%d;", n2);
      }
    }      
    fprintf(fp, "\n\t\t\telse\n\t\t\t\tstate = Trap;");
  }
  
  /*-------------------------------------------------------
   *        default: state = Trap;
   *      endcase
   *    end
   * endmodule
   *-------------------------------------------------------
   */
  fprintf(fp, "\n\t\tdefault: state = Trap;\n\t\tendcase\n\tend\nendmodule\n");
  
  /* free the name array */
  array_free(InputNames);
  for(i=0; i<array_n(Name2LabelIdx); i++) {
    st_table *tmptbl = array_fetch(st_table *, Name2LabelIdx, i);
    st_free_table(tmptbl);
  }
  array_free(Name2LabelIdx);
  
  return result;
}

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

  Synopsis    [Translate the automaton to SMV file.]

  Description [The Hrc_Manager may or may not be provided. If not, the blifmv
  file generated is not complete (inputs are assummed to be boolean.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Ltl_AutomatonToSmv(
  FILE *fp,             
  Ntk_Network_t *network,
  Ltl_Automaton_t *A)     
{
    return 1;
}

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


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

  Synopsis    [Return a array of all the inputnames of the automaton.]
  
  Description [InputNames and Name2LabelIdx are two "array_t" provided by the
  caller. InputNames will be filled by all the labels on the automaton nodes;
  Each item of Name2LabelIdx is a "st_table" from a label to all the related
  formulae in A->labelTable that contains the label.]
  
  SideEffects []

******************************************************************************/
static void
AutomatonGetInputNames(
  Ltl_Automaton_t *A,
  array_t *InputNames,
  array_t *Name2LabelIdx)
{
  st_table *Visited = st_init_table(strcmp, st_strhash);
  Ctlsp_Formula_t *F;
  Ctlsp_FormulaType F_type;
  long i, index, counter;

  counter = 0;
  for (i=0; i<array_n(A->labelTable); i++) {
    /* get the positive formula string */
    F = array_fetch(Ctlsp_Formula_t *, A->labelTable, i);
    F_type = Ctlsp_FormulaReadType(F);
    /* if it's not an AP (just a propositional formula), skip ... */
    if (F_type != Ctlsp_NOT_c && F_type != Ctlsp_ID_c)
      continue;
    if (F_type == Ctlsp_NOT_c) 
      F = Ctlsp_FormulaReadLeftChild(F);
    /* put into the InputNames array */
    if (!st_lookup(Visited, Ctlsp_FormulaReadVariableName(F),&index)){
      st_table *tmptbl = st_init_table(st_numcmp, st_numhash);
      st_insert(tmptbl, (char *) i, (char *)i);
      
      array_insert(st_table *, Name2LabelIdx, counter, tmptbl);
      array_insert(char *, InputNames, counter,
		   Ctlsp_FormulaReadVariableName(F));
      
      st_insert(Visited, Ctlsp_FormulaReadVariableName(F), (char *)counter++);
    }else {
      st_table *tmptbl = array_fetch(st_table *, Name2LabelIdx, index);
      st_insert(tmptbl, (char *)i, (char *)i);
    }
  }
  
  st_free_table(Visited);
}
    
/**Function********************************************************************

  Synopsis    [Return the upper bound number of nondeterministic selectors.]
  
  Description [The automaton is nondeterministic, but the blif_mv file should
  be deterministic. Selector (variable with random output) is used to make
  the .table determinstic. We need to know how many outputs the Selector
  should have. Here we take the maximum out-degree among all nodes as the
  upper bound estimation.] 
  
  SideEffects []

******************************************************************************/
static int
AutomatonCountSelector(
  Ltl_Automaton_t *A)
{
  int sel_num = st_count(A->Init);
  int local_num;
  lsGen lsgen;
  vertex_t *vtx;
  
  foreach_vertex(A->G, lsgen, vtx) {
    local_num = lsLength(g_get_out_edges(vtx));
    if (sel_num < local_num)
      sel_num = local_num;
  }
  
  return sel_num;
}


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

  Synopsis    [Determine if "Init" state is necessary.]
  
  Description [If there exists such a state 'ns', "Init" is not necessary:
  (1) ns  is in Aut->Init
  (2) there is a edge from ns to every state in Aut->Init (including itself)
  In another word, ns is equivalent to "Init".
  (3) there is no edge fron ns to states not in Aut->Init.

  Return the index of the state 'ns' if exist, otherwise return -1.  ]
  
  SideEffects []

******************************************************************************/
static int
AutomatonComputeInitState(
  Ltl_Automaton_t *A)
{
  int initIdx = -1;
  vertex_t *vtx, *vtx2, *s;
  edge_t *e;
  st_generator *stgen, *stgen2;
  lsGen lsgen;

  st_foreach_item(A->Init, stgen, &vtx, NIL(char *)) {
    int isInit = 1;
    /* first, compute the set of sucessors of 'vtx' */
    lsList Img = g_get_out_edges(vtx);
    st_table *uTable = st_init_table(st_ptrcmp, st_ptrhash);
    lsForEachItem(Img, lsgen, e) {
      s = g_e_dest(e);
      st_insert(uTable,  s,  s);
    }
    /* then, test if it is equivalent to 'A->Init': No more, No less */
    st_foreach_item(A->Init, stgen2, &vtx2, NIL(char *)) {
      if (!st_is_member(uTable, vtx2)) {
	isInit = 0;
	st_free_gen(stgen2);
	break;
      }
    }
    if (isInit) {
      st_foreach_item(uTable, stgen2, &vtx2, NIL(char *)) {
	if (!st_is_member(A->Init, vtx2)) {
	  isInit = 0;
	  st_free_gen(stgen2);
	  break;
	}
      }
    }
    st_free_table(uTable);

    if (isInit == 1) {
      initIdx = ((Ltl_AutomatonNode_t *)vtx->user_data)->index;
      st_free_gen(stgen);
      break;
    }
  }
   
  return initIdx;
}

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

  Synopsis    [Given a composite label, return a list of label (each of which
  is a cube.]
  
  Description [The composite label can any combination of !, + , *.]
    
  SideEffects []

******************************************************************************/
/*static lsList
AutomatonLabelGetCubes(
  Ltl_Automaton_t *A,
  LtlSet_t *compositeLabel,
  Ntk_Network_t *network)
{
  LtlTableau_t *tableau = A->tableau;
  int size = tableau->labelIndex;
  LtlSet_t *tempSet, *tempSet2, *tempSet3;
  lsList conjunctList;
  lsList disjunctList;
  lsList tempList, tempList2, tempList3;
  lsGen lsgen, lsgen2;
  int i;

  if (LtlSetIsEmpty(compositeLabel)) {
    tempList = lsCreate();
    lsNewEnd(tempList, (lsGeneric)LtlSetNew(size), (lsHandle *)0);
    return tempList;
  }
  
  first, get a list of disjunctLists (which should be conjoin together
    to form a cartesian product 
   
  conjunctList = lsCreate();
  tempSet = LtlSetNew(size);
  for (i=0; i<size; i++) {
    if (LtlSetGetElt(compositeLabel, i)) {
      if (Ctlsp_LtlFormulaIsAtomicPropositional(tableau->labelTable[i]))
	LtlSetSetElt(tempSet, i);
      else {
	disjunctList = GetCubes_Aux(A, i);
	lsNewEnd(conjunctList, (lsGeneric)disjunctList, (lsHandle *)0);
      }
    }
  }
  if (LtlSetIsEmpty(tempSet))
    LtlSetFree(tempSet);
  else {
    disjunctList = lsCreate();
    lsNewEnd(disjunctList, (lsGeneric)tempSet, (lsHandle *)0);
    lsNewBegin(conjunctList, (lsGeneric)disjunctList, (lsHandle *)0);
  }
    

  compute the cartesian product of the conjuncts 
  while(lsLength(conjunctList)>1) {
    lsList thisList;
    lsList leftList;
    lsList rightList;
    
    lsDelBegin(conjunctList, (lsGeneric *)&leftList);
    lsDelBegin(conjunctList, (lsGeneric *)&rightList);
     form the cartesian product of the two lists 
    thisList = lsCreate();
    lsForEachItem(leftList, lsgen, tempSet) {
      lsForEachItem(rightList, lsgen2, tempSet2) {
	tempSet3 = LtlSetNew(size);
	LtlSetOR(tempSet3, tempSet, tempSet2);
	
	if (0)
	  fprintf(vis_stdout,
		  "tempSet = %d  tempSet2 = %d tempSet3 = %d\n",
		  LtlSetIsEmpty(tempSet),
		  LtlSetIsEmpty(tempSet2),
		  LtlSetIsEmpty(tempSet3));
	
	 if no contradictory, retain it 
	if (LtlSetIsContradictory(tempSet3,tableau->labelTableNegate))
	  LtlSetFree(tempSet3);
	else
	  lsNewEnd(thisList, (lsGeneric)tempSet3, (lsHandle *)0);
      }
    }
    lsDestroy(leftList, (void (*)(lsGeneric))LtlSetFree);
    lsDestroy(rightList, (void (*)(lsGeneric))LtlSetFree);
    
    lsNewBegin(conjunctList, (lsGeneric)thisList, (lsHandle *)0);
  }
  
  lsDelBegin(conjunctList, (lsGeneric *)&tempList);
  lsDestroy(conjunctList, (void(*)(lsGeneric))0);

   remove redundant minterms from 'tempList' 
  tempList3 = lsCreate();
  tempList2 = lsCopy(tempList, (lsGeneric(*)(lsGeneric))0);
  lsForEachItem(tempList, lsgen, tempSet) {
     If tempSet is a superset of other cubes, discard it 
    int flag = 1;
    lsForEachItem(tempList2, lsgen2, tempSet2) {
      if (tempSet != tempSet2 && LtlSetInclude(tempSet, tempSet2)) {
	flag = 0;
	lsFinish(lsgen2);
	break;
      }
    }
    if (!flag) continue;
     If tempSet is an "emptyset" (for example, comtains both
     signal=0 and signal=1, where signal has only these two
      values),  discard it 
     
    flag = 1;
    if (network != NIL(Ntk_Network_t)) {
      Fsm_Fsm_t *fsm = Fsm_NetworkReadOrCreateFsm(network);
      if (fsm != NIL(Fsm_Fsm_t)) {
	mdd_t *minterm = LtlSetModelCheckFormulae(tempSet, 
						  A->labelTable, 
						  fsm);
	flag = !(mdd_is_tautology(minterm, 0));
	mdd_free(minterm);
      }
    }
    if (!flag) continue;
     otherwise, save a copy into tempList3 
    lsNewBegin(tempList3, (lsGeneric)LtlSetCopy(tempSet), (lsHandle *)0); 
  }
  lsDestroy(tempList2, (void(*)(lsGeneric))0);
  lsDestroy(tempList, (void (*)(lsGeneric))LtlSetFree);
  tempList = tempList3;

  return tempList;
}
  */

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

  Synopsis    [Given a index in A->tableau->labelTable, return a list of label
  (each of which  is a cube.]
  
  Description [The formula A->tableau->labelTable[index] can be  any
  combination of !, + , *.]
    
  SideEffects []

******************************************************************************/
static lsList
GetCubes_Aux(
  Ltl_Automaton_t *A,
  int index)
{
  Ctlsp_Formula_t *F = A->tableau->labelTable[index];
  int size = A->tableau->labelIndex;
  lsList leftList;
  lsList rightList;
  lsList thisList =(lsList)0;
  lsGen lsgen, lsgen2;
  LtlSet_t *tempSet, *tempSet2, *tempSet3;
  
  if (Ctlsp_LtlFormulaIsAtomicPropositional(F)) {
    thisList = lsCreate();
    tempSet = LtlSetNew(size);
    LtlSetSetElt(tempSet, Ctlsp_FormulaReadLabelIndex(F));
    lsNewEnd(thisList, (lsGeneric)tempSet, (lsHandle *)0);
  }else {
    Ctlsp_Formula_t *F_left = Ctlsp_FormulaReadLeftChild(F);
    Ctlsp_Formula_t *F_right = Ctlsp_FormulaReadRightChild(F);
    
    switch(Ctlsp_FormulaReadType(F)) {
    case Ctlsp_OR_c:
      leftList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_left));
      rightList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_right));
      /* merge two list together */
      thisList = leftList;
      lsForEachItem(rightList, lsgen, tempSet) {
	lsNewEnd(thisList, (lsGeneric)tempSet, (lsHandle *)0);
      }
      lsDestroy(rightList, (void (*)(lsGeneric))0);
      break;
    case Ctlsp_AND_c:
      leftList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_left));
      rightList = GetCubes_Aux(A, Ctlsp_FormulaReadLabelIndex(F_right));
      /* generate the cartesian product of the two lists */
      thisList = lsCreate();
      lsForEachItem(leftList, lsgen, tempSet) {
	lsForEachItem(rightList, lsgen2, tempSet2) {
	  tempSet3 = LtlSetNew(size);
	  LtlSetOR(tempSet3, tempSet, tempSet2);
	  lsNewEnd(thisList, (lsGeneric)tempSet3, (lsHandle *)0);
	}
      }
      lsDestroy(leftList, (void (*)(lsGeneric))LtlSetFree);
      lsDestroy(rightList, (void (*)(lsGeneric))LtlSetFree);
      break;
    default:
      assert(0);
      break;
    }
  }
  
  return thisList;
}


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

  Synopsis    [Given a string, do the following replacement.]
  
  Description [
  =   =>   ==
  +   =>   ||
  *   =>   &&
  .   =>   _
  <   =>   _
  >   =>   _  ]
    
  SideEffects [The caller should free the result]

******************************************************************************/
static char *
StringNormalize(
  char *inputString)
{
  char *normalString = ALLOC(char, strlen(inputString)*2);
  char *from = inputString;
  char *to = normalString;
  
  while( *from ) {
    switch(*from) {
    case '=':
      *(to++) = '=';
      *(to) = '=';
      break;
    case '+':
      *(to++) = '|';
      *(to) = '|';
      break;
    case '*':
      *(to++) = '&';
      *(to) = '&';
      break;
    case '.':
    case '<':
    case '>':
      *(to) = '_';
      break;
    default:
      *(to) = *from;
    }
    from++;
    to++;
  }
  *to = '\0';
  
  return normalString;
}

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

  Synopsis    [Create the "label" signal in blif_mv format and print out.]
  
  Description [Assume that the label is a propositional formula with *, +, !.
  *
  * For Ctlsp_ID_c/Ctlsp_NOT_c:
  *   .table in1 n1_##_label$AUT
  *   !(RED) 1
  * For Ctlsp_AND_c:
  *   .table n1_#1_label$AUT n1_#2_label$AUT n1_##_label$AUT
  *   1 1  1
  * For Ctlsp_OR_c:
  *   .table n1_#1_label$AUT n1_#2_label$AUT n1_##_label$AUT
  *   1 -  1
  *   - 1  1
  ]
  
  SideEffects []

******************************************************************************/
static void
AutomatonVtxLabelToBlifMv(
  FILE *fp,
  Ltl_Automaton_t *A,
  vertex_t *vtx)
{
    /* each 'compLabel' is a "propositional formulae" */
    LtlSet_t *compositeLabel = LtlAutomatonVertexGetLabels(vtx);
    int idx = Ltl_AutomatonVtxGetNodeIdx(vtx);
    int size = A->tableau->labelIndex;
    int i;
    st_table *CreatedSignals;
	
    if (LtlSetIsEmpty(compositeLabel)) {
	fprintf(fp, "\n.table n%d_label$AUT\n1\n", idx);
	return;
    }
    
    /* first, we should create the signals for each subformula */
    CreatedSignals = st_init_table(st_ptrcmp, st_ptrhash);
    for (i=0; i<size; i++) {
      if (LtlSetGetElt(compositeLabel, i))
	VtxLabelToBlifMv_Aux(fp, A, idx, i, CreatedSignals);
    }
    st_free_table(CreatedSignals);
    
    /* the label signal is the AND or all the conjuncts */
    fprintf(fp, "\n.table ");
    for (i=0; i<size; i++) {
      if (LtlSetGetElt(compositeLabel, i))
	fprintf(fp, "n%d_%d_label$AUT ", idx, i);
    }
    fprintf(fp, "  -> n%d_label$AUT\n.default 0\n", idx);
    for (i=0; i<size; i++) {
      if (LtlSetGetElt(compositeLabel, i))
	fprintf(fp, "1 ");
    }
    fprintf(fp, "1\n");

}

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

  Synopsis    [Create the "label" signal in blif_mv format and print out.]
  
  Description [Assume that "i" is the index in the label table]
  
  SideEffects []

******************************************************************************/
static void
VtxLabelToBlifMv_Aux(
  FILE *fp,
  Ltl_Automaton_t *A,
  int node_idx,
  int index,
  st_table *CreatedSignals)
{
    Ctlsp_Formula_t *F = A->tableau->labelTable[index];
    Ctlsp_Formula_t *F_left, *F_right;
    int l_index, r_index;

    if (st_is_member(CreatedSignals, F))
	return;
    else
	st_insert(CreatedSignals, F, (char *)0);
  
    switch(Ctlsp_FormulaReadType(F)) {
    case Ctlsp_ID_c:
	fprintf(fp, "\n.table %s -> n%d_%d_label$AUT\n.default 0\n%s 1",
		(char *)Ctlsp_FormulaReadVariableName(F),
		node_idx, index,
		(char *)Ctlsp_FormulaReadValueName(F));
	break;
    case Ctlsp_NOT_c:
	F_left = Ctlsp_FormulaReadLeftChild(F);
	fprintf(fp, "\n.table %s -> n%d_%d_label$AUT\n.default 1\n%s 0",
		(char *)Ctlsp_FormulaReadVariableName(F_left),
		node_idx, index,
		(char *)Ctlsp_FormulaReadValueName(F_left));
	break;
    case Ctlsp_AND_c:
	F_left = Ctlsp_FormulaReadLeftChild(F);
	F_right = Ctlsp_FormulaReadRightChild(F);
	l_index = Ctlsp_FormulaReadLabelIndex(F_left);
	r_index = Ctlsp_FormulaReadLabelIndex(F_right);
	VtxLabelToBlifMv_Aux(fp, A, node_idx, l_index, CreatedSignals);
	VtxLabelToBlifMv_Aux(fp, A, node_idx, r_index, CreatedSignals);
	fprintf(fp,"\n.table n%d_%d_label$AUT n%d_%d_label$AUT -> n%d_%d_label$AUT\n.default 0\n1 1 1",
		node_idx, l_index,
		node_idx, r_index,
		node_idx, index);
	break;
    case Ctlsp_OR_c:
	F_left = Ctlsp_FormulaReadLeftChild(F);
	F_right = Ctlsp_FormulaReadRightChild(F);
	l_index = Ctlsp_FormulaReadLabelIndex(F_left);
	r_index = Ctlsp_FormulaReadLabelIndex(F_right);
	VtxLabelToBlifMv_Aux(fp, A, node_idx, l_index, CreatedSignals);
	VtxLabelToBlifMv_Aux(fp, A, node_idx, r_index, CreatedSignals);
	fprintf(fp,
	"\n.table n%d_%d_label$AUT n%d_%d_label$AUT -> n%d_%d_label$AUT\n.default 0\n1 - 1\n- 1 1",
		node_idx, l_index,
		node_idx, r_index,
		node_idx, index);
	break;
    default:
	fail("unkown formula type");
    }
}