src/ltl/ltl.c

Go to the documentation of this file.

#include "ltlInt.h"
#include <errno.h>

static char rcsid[] UNUSED = "$Id: ltl.c,v 1.74 2009/04/11 01:41:30 fabio Exp $";

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

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

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

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static jmp_buf timeOutEnv;


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

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

static int CommandLtlMc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandLtl2Aut(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static LtlMcOption_t * ParseLtlMcOptions(int argc, char **argv);
static LtlMcOption_t * ParseLtlTestOptions(int argc, char **argv);
static boolean LtlMcAtomicFormulaCheckSemantics(Ctlsp_Formula_t *formula, Ntk_Network_t *network, boolean inputsAllowed);
static void TimeOutHandle(void);
static void ShuffleMddIdsToTop(mdd_manager *mddManager, array_t *mddIdArray);

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

void
Ltl_Init(void)
{
  /* LTL model checking. Before using this command, the design must be read
   * and 'init_verify' has been executed.
   */
  Cmd_CommandAdd("ltl_model_check", CommandLtlMc,  0);

  /* Test the LTL->Buechi Automaton Translator, may or may not need to read
   * the design. But If the design is read, the semantic of the formula
   * will be checked on the model before translation
   */
  Cmd_CommandAdd("ltl_to_aut", CommandLtl2Aut, 0);
}


void
Ltl_End(void)
{
}


Ltl_Automaton_t *
Ltl_McFormulaToAutomaton(
  Ntk_Network_t *network,
  Ctlsp_Formula_t *Formula,
  int options_algorithm,
  int options_rewriting,
  int options_prunefair,
  int options_iocompatible,
  int options_directsim,
  int options_reversesim,
  int options_directsimMaximize,
  int options_verbosity,
  int checkSemantics
  )
{
  LtlMcOption_t *options = LtlMcOptionAlloc();
  Ltl_Automaton_t *aut;

  options->algorithm = (Ltl2AutAlgorithm) options_algorithm;
  if (options_algorithm == Ltl2Aut_WRING_c) {
    options->rewriting = 1;
    options->prunefair = 1;
    options->iocompatible = 1;
    options->directsim = 1;
    options->reversesim = 1;
  }else {
    options->rewriting = options_rewriting;
    options->prunefair = options_prunefair;
    options->iocompatible = options_iocompatible;
    options->directsim = options_directsim;
    options->reversesim = options_reversesim;
  }
  options->directsimMaximize = options_directsimMaximize;
  options->verbosity = (Mc_VerbosityLevel) options_verbosity;

  aut = LtlMcFormulaToAutomaton(network, Formula, options, checkSemantics);

  LtlMcOptionFree(options);

  return aut;
}


Hrc_Manager_t *
Ltl_McAutomatonToNetwork(
  Ntk_Network_t *designNetwork,
  Ltl_Automaton_t *automaton,
  int verbosity)
{
  FILE *fp;
  Hrc_Manager_t *buechiHrcMgr;
  Hrc_Node_t    *buechiHrcNode;
  Ntk_Network_t *buechiNetwork;
  int flag;

  /* 1) translate the automaton to a temporary blif_mv file */
  fp = tmpfile();
  if (fp == NIL(FILE)) {
    fail("Aut->Ntk: can't open temp file");
  }
#ifdef DEBUG_LTLMC
  if (verbosity >= 2) {
    fprintf(vis_stdout, "\nPrint the automaton Blif_Mv file:\n");
    flag = Ltl_AutomatonToBlifMv(vis_stdout, designNetwork, automaton);
    fprintf(vis_stdout, "\n");
    fflush(vis_stdout);
  }
#endif
  flag = Ltl_AutomatonToBlifMv(fp, designNetwork, automaton);
  if (!flag) {
    return NIL(Hrc_Manager_t);
  }

  /* 2) read and parse the tmp blifmv file */
  rewind(fp);
  error_init();
  buechiHrcMgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), 0, 0, 0);
  fclose(fp);
  if (buechiHrcMgr == NIL(Hrc_Manager_t))
    fail(error_string());

  /* 3) flatten_hierarchy */
  buechiHrcNode = Hrc_ManagerReadCurrentNode(buechiHrcMgr);
  buechiNetwork = Ntk_HrcNodeConvertToNetwork(buechiHrcNode, TRUE, (lsList)0);
  Hrc_NodeAddApplInfo(buechiHrcNode, NTK_HRC_NODE_APPL_KEY,
                      (Hrc_ApplInfoFreeFn) Ntk_NetworkFreeCallback,
                      (Hrc_ApplInfoChangeFn) NULL,
                      (void *) buechiNetwork);

  /* 4) static_order (!!! using the default mddManager) */
  Ntk_NetworkSetMddManager(buechiNetwork,
                           Ntk_NetworkReadMddManager(designNetwork));
  Ord_NetworkOrderVariables(buechiNetwork,
                            Ord_RootsByDefault_c,
                            Ord_NodesByDefault_c,
                            FALSE,
                            Ord_InputAndLatch_c,
                            Ord_Unassigned_c,
                            (lsList)NULL,
                            0);

  return buechiHrcMgr;
}

boolean
Ltl_FormulaStaticSemanticCheckOnNetwork(
  Ctlsp_Formula_t *formula,
  Ntk_Network_t *network,
  boolean inputsAllowed
  )
{
  boolean lCheck;
  boolean rCheck;
  Ctlsp_Formula_t *leftChild;
  Ctlsp_Formula_t *rightChild;

  if(formula == NIL(Ctlsp_Formula_t)){
    return TRUE;
  }

  if(Ctlsp_FormulaReadType(formula) == Ctlsp_ID_c){
    return LtlMcAtomicFormulaCheckSemantics(formula, network, inputsAllowed);
  }

  leftChild = Ctlsp_FormulaReadLeftChild(formula);
  rightChild = Ctlsp_FormulaReadRightChild(formula);

  lCheck = Ltl_FormulaStaticSemanticCheckOnNetwork(leftChild, network,
                                                   inputsAllowed);
  if(!lCheck)
    return FALSE;

  rCheck = Ltl_FormulaStaticSemanticCheckOnNetwork(rightChild, network,
                                                   inputsAllowed);
  if (!rCheck)
    return FALSE;

  return TRUE;
}


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

Ltl_Automaton_t *
LtlMcFormulaToAutomaton(
  Ntk_Network_t *network,
  Ctlsp_Formula_t *Formula,
  LtlMcOption_t *options,
  int checkSemantics)
{

  char *tmpString;
  Ctlsp_Formula_t *ltlFormula, *negFormula;
  LtlTableau_t *tableau;
  Ltl_Automaton_t *automaton;

  /* check the semantic of the formula on the given network */
  if (checkSemantics && network != NIL(Ntk_Network_t)) {
    if (!network) {
      fprintf(vis_stderr,
              "ltl_mc error: empty network. use flatten_hierarchy\n");
      return NIL(Ltl_Automaton_t);
    }
    error_init();
    if (!Ltl_FormulaStaticSemanticCheckOnNetwork(Formula, network, 1)) {
      fprintf(vis_stderr,
              "ltl_mc error: formula semantic check on design fails:\n%s\n",
              error_string());
      return NIL(Ltl_Automaton_t);
    }
  }

  /* print out the given LTL formula */
  fprintf(vis_stdout, "Formula: ");
  Ctlsp_FormulaPrint(vis_stdout, Formula);
  fprintf(vis_stdout, "\n");

  /* Negate Formula and Expand the abbreaviations */
  negFormula = Ctlsp_FormulaCreate(Ctlsp_NOT_c, Formula, NIL(Ctlsp_Formula_t));
  ltlFormula = Ctlsp_LtlFormulaExpandAbbreviation(negFormula);
  tmpString = Ctlsp_FormulaConvertToString(negFormula);
  FREE(negFormula);
#ifdef DEBUG_LTLMC
  if (options->verbosity)
    fprintf(vis_stdout, "\nNegation Print: %s\n", tmpString);
#endif

  /* 1) Simplify the formula by 'Rewriting' */
  if (options->rewriting) {
    Ctlsp_Formula_t *tmpF = ltlFormula;
    ltlFormula = Ctlsp_LtlFormulaSimpleRewriting(ltlFormula);
    Ctlsp_FormulaFree(tmpF);
  }

  /* create the alph_beta table */
  tableau = LtlTableauGenerateTableau(ltlFormula);
  tableau->verbosity = options->verbosity;
  tableau->algorithm = options->algorithm;
  tableau->booleanmin = options->booleanmin;
#ifdef DEBUG_LTLMC
  /* print out the tableau rules */
  if (options->verbosity > 1)
    LtlTableauPrint(vis_stdout, tableau);
#endif

  /* we dont' need this formula any more */
  Ctlsp_FormulaFree(ltlFormula);


  /* 2) create the automaton */
  automaton = LtlAutomatonGeneration(tableau);
  automaton->name = tmpString;

  /* 3-1) minimize the automaton by Pruning fairness */
  if (options->prunefair) {
#ifdef DEBUG_LTLMC
    if (options->verbosity >= McVerbosityMax_c) {
      Ltl_AutomatonPrint(automaton, options->verbosity);
      fprintf(vis_stdout, "\nPruneF-Minimization:\n");
    }
#endif
    Ltl_AutomatonMinimizeByPrune(automaton, options->verbosity) ;
  }

  /* 3-2) minimize the automaton by I/O compatible and dominance */
  if (options->iocompatible) {
#ifdef DEBUG_LTLMC
    if (options->verbosity >= McVerbosityMax_c) {
      Ltl_AutomatonPrint(automaton, options->verbosity);
      fprintf(vis_stdout, "\nIOC-Minimization:\n");
    }
#endif
    while(Ltl_AutomatonMinimizeByIOCompatible(automaton,options->verbosity));
  }

  /* 3-3) minimize the automaton by Direct Simulation */
  if (options->directsim) {
#ifdef DEBUG_LTLMC
    if (options->verbosity >= McVerbosityMax_c) {
      Ltl_AutomatonPrint(automaton, options->verbosity);
      fprintf(vis_stdout, "\nDirSim-Minimization:\n");
    }
#endif
    Ltl_AutomatonMinimizeByDirectSimulation(automaton, options->verbosity);
  }

  /* 3-4) minimize the automaton by Direct Simulation */
  if (options->reversesim) {
#ifdef DEBUG_LTLMC
    if (options->verbosity >= McVerbosityMax_c) {
      Ltl_AutomatonPrint(automaton, options->verbosity);
      fprintf(vis_stdout, "\nRevSim-Minimization:\n");
    }
#endif
    Ltl_AutomatonMinimizeByReverseSimulation(automaton, options->verbosity);
  }

  /* 3-5) minimize the automaton by Pruning fairness */
  if (options->prunefair) {
#ifdef DEBUG_LTLMC
    if (options->verbosity >= McVerbosityMax_c) {
      Ltl_AutomatonPrint(automaton, options->verbosity);
      fprintf(vis_stdout, "\nPruneF-Minimization:\n");
    }
#endif
    Ltl_AutomatonMinimizeByPrune(automaton, options->verbosity) ;
  }
  /* print out the Buechi automaton */
  if (options->verbosity) {
    Ltl_AutomatonPrint(automaton, options->verbosity);
  }

  return automaton;
}

void
LtlFsmLoadFairness(
  Fsm_Fsm_t *compFsm,
  Fsm_Fairness_t *designFairness,
  int NumberOfFairSets,
  int *AutomatonStrength)
{
  array_t *fairformulaArray;
  Ctlp_Formula_t *F;
  int j;

  /* The fairness constraint on the model (before ltl_model_check is invoked)
   * should be Buechi fairness
   */
  if (!Fsm_FairnessTestIsBuchi(designFairness)) {
    fprintf(vis_stderr, "ltl_mc error: Can not handle non-Buchi Fairness \n");
    assert(0);
  }

  /* store the new fairness constraint (for compFsm) */
  fairformulaArray = array_alloc(Ctlp_Formula_t *, 0);

  /* copy the fairness constraints from the automaton */
  if (*AutomatonStrength == Mc_Aut_Strong_c/*2*/) {
    if (NumberOfFairSets > 0) {
      for (j=0; j<NumberOfFairSets; j++) {
        char tmpstr[30];
        sprintf(tmpstr, "fair%d$AUT$NTK2", j+1);
        F = Ctlp_FormulaCreate(Ctlp_ID_c, (void *)util_strsav(tmpstr),
                               (void *)util_strsav("1"));
        array_insert_last(Ctlp_Formula_t *, fairformulaArray, F);
      }
    }else {
      F = Ctlp_FormulaCreate(Ctlp_ID_c, (void *)util_strsav("fair1$AUT$NTK2"),
                             (void *)util_strsav("1"));
      array_insert_last(Ctlp_Formula_t *, fairformulaArray, F);
    }
  }

  /* copy the fairness constraints on the model */
  for (j=0; j<Fsm_FairnessReadNumConjunctsOfDisjunct(designFairness, 0); j++) {
    F = Fsm_FairnessReadFinallyInfFormula(designFairness, 0, j);
    if (array_n(fairformulaArray) && Ctlp_FormulaReadType(F) == Ctlp_TRUE_c)
      continue;
    array_insert_last(Ctlp_Formula_t *,fairformulaArray, Ctlp_FormulaDup(F));
  }

  /* this is a conservative conclusion ! */
  if (*AutomatonStrength == Mc_Aut_Terminal_c /*0*/) {
    F = array_fetch(Ctlp_Formula_t *, fairformulaArray, 0);
    if (array_n(fairformulaArray) > 1 ||
        Ctlp_FormulaReadType(F) != Ctlp_TRUE_c) {
      *AutomatonStrength = Mc_Aut_Weak_c /*1*/;
    }
  }

  /* update the fairness constraints on 'compFsm' */
  Fsm_FsmFairnessUpdate(compFsm, fairformulaArray);

  array_free(fairformulaArray);
}

LtlMcOption_t *
LtlMcOptionAlloc(void)
{
  LtlMcOption_t *result = ALLOC(LtlMcOption_t, 1);
  if (result == NIL(LtlMcOption_t))
    return NIL(LtlMcOption_t);
  memset(result, 0, sizeof(LtlMcOption_t));

  result->algorithm = Ltl2Aut_WRING_c;
  result->schedule = McGSH_EL_c;
  result->lockstep = MC_LOCKSTEP_OFF;
  result->outputformat = Aut2File_ALL_c;

  return result;
}

void
LtlMcOptionFree(
  LtlMcOption_t *result)
{
  if (result->ltlFile)
    fclose(result->ltlFile);

  if (result->debugFile)
    fclose(result->debugFile);

  if (result->outputfilename)
    FREE(result->outputfilename);

  FREE(result);
}


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

static int
CommandLtlMc(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  array_t *ltlArray;
  LtlMcOption_t *options;
  Ctlsp_Formula_t *ltlFormula;
  Ltl_Automaton_t *automaton;
  LtlTableau_t *tableau;
  Hrc_Manager_t *buechiHrcMgr;
  Hrc_Node_t *designNode;
  Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
  Fsm_Fsm_t *compFsm = NIL(Fsm_Fsm_t);
  Ntk_Network_t *designNetwork,*buechiNetwork = NIL(Ntk_Network_t);
  Ntk_Node_t *node1, *node2;
  array_t *modelCareStatesArray;
  lsGen lsgen2;
  lsList nodeList;
  graph_t *partition, *save_partition;
  mdd_t *fairInitStates, *modelCareStates, *mddOne;
  char *designModelName, *name1;
  int i;
  long startLtlMcTime, endLtlMcTime;
  static int timeOutPeriod = 0;

  Img_ResetNumberOfImageComputation(Img_Both_c);

  if (!(options = ParseLtlMcOptions(argc, argv))) {
    return 1;
  }
  timeOutPeriod = options->timeOutPeriod;

  if (options->dbgLevel != 0 && options->direction == McFwd_c) {
    (void) fprintf(vis_stderr, "** ltl_mc error: -d is incompatible with -F\n");
    LtlMcOptionFree(options);
    return 1;
  }
  if (options->dcLevel !=  McDcLevelRch_c && options->direction == McFwd_c) {
    (void) fprintf(vis_stderr, "** ltl_mc error: -F can only be used with -D1\n");
    LtlMcOptionFree(options);
    return 1;
  }

  /* 'designFsm' and 'designNetwork' are for the model */
  designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  if (designFsm == NIL(Fsm_Fsm_t)) {
    return 1;
  }
  designNetwork = Ntk_HrcManagerReadCurrentNetwork(*hmgr);

  /* Parse LTL formulae */
  ltlArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
  if (ltlArray != NIL(array_t)) {
    array_t *tmpArray = Ctlsp_FormulaArrayConvertToLTL(ltlArray);
    Ctlsp_FormulaArrayFree(ltlArray);
    ltlArray = tmpArray;
  }
  if (ltlArray == NIL(array_t)) {
    (void) fprintf(vis_stderr,
                   "** ltl_mc error: error in parsing formulas from file\n");
    LtlMcOptionFree(options);
    return 1;
  }
  /* Semantic Check of the Ltl formula array on the network */
  arrayForEachItem(Ctlsp_Formula_t *, ltlArray, i, ltlFormula) {
    if (!Ltl_FormulaStaticSemanticCheckOnNetwork(ltlFormula,
                                                 designNetwork, 1)) {
      fprintf(vis_stderr,
              "ltl_mc error: formula semantic check on design fails:\n%s\n",
              error_string());
      Ctlsp_FormulaArrayFree(ltlArray);
      LtlMcOptionFree(options);
      return 1;
    }
  }

  /* Set time out processing (if timeOutPeriod is set) */
  if (timeOutPeriod > 0) {
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout, "# LTL_MC: Ltl modelchecking - timeout occurred after %d seconds.\n", timeOutPeriod);
      (void) fprintf(vis_stdout, "# LTL_MC: data may be corrupted.\n");
      if (options->verbosity > McVerbosityNone_c) {
        (void) fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n", Img_GetNumberOfImageComputation(Img_Forward_c), Img_GetNumberOfImageComputation(Img_Backward_c));
      }
      alarm(0);
      return 1;
    }
  }
  startLtlMcTime = util_cpu_time();

  mddOne = mdd_one(Ntk_NetworkReadMddManager(designNetwork));

  /* Start LTL model checking for each formula */
  for (i=0; i<array_n(ltlArray); i++) {
    st_table *tbl;
    array_t *mddIds;
    lsList rootList;
    int NumberOfFairSet, AutomatonStrength;
    long initialTime, finalTime; /* for checking each formula */
    int nImgComps, nPreComps;

    /* stats */
    if (options->verbosity > McVerbosityNone_c) {
      initialTime = util_cpu_time();
      nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
      nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
    } else {
      /* to remove uninitialized variable warning */
      initialTime = 0;
      nImgComps = 0;
      nPreComps = 0;
    }
    ltlFormula = array_fetch(Ctlsp_Formula_t *, ltlArray, i);

    /*---------------------------------------------------------------------
     * 1) create the Buechi Automaton/Network/Mdd_Order/Partition in a new
     * Hrc_Manager. It shares nothing with the Design but the mddManager.
     *--------------------------------------------------------------------*/
    automaton = LtlMcFormulaToAutomaton(designNetwork, ltlFormula, options, 1);
    assert(automaton != NIL(Ltl_Automaton_t));

    if (options->noStrengthReduction)
      AutomatonStrength = Mc_Aut_Strong_c /*2*/;
    else
      AutomatonStrength = Ltl_AutomatonGetStrength(automaton);

    /* add arcs by Direct Simulation, to reduce the counter-example length */
    if (options->directsimMaximize) {
#ifdef DEBUG_LTLMC
      if (options->verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, options->verbosity);
        fprintf(vis_stdout, "\nDirSim-Maximization:\n");
      }
#endif
      Ltl_AutomatonMaximizeByDirectSimulation(automaton, options->verbosity);
    }
    NumberOfFairSet = lsLength(automaton->Fair);
    buechiHrcMgr = Ltl_McAutomatonToNetwork(designNetwork, automaton,
                                            options->verbosity);
    assert(buechiHrcMgr != NIL(Hrc_Manager_t));
    tableau = automaton->tableau;
    Ltl_AutomatonFree((gGeneric) automaton);
    LtlTableauFree(tableau);
    buechiNetwork =  Ntk_HrcManagerReadCurrentNetwork(buechiHrcMgr);

    /*---------------------------------------------------------------------
     * 2) build (M x A) by attaching buechiNetwork(A) to designNetwork(M).
     * The result network M x A (designNetwork) shares some data with the
     * buechiNetwork (Variables, and Tables). The newly created nodes in
     * designNetwork retain their MddId in buechiNetwork
     *--------------------------------------------------------------------*/
    /* 2-a) Retrieve the Model (in the default hrc_manager) */
    designNode = Hrc_ManagerReadCurrentNode(*hmgr);
    designModelName = Hrc_NodeReadModelName(designNode);
    /* 2-b) Attach buechiNetwork to designNetwork */
    tbl = st_init_table(strcmp, st_strhash);
    Ntk_NetworkAppendNetwork(designNetwork, buechiNetwork, tbl);
    st_free_table(tbl);

    /* Here we have the choice of incrementally build the partition,
     * or build it from scratch. In both cases, the original partition
     * will be saved (and restored later)
     */
    if (!options->noIncrementalPartition) {
      rootList = lsCreate();
      mddIds = array_alloc(int, 2);
      /* 2-c) Assign MddId to the newly-created nodes */
      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
        if (!Ntk_NodeTestIsPrimaryInput(node2)) {
          name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
          node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
          Ntk_NodeSetMddId(node1, Ntk_NodeReadMddId(node2));
          if (!strcmp(name1, "state$AUT$NTK2"))
            array_insert(int, mddIds, 1, Ntk_NodeReadMddId(node1));
          else if (!strcmp(name1, "state$AUT$NS$NTK2"))
            array_insert(int, mddIds, 0, Ntk_NodeReadMddId(node1));
          else if (!strcmp(name1, "selector$AUT$NTK2"))
            array_insert(int, mddIds, 2, Ntk_NodeReadMddId(node1));
          FREE(name1);
          if (Ntk_NodeTestIsCombOutput(node1))
            lsNewEnd(rootList, (lsGeneric)node1, (lsHandle *)0);
        }
      }
      /* move the automaton variables to the top most -- this is believed
       * to be an optimal ordering */
      if (!options->noShuffleToTop)
        ShuffleMddIdsToTop(Ntk_NetworkReadMddManager(designNetwork), mddIds);
      array_free(mddIds);

      /* 2-d) Create the Partition information for (M x A) */
      save_partition = Part_NetworkReadPartition(designNetwork);
      partition = Part_PartitionDuplicate(save_partition);
      Part_UpdatePartitionFrontier(designNetwork, partition, rootList,
                                   (lsList)0, mddOne);
      Ntk_NetworkSetApplInfo(designNetwork, PART_NETWORK_APPL_KEY,
                             (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                             (void *)partition);
      lsDestroy(rootList, (void (*)(lsGeneric))0);

    }else {
      mddIds = array_alloc(int, 2);
      /* 2-c) Assign MddId to the newly-created nodes */
      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
        if (Ntk_NodeTestIsPrimaryInput(node2))  continue;
        name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
        node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
        Ntk_NodeSetMddId(node1, Ntk_NodeReadMddId(node2));
        if (!strcmp(name1, "state$AUT$NTK2"))
          array_insert(int, mddIds, 1, Ntk_NodeReadMddId(node1));
        else if (!strcmp(name1, "state$AUT$NS$NTK2"))
          array_insert(int, mddIds, 0, Ntk_NodeReadMddId(node1));
        else if (!strcmp(name1, "selector$AUT$NTK2"))
          array_insert(int, mddIds, 2, Ntk_NodeReadMddId(node1));
        FREE(name1);
      }
      /* move the automaton variables to the top most. This might be the
       * best BDD variable ordering for (M x A)! */
      if (!options->noShuffleToTop)
        ShuffleMddIdsToTop(Ntk_NetworkReadMddManager(designNetwork), mddIds);
      array_free(mddIds);

      /* 2-d) Create the Partition information for (M x A) */
      nodeList = lsCreate();
      partition = Part_NetworkCreatePartition(designNetwork,
                                              designNode,
                                              designModelName,
                                              (lsList)0,
                                              (lsList)0,
                                              NIL(mdd_t),
                                              Part_Default_c,
                                              nodeList,
                                              FALSE, 0, 0);
      save_partition = Part_NetworkReadPartition(designNetwork);
      Ntk_NetworkSetApplInfo(designNetwork, PART_NETWORK_APPL_KEY,
                             (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                             (void *)partition);

      lsDestroy(nodeList, (void (*)(lsGeneric))0);
    }

    /*---------------------------------------------------------------------
     * 3) Create the FSM for (M x A) and load Fairness constraints
     *--------------------------------------------------------------------*/
    /* try to get a reduced Fsm (w.r.t. each individual property) first */
    {
      array_t *ctlArray = array_alloc(Ctlp_Formula_t *, 0);
      Ctlp_Formula_t *ctlF = Ctlp_FormulaCreate(Ctlp_ID_c,
                                                util_strsav("state$AUT$NTK2"),
                                                util_strsav("Trap"));
      array_insert(Ctlp_Formula_t *, ctlArray, 0, ctlF);
      compFsm = Mc_ConstructReducedFsm(designNetwork, ctlArray);
      Ctlp_FormulaFree(ctlF);
      array_free(ctlArray);
      if (compFsm == NIL(Fsm_Fsm_t))
        compFsm = Fsm_FsmCreateFromNetworkWithPartition(designNetwork,
                                                        NIL(graph_t));
    }
    /* merge fairnesses from outside and those from the automaton ... */
    LtlFsmLoadFairness(compFsm, Fsm_FsmReadFairnessConstraint(designFsm),
                       NumberOfFairSet, &AutomatonStrength);


    /*---------------------------------------------------------------------
     * 4) Language emptiness checking (store result if necessary)
     *--------------------------------------------------------------------*/
    if (options->dcLevel == McDcLevelArdc_c) {
      Fsm_ArdcOptions_t *ardcOptions = Fsm_ArdcAllocOptionsStruct();
      array_t *tmpArray;
      long startRchTime;
      Fsm_ArdcGetDefaultOptions(ardcOptions);
      startRchTime = util_cpu_time();
      tmpArray =
        Fsm_ArdcComputeOverApproximateReachableStates(compFsm, 0,
                                                      options->verbosity,
                                                      0, 0, 0, 0, 0, 0,
                                                      ardcOptions);
      modelCareStatesArray = mdd_array_duplicate(tmpArray);
      FREE(ardcOptions);
      if (options->verbosity > McVerbosityNone_c)
        Fsm_ArdcPrintReachabilityResults(compFsm,
                                         util_cpu_time() - startRchTime);
    }else if (options->dcLevel >= McDcLevelRch_c) {
      long startRchTime;
      startRchTime = util_cpu_time();
      modelCareStates =
        Fsm_FsmComputeReachableStates(compFsm, 0, options->verbosity, 0, 0,
                                      (options->lockstep != MC_LOCKSTEP_OFF),
                                      0, 0, Fsm_Rch_Default_c, 0, 0,
                                      NIL(array_t), FALSE, NIL(array_t));
      if (options->verbosity > McVerbosityNone_c) {
        Fsm_FsmReachabilityPrintResults(compFsm,
                                        util_cpu_time() - startRchTime,
                                        Fsm_Rch_Default_c);
      }
      modelCareStatesArray = array_alloc(mdd_t *, 0);
      array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
    } else {
      modelCareStates = mdd_one(Fsm_FsmReadMddManager(compFsm));
      modelCareStatesArray = array_alloc(mdd_t *, 0);
      array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
    }
    /*
    Fsm_MinimizeTransitionRelationWithReachabilityInfo(compFsm,
                                                       Img_Backward_c,
                                                       options->verbosity > 1);
    */

    /* language emptiness checking */
    fairInitStates = Mc_FsmCheckLanguageEmptiness(compFsm,
                                                  modelCareStatesArray,
                                                  (Mc_AutStrength_t) AutomatonStrength,
                                                  options->leMethod,
                                                  options->dcLevel,
                                                  options->dbgLevel,
                                                  options->printInputs,
                                                  options->verbosity,
                                                  options->schedule,
                                                  options->direction,
                                                  options->lockstep,
                                                  options->debugFile,
                                                  options->useMore,
                                                  options->simValue,
                                                  "LTL_MC");
    mdd_array_free(modelCareStatesArray);

    if (fairInitStates)
      mdd_free(fairInitStates);

    /*---------------------------------------------------------------------
     * 5) Remove 'A' from designNetwork (M x A), which contains 3 steps:
     * a) free compFsm/partition
     * b) remove newly-created nodes from designNetwork;
     * c) destory buechiHrcMgr (buechiNetwork)
     *--------------------------------------------------------------------*/
    Ntk_NetworkAddApplInfo(designNetwork, PART_NETWORK_APPL_KEY,
                           (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                           (void *)save_partition);
    Fsm_FsmFree(compFsm);
    {
      int tmpi, tmpj;
      Ntk_Node_t *node3, *node4;
      /* first, remove the newly-added A nodes ('xxxlabel$AUT$NTK2') from the
       * fanout list of the M nodes */
      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
        if (strstr(Ntk_NodeReadName(node2), "label$AUT") == NULL)
          continue;
        name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
        node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
        FREE(name1);
        assert(node1);
        Ntk_NodeForEachFanin(node1, tmpi, node3) {
          array_t *oldFanouts = Ntk_NodeReadFanouts(node3);
          array_t *newFanouts;
          if (oldFanouts != NIL(array_t)) {
            newFanouts = array_alloc(Ntk_Node_t *, 0);
            arrayForEachItem(Ntk_Node_t *, oldFanouts, tmpj, node4) {
              if (node4 != node1)
                array_insert_last(Ntk_Node_t *, newFanouts, node4);
            }
            Ntk_NodeSetFanouts(node3, newFanouts);
          }
        }
      }
      /* Now we can safely remove all the newly-added A nodes */
      Ntk_NetworkForEachNode(buechiNetwork, lsgen2, node2) {
        if (Ntk_NodeTestIsPrimaryInput(node2))  continue;
        name1 = util_strcat3(Ntk_NodeReadName(node2),"$NTK2", "");
        node1 = Ntk_NetworkFindNodeByName(designNetwork, name1);
        FREE(name1);
        Ntk_NodeRemoveFromNetwork(designNetwork, node1, 1, 1, 0);
        Ntk_NodeFree(node1);
      }
    }
    Ntk_NetworkSetMddManager(buechiNetwork, (mdd_manager *)0);
    Hrc_ManagerFree(buechiHrcMgr);

    if (options->verbosity > McVerbosityNone_c) {
      finalTime = util_cpu_time();
      fprintf(vis_stdout, "-- ltl_mc time = %10g\n",
        (double)(finalTime - initialTime) / 1000.0);
      fprintf(vis_stdout,
              "-- %d image computations and %d preimage computations\n",
              Img_GetNumberOfImageComputation(Img_Forward_c) - nImgComps,
              Img_GetNumberOfImageComputation(Img_Backward_c) - nPreComps);
    }
  }

  /* Print stats if verbose. */
  endLtlMcTime = util_cpu_time();
  if (options->verbosity > McVerbosityNone_c) {
    fprintf(vis_stdout, "-- total ltl_mc time: %10g\n",
            (double)(endLtlMcTime-startLtlMcTime)/1000.0);
    fprintf(vis_stdout,
            "-- total %d image computations and %d preimage computations\n",
            Img_GetNumberOfImageComputation(Img_Forward_c),
            Img_GetNumberOfImageComputation(Img_Backward_c));
  }

  /* Clean-ups */
  Ctlsp_FormulaArrayFree(ltlArray);
  LtlMcOptionFree(options);
  mdd_free(mddOne);

  alarm(0);
  return 0;             /* normal exit */
}

static int
CommandLtl2Aut(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  array_t        *ltlArray;
  Ctlsp_Formula_t        *ltlFormula;
  LtlTableau_t           *tableau;
  Ltl_Automaton_t        *automaton;
  int            i;
  LtlMcOption_t *options;
  int            verbosity = 0;   /* verbosity level */
  int            algorithm = 0;   /* translation algorithm */
  int            rewriting = 0;   /* simplify Formula by rewriting */
  int            booleanmin = 0;  /* boolean minimization */
  int            prunefair = 0;   /* prune fairness */
  int            iocompatible = 0;/* simplify by io-compatible */
  int            directsim = 0;   /* simplify by Direct simulation */
  int            reversesim = 0;  /* simplify by reverse simulation */
  int            directsimMaximize = 0;   /* simplify by Direct simulation */
  Ntk_Network_t  *network;
  char  *tmpString;
  long           beginTime, finalTime;


  if (!(options = ParseLtlTestOptions(argc, argv))) {
    return 1;
  }
  rewriting = options->rewriting;
  verbosity = options->verbosity;
  algorithm = options->algorithm;
  booleanmin = options->booleanmin;
  prunefair = options->prunefair;
  iocompatible = options->iocompatible;
  directsim = options->directsim;
  reversesim = options->reversesim;
  directsimMaximize = options->directsimMaximize;

  beginTime = util_cpu_time();
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);

  /* Parse the LTL Formulae */
  ltlArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
  if (ltlArray != NIL(array_t)) {
    array_t *tmpArray = Ctlsp_FormulaArrayConvertToLTL(ltlArray);
    Ctlsp_FormulaArrayFree(ltlArray);
    ltlArray = tmpArray;
  }
  if (ltlArray == NIL(array_t)) {
    (void) fprintf(vis_stderr,
                   "** ltl_to_aut error: error in parsing formulas file\n");
    LtlMcOptionFree(options);
    return 1;
  }

  /* For each LTL formula, build a Buechi automaton ... */
  for (i=0; i<array_n(ltlArray); i++) {
    ltlFormula = array_fetch(Ctlsp_Formula_t *, ltlArray, i);
    tmpString = Ctlsp_FormulaConvertToString(ltlFormula);

    /* expand the abbreaviations */
    ltlFormula = Ctlsp_LtlFormulaExpandAbbreviation(ltlFormula);
    fprintf(vis_stdout, "\nFormula: %s\n", tmpString);

    /* 1) Simplify the formula by 'Rewriting' */
    if (rewriting) {
      Ctlsp_Formula_t *tmpF = ltlFormula;
      ltlFormula = Ctlsp_LtlFormulaSimpleRewriting(ltlFormula);
      tmpString = Ctlsp_FormulaConvertToString(ltlFormula);
      Ctlsp_FormulaFree(tmpF);
    }

    /* create the alph_beta table */
    tableau = LtlTableauGenerateTableau(ltlFormula);
    tableau->verbosity = verbosity;
    tableau->algorithm = algorithm;
    tableau->booleanmin = booleanmin;
    /* print out the tableau rules */
    if (verbosity >= McVerbosityMax_c)
      LtlTableauPrint(vis_stdout, tableau);

    /* 2) create the automaton */
    automaton = LtlAutomatonGeneration(tableau);
    automaton->name = tmpString;

    /* 3) minimize the automaton by Pruning fairness */
    if (prunefair) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nPruneF-Minimization:\n");
      }
      Ltl_AutomatonMinimizeByPrune(automaton, verbosity) ;
    }

    /* 4) minimize the automaton by I/O compatible and dominance */
    if (iocompatible) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nIOC-Minimization:\n");
      }
      while(Ltl_AutomatonMinimizeByIOCompatible(automaton, verbosity));
    }

    /* 5) minimize the automaton by Direct Simulation */
    if (directsim) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nDirSim-Minimization:\n");
      }
      Ltl_AutomatonMinimizeByDirectSimulation(automaton, verbosity);
    }

    /* 6) minimize the automaton by Reverse Simulation */
    if (reversesim) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nRevSim-Minimization:\n");
      }
      Ltl_AutomatonMinimizeByReverseSimulation(automaton, verbosity);
    }

    /* 7/3) minimize the automaton by Pruning fairness */
    if (prunefair) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nPruneF-Minimization:\n");
      }
      Ltl_AutomatonMinimizeByPrune(automaton, verbosity) ;
    }

    /* 8) add arcs by Direct Simulation, to reduce counter-example length */
    if (directsimMaximize) {
      if (verbosity >= McVerbosityMax_c) {
        Ltl_AutomatonPrint(automaton, verbosity);
        fprintf(vis_stdout, "\nDirSim-Maximization:\n");
      }
      Ltl_AutomatonMaximizeByDirectSimulation(automaton, verbosity);
    }

    /* print out the Buechi automaton */
    Ltl_AutomatonPrint(automaton, verbosity+1);

    /* write the automaton in a file in the proper format */
    if (options->outputfilename) {
      FILE *fp;
      fp = Cmd_FileOpen( options->outputfilename, (char *)((i==0)?"w":"a"),
                         NIL(char *), 0);
      if (options->outputformat == Aut2File_DOT_c)
        Ltl_AutomatonToDot(fp, automaton, 0);
      else if (options->outputformat == Aut2File_BLIFMV_c)
        Ltl_AutomatonToBlifMv(fp, network, automaton);
      else if (options->outputformat == Aut2File_VERILOG_c)
        Ltl_AutomatonToVerilog(fp, network, automaton);
      else {
        Ltl_AutomatonToDot(fp, automaton, 0);
        Ltl_AutomatonToBlifMv(fp, network, automaton);
        Ltl_AutomatonToVerilog(fp, network, automaton);
      }
      fclose(fp);
    }

    /* Clean-ups: the current formula*/
    Ltl_AutomatonFree((gGeneric) automaton);
    LtlTableauFree(tableau);
    Ctlsp_FormulaFree(ltlFormula);
  }

  /* Clean-ups */
  Ctlsp_FormulaArrayFree(ltlArray);
  LtlMcOptionFree(options);

  finalTime = util_cpu_time();
  fprintf(vis_stdout, "# LTL_TO_AUT time: %10g\n",
          (double)(finalTime-beginTime)/1000.0);

  return 0;             /* normal exit */
}


static LtlMcOption_t *
ParseLtlMcOptions(
  int argc,
  char **argv)
{
  LtlMcOption_t *options = LtlMcOptionAlloc();
  char *ltlFileName = (char *)0;
  char *debugOutName = (char *)0;
  Mc_GSHScheduleType schedule = McGSH_EL_c;
  Mc_FwdBwdAnalysis direction = McBwd_c;
  int lockstep = MC_LOCKSTEP_OFF;
  int c;

  if (options == NIL(LtlMcOption_t))
    return NIL(LtlMcOption_t);
  options->leMethod = Mc_Le_Default_c;
  options->dcLevel = McDcLevelRch_c;
  options->noStrengthReduction = 0;
  options->noIncrementalPartition = 0;

  /* Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "a:bd:f:t:A:D:v:S:L:FhimsXYM")) != EOF) {
    switch(c) {
    case 'a':
      options->algorithm = (Ltl2AutAlgorithm) atoi(util_optarg);
      if (options->algorithm < 0 || options->algorithm > 3)
        goto usage;
      break;
    case 'b':
      options->booleanmin = 1;
      break;
    case 'd':
      options->dbgLevel = (LtlMcDbgLevel) atoi(util_optarg);
      break;
    case 'f':
      debugOutName = util_strsav(util_optarg);
      break;
    case 't':
      options->timeOutPeriod = atoi(util_optarg);
      break;
    case 'A':
      options->leMethod = (Mc_LeMethod_t) atoi(util_optarg);
      break;
    case 'D':
      options->dcLevel = (Mc_DcLevel) atoi(util_optarg);
      break;
    case 'v':
      options->verbosity = (Mc_VerbosityLevel) atoi(util_optarg);
      break;
    case 'S' :
      schedule = Mc_StringConvertToScheduleType(util_optarg);
      break;
    case 'L' :
      lockstep = Mc_StringConvertToLockstepMode(util_optarg);
      break;
    case 'F' :
      direction = McFwd_c;
      break;
    case 'i':
      options->printInputs = 1;
      break;
    case 'm':
      options->useMore = TRUE;
      break;
    case 's' :
      options->simValue = TRUE;
      break;
    case 'X':
      options->noStrengthReduction = 1;
      break;
    case 'Y':
      options->noIncrementalPartition = 1;
      break;
    case 'Z':
      options->noShuffleToTop = 1;
      break;
    case 'M':
      options->directsimMaximize = 1;
      break;
    case 'h':
      goto usage;
    default:
      goto usage;
    }
  }
  if (options->algorithm == Ltl2Aut_WRING_c) {
    options->rewriting =    TRUE;
    options->prunefair =    TRUE;
    options->directsim =    TRUE;
    options->reversesim =   TRUE;
    options->iocompatible = TRUE;
  }

  if (schedule == McGSH_Unassigned_c) {
    (void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
    goto usage;
  } else {
    options->schedule = schedule;
  }
  if (lockstep == MC_LOCKSTEP_UNASSIGNED) {
    (void) fprintf(vis_stderr, "invalid lockstep option: %s\n", util_optarg);
    goto usage;
  } else {
    options->lockstep = lockstep;
  }
  options->direction = direction;

  /* Open the ltl file.
   */
  if (argc - util_optind == 0) {
    (void) fprintf(vis_stderr, "** ltl_mc error: file containing ltl formulae not provided\n");
    goto usage;
  }
  else if (argc - util_optind > 1) {
    (void) fprintf(vis_stderr, "** ltl_mc error: too many arguments\n");
    goto usage;
  }
  ltlFileName = util_strsav(argv[util_optind]);

  /* Read LTL Formulae */
  if (!ltlFileName)
    goto usage;
  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
  if (options->ltlFile == NIL(FILE)) {
    (void) fprintf(vis_stdout,  "** ltl_mc error: error in opening file %s\n", ltlFileName);
    FREE(ltlFileName);
    LtlMcOptionFree(options);
    return NIL(LtlMcOption_t);
  }
  FREE(ltlFileName);

  if (debugOutName != NIL(char)) {
    options->debugFile = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
    if (options->debugFile == NIL(FILE)) {
      (void) fprintf(vis_stdout,"** ltl_mc error: error in opening file %s\n", debugOutName);
      FREE(debugOutName);
      LtlMcOptionFree(options);
      return NIL(LtlMcOption_t);
    }
    FREE(debugOutName);
  }

  return options;

 usage:
  (void) fprintf(vis_stderr, "usage: ltl_model_check [-a ltl2aut_algorithm][-b][-d dbg_level][-f dbg_file][-h][-i][-m][-s][-t period][-v verbosity_level][-A le_method][-D dc_level][-L lockstep_mode][-S schedule][-F][-X][-Y][-M] <ltl_file>\n");
  (void) fprintf(vis_stderr, "    -a <ltl2aut_algorithm>\n");
  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 0 => GPVW\n");
  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 1 => GPVW+\n");
  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 2 => LTL2AUT\n");
  (void) fprintf(vis_stderr, "        ltl2aut_algorithm = 3 => WRING (Default)\n");
  (void) fprintf(vis_stderr, "    -b \tUse boolean minimization in automaton generation\n");
  (void) fprintf(vis_stderr, "    -d <dbg_level>\n");
  (void) fprintf(vis_stderr, "        debug_level = 0 => no debugging (Default)\n");
  (void) fprintf(vis_stderr, "        debug_level = 1 => automatic debugging\n");
  (void) fprintf(vis_stderr, "    -f <dbg_out>\n");
  (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
  (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
  (void) fprintf(vis_stderr, "    -m \tPipe debugger output through the UNIX utility more.\n");
  (void) fprintf(vis_stderr, "    -s \tWrite error trace in sim format.\n");
  (void) fprintf(vis_stderr, "    -v <verbosity_level>\n");
  (void) fprintf(vis_stderr, "        verbosity_level = 0 => no feedback (Default)\n");
  (void) fprintf(vis_stderr, "        verbosity_level = 1 => code status\n");
  (void) fprintf(vis_stderr, "        verbosity_level = 2 => code status and CPU usage profile\n");
  (void) fprintf(vis_stderr, "    -t <period> time out period\n");
  (void) fprintf(vis_stderr, "    -A <le_method>\n");
  (void) fprintf(vis_stderr, "        le_method = 0 => no use of Divide and Compose (Default)\n");
  (void) fprintf(vis_stderr, "        le_method = 1 => use Divide and Compose\n");
  (void) fprintf(vis_stderr, "    -D <dc_level>\n");
  (void) fprintf(vis_stderr, "        dc_level = 0 => no use of don't cares\n");
  (void) fprintf(vis_stderr, "        dc_level = 1 => use unreached states as don't cares (Default)\n");
  (void) fprintf(vis_stderr, "        dc_level = 2 => use unreached states as don't cares\n");

  (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
  (void) fprintf(vis_stderr, "        dc_level = 3 => use over-approximate unreached states as don't cares\n");
  (void) fprintf(vis_stderr, "                        and aggressive use of DC's to simplify MDD's\n");
  (void) fprintf(vis_stderr, "    -L <lockstep_mode>\n");
  (void) fprintf(vis_stderr, "       lockstep_mode is one of {off,on,all,n}\n");
  (void) fprintf(vis_stderr, "    -S <schedule>\n");
  (void) fprintf(vis_stderr, "       schedule is one of {EL,EL1,EL2,budget,random,off}\n");
  (void) fprintf(vis_stderr, "    -F \tUse forward analysis in fixpoint computation.\n");
  (void) fprintf(vis_stderr, "    -X \tDisable strength reduction (using different decision procedure \n");
  (void) fprintf(vis_stderr, "       \tfor strong, weak, terminal automaton).\n");
  (void) fprintf(vis_stderr, "    -Y \tDisable incremental partition of the composed system (M x A).\n");
  (void) fprintf(vis_stderr, "    -Z \tAdd arcs into the Buechi automaton by direct simulation relation.\n");

  (void) fprintf(vis_stderr, "    -M \tAdd arcs to the automaton to reduce counter-example length.\n");
  (void) fprintf(vis_stderr, "    <ltl_file> The input file containing LTL formulae to be checked.\n");
  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");

  LtlMcOptionFree(options);
  return NIL(LtlMcOption_t);
}

static LtlMcOption_t *
ParseLtlTestOptions(
  int argc,
  char **argv)
{
  LtlMcOption_t *options = LtlMcOptionAlloc();
  char *ltlFileName = (char *)0;
  int c;

  if (options == NIL(LtlMcOption_t))
    return NIL(LtlMcOption_t);

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "wbpdMrif:m:v:o:t:h")) != EOF) {
    switch(c) {
    case 'w':
      options->rewriting = 1;
      break;
    case 'b':
      options->booleanmin = 1;
      break;
    case 'p':
      options->prunefair = 1;
      break;
    case 'd':
      options->directsim = 1;
      break;
    case 'M':
      options->directsimMaximize = 1;
      break;
    case 'r':
      options->reversesim = 1;
      break;
    case 'i':
      options->iocompatible = 1;
      break;
    case 'f':
      ltlFileName = util_strsav(util_optarg);
      break;
    case 'm':
      options->algorithm = (Ltl2AutAlgorithm) atoi(util_optarg);
      break;
    case 'v':
      options->verbosity = (Mc_VerbosityLevel) atoi(util_optarg);
      break;
    case 'o':
      options->outputfilename = util_strsav(util_optarg);
      break;
    case 't':
      options->outputformat = (Aut2FileType) atoi(util_optarg);
      break;
    case 'h':
      goto usage;
    default:
      goto usage;
    }
  }

  /* 'Wring' is equivalent to
  *    LTL2AUT +
  *    rewriting +
  *    prunefair + directsim + reversesim + iocompatible
  */
  if (options->algorithm ==3) {
    options->rewriting = 1;
    options->prunefair = 1;
    options->directsim = 1;
    options->reversesim = 1;
    options->iocompatible = 1;
  }

  /* Read LTL Formulae */
  if (!ltlFileName)
    goto usage;

  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
  FREE(ltlFileName);
  if (options->ltlFile == NIL(FILE)) {
    (void) fprintf(vis_stdout,  "** ltl_to_aut error: error in opening file %s\n", ltlFileName);
    LtlMcOptionFree(options);
    return NIL(LtlMcOption_t);
  }

  return options;

  usage:
  (void) fprintf(vis_stderr, "usage: ltl_to_aut <-f ltl_file> [-m algorithm] [-o output_file] [-t output_format] [-w] [-b] [-p] [-d] [-r] [-i] [-M] [-v verbosity_level] [-h]\n");
  (void) fprintf(vis_stderr, "    -f <ltl_file>\n");
  (void) fprintf(vis_stderr, "       The input file containing LTL formulae\n");
  (void) fprintf(vis_stderr, "    -m <algorithm>\n");
  (void) fprintf(vis_stderr, "        algorithm = 0 => GPVW\n");
  (void) fprintf(vis_stderr, "        algorithm = 1 => GPVW+\n");
  (void) fprintf(vis_stderr, "        algorithm = 2 => LTL2AUT\n");
  (void) fprintf(vis_stderr, "        algorithm = 3 => Wring (default)\n");
  (void) fprintf(vis_stderr, "    -o <output_file>\n");
  (void) fprintf(vis_stderr, "       Write the automata to output_file\n");
  (void) fprintf(vis_stderr, "    -t <output_format>\n");
  (void) fprintf(vis_stderr, "        output_format = 0 => dot\n");
  (void) fprintf(vis_stderr, "        output_format = 1 => blif_mv\n");
  (void) fprintf(vis_stderr, "        output_format = 2 => verilog\n");
  (void) fprintf(vis_stderr, "        output_format = 3 => all (default)\n");
  (void) fprintf(vis_stderr, "    -w \tRewriting the formula\n");
  (void) fprintf(vis_stderr, "    -b \tBoolean minimization \n");
  (void) fprintf(vis_stderr, "    -p \tPruning the fairness\n");
  (void) fprintf(vis_stderr, "    -d \tDirect-simulation minimization\n");
  (void) fprintf(vis_stderr, "    -r \tReverse-simulation minimization\n");
  (void) fprintf(vis_stderr, "    -i \tI/O compatible minimization\n");
  (void) fprintf(vis_stderr, "    -M \tAdd arcs by direct-simulation to reduce the counter-example length\n");
  (void) fprintf(vis_stderr, "    -v <verbosity>\n");
  (void) fprintf(vis_stderr, "       \tVerbosity can be 0,1,2,3\n");
  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");

  LtlMcOptionFree(options);
  return NIL(LtlMcOption_t);
}


static boolean
LtlMcAtomicFormulaCheckSemantics(
  Ctlsp_Formula_t *formula,
  Ntk_Network_t *network,
  boolean inputsAllowed)
{
  char *nodeNameString = Ctlsp_FormulaReadVariableName( formula );
  char *nodeValueString = Ctlsp_FormulaReadValueName( formula );
  Ntk_Node_t *node = Ntk_NetworkFindNodeByName( network, nodeNameString );

  Var_Variable_t *nodeVar;
  int nodeValue;

  if ( !node ) {
    error_append("Could not find node corresponding to the name\n\t- ");
    error_append( nodeNameString );
    return FALSE;
  }

  nodeVar = Ntk_NodeReadVariable( node );
  if ( Var_VariableTestIsSymbolic( nodeVar ) ){
    nodeValue = Var_VariableReadIndexFromSymbolicValue( nodeVar, nodeValueString );
    if ( nodeValue == -1 ) {
      error_append("Value specified in RHS is not in domain of variable\n");
      error_append( Ctlsp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlsp_FormulaReadValueName( formula ) );
      return FALSE;
    }
  }
  else {
    int check;

    check = Cmd_StringCheckIsInteger(nodeValueString, &nodeValue);
    if( check==0 ) {
      error_append("Value in the RHS is illegal\n");
      error_append( Ctlsp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlsp_FormulaReadValueName( formula ) );
      return FALSE;
    }
    if( check==1 ) {
      error_append("Value in the RHS is out of range of int\n");
      error_append( Ctlsp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlsp_FormulaReadValueName( formula ) );
      return FALSE;
    }
    if ( !(Var_VariableTestIsValueInRange( nodeVar, nodeValue ) ) ) {
      error_append("Value specified in RHS is not in domain of variable\n");
      error_append( Ctlsp_FormulaReadVariableName( formula ) );
      error_append("=");
      error_append( Ctlsp_FormulaReadValueName( formula ) );
      return FALSE;
    }
  }

  if(!inputsAllowed){
    boolean coverSupport;
    lsGen tmpGen;
    Ntk_Node_t *tmpNode;
    st_table *supportNodes    = st_init_table(st_ptrcmp, st_ptrhash);
    array_t *thisNodeArray = array_alloc( Ntk_Node_t *, 0);

    array_insert_last( Ntk_Node_t *, thisNodeArray, node );
    Ntk_NetworkForEachNode(network, tmpGen, tmpNode) {
      if (Ntk_NodeTestIsConstant(tmpNode) || Ntk_NodeTestIsLatch(tmpNode)) {
        st_insert(supportNodes,  tmpNode, NIL(char));
      }
    }

    coverSupport = Ntk_NetworkTestLeavesCoverSupportOfRoots(network,
                                                            thisNodeArray,
                                                            supportNodes);
    array_free(thisNodeArray);
    st_free_table(supportNodes);

    if ( coverSupport == FALSE ) {
      char *tmpString =
        util_strcat3( "\nNode ", nodeNameString,
                      " is not driven only by latches and constants.\n");
      error_append(tmpString);
      return FALSE;
    }
  }

  return TRUE;
}

static void
TimeOutHandle(void)
{
  longjmp(timeOutEnv, 1);
}

static void
ShuffleMddIdsToTop(mdd_manager *mddManager, array_t *mddIdArray)
{
  array_t *mvar_list = mdd_ret_mvar_list(mddManager);
  int *invPermArray = ALLOC(int, bdd_num_vars(mddManager));
  int invPermIndex, i, j, bvarId, mddId, result;
  st_table *stored = st_init_table(st_ptrcmp, st_ptrhash);
  mvar_type mvar;

  /* put mddId on the top most */
  invPermIndex = 0;
  arrayForEachItem(int, mddIdArray, j, mddId) {
    if (mddId == 0) continue;
    mvar = array_fetch(mvar_type, mvar_list, mddId);
    for (i = 0; i<mvar.encode_length; i++) {
      bvarId = mdd_ret_bvar_id(&mvar, i);
      invPermArray[invPermIndex++] = bvarId;
      st_insert(stored, (char *) (long) bvarId, (char *)0);
    }
  }
  /* shift every one else down */
  for (i = 0; (unsigned) i< bdd_num_vars(mddManager); i++) {
    bvarId = bdd_get_id_from_level(mddManager, i);
    if (!st_is_member(stored, (char *) (long) bvarId)) {
      invPermArray[invPermIndex++] = bvarId;
    }
  }
  /* call bdd_shuffle */
  result = bdd_shuffle_heap(mddManager, invPermArray);
#ifdef DEBUG_LTLMC
  if (result)
    fprintf(vis_stdout, "\nShuffle automaton vars to the top: success!\n");
  else
    fprintf(vis_stdout, "\nShuffle automaton vars to the top: failure!\n");
#endif

  /* Clean up */
  st_free_table(stored);
  FREE(invPermArray);
}