source: vis_dev/vis-2.3/src/mc/mcCmd.c

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

  FileName    [mcCmd.c]

  PackageName [mc]

  Synopsis    [Functions for CTL model checking commands.]

  Description [This file contains the functions implementing the CTL
  model checking commands.]

  SeeAlso     []

  Author      [Adnan Aziz, Tom Shiple, Rajeev Ranjan, In-Ho Moon,
  Roderick Bloem, and others]

  Copyright   [Copyright (c) 2002-2005, Regents of the University of Colorado

  All rights reserved.

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

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

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

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

#include "ctlpInt.h"
#include "grab.h"
#include "puresat.h"
#include "mcInt.h"


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

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

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

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

#ifndef lint
static char rcsid[] UNUSED = "$Id: mcCmd.c,v 1.27 2009/04/11 01:43:30 fabio Exp $";
#endif

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

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

static jmp_buf timeOutEnv;
static int mcTimeOut;           /* timeout value */
static long alarmLapTime;       /* starting CPU time for timeout */

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

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

static int CommandMc(Hrc_Manager_t **hmgr, int argc, char **argv);
static McOptions_t * ParseMcOptions(int argc, char **argv);
static int CommandLe(Hrc_Manager_t **hmgr, int argc, char **argv);
static McOptions_t * ParseLeOptions(int argc, char **argv);
static int CommandInv(Hrc_Manager_t **hmgr, int argc, char **argv);
static McOptions_t * ParseInvarOptions(int argc, char **argv);
static void TimeOutHandle(void);
static int UpdateResultArray(mdd_t *reachableStates, array_t *invarStatesArray, int *resultArray);
static void PrintInvPassFail(array_t *invarFormulaArray, int *resultArray);

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

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


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

  Synopsis [Initialize mc package]

  SideEffects []

******************************************************************************/
void
Mc_Init(void)
{
  Cmd_CommandAdd("model_check", CommandMc, /* doesn't changes_network */ 0);
  Cmd_CommandAdd("check_invariant", CommandInv, /* doesn't changes_network */ 0);
  Cmd_CommandAdd("lang_empty", CommandLe, /* doesn't changes_network */ 0);
  Cmd_CommandAdd("_init_state_formula", McCommandInitState, /* doesn't changes_network */ 0);
}


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

  Synopsis [End mc package]

  SideEffects []

******************************************************************************/
void
Mc_End(void)
{
}

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


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


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

  Synopsis [Check CTL formulas given in file are modeled by flattened network]

  CommandName [model_check]

  CommandSynopsis [perform fair CTL model checking on a flattened network]

  CommandArguments [ \[-b\] \[-c\] \[-d <dbg_level>\]
  \[-f <dbg_file>\] \[-g <hints_file>\] \[-h\] \[-i\] \[-m\] \[-r\]
  \[-t <time_out_period>\]\[-v <verbosity_level>\]
  \[-D <dc_level>\] \[-F\] \[-S <schedule>\] \[-V\] \[-B\] \[-I\]
  \[-C\] \[-w  <node_file>\] \[-W\] \[-G\] <ctl_file>]

  CommandDescription [Performs fair CTL model checking on a flattened
  network.  Before calling this command, the user should have
  initialized the design by calling the command <A
  HREF="init_verifyCmd.html"> <code> init_verify</code></A>.
  Regardless of the options, no 'false positives' or 'false negatives'
  will occur: the result is correct for the given circuit.  <p>

  Properties to be verified should be provided as CTL formulas in the
  file <code>ctl_file</code>.  Note that the support of any wire
  referred to in a formula should consist only of latches.  For the
  precise syntax of CTL formulas, see the <A
  HREF="../ctl/ctl/ctl.html"> VIS CTL and LTL syntax manual</A>.  <p>

  Properties of the form <code> AG f</code>, where  <code>f</code> is a formula not
  involving path quantifiers are referred to as invariants; for such properties
  it may be substantially faster to use the <A HREF="check_invariantCmd.html">
  <code> check_invariant</code></A> command.
  <p>

  A fairness constraint can be specified by invoking the
  <A HREF="read_fairnessCmd.html"><code>read_fairness</code></A> command;
  if none is specified, all paths are taken to be fair.
  If some initial states
  do not lie on a fair path, the model checker prints a message to this effect.
  <p>

  A formula passes iff it is true for all initial states of the
  system.  Therefore, in the presence of multiple initial states, if a
  formula fails, the negation of the formula may also fail.<p>

  If a formula does not pass, a (potentially partial) proof of failure
  (referred to as a debug trace) is demonstrated. Fair paths are
  represented by a finite sequence of states (the stem) leading to a
  fair cycle, i.e. a cycle on which there is a state from each
  fairness condition. The level of detail of the proof can be
  specified (see option <code>-d</code>). <p>

  Both backward (future tense CTL formulas) and forward (past tense CTL
  formulas) model checking can be performed. Forward model checking is
  based on Iwashita's ICCAD96 paper. Future tense CTL formulas are
  automatically converted to past tense ones as much as possible in
  forward model checking. <p>

  Command options:
  <p>

  <dl>

  <dt> -b
  <dd> Use backward analysis when performing debugging; the default is
  to use forward analysis. This should be tried when the debugger spends a
  large amount of time when creating a path to a fair cycle. This option is not
  compatible with forward model checking option (-F).</dd><p>

  <dt> -c
  <dd> Use the formula tree so that there is no sharing of sub-formulae among
  the formulae in the input file. This option is useful in the following
  scenario - formulae A, B and C are being checked in order and there is
  sub-formula sharing between A and C. If the BDDs corresponding to the shared
  sub-formula is huge then computation for B might not be able to finish
  without using this option.
  </dd><p>

  <dt> -d <code> &lt;dbg_level&gt; </code> <dd> Specify the amount of
  debugging performed when the system fails a formula being checked.
  Note that it may not always be possible to give a simple
  counter-example to show that a formula is false, since this may
  require enumerating all paths from a state.  In such a case the
  model checker will print a message to this effect.  This option is
  incompatible with -F.</dd>  <p>
  <dd> <code> dbg_level</code> must be one of the following:

  <p><code>0</code>: No debugging performed.
  <code>dbg_level</code>=<code>0</code> is the default.

  <p><code>1</code>: Debugging with minimal output: generate counter-examples
  for universal formulas (formulas of the form <code>AX|AF|AU|AG</code>) and
  witnesses for existential formulas (formulas of the form
  <code>EX|EF|EU|EG</code>).  States on a path are not further analyzed.

  <p><code>2</code>: Same as <code>dbg_level</code>=<code>1</code>, but more
  verbose. (The subformulas are printed, too.)

  <p><code>3</code>: Maximal automatic debugging: as for level <code>1</code>,
  except that states occurring on paths will be recursively analyzed.

  <p><code>4</code>: Manual debugging: at each state, the user is queried if
  more feedback is desired.
  </dd>

  <p>

  <dt> -f &lt;<code>dbg_file</code>&gt;
  <dd> Write the debugger output to <code>dbg_file</code>.
  This option is incompatible with -F.
  Notes: when you use -d4 (interactive mode), -f is not recommended, since you
  can't see the output of vis on stdout.</dd>

  <dt> -g &lt;<code>hints_file</code>&gt; <dd> Use guided search.  The file
  <code>hints_file</code> contains a series of hints.  A hint is a formula that
  does not contain any temporal operators, so <code>hints_file</code> has the
  same syntax as a file of invariants used for check_invariant.  The hints are
  used in the order given to change the transition relation.  In the case of
  least fixpoints (EF, EU), the transition relation is conjoined with the hint,
  whereas for greatest fixpoints the transition relation is disjoined with the
  negation of the hint.  If the hints are cleverly chosen, this may speed up
  the computation considerably, because a search with the changed transition
  relation may be much simpler than one with the original transition relation,
  and results obtained can be reused, so that we may never have to do a
  complicated search with the original relation.  Note: hints in terms of
  primary inputs are not useful for greatest fixpoints.  See also: Ravi and
  Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and
  Somenzi, Efficient Decision Procedures for Model Checking of Linear Time
  Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search
  for CTL Model Checking, DAC'00.

  <p>For formulae that contain both least and greatest fixpoints, the
  behavior depends on the flag <code>guided_search_hint_type</code>.
  If it is set to local (default) then every subformula is evaluated
  to completion, using all hints in order, before the next subformula
  is started.  For pure ACTL or pure ECTL formulae, we can also set
  guided_search_hint_type to global, in which case the entire formula
  is evaluated for one hint before moving on to the next hint, using
  underapproximations.  The description of the options for guided
  search can be found in the help page for
  print_guided_search_options.

  <p>model_check will call reachability without any guided search, even
  if -g is used.  If you want to perform reachability with guided
  search, call rch directly.

  <p>Incompatible with -F.</dd>

  <dt> -h
  <dd> Print the command usage.</dd>
  <p>

  <dt> -i
  <dd> Print input values causing transitions between states during debugging.
  Both primary and pseudo inputs are printed.
  This option is incompatible with -F.</dd>
  <p>

  <dt> -m
  <dd> Pipe debugger output through the UNIX utility  more.
  This option is incompatible with -F.</dd>
  <p>

  <dt> -r
  <dd> Reduce the FSM derived from the flattened network with respect to each
  formula being checked. By default, the FSM is reduced with respect to the
  conjunction of the formulae in the input file. If this option is used and
  don't cares are being used for simplification, then subformula sharing is
  disabled (result might be incorrect otherwise).</dd>
  <p>

  <dd> The truth of  a formula may be independent of parts of the network
  (such as when wires have been abstracted; see
  <A HREF="flatten_hierarchyCmd.html"><code>flatten_hierarchy</code></A>).
  These parts are effectively removed when this option is invoked; this may
  result in more efficient model checking.</dd>
  <p>

  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
  <dd> Specify the time out period (in seconds) after which the command
  aborts. By default this option is set to infinity.</dd>
  <p>

  <dt> -v  <code>&lt;verbosity_level&gt;</code>
  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage
  and code status.

  <br><code>verbosity_level</code>  must be one of the following:<p>

  <code>0</code>: No feedback provided. This is the default.<p>

  <code>1</code>: Feedback on code location.<p>

  <code>2</code>: Feedback on code location and CPU usage.</dd><p>

  <dt> -B
  <dd> Check for vacuously passing formulae using the algorithm of Beer et al.
  (CAV97).  The algorithm applies to a subset of ACTL (w-ACTL) and replaces
  the smallest important subformula of a passing property with either FALSE
  or TRUE depending on its negation parity.  It then applies model checking
  to the resulting witness formula.  If the witness formula also passes, then
  the original formula is deemed to pass vacuously.  If the witness formula
  fails, a counterexample to it provides an interesting witness to the
  original passing formula.  See the CAV97 paper for the definitions of
  w-ACTL, important subformula, and interesting witness.  In short, one of the
  operands of a binary operator in a w-ACTL formula must be a propositional
  formula.  See also the -V option.
  </dd><p>

  <dt> -C
  <dd> Compute coverage of all observable signals in a set of CTL formulae
  using the algorithm of Hoskote, Kam, Ho, Zhao (DAC'99). If the verbosity
  level (-v option) is equal to 0, only the coverage stats are printed. If
  verbosity level is greater than zero, then detailed information of the
  computation at each step of the algorithm is also provided.
  Debug information is provided in the form of states not covered for each
  observable signal if the dbg_level (-d option) is greater than 0. The number
  of states printed is set by the vis environment variable
  'nr_uncoveredstates'. By default the number of states printed is 1.
  The value of nr_uncoveredstates can be set using the set command.
  See also the -I option.</dd>
  <p>

  <dt> -D <code> &lt;dc_level&gt; </code>

  <dd> Specify extent to which don't cares are used to simplify MDDs in model
  checking.  Don't cares are minterms on which the values taken by functions
  do not affect the computation; potentially, these minterms can be used to
  simplify MDDs and reduce the time taken to perform model checking.  The -g
  flag for guided search does not affect the way in which the don't-care
  conditions are computed.

  <br>
  <code> dc_level </code> must be one of the following:
  <p>

  <code> 0 </code>: No don't cares are used.

  <p> <code> 1 </code>: Use unreachable states as don't cares. This is the
  default.

  <p> <code> 2 </code>: Use unreachable states as don't cares and in the EU
  computation, use 'frontiers' for image computation.<p>

  <code> 3 </code>: First compute an overapproximation of the reachable states
  (ARDC), and use that as the cares set.  Use `frontiers' for image
  computation.  For help on controlling options for ARDC, look up help on the
  command: <A HREF="print_ardc_optionsCmd.html">print_ardc_options</A>. Refer
  to Moon, Jang, Somenzi, Pixley, Yuan, "Approximate Reachability Don't Cares
  for {CTL} Model Checking", ICCAD98, and to two papers by Cho et al, IEEE TCAD
  December 1996: one is for State Space Decomposition and the other is for
  Approximate FSM Traversal.</dd>
  <p>

  <dt> -F
  <dd> Use forward model checking based on Iwashita's method in ICCAD96.
  Future tense CTL formulas are automatically converted to past tense
  ones as much as possible. Converted forward formulas are printed when
  verbosity is greater than 0. Debug options (-b, -d, -f, -i, and -m)
  are ignored with this option. We have seen that forward model checking
  was much faster than backward in many cases, also forward was much slower
  than backward in many cases.</dd>
  <p>

  <dt> -I
  <dd> Compute coverage of all observable signals in a set of CTL formulae
  using an improved algorithm of Jayakumar, Purandare, Somenzi (DAC'03). If
  the verbosity level (-v option) is equal to 0, only the coverage stats are
  printed. If verbosity level is greater than zero, then detailed information
  of the computation at each step of the algorithm is also provided.
  Debug information is provided in the form of states not covered for each
  observable signal if the dbg_level (-d option) is greater than 0. The number
  of states printed is set by the vis environment variable
  'nr_uncoveredstates'. By default the number of states printed is 1.
  The value of nr_uncoveredstates can be set using the set command.
  Compared to the -C option, this one produces more accurate results and deals
  with a larger subset of CTL.</dd>
  <p>

  <dt> -S <code> &lt;schedule&gt; </code>

  <dd> Specify schedule for GSH algorithm, which generalizes the
  Emerson-Lei algorithm and is used to compute greatest fixpoints.
  The choice of schedule affects the sequence in which EX and EU
  operators are applied.  It makes a difference only when fairness
  constraints are specified.

  <br>
  <code> &lt;schedule&gt; </code> must be one of the following:

  <p> <code> EL </code>: EU and EX operators strictly alternate.  This
  is the default.

  <p> <code> EL1 </code>: EX is applied once for every application of all EUs.

  <p> <code> EL2 </code>: EX is applied repeatedly after each application of
  all EUs.

  <p> <code> budget </code>: a hybrid of EL and EL2.

  <p> <code> random </code>: enabled operators are applied in
  (pseudo-)random order.

  <p> <code> off </code>: GSH is disabled, and the old algorithm is
  used instead.  The old algorithm uses the <code> EL </code> schedule, but
  the termination checks are less sophisticated than in GSH.</dd>
  <p>

  <dt> -V
  <dd> Check for vacuously passing formulae with the algorithm
  of Purandare and Somenzi (CAV2002).  The algorithm applies to all of
  CTL, and to both passing and failing properties.  It says whether a
  passing formula may be strengthened and still pass, and whether a
  failing formula may be weakened and still fail.  It considers all
  leaves of a formula that are under one negation parity (e.g., not
  descendants of a XOR or EQ node) for replacement by either TRUE or
  FALSE.  See also the -B option.
  </dd><p>


  <dt> -w  &lt;<code>node_file</code>&gt;

  This option invoked the algorithm to generate an error trace divided
  into fated and free segements. Fate represents the inevitability and
  free is asserted when there is no inevitability. This can be formulated
  as a two-player concurrent reachability game. The two players are
  the environment and the system. The node_file is given to specify the
  variables the are controlled by the system.

  <dt> -W <dt>

  This option represents the case that all input variables are controlled
  by system.

  <dt> -G <dt>

  We proposed two algorithm to generate segemented counter example.
  They are general and restrcited algorithm. Bu default we use restricted
  algorithm. We can invoke general algorithm with -G option.

  For more information, please check the STTT'04
  paper of Jin et al., "Fate and Free Will in Error Traces" <p>

  <dt> <code> &lt;ctl_file&gt; </code>

  <dd> File containing CTL formulas to be model checked.
  </dl>

  Related "set" options:
  <dl>
  <dt> ctl_change_bracket &lt;yes/no&gt;
  <dd> Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names,
  therefore CTL parser does the same thing. However, in some cases a user
  does not want to change node names in CTL parsing. Then, use this set
  option by giving "no". Default is "yes".
  <p>
  <dt>guided_search_hint_type</dt> <dd>Switches between local and
  global hints (see the -g option, or the help page for set).
  </dl>

  See also commands : approximate_model_check, incremental_ctl_verification
  ]

  Description [First argument is a file containing a set of CTL formulas - see
  ctlp package for grammar. Second argument is an FSM that we will check the
  formulas on. Formulas are checked by calling the recursive function
  Mc_ModelCheckFormula. When the formula fails, the debugger is invoked.]

  Comment [Ctlp creates duplicate formulas when converting to
  existential form; e.g.  when converting AaUb. We aren't using this
  fact, which leads to some performance degradation.

  A system satisfies a formula if all its initial states are in the satisfying
  set of the formula.  Hence, we do not need to continue the computation if we
  know that all initial states are in the satisfying set, or if there are
  initial states that we are sure are not in the satisfying set.  This is what
  early termination does: it supplies an extra termination condition for the
  fixpoints that kicks in when we can decide the truth of the formula.  Note
  that this leads to some nasty consequences in storing the satisfying sets.
  A computation that has terminated early does not yield the exact satisfying
  set, and hence we can not always reuse this result when there is subformula
  sharing.]

  SideEffects []

  SeeAlso [CommandInv]

******************************************************************************/
static int
CommandMc(
  Hrc_Manager_t **hmgr,
  int argc,
  char **argv)
{
 /* options */
  McOptions_t         *options;
  Mc_VerbosityLevel   verbosity;
  Mc_DcLevel          dcLevel;
  FILE                *ctlFile;
  int                 timeOutPeriod     = 0;
  Mc_FwdBwdAnalysis   traversalDirection;
  int                 buildOnionRings   = 0;
  FILE                *guideFile;
  FILE                *systemFile;
  Mc_GuidedSearch_t   guidedSearchType  = Mc_None_c;
  Ctlp_FormulaArray_t *hintsArray       = NIL(Fsm_HintsArray_t);
  array_t             *hintsStatesArray = NIL(array_t); /* array of mdd_t* */
  st_table            *systemVarBddIdTable;
  boolean             noShare           = 0;
  Mc_GSHScheduleType  GSHschedule;
  boolean             checkVacuity;
  boolean             performCoverageHoskote;
  boolean             performCoverageImproved;

  /* CTL formulae */
  array_t *ctlArray;
  array_t *ctlNormalFormulaArray;
  int i;
  int numFormulae;
  /* FSM, network and image */
  Fsm_Fsm_t       *totalFsm = NIL(Fsm_Fsm_t);
  Fsm_Fsm_t       *modelFsm = NIL(Fsm_Fsm_t);
  Fsm_Fsm_t       *reducedFsm = NIL(Fsm_Fsm_t);
  Ntk_Network_t   *network;
  mdd_t           *modelCareStates = NIL(mdd_t);
  array_t         *modelCareStatesArray = NIL(array_t);
  mdd_t           *modelInitialStates;
  mdd_t           *fairStates;
  Fsm_Fairness_t  *fairCond;
  mdd_manager     *mddMgr;
  array_t         *bddIdArray;
  Img_ImageInfo_t *imageInfo;
  Mc_EarlyTermination_t *earlyTermination;
  /* Coverage estimation */
  mdd_t           *totalcoveredstates = NIL(mdd_t);
  array_t         *signalTypeList = array_alloc(int,0);
  array_t         *signalList = array_alloc(char *,0);
  array_t         *statesCoveredList = array_alloc(mdd_t *,0);
  array_t         *newCoveredStatesList = array_alloc(mdd_t *,0);
  array_t         *statesToRemoveList = array_alloc(mdd_t *,0);

  /* Early termination is only partially implemented right now.  It needs
     distribution over all operators, including limited cases of temporal
     operators.  That should be relatively easy to implement. */

  /* time keeping */
  long totalInitialTime; /* for model checking */
  long initialTime, finalTime; /* for model checking */

  error_init();
  Img_ResetNumberOfImageComputation(Img_Both_c);

  /* read options */
  if (!(options = ParseMcOptions(argc, argv))) {
    return 1;
  }
  verbosity = McOptionsReadVerbosityLevel(options);
  dcLevel = McOptionsReadDcLevel(options);
  ctlFile = McOptionsReadCtlFile(options);
  timeOutPeriod = McOptionsReadTimeOutPeriod(options);
  traversalDirection = McOptionsReadTraversalDirection(options);
  buildOnionRings =
    (McOptionsReadDbgLevel(options) != McDbgLevelNone_c || verbosity);
  noShare = McOptionsReadUseFormulaTree(options);
  GSHschedule = McOptionsReadSchedule(options);
  checkVacuity = McOptionsReadVacuityDetect(options);
   /* for the command mc -C foo.ctl */
  performCoverageHoskote = McOptionsReadCoverageHoskote(options);
  /* for the command mc -I foo.ctl */
  performCoverageImproved = McOptionsReadCoverageImproved(options);

  /* Check for incompatible options and do some option-specific
   * intializations.
   */

  if (traversalDirection == McFwd_c) {
    if (checkVacuity) {
      fprintf(vis_stderr, "** mc error: -V and -B are incompatible with -F\n");
      McOptionsFree(options);
      return 1;
    }
    if (performCoverageHoskote || performCoverageImproved) {
      fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -F\n");
      McOptionsFree(options);
      return 1;
    }
  }

  if (checkVacuity) {
    if (performCoverageHoskote || performCoverageImproved) {
      fprintf(vis_stderr, "** mc error: -I and -C are incompatible with -V and -B\n");
      McOptionsFree(options);
      return 1;
    }
  }

  guideFile =  McOptionsReadGuideFile(options);

  if(guideFile != NIL(FILE) ){
    guidedSearchType = Mc_ReadGuidedSearchType();
    if(guidedSearchType == Mc_None_c){  /* illegal setting */
      fprintf(vis_stderr, "** mc error: Unknown  hint type\n");
      fclose(guideFile);
      McOptionsFree(options);
      return 1;
    }

    if(traversalDirection == McFwd_c){  /* illegal combination */
      fprintf(vis_stderr, "** mc error: -g is incompatible with -F\n");
      fclose(guideFile);
      McOptionsFree(options);
      return 1;
    }

    if(Img_UserSpecifiedMethod() != Img_Iwls95_c &&
       Img_UserSpecifiedMethod() != Img_Monolithic_c &&
       Img_UserSpecifiedMethod() != Img_Mlp_c){
      fprintf(vis_stderr, "** mc error: -g only works with iwls95, MLP, or monolithic image methods.\n");
      fclose(guideFile);
      McOptionsFree(options);
      return 1;
    }

    hintsArray = Mc_ReadHints(guideFile);
    fclose(guideFile); guideFile = NIL(FILE);
    if( hintsArray == NIL(array_t) ){
      McOptionsFree(options);
      return 1;
    }

  } /* if guided search */

  /* If don't-cares are used, -r implies -c.  Note that the satisfying
     sets of a subformula are only in terms of propositions therein
     and their cone of influence.  Hence, we can share satisfying sets
     among formulae.  I don't quite understand what the problem with
     don't-cares is (RB) */
  if (McOptionsReadReduceFsm(options))
    if (dcLevel != McDcLevelNone_c)
      McOptionsSetUseFormulaTree(options, TRUE);

  if (traversalDirection == McFwd_c &&
      McOptionsReadDbgLevel(options) != McDbgLevelNone_c) {
    McOptionsSetDbgLevel(options, McDbgLevelNone_c);
    (void)fprintf(vis_stderr, "** mc warning : option -d is ignored.\n");
  }

  /* Read CTL formulae */
  ctlArray = Ctlsp_FileParseCTLFormulaArray(ctlFile);
  fclose(ctlFile); ctlFile = NIL(FILE);
  if (ctlArray == NIL(array_t)) {
    (void) fprintf(vis_stderr,
                   "** mc error: error in parsing formulas from file\n");
    McOptionsFree(options);
    return 1;
  }

  /* read network */
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    fprintf(vis_stdout, "%s\n", error_string());
    error_init();
    Ctlp_FormulaArrayFree(ctlArray);
    McOptionsFree(options);
    return 1;
  }

  /* read fsm */
  totalFsm = Fsm_NetworkReadOrCreateFsm(network);
  if (totalFsm == NIL(Fsm_Fsm_t)) {
    fprintf(vis_stdout, "%s\n", error_string());
    error_init();
    Ctlp_FormulaArrayFree(ctlArray);
    McOptionsFree(options);
    return 1;
  }

  /* Assign variables to system if doing FAFW */
  systemVarBddIdTable = NIL(st_table);
  systemFile = McOptionsReadSystemFile(options);
  if (systemFile != NIL(FILE)) {
    systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile);
    fclose(systemFile); systemFile = NIL(FILE);
    if (systemVarBddIdTable == (st_table *)-1 ) { /* FS: error message? */
      Ctlp_FormulaArrayFree(ctlArray);
      McOptionsFree(options);
      return 1;
    }
  } /* if FAFW */

  if(options->FAFWFlag && systemVarBddIdTable == 0) {
    systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm);
  }

  if (verbosity > McVerbosityNone_c)
    totalInitialTime = util_cpu_time();
  else /* to remove uninitialized variable warning */
    totalInitialTime = 0;

  if(traversalDirection == McFwd_c){
    mdd_t *totalInitialStates;
    double nInitialStates;

    totalInitialStates = Fsm_FsmComputeInitialStates(totalFsm);
    nInitialStates = mdd_count_onset(Fsm_FsmReadMddManager(totalFsm),
                                     totalInitialStates,
                                     Fsm_FsmReadPresentStateVars(totalFsm));
    mdd_free(totalInitialStates);

    /* If the number of initial states is only one, we can use both
     * conversion formulas(init ^ f != FALSE and init ^ !f == FALSE),
     * however, if we have multiple initial states, we should use
     * p0 ^ !f == FALSE.
     */
    ctlNormalFormulaArray =
      Ctlp_FormulaArrayConvertToForward(ctlArray, (nInitialStates == 1.0),
                                        noShare);
    /* end conversion for forward traversal */
  } else if (noShare) { /* conversion for backward, no sharing */
    ctlNormalFormulaArray =
      Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
  }else{ /* conversion for backward, with sharing */
    /* Note that converting to DAG after converting to existential form would
       lead to more sharing, but it cannot be done since equal subformula that
       are converted from different formulae need different pointers back to
       their originals */
    if (checkVacuity) {
      ctlNormalFormulaArray =
        Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
    }
    else {
      array_t *temp = Ctlp_FormulaArrayConvertToDAG( ctlArray );
      array_free( ctlArray );
      ctlArray = temp;
      ctlNormalFormulaArray =
        Ctlp_FormulaDAGConvertToExistentialFormDAG(ctlArray);
    }
  }
  /* At this point, ctlNormalFormulaArray contains the formulas that are
     actually going to be checked, and ctlArray contains the formulas from
     which the conversion has been done.  Both need to be kept around until the
     end, for debugging purposes. */

  numFormulae = array_n(ctlNormalFormulaArray);

  /* time out */
  if (timeOutPeriod > 0) {
    /* Set the static variables used by the signal handler. */
    mcTimeOut = timeOutPeriod;
    alarmLapTime = util_cpu_ctime();
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout,
                "# MC: timeout occurred after %d seconds.\n", timeOutPeriod);
      (void) fprintf(vis_stdout, "# MC: data may be corrupted.\n");
      if (verbosity > McVerbosityNone_c) {
        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;
    }
  }

  /* Create reduced fsm, if necessary */
  if (!McOptionsReadReduceFsm(options)){
    /* We want to minimize only when "-r" option is not specified */
    /* reduceFsm would be NIL, if there is no reduction observed */
    assert (reducedFsm == NIL(Fsm_Fsm_t));
    reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray);
    if (reducedFsm != NIL(Fsm_Fsm_t) && verbosity != McVerbosityNone_c) {
      mddMgr = Fsm_FsmReadMddManager(reducedFsm);
      bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr,
                   Fsm_FsmReadPresentStateVars(reducedFsm));
      (void)fprintf(vis_stdout,"Local system includes ");
      (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n",
                    array_n(Fsm_FsmReadPresentStateVars(reducedFsm)),
                    array_n(bddIdArray));
      array_free(bddIdArray);
    }
  }

  /************** for all formulae **********************************/
  for(i = 0; i < numFormulae; i++) {
    int nImgComps, nPreComps;
    boolean result;
    Ctlp_Formula_t *ctlFormula = array_fetch(Ctlp_Formula_t *,
                                             ctlNormalFormulaArray, i);

    modelFsm = NIL(Fsm_Fsm_t);

    /* do a check */
    if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
      (void) fprintf(vis_stdout,
                     "** mc error: error in parsing Atomic Formula:\n%s\n",
                     error_string());
      error_init();
      Ctlp_FormulaFree(ctlFormula);
      continue;
    }

    /* Create reduced fsm */
    if (McOptionsReadReduceFsm(options)) {
      /* We have not done top level reduction. */
      /* Using the same variable reducedFsm here   */
      array_t *oneFormulaArray = array_alloc(Ctlp_Formula_t *, 1);

      assert(reducedFsm == NIL(Fsm_Fsm_t));
      array_insert_last(Ctlp_Formula_t *, oneFormulaArray, ctlFormula);
      reducedFsm = McConstructReducedFsm(network, oneFormulaArray);
      array_free(oneFormulaArray);

      if (reducedFsm && verbosity != McVerbosityNone_c) {
        mddMgr = Fsm_FsmReadMddManager(reducedFsm);
        bddIdArray = mdd_id_array_to_bdd_id_array(mddMgr,
                       Fsm_FsmReadPresentStateVars(reducedFsm));
        (void)fprintf(vis_stdout,"Local system includes ");
        (void)fprintf(vis_stdout,"%d (%d) multi-value (boolean) variables.\n",
                      array_n(Fsm_FsmReadPresentStateVars(reducedFsm)),
                      array_n(bddIdArray));
        array_free(bddIdArray);
      }
    }/* if readreducefsm */

    /* Let us see if we got any reduction via top level or via "-r" */
    if (reducedFsm == NIL(Fsm_Fsm_t))
      modelFsm = totalFsm; /* no reduction */
    else
      modelFsm = reducedFsm; /* some reduction at some point */

    /* compute initial states */
    modelInitialStates = Fsm_FsmComputeInitialStates(modelFsm);
    if (modelInitialStates == NIL(mdd_t)) {
      int j;
      (void) fprintf(vis_stdout,
      "** mc error: Cannot build init states (mutual latch dependency?)\n%s\n",
                     error_string());
      if (modelFsm != totalFsm)
        Fsm_FsmFree(reducedFsm);

      alarm(0);

      for(j = i; j < numFormulae; j++)
        Ctlp_FormulaFree(
          array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) );
      array_free( ctlNormalFormulaArray );

      Ctlp_FormulaArrayFree( ctlArray );

      McOptionsFree(options);

      return 1;
    }

    earlyTermination = Mc_EarlyTerminationAlloc(McAll_c, modelInitialStates);

    if(hintsArray != NIL(Ctlp_FormulaArray_t)) {
      hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray);
      if( hintsStatesArray == NIL(array_t) ||
          (guidedSearchType == Mc_Global_c &&
           Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)) {
        int j;

        if( guidedSearchType == Mc_Global_c &&
            Ctlp_CheckClassOfExistentialFormula(ctlFormula) == Ctlp_Mixed_c)
          fprintf(vis_stderr, "** mc error: global hints incompatible with "
                  "mixed formulae\n");

        Mc_EarlyTerminationFree(earlyTermination);
        mdd_free(modelInitialStates);
        if (modelFsm != totalFsm)
          Fsm_FsmFree(reducedFsm);
        alarm(0);
        for(j = i; j < numFormulae; j++)
          Ctlp_FormulaFree(
            array_fetch( Ctlp_Formula_t *, ctlNormalFormulaArray, j ) );
        array_free( ctlNormalFormulaArray );
        Ctlp_FormulaArrayFree( ctlArray );
        McOptionsFree(options);
        return 1;
      } /* problem with hints */
    } /* hints exist */

    /* stats */
    if (verbosity > McVerbosityNone_c) {
      initialTime = util_cpu_time();
      nImgComps = Img_GetNumberOfImageComputation(Img_Forward_c);
      nPreComps = Img_GetNumberOfImageComputation(Img_Backward_c);
    } else { /* to remove uninitialized variable warnings */
      initialTime = 0;
      nImgComps = 0;
      nPreComps = 0;
    }
    mddMgr = Fsm_FsmReadMddManager(modelFsm);

        mdd_FunctionPrintMain(mddMgr,modelInitialStates,"INIT_MC",vis_stdout);
        
    /* compute don't cares. */
    if (modelCareStatesArray == NIL(array_t)) {
      long iTime; /* starting time for reachability analysis */
      if (verbosity > McVerbosityNone_c && i == 0)
        iTime = util_cpu_time();
      else /* to remove uninitialized variable warnings */
        iTime = 0;

      /* ardc */
      if (dcLevel == McDcLevelArdc_c) {
        Fsm_ArdcOptions_t *ardcOptions = McOptionsReadArdcOptions(options);

        modelCareStatesArray = Fsm_ArdcComputeOverApproximateReachableStates(
          modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
        if (verbosity > McVerbosityNone_c && i == 0)
          Fsm_ArdcPrintReachabilityResults(modelFsm, util_cpu_time() - iTime);

      /* rch dc */
      } else if (dcLevel >= McDcLevelRch_c) {
        modelCareStates =
          Fsm_FsmComputeReachableStates(modelFsm, 0, 1, 0, 0, 0, 0, 0,
                                        Fsm_Rch_Default_c, 0, 0,
                                        NIL(array_t), FALSE, NIL(array_t));
        if (verbosity > McVerbosityNone_c && i == 0) {
          Fsm_FsmReachabilityPrintResults(modelFsm, util_cpu_time() - iTime,
                                          Fsm_Rch_Default_c);
        }

        modelCareStatesArray = array_alloc(mdd_t *, 0);
        array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates);
      } else {
        modelCareStates = mdd_one(mddMgr);
        modelCareStatesArray = array_alloc(mdd_t *, 0);
        array_insert(mdd_t *, modelCareStatesArray, 0, modelCareStates);
      }
    }

    Fsm_MinimizeTransitionRelationWithReachabilityInfo(
      modelFsm, (traversalDirection == McFwd_c) ? Img_Both_c : Img_Backward_c,
      verbosity > 1);

    /* fairness conditions */
    fairStates = Fsm_FsmComputeFairStates(modelFsm, modelCareStatesArray,
                                          verbosity, dcLevel, GSHschedule,
                                          McBwd_c, FALSE);
    fairCond = Fsm_FsmReadFairnessConstraint(modelFsm);

    if (mdd_lequal(modelInitialStates, fairStates, 1, 0)) {
      (void)fprintf(vis_stdout,
                    "** mc warning: There are no fair initial states\n");
    }
    else if (!mdd_lequal(modelInitialStates, fairStates, 1, 1)) {
      (void)fprintf(vis_stdout,
                    "** mc warning: Some initial states are not fair\n");
    }

    /* some user feedback */
    if (verbosity != McVerbosityNone_c) {
      (void)fprintf(vis_stdout, "Checking formula[%d] : ", i + 1);
      Ctlp_FormulaPrint(vis_stdout,
                        Ctlp_FormulaReadOriginalFormula(ctlFormula));
      (void)fprintf (vis_stdout, "\n");
      if (traversalDirection == McFwd_c) {
        (void)fprintf(vis_stdout, "Forward formula : ");
        Ctlp_FormulaPrint(vis_stdout, ctlFormula);
        (void)fprintf(vis_stdout, "\n");
      }
    }

    /************** the actual computation **********************************/
    if (checkVacuity) {
      McVacuityDetection(modelFsm, ctlFormula, i,
                         fairStates, fairCond, modelCareStatesArray,
                         earlyTermination, hintsStatesArray,
                         guidedSearchType, modelInitialStates,
                         options);
    }
    else { /* Normal Model Checking */
      mdd_t *ctlFormulaStates =
        Mc_FsmEvaluateFormula(modelFsm, ctlFormula, fairStates,
                              fairCond, modelCareStatesArray,
                              earlyTermination, hintsStatesArray,
                              guidedSearchType, verbosity, dcLevel,
                              buildOnionRings, GSHschedule);

      McEstimateCoverage(modelFsm, ctlFormula, i, fairStates, fairCond,
                         modelCareStatesArray, earlyTermination,
                         hintsStatesArray, guidedSearchType, verbosity,
                         dcLevel, buildOnionRings, GSHschedule,
                         traversalDirection, modelInitialStates,
                         ctlFormulaStates, &totalcoveredstates,
                         signalTypeList, signalList, statesCoveredList,
                         newCoveredStatesList, statesToRemoveList,
                         performCoverageHoskote, performCoverageImproved);

      Mc_EarlyTerminationFree(earlyTermination);
      if(hintsStatesArray != NIL(array_t))
        mdd_array_free(hintsStatesArray);
      /* Set up things for possible FAFW analysis of counterexample. */
      Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag);
      Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable);
      /* user feedback on succes/fail */
      result = McPrintPassFail(mddMgr, modelFsm, traversalDirection,
                               ctlFormula, ctlFormulaStates,
                               modelInitialStates, modelCareStatesArray,
                               options, verbosity);
      Fsm_FsmSetFAFWFlag(modelFsm, 0);
      Fsm_FsmSetSystemVariableFAFW(modelFsm, NULL);
      mdd_free(ctlFormulaStates);
    }

    if (verbosity > McVerbosityNone_c) {
      finalTime = util_cpu_time();
      fprintf(vis_stdout, "-- 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);
    }
    mdd_free(modelInitialStates);
    mdd_free(fairStates);
    Ctlp_FormulaFree(ctlFormula);

    if ((McOptionsReadReduceFsm(options)) &&
        (reducedFsm != NIL(Fsm_Fsm_t))) {
      /*
      ** We need to free the reducedFsm only if it was created under "-r"
      ** option and was non-NIL.
      */
      Fsm_FsmFree(reducedFsm);
      reducedFsm = NIL(Fsm_Fsm_t);
      modelFsm = NIL(Fsm_Fsm_t);
      if (modelCareStates) {
        mdd_array_free(modelCareStatesArray);
        modelCareStates = NIL(mdd_t);
        modelCareStatesArray = NIL(array_t);
      } else if (modelCareStatesArray) {
        modelCareStatesArray = NIL(array_t);
      }
    }
  }/* for all formulae */

  if (verbosity > McVerbosityNone_c) {
    finalTime = util_cpu_time();
    fprintf(vis_stdout, "-- total mc time = %10g\n",
      (double)(finalTime - totalInitialTime) / 1000.0);
    fprintf(vis_stdout,
            "-- total %d image computations and %d preimage computations\n",
            Img_GetNumberOfImageComputation(Img_Forward_c),
            Img_GetNumberOfImageComputation(Img_Backward_c));
    /* Print tfm options if we have a global fsm. */
    if (!McOptionsReadReduceFsm(options) && modelFsm != NIL(Fsm_Fsm_t)) {
      imageInfo = Fsm_FsmReadImageInfo(modelFsm);
      if (Img_ImageInfoObtainMethodType(imageInfo) == Img_Tfm_c ||
          Img_ImageInfoObtainMethodType(imageInfo) == Img_Hybrid_c) {
        Img_TfmPrintStatistics(imageInfo, Img_Both_c);
      }
    }
  }

  /* Print results of coverage computation */
  McPrintCoverageSummary(modelFsm, dcLevel,
                         options, modelCareStatesArray,
                         modelCareStates, totalcoveredstates,
                         signalTypeList, signalList, statesCoveredList,
                         performCoverageHoskote, performCoverageImproved);
  mdd_array_free(newCoveredStatesList);
  mdd_array_free(statesToRemoveList);
  array_free(signalTypeList);
  array_free(signalList);
  mdd_array_free(statesCoveredList);
  if (totalcoveredstates != NIL(mdd_t))
    mdd_free(totalcoveredstates);

  if (modelCareStates) {
    mdd_array_free(modelCareStatesArray);
  }

  if(hintsArray)
    Ctlp_FormulaArrayFree(hintsArray);

  if ((McOptionsReadReduceFsm(options) == FALSE) &&
      (reducedFsm != NIL(Fsm_Fsm_t))) {
    /* If "-r" was not specified and we did some reduction at top
       level, we need to free it */
    Fsm_FsmFree(reducedFsm);
    reducedFsm = NIL(Fsm_Fsm_t);
    modelFsm = NIL(Fsm_Fsm_t);
  }

  if(systemVarBddIdTable)
    st_free_table(systemVarBddIdTable);
  array_free(ctlNormalFormulaArray);
  (void) fprintf(vis_stdout, "\n");

  Ctlp_FormulaArrayFree(ctlArray);
  McOptionsFree(options);
  alarm(0);
  return 0;
}


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

  Synopsis    [Parse command line options for mc.]

  SideEffects []

******************************************************************************/
static McOptions_t *
ParseMcOptions(
  int argc,
  char **argv)
{
  unsigned int i;
  int c;
  char *guideFileName = NIL(char);
  char *variablesForSystem = NIL(char);
  FILE *guideFile = NIL(FILE);
  FILE *systemFile = NIL(FILE);
  boolean doCoverageHoskote = FALSE;
  boolean doCoverageImproved = FALSE;
  boolean useMore = FALSE;
  boolean reduceFsm = FALSE;
  boolean printInputs = FALSE;
  boolean useFormulaTree = FALSE;
  boolean vd = FALSE;
  boolean beer = FALSE;
  boolean FAFWFlag = FALSE;
  boolean GFAFWFlag = FALSE;
  FILE *inputFp=NIL(FILE);
  FILE *debugOut=NIL(FILE);
  char *debugOutName=NIL(char);
  Mc_DcLevel dcLevel = McDcLevelRch_c;
  McDbgLevel dbgLevel = McDbgLevelNone_c;
  Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
  Mc_FwdBwdAnalysis fwdBwd = McFwd_c;
  McOptions_t *options = McOptionsAlloc();
  int timeOutPeriod = 0;
  Mc_FwdBwdAnalysis traversalDirection = McBwd_c;
  Fsm_ArdcOptions_t *ardcOptions;
  Mc_GSHScheduleType schedule = McGSH_EL_c;

  /*
   * Parse command line options.
   */

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "bcirmg:hv:d:D:VBf:t:CIFR:S:GWw:")) != EOF) {
    switch(c) {
    case 'g':
      guideFileName = util_strsav(util_optarg);
      break;
    case 'h':
      goto usage;
    case 'v':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
      break;
    case 'd':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      dbgLevel = (McDbgLevel) atoi(util_optarg);
      break;
    case 'D':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      dcLevel = (Mc_DcLevel) atoi(util_optarg);
      break;
    case 'b':
      fwdBwd = McBwd_c;
      break;
    case 'V':         /*Vacuity detection option*/
      vd = TRUE;
      break;
    case 'B':         /*Vacuity detection Beer et al method option*/
      vd = TRUE;
      beer = TRUE;
      break;
    case 'f':
      debugOutName = util_strsav(util_optarg);
      break;
    case 'm':
      useMore = TRUE;
      break;
    case 'r' :
      reduceFsm = TRUE;
      break;
    case 'c':
      useFormulaTree = TRUE;
      break;
    case 't' :
      timeOutPeriod  = atoi(util_optarg);
      break;
    case 'i' :
      printInputs = TRUE;
      break;
    case 'F' :
      traversalDirection = McFwd_c;
      break;
    case 'S' :
      schedule = McStringConvertToScheduleType(util_optarg);
      break;
    case 'w':
      variablesForSystem = util_strsav(util_optarg);
    case 'W':
      FAFWFlag = 1;
      break;
    case 'G':
      GFAFWFlag = 1;
      break;
    case 'C' :
      doCoverageHoskote = TRUE;
      break;
    case 'I' :
      doCoverageImproved = TRUE;
      break;
    default:
      goto usage;
    }
  }

  /*
   * Open the ctl file.
   */
  if (argc - util_optind == 0) {
    (void) fprintf(vis_stderr, "** mc error: file containing ctl formulas not provided\n");
    goto usage;
  }
  else if (argc - util_optind > 1) {
    (void) fprintf(vis_stderr, "** mc error: too many arguments\n");
    goto usage;
  }

  McOptionsSetFwdBwd(options, fwdBwd);
  McOptionsSetUseMore(options, useMore);
  McOptionsSetReduceFsm(options, reduceFsm);
  McOptionsSetVacuityDetect(options, vd);
  McOptionsSetBeerMethod(options, beer);
  McOptionsSetUseFormulaTree(options, useFormulaTree);
  McOptionsSetPrintInputs(options, printInputs);
  McOptionsSetTimeOutPeriod(options, timeOutPeriod);
  McOptionsSetFAFWFlag(options, FAFWFlag + GFAFWFlag);
  McOptionsSetCoverageHoskote(options, doCoverageHoskote);
  McOptionsSetCoverageImproved(options, doCoverageImproved);

  if((FAFWFlag > 0 || GFAFWFlag > 0) &&  dbgLevel == 0) {
    fprintf(vis_stderr, "** mc warning : -w and -W options are ignored without -d option\n");
  }

  if((FAFWFlag > 0 || GFAFWFlag > 0) &&  printInputs == 0) {
    fprintf(vis_stderr, "** mc warning : -i is recommended with -w or -W option\n");
  }
  if(FAFWFlag) {
    if (bdd_get_package_name() != CUDD) {
      fprintf(vis_stderr, "** mc warning : -w and -W option is only available with CUDD\n");
      FAFWFlag = 0;
      FREE(variablesForSystem);
      variablesForSystem = NIL(char);
    }
  }


  if (schedule == McGSH_Unassigned_c) {
    (void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
    goto usage;
  } else {
    McOptionsSetSchedule(options, schedule);
  }
  inputFp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
  if (inputFp == NIL(FILE)) {
    McOptionsFree(options);
    if (guideFileName != NIL(char)) FREE(guideFileName);
    return NIL(McOptions_t);
  }
  McOptionsSetCtlFile(options, inputFp);

  if (debugOutName != NIL(char)) {
    debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
    FREE(debugOutName);
    if (debugOut == NIL(FILE)) {
      McOptionsFree(options);
      if (guideFileName != NIL(char)) FREE(guideFileName);
      return NIL(McOptions_t);
    }
  }
  McOptionsSetDebugFile(options, debugOut);


  if (guideFileName != NIL(char)) {
    guideFile = Cmd_FileOpen(guideFileName, "r", NIL(char *), 0);
    if (guideFile == NIL(FILE)) {
      fprintf(vis_stderr, "** mc error: cannot open guided search file %s.\n",
              guideFileName);
      FREE(guideFileName);
      guideFileName = NIL(char);
      McOptionsFree(options);
      return NIL(McOptions_t);
    }
    FREE(guideFileName);
    guideFileName = NIL(char);
  }
  McOptionsSetGuideFile(options, guideFile);

  if (variablesForSystem != NIL(char)) {
    systemFile = Cmd_FileOpen(variablesForSystem, "r", NIL(char *), 0);
    if (systemFile == NIL(FILE)) {
      fprintf(vis_stderr, "** mc error: cannot open system variables file for FAFW %s.\n",
              variablesForSystem);
      FREE(variablesForSystem);
      variablesForSystem = NIL(char);
      McOptionsFree(options);
      return NIL(McOptions_t);
    }
    FREE(variablesForSystem);
    variablesForSystem = NIL(char);
  }
  McOptionsSetVariablesForSystem(options, systemFile);

  if ((verbosityLevel != McVerbosityNone_c) &&
       (verbosityLevel != McVerbosityLittle_c) &&
       (verbosityLevel != McVerbositySome_c) &&
       (verbosityLevel != McVerbosityMax_c)) {
    goto usage;
  }
  else {
    McOptionsSetVerbosityLevel(options, verbosityLevel);
  }

  if ((dbgLevel != McDbgLevelNone_c) &&
       (dbgLevel != McDbgLevelMin_c) &&
       (dbgLevel != McDbgLevelMinVerbose_c) &&
       (dbgLevel != McDbgLevelMax_c) &&
       (dbgLevel != McDbgLevelInteractive_c)) {
    goto usage;
  }
  else {
    McOptionsSetDbgLevel(options, dbgLevel);
  }

  if ((dcLevel != McDcLevelNone_c) &&
       (dcLevel != McDcLevelRch_c ) &&
       (dcLevel != McDcLevelRchFrontier_c ) &&
       (dcLevel != McDcLevelArdc_c )) {
    goto usage;
  }
  else {
    McOptionsSetDcLevel(options, dcLevel);
  }

  McOptionsSetTraversalDirection(options, traversalDirection);
  if (dcLevel == McDcLevelArdc_c) {
    ardcOptions = Fsm_ArdcAllocOptionsStruct();
    Fsm_ArdcGetDefaultOptions(ardcOptions);
  } else
    ardcOptions = NIL(Fsm_ArdcOptions_t);
  McOptionsSetArdcOptions(options, ardcOptions);

  return options;

  usage:
  (void) fprintf(vis_stderr, "usage: model_check [-b][-c][-d dbg_level][-f dbg_file][-g <hintfile>][-h][-i][-m][-r][-V][-B][-t period][-C][-I][-P][-v verbosity_level][-D dc_level][-F][-S <schedule>] <ctl_file>\n");
  (void) fprintf(vis_stderr, "    -b \tUse backward analysis in debugging\n");
  (void) fprintf(vis_stderr, "    -c \tNo sharing of CTL parse tree. This option does not matter for vacuity detection.\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 minimal debugging\n");
  (void) fprintf(vis_stderr, "        debug_level = 2 => automatic minimal debugging with extra verbosity\n");
  (void) fprintf(vis_stderr, "        debug_level = 3 => automatic maximal debugging\n");
  (void) fprintf(vis_stderr, "        debug_level = 4 => interactive 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, "    -g <hint_file> \tSpecify file for guided search.\n");
  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");
  (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
  (void) fprintf(vis_stderr, "    -m \tPipe debug output through more.\n");
  (void) fprintf(vis_stderr, "    -r  reduce FSM with respect to formula being verified\n");
  (void) fprintf(vis_stderr, "    -t <period> time out period\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, "    -w <node file> \tSpecify variables controlled by system.\n");
  (void) fprintf(vis_stderr, "    -B  vacuity detection for w-ACTL formulae using method of Beer et al \n");
  (void) fprintf(vis_stderr, "    -C Compute coverage of all observable signals using Hoskote et.al's implementation\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, "    -F \tUse forward model checking.\n");
  (void) fprintf(vis_stderr, "    -G \tUse general fate and free will algorithm.\n");
  (void) fprintf(vis_stderr, "    -I Compute coverage of all observable signals using improved coverage implementation\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, "    -V  thorough vacuity detection\n");
  (void) fprintf(vis_stderr, "    -W \tUse fate and free will algorithm when all the variables are controlled by system.\n");
  (void) fprintf(vis_stderr, "    <ctl_file> The input file containing CTL formula to be checked.\n");

  if (guideFileName != NIL(char)) FREE(guideFileName);
  McOptionsFree(options);

  return NIL(McOptions_t);
}


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

  Synopsis [Check whether language of FSM is empty.]

  CommandName [lang_empty]

  CommandSynopsis [perform language emptiness check on a flattened network]

  CommandArguments [ \[-b\] \[-d &lt;dbg_level&gt;\] \[-f &lt;dbg_file&gt;\]
  \[-h\] \[-i\] \[-s\] \[-t &lt;time_out_period&gt;\]
  \[-v &lt;verbosity_level&gt;\]
  \[-A &lt;le_method&gt;\] \[-D &lt;dc_level&gt;\]
  \[-S &lt;schedule&gt;\] \[-L &lt;lockstep_mode&gt;\] ]

  CommandDescription [
  Performs language emptiness check on a flattened network.  The
  language is not empty when there is a fair path starting at an
  initial state.  Before calling this command, the user should have
  initialized the design by calling the command <A
  HREF="init_verifyCmd.html"> <code> init_verify</code></A>.  <p>

  A fairness constraint can be read in by calling the
  <A HREF="read_fairnessCmd.html"><code>read_fairness</code></A> command;
  if none is specified, all paths are taken to be fair.
  <p>

  The system is reduced automatically with respect to the set of
  fairness constraints.  If the language is not empty, a proof of this
  fact is generated.  A proof is a fair path starting at an initial
  state.  This is represented by a finite sequence of states starting
  at an initial state (the stem) leading to a fair cycle, i.e., a
  cycle on which there lies a state from each fairness condition.
  <p>

  Command options:
  <p>

  <dl>

  <dt> -b
  <dd> Use backward analysis when performing debugging; the default is to use forward
           analysis. This should be tried when the debugger spends a large amount of time when
           creating a path to a fair cycle.
  <p>

  <dt> -d <code> &lt;dbg_level&gt; </code>
  <dd> Specify whether to demonstrate a proof of the language non-emptiness
  <p>
  <dd>
  <code> dbg_level</code> must be one of the following:
  <p>

  <code> 0 </code>: No debugging  performed. This is the default.
  <p>

  <code> 1 </code>: Generate a path to a fair cycle.
  <p>

  <dt> -f &lt;<code>dbg_file</code>&gt;
  <dd> Write the debugger output to <code>dbg_file</code>.
  <p>

  <dt> -h
  <dd> Print the command usage.
  <p>

  <dt> -m
  <dd> Pipe debugger output through the UNIX utility more.
  <p>

  <dt> -i
  <dd> Print input values causing transitions between states during debugging.
  Both primary and pseudo inputs are printed.
  <p>

  <dt> -s
  <dd> Print debug output in the format accepted by the
       <A HREF="simulateCmd.html"><code>simulate</code></A> command.
  <p>

  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
  <dd> Specify the time out period (in seconds) after which the command
  aborts.  By default this option is set to infinity.
  <p>

  <dt> -v  <code>&lt;verbosity_level&gt;</code>
  <dd> Specify verbosity level. This sets the amount of feedback on CPU
  usage and code status.
  <p>

  <dd>
  <code>verbosity_level</code> must be one of the following:
  <p>

  <code> 0 </code>: No feedback provided. This is the default.<p>

  <code> 1 </code>: Feedback on code location.<p>

  <code> 2 </code>: Feedback on code location and CPU usage.<p>

  <dt> -A <code> &lt;le_method&gt; </code>
  <dd>
  Specify whether the compositional SCC analysis algorithm, Divide and
  Compose (DnC), is enabled for language emptiness checking.
  The DnC algorithm first enumerates fair SCCs in an over-approximated
  abstract model, and then successively refines them in the more
  concrete models.
  Since non-fair SCCs can be ignored in the more concrete models, a
  potentially large part of the state space are pruned away early on
  when the computations are cheap.
  <p>

  <dd>
  <code> le_method </code> must be one of the following:
  <p>

  <code> 0 </code>: no use of Divide and Compose (Default). <p>
  <code> 1 </code>: use Divide and Compose. <p>

  <dt> -D <code> &lt;dc_level&gt; </code>
  <dd> Specify extent to which don't cares are used to simplify MDDs.
  Don't cares are minterms on which the value taken by functions does not affect the computation;
  potentially, these minterms can be used to simplify MDDs and reduce time taken to perform
  MDD computations.
  <p>

  <dd>
  <code> dc_level </code> must be one of the following:
  <p>

  <code> 0 </code>: No don't cares are used. <p>
  <code> 1 </code>: Use unreachable states as don't cares.  This is the
  default. <p>

  <dt> -S <code> &lt;schedule&gt; </code>

  <dd> Specify schedule for GSH algorithm, which generalizes the
  Emerson-Lei algorithm and is used to compute greatest fixpoints.
  The choice of schedule affects the sequence in which EX and EU
  operators are applied.  It makes a difference only when fairness
  constraints are specified.

  <br>
  <code> &lt;schedule&gt; </code> must be one of the following:

  <p> <code> EL </code>: EU and EX operators strictly alternate.  This
  is the default.

  <p> <code> EL1 </code>: EX is applied once for every application of all EUs.

  <p> <code> EL2 </code>: EX is applied repeatedly after each application of
  all EUs.

  <p> <code> budget </code>: a hybrid of EL and EL2.

  <p> <code> random </code>: enabled operators are applied in
  (pseudo-)random order.

  <p> <code> off </code>: GSH is disabled, and the old algorithm is
  used instead.  The old algorithm uses the <code> EL </code>, but the
  termination checks are less sophisticated than in GSH.
  <p>

  <dt> -F

  <dd> Use forward analysis in the computation of the greatest fixpoint.
  This option is incompatible with -d 1 or higher and can only be used
  with -D 1.

  <dt> -L <code> &lt;lockstep_mode&gt; </code>

  <dd> Use the lockstep algorithm, which is based on fair SCC enumeration.

  <br>
  <code> &lt;lockstep_mode&gt; </code> must be one of the following:

  <p> <code> off </code>: Lockstep is disabled.  This is the default.
  Language emptiness is checked by computing a hull of the fair SCCs.

  <p> <code> on </code>: Lockstep is enabled.

  <p> <code> all </code>: Lockstep is enabled; all fair SCCs are
  enumerated instead of terminating as soon as one is found.  This can
  be used to study the SCCs of a graph, but it is slower than the
  default option.

  <p> <code> n </code>: (n is a positive integer).  Lockstep is
  enabled and up to <code> n </code> fair SCCs are enumerated.  This
  is less expensive than <code> all </code>, but still less efficient
  than <code> on </code>, even when <code> n = 1 </code>.

  </dl>

  ]

  SideEffects []

  SeeAlso []

******************************************************************************/
static int
CommandLe(
  Hrc_Manager_t **hmgr,
  int argc,
  char **argv)
{
  McOptions_t *options;
  Mc_VerbosityLevel verbosity;
  Mc_LeMethod_t leMethod;
  Mc_DcLevel dcLevel;
  McDbgLevel dbgLevel;
  FILE *dbgFile= NIL(FILE);
  boolean printInputs = FALSE;
  int timeOutPeriod = 0;
  Mc_GSHScheduleType GSHschedule;
  Mc_FwdBwdAnalysis GSHdirection;
  int lockstep;
  int useMore;
  int simValue;
  int reduceFsm_flag = 1;
  long startRchTime;
  mdd_t *modelCareStates;
  Fsm_Fsm_t *totalFsm;
  Fsm_Fsm_t *modelFsm, *reducedFsm = NIL(Fsm_Fsm_t);
  mdd_t *fairInitStates;
  array_t *modelCareStatesArray;
  long initialTime, finalTime; /* for lang_empty checking */

  Img_ResetNumberOfImageComputation(Img_Both_c);

  /* Read options and set timeout if requested. */
  if (!(options = ParseLeOptions(argc, argv))) {
    return 1;
  }

  totalFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  if (totalFsm == NIL(Fsm_Fsm_t)) {
    (void) fprintf(vis_stdout, "%s\n", error_string());
    error_init();
    McOptionsFree(options);
    return 1;
  }

  initialTime = util_cpu_time();

  verbosity     = McOptionsReadVerbosityLevel(options);
  leMethod      = McOptionsReadLeMethod(options);
  dcLevel       = McOptionsReadDcLevel(options);
  dbgLevel      = McOptionsReadDbgLevel(options);
  printInputs   = McOptionsReadPrintInputs(options);
  timeOutPeriod = McOptionsReadTimeOutPeriod(options);
  GSHschedule   = McOptionsReadSchedule(options);
  GSHdirection  = McOptionsReadTraversalDirection(options);
  lockstep      = McOptionsReadLockstep(options);
  dbgFile       = McOptionsReadDebugFile(options);
  useMore       = McOptionsReadUseMore(options);
  simValue      = McOptionsReadSimValue(options);

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

  if (timeOutPeriod > 0) {
    /* Set the static variables used by the signal handler. */
    mcTimeOut = timeOutPeriod;
    alarmLapTime  = util_cpu_ctime();
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout,
                     "# LE: language emptiness - timeout occurred after %d seconds.\n",
                     timeOutPeriod);
      (void) fprintf(vis_stdout, "# LE: data may be corrupted.\n");
      if (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;
    }
  }

  /* Reduce FSM to cone of influence of fairness constraints. */
  if (reduceFsm_flag) {
    Ntk_Network_t *network = Fsm_FsmReadNetwork(totalFsm);
    array_t *ctlNormalFormulaArray = array_alloc(Ctlp_Formula_t *, 0);
    reducedFsm = McConstructReducedFsm(network, ctlNormalFormulaArray);
    array_free(ctlNormalFormulaArray);
  }

  if (reducedFsm == NIL(Fsm_Fsm_t)) {
    modelFsm = totalFsm;
  }else {
    modelFsm = reducedFsm;
  }

  /* Find care states and put them in an array */
  if (dcLevel == McDcLevelArdc_c) { /* aRDC */
    Fsm_ArdcOptions_t *ardcOptions = Fsm_ArdcAllocOptionsStruct();
    array_t *tmpArray;
    Fsm_ArdcGetDefaultOptions(ardcOptions);

    if (verbosity > 0)
      startRchTime = util_cpu_time();
    else /* to remove uninitialized variable warning */
      startRchTime = 0;
    tmpArray = Fsm_ArdcComputeOverApproximateReachableStates(
      modelFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
    modelCareStatesArray = mdd_array_duplicate(tmpArray);

    FREE(ardcOptions);

    if (verbosity > 0 )
      Fsm_ArdcPrintReachabilityResults(modelFsm,
                                       util_cpu_time() - startRchTime);

  }else if (dcLevel >= McDcLevelRch_c) { /*RDC*/
    if (verbosity > 0)
      startRchTime = util_cpu_time();
    else /* to remove uninitialized variable warning */
      startRchTime = 0;
    modelCareStates =
      Fsm_FsmComputeReachableStates(modelFsm, 0, verbosity, 0, 0,
                                    (lockstep != MC_LOCKSTEP_OFF), 0, 0,
                                    Fsm_Rch_Default_c, 0, 0,
                                    NIL(array_t), FALSE, NIL(array_t));
    if (verbosity > 0) {
      Fsm_FsmReachabilityPrintResults(modelFsm,
                                      util_cpu_time() - startRchTime,
                                      Fsm_Rch_Default_c);
    }
    modelCareStatesArray = array_alloc(mdd_t *, 0);
    array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);

  } else {  /* mdd_one */
    modelCareStates = mdd_one(Fsm_FsmReadMddManager(modelFsm));
    modelCareStatesArray = array_alloc(mdd_t *, 0);
    array_insert_last(mdd_t *, modelCareStatesArray, modelCareStates);
  }


  fairInitStates = Mc_FsmCheckLanguageEmptiness(modelFsm,
                                                modelCareStatesArray,
                                                Mc_Aut_Strong_c,
                                                leMethod,
                                                dcLevel,
                                                dbgLevel,
                                                printInputs,
                                                verbosity,
                                                GSHschedule,
                                                GSHdirection,
                                                lockstep,
                                                dbgFile,
                                                useMore,
                                                simValue,
                                                "LE");

  if (verbosity > McVerbosityNone_c) {
    finalTime = util_cpu_time();
    fprintf(vis_stdout, "-- total le time = %10g\n",
            (double)(finalTime - initialTime) / 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 up. */
  if (fairInitStates) {
    mdd_free(fairInitStates);
  }
  mdd_array_free(modelCareStatesArray);
  McOptionsFree(options);
  if (reducedFsm) {
    Fsm_FsmFree(reducedFsm);
  }

  alarm(0);
  return 0;

} /* CommandLe */


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

  Synopsis    [Parse command line options for lang_empty.]

  SideEffects []

******************************************************************************/
static McOptions_t *
ParseLeOptions(
  int argc,
  char **argv)
{
  unsigned int i;
  int c;
  boolean useSimFormat = FALSE;
  FILE *debugOut=NIL(FILE);
  char *debugOutName=NIL(char);
  Mc_DcLevel dcLevel = McDcLevelRch_c;
  Mc_LeMethod_t leMethod = Mc_Le_Default_c;
  McDbgLevel dbgLevel = McDbgLevelNone_c;
  Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
  Mc_FwdBwdAnalysis fwdBwd = McFwd_c;
  McOptions_t *options = McOptionsAlloc();
  boolean printInputs = FALSE;
  boolean useMore = FALSE;
  int timeOutPeriod = 0;
  Mc_GSHScheduleType schedule = McGSH_EL_c;
  Mc_FwdBwdAnalysis direction = McBwd_c;
  int lockstep = MC_LOCKSTEP_OFF;
  Fsm_ArdcOptions_t *ardcOptions;

  /*
   * Parse command line options.
   */

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "bihmt:v:d:A:D:f:sS:L:F")) != EOF) {
    switch(c) {
    case 'h':
      goto usage;
    case 'v':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
      break;
    case 'd':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      dbgLevel = (McDbgLevel) atoi(util_optarg);
      break;
    case 'A':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      leMethod = (Mc_LeMethod_t) atoi(util_optarg);
      break;
    case 'D':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      dcLevel = (Mc_DcLevel) atoi(util_optarg);
      break;
    case 'f':
      debugOutName = util_strsav(util_optarg);
      break;
    case 's':
      useSimFormat = TRUE;
      break;
    case 't':
      timeOutPeriod = atoi(util_optarg);
      break;
    case 'i':
      printInputs = TRUE;
      break;
    case 'm':
      useMore = TRUE;
      break;
    case 'b':
      fwdBwd = McBwd_c;
      break;
    case 'S' :
      schedule = McStringConvertToScheduleType(util_optarg);
      break;
    case 'L' :
      lockstep = McStringConvertToLockstepMode(util_optarg);
      break;
    case 'F' :
      direction = McFwd_c;
      break;
    default:
      goto usage;
    }
  }

  if (schedule == McGSH_Unassigned_c) {
    (void) fprintf(vis_stderr, "unknown schedule: %s\n", util_optarg);
    goto usage;
  } else {
    McOptionsSetSchedule(options, schedule);
  }
  McOptionsSetTraversalDirection(options, direction);
  if (lockstep == MC_LOCKSTEP_UNASSIGNED) {
    (void) fprintf(vis_stderr, "invalid lockstep option: %s\n", util_optarg);
    goto usage;
  } else {
    McOptionsSetLockstep(options, lockstep);
  }
  if ((verbosityLevel != McVerbosityNone_c) &&
       (verbosityLevel != McVerbosityLittle_c) &&
       (verbosityLevel != McVerbositySome_c) &&
       (verbosityLevel != McVerbosityMax_c)) {
    goto usage;
  }
  else {
    McOptionsSetVerbosityLevel(options, verbosityLevel);
  }

  if (debugOutName != NIL(char)) {
    debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
    if (debugOut == NIL(FILE)) {
      McOptionsFree(options);
      return NIL(McOptions_t);
    }
  }
  McOptionsSetDebugFile(options, debugOut);

  if ((dbgLevel != McDbgLevelNone_c) &&
       (dbgLevel != McDbgLevelMin_c)) {
    goto usage;
  }
  else {
    McOptionsSetDbgLevel(options, dbgLevel);
  }

  if ((dcLevel != McDcLevelNone_c)  &&
       (dcLevel != McDcLevelRch_c )  &&
       (dcLevel != McDcLevelRchFrontier_c )  &&
       (dcLevel != McDcLevelArdc_c )) {
    goto usage;
  }
  else {
    McOptionsSetDcLevel(options, dcLevel);
  }

  if ((leMethod != Mc_Le_Default_c) &&
      (leMethod != Mc_Le_Dnc_c)) {
    goto usage;
  }
  else {
    McOptionsSetLeMethod(options, leMethod);
  }

  /* set Ardc options for le : C.W. */
  if (dcLevel == McDcLevelArdc_c) {
      ardcOptions = Fsm_ArdcAllocOptionsStruct();
      Fsm_ArdcGetDefaultOptions(ardcOptions);
  } else
      ardcOptions = NIL(Fsm_ArdcOptions_t);
  McOptionsSetArdcOptions(options, ardcOptions);

  McOptionsSetFwdBwd(options, fwdBwd);
  McOptionsSetSimValue(options, useSimFormat);
  McOptionsSetUseMore(options, useMore);
  McOptionsSetPrintInputs(options, printInputs);
  McOptionsSetTimeOutPeriod(options, timeOutPeriod);
  return options;

  usage:
  (void) fprintf(vis_stderr, "usage: lang_empty [-b][-d dbg_level][-f dbg_file][-h][-i][-m][-s][-t period][-v verbosity_level][-A <le_method>][-D <dc_level>][-S <schedule>][-F][-L <lockstep_mode>]\n");
  (void) fprintf(vis_stderr, "    -b \tUse backward analysis in debugging\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, "    -h \tPrints this usage message.\n");
  (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
  (void) fprintf(vis_stderr, "    -m \tPipe debug output through more\n");
  (void) fprintf(vis_stderr, "    -s \tWrite error trace in sim format.\n");
  (void) fprintf(vis_stderr, "    -t <period> time out period\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 => feedback\n");
  (void) fprintf(vis_stderr, "        verbosity_level = 2 => feedback and CPU usage profile\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, "    -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, "    -L <lockstep_mode>\n");
  (void) fprintf(vis_stderr, "       lockstep_mode is one of {off,on,all,n}\n");

  McOptionsFree(options);

  return NIL(McOptions_t);
}


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

  Synopsis [checks that all reachable states in flattened network satisfy invariants]

  CommandName [check_invariant]

  CommandSynopsis [check all states reachable in flattened network satisfy specified invariants]

  CommandArguments [ \[-c\] \[-d &lt;dbg_level&gt;\] \[-g
  &lt;<code>hints_file</code>&gt;\] \[-f\] \[-h\] \[-i\] \[-m\] \[-r\]
  \[-t &lt;time_out_period&gt;\] \[-v &lt;verbosity_level&gt;\] \[-A &lt;reachability_analysis_type&gt;\] \[-D\] &lt;invar_file&gt;]

  CommandDescription [Performs invariant checking on a flattened
  network.  Before calling this command, the user should have
  initialized the design by calling the command <A
  HREF="init_verifyCmd.html"> <code> init_verify</code></A>.
  <p>

  If the option -A3 (abstraction refinement method GRAB) is used, the command
  <A
  HREF="build_partition_maigsCmd.html"><code>build_partition_maigs</code></A>
  should also have been executed. However, in this case, the default BDD
  manager and network partition are not mandatory, though they will be used if
  available. (In other words, the user must run the commands <A
  HREF="flatten_hierarchyCmd.html"><code> flatten_hierarchy</code></A> and <A
  HREF="build_partition_maigsCmd.html"><code>build_partition_maigs</code></A>, but
  doesn't have to run the commands <A
  HREF="static_orderCmd.html"><code>static_order</code></A> and <A
  HREF="build_partition_mddsCmd.html"><code>build_partition_mdds</code></A> before
  calling this command.) For extremely large networks, it is actually favorable
  not to build them for the entire concrete model, but let this procedure
  assign bdd ids and construct the partition incrementally.

  <p>

  Option -A4 means abstraction refinement approach using puresat algorithm,
  which is entirely based on SAT solver.
  <p>

  An invariant is a set of states.
  Checking the invariant is the process of determining that all states reachable
  from the initial states lie in the invariant.
  <p>


  One way of defining an invariant is through a CTL formula which has no path operators.
  Such formulas should be specified in the file <code>invar_file</code>.
  Note that the support  of any wire referred to in a formula should consist only
  of latches.
  For the precise syntax of CTL formulas,
  see the <A HREF="../ctl/ctl/ctl.html"> VIS CTL and LTL syntax manual</A>.
  <p>

  <code>check_invariant</code> ignores all fairness conditions associated with the FSM.
  <p>

  <code>check_invariant<code> involves reachability analysis where at
   every step of the reachability computation all the specified
   invariants are checked in the reachable states computed thus
   far. If some invariant does not hold, a proof of failure is
   demonstrated. This consists of a path starting from an initial
   state to a state lying outside the invariant. This path is made as
   short as possible. For the -A 0 option or default -A option, it is
   the shortest path leading to a state outside the invariant. If a
   set of invariants is specified, the failed formulas are reported as
   soon as they are detected. The check is continued with the
   remaining invariants.<p>

  Command options:
  <p>

  <dl>

  <dt> -d <code> &lt;dbg_level&gt; </code>
  <dd> Specify the amount of debugging performed when the system fails a formula being checked.
  <p>
  <dd>
  <code> dbg_level</code> must be one of the following:
  <p>

  <code> 0 </code>: No debugging  performed. This is the default.
  <p>

  <code> 1 </code>: Generate a path from an initial state to a state
  lying outside the invariant. This option stores the onion rings just
  as specifying -f would have. Therefore, it may take more time and
  memory if the formula passes. This option is incompatible with -A 2
  option. <p>

  <dt> -f
  <dd> Store the set of new states (onion rings) reached at each step of
  invariant. This option is likely to use more memory but possibly
  faster results for invariants that fail. Therefore, the debug
  information for a failed invariant, if requested, may be provided
  faster. This option is not compatible with -A 2 options.<p>

  <dt> -g &lt;<code>hints_file</code>&gt;</dt>

  <dd> Use guided search.  The file <code>hints_file</code> contains a
  series of hints.  A hint is a formula that does not contain any
  temporal operators, so <code>hints_file</code> has the same syntax
  as a file of invariants used for check_invariant.  The hints are
  used in the order given to change the transition relation.  The
  transition relation is conjoined with the hint to yield an
  underapproximation of the transition relation.  If the hints are
  cleverly chosen, this may speed up the computation considerably,
  because a search with the changed transition relation may be much
  simpler than one with the original transition relation, and results
  obtained can be reused, so that we may never have to do an expensive
  search with the original relation.  See also: Ravi and Somenzi,
  Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and
  Somenzi, Efficient Decision Procedures for Model Checking of Linear
  Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic
  Guided Search for CTL Model Checking, DAC'00. This option is not
  compatible with -A 2 option. The description of some options for
  guided search can be found in the help page for
  print_guided_search_options. <p>

  <dt> -h
  <dd> Print the command usage.
  <p>

  <dt> -c
  <dd> Use the formula tree so that subformulae are not shared among the CTL
  formulae in the input file. This option is useful in the following
  scenario - formulae A, B and C are being checked in order and there is
  sub-formula sharing between A and C. If the BDDs corresponding to the shared
  sub-formula is huge then computation for B might not be able to finish
  without using this option.
  <p>

  <dt> -i
  <dd> Print input values causing transitions between states during
  debugging. Both primary and pseudo inputs are printed.  <p>

  <dt> -m
  <dd> Pipe debugger output through the UNIX utility  more.
  <p>

  <dt> -r
  <dd> Reduce the FSM derived from the flattened network with respect to each
  of the invariants in the input file. By default, the FSM is reduced with
  respect to the conjunction of the invariants in the input file. If this
  option is used and don't cares are being used for simplification, then
  subformula sharing is disabled (result might be incorrect otherwise).
  <p>

  <dd> The truth of  an invariant  may be independant  of  parts of the network (such as when wires have
  been abstracted; see <A HREF="flatten_hierarchyCmd.html"><code>flatten_hierarchy</code></A>).
  These parts are effectively removed when this option is invoked; this may result in
  more efficient invariant checking.
  <p>

  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
  <dd> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
  <p>
  <dt> -v  <code>&lt;verbosity_level&gt;</code>
  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage and code status.
  <p>

  <dd>
  <code>verbosity_level</code>  must be one of the following:
  <p>

  <code> 0 </code>: No feedback provided. This is the default.<p>

  <code> 1 </code>: Feedback on code location.<p>

  <code> 2 </code>: Feedback on code location and CPU usage.<p>

  <dt> -A &lt;reachability_analysis_type&gt;
  <dd> This option allows specification of the type of reachability computation. <p>

  0:  (default) Breadth First Search. No approximate reachability computation. <p>

  1: High Density Reachability Analysis (HD). Computes reachable states in a
  manner that keeps BDD sizes under control. May be faster than BFS in some
  cases. For larger circuits, this option could compute more reachable states
  than the -A 0 option for the same memory constraints, consequently may prove
  more invariants false. For help on controlling options for HD, look up help
  on the command: print_hd_options <A HREF="print_hd_optionsCmd.html"> <code>
  print_hd_options</code></A>. Refer Ravi & Somenzi, ICCAD95.  The path
  generated for a failed invariant using this method may not be the shortest
  path. This option is available only when compiled with the CUDD package. <p>

  2. Approximate Reachability Don't Cares(ARDC). Computes over-approximated
  reachable states in the reachability analysis step. This may be faster than
  the -A 0 option . The invariants are checked in the over-approximation. This
  may produce false negatives, but these are resolved internally using the
  exact reachable states. The final results produced are the same as those for
  exact reachable states. For help on controlling options for ARDC, look up
  help on the command: print_ardc_options. <A
  HREF="print_ardc_optionsCmd.html"><code> print_ardc_options</code></A> Refer
  2 papers in TCAD96 Dec. Cho et al, one is for State Space Decomposition and
  the other is for Approximate FSM Traversal. This option is incompatible with
  -d 1 and -g options.<p>

  3. The GRAB Abstraction Refinement Method. Conducts the reachability
  analysis on an abstract model. If the invariants are true in the
  abstract model, they are also true in the original model. If the
  invariants are false, the abstract counter-examples are used to
  refine the abstract model (since it is still inconclusive). This
  procedure iterates until a conclusive result is reached.  Note that,
  with this option, "build_partitioned_mdds" and "static_order" does
  not have to be executed before calling "check_invariants," though
  the default BDD partition and order will be reused if available.
  (When checking extremely large models, skipping either or both
  "static_order" and "build_partitioned_mdds" can often make the
  verification much faster.)  The grainularity of abstraction
  refinement also depends on the parameter "partition_threshold",
  which by default is 5000; one can use the VIS command "set
  partition_threshold 1000" to change its value. For experienced users
  who want to fine-tune the different parameters of GRAB, please try
  the test command "_grab_test" ("_grab_test -h" prints out its usage
  information).  Refer to Wang et al., ICCAD2003 and ICCD2004 for more
  information about the GRAB algorithm. Note that this option is
  incompatible with the "-d 1" and "-g" options.  <p>

  4. Abstraction refinement approach using puresat algorithm, which is
  entirely based on SAT solver. It has several parts:

  * Localization base Abstraction
  * K-induction to prove the truth of a property
  * Bounded Model Checking to find bugs
  * Incremental concretization based methods to verify abstract bugs
  * UNSAT proof based method to obtain refinement
  * Refinement minization to guarrantee a minimal refinement

  For more information, please check the BMC'03 and STTT'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", and " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure" <p>

  <dt> -D</dt>

  <dd>First compute an overapproximation to the reachable states.  Minimize the
  transition relation using this approximation, and then compute the set of
  reachable states exactly. This may accelerate reachability analysis. Refer to
  the paper by Moon et al, ICCAD98. The BDD minimizing method can be chosen by
  using "set image_minimize_method <method>" <A HREF = "setCmd.html">
  <code>set</code></A>.  This option is incompatible with -g.  <p>

  <dt> -F &lt;<code>dbg_file</code>&gt;
  <dd> Write the debugger output to <code>dbg_file</code>.
  <p>

  <dt> -w  &lt;<code>node_file</code>&gt;

  This option invokes the algorithm to generate an error trace divided
  into fated and free segements. Fate represents the inevitability and
  free is asserted when there is no inevitability. This can be formulated
  as a two-player concurrent reachability game. The two players are
  the environment and the system. The node_file is given to specify the
  variables the are controlled by the system.

  <dt> -W <dt>

  This option represents the case that all input variables are controlled
  by system.

  <dt> -G <dt>

  We proposed two algorithms to generate segmented counterexamples:
  general and restricted. By default we use the restricted
  algorithm. We can invoke the general algorithm with -G option.

  For more information, please read the STTT'04
  paper by Jin et al., "Fate and Free Will in Error Traces" <p>

  <dt> &lt;invarFile&gt;
  <dd> File containing invariants to be checked.
  <p>
  </dl>

  <dt> Related "set" options: <p>
  <dt> rch_simulate &lt;#&gt;
  <dd> The set option can be used to set this flag rch_simulate to specify the
  number of random vectors to be simulated. Default value for this number is 0.
  <p>

  <dt> ctl_change_bracket &lt;yes/no&gt;
  <dd> Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names,
  therefore CTL parser does the same thing. However, in some cases a user
  does not want to change node names in CTL parsing. Then, use this set
  option by giving "no". Default is "yes".
  <p>

  <dt> See also command : compute_reach <p>


  ]

  SideEffects []

  SeeAlso [CommandMc]

******************************************************************************/
static int
CommandInv(
  Hrc_Manager_t **hmgr,
  int argc,
  char **argv)
{
  int i, j;
  mdd_t *tautology;
  McOptions_t *options;
  FILE *invarFile;
  array_t *invarArray, *formulas, *sortedFormulaArray;
  static Fsm_Fsm_t *totalFsm, *modelFsm;
  mdd_manager *mddMgr;
  Ntk_Network_t *network;
  Mc_VerbosityLevel verbosity;
  Mc_DcLevel dcLevel;
  array_t *invarNormalFormulaArray, *invarStatesArray;
  int timeOutPeriod = 0;
  int debugFlag;
  int buildOnionRings;
  Fsm_RchType_t approxFlag;
  int ardc;
  int someLeft;
  Ctlp_Formula_t *invarFormula;
  mdd_t *invarFormulaStates;
  mdd_t *reachableStates;
  array_t *fsmArray;
  int printStep = 0;
  long initTime, finalTime;
  array_t *careSetArray;
  FILE              *guideFile;
  FILE          *systemFile;
  st_table      *systemVarBddIdTable;
  Ctlp_FormulaArray_t *hintsArray    = NIL(Fsm_HintsArray_t);
  array_t             *hintsStatesArray = NIL(array_t); /* array of mdd_t* */

  error_init();
  initTime = util_cpu_time();

  /* get command line options */
  if (!(options = ParseInvarOptions(argc, argv))) {
    return 1;
  }
  verbosity = McOptionsReadVerbosityLevel(options);
  dcLevel = McOptionsReadDcLevel(options);
  invarFile = McOptionsReadCtlFile(options);
  timeOutPeriod = McOptionsReadTimeOutPeriod(options);
  approxFlag = McOptionsReadInvarApproxFlag(options);
  buildOnionRings = (int)McOptionsReadInvarOnionRingsFlag(options);

  /* read the array of invariants */
  invarArray = Ctlp_FileParseFormulaArray(invarFile);
  fclose(invarFile);
  if (invarArray == NIL(array_t)) {
    (void) fprintf(vis_stderr, "** inv error: Error in parsing invariants from file\n");
    McOptionsFree(options);
    return 1;
  }
  if (array_n(invarArray) == 0) {
    (void) fprintf(vis_stderr, "** inv error: No formula in file\n");
    McOptionsFree(options);
    return 1;
  }

  /* read the netwrok */
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    fprintf(vis_stderr, "%s\n", error_string());
    error_init();
    McOptionsFree(options);
    return 1;
  }

  /**************************************************************************
   * if "-A 3" is enabled (using the abstraction refinement method GRAB ),
   *    call GRAB.
   **************************************************************************/
  if (approxFlag == Fsm_Rch_Grab_c) {

    if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
      McOptionsFree(options);
      fprintf(vis_stderr,
              "** inv error: To use GRAB, please run build_partition_maigs first\n");
      /*McOptionsFree(options);*/
      return 1;
    }

    if (timeOutPeriod > 0) {
      /* Set the static variables used by the signal handler. */
      mcTimeOut = timeOutPeriod;
      alarmLapTime = util_cpu_ctime();
      (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
      (void) alarm(timeOutPeriod);
      if (setjmp(timeOutEnv) > 0) {
        (void) fprintf(vis_stdout,
           "# INV: Checking Invariant: timeout occurred after %d seconds.\n",
                       timeOutPeriod);
        (void) fprintf(vis_stdout, "# INV: data may be corrupted.\n");
        alarm(0);
        return 1;
      }
    }

    Grab_NetworkCheckInvariants(network,
                                invarArray,
                                "GRAB", /* refineAlgorithm, */
                                TRUE,   /* fineGrainFlag, */
                                TRUE,   /* refineMinFlag, */
                                FALSE,  /* useArdcFlag, */
                                2,      /* cexType = SOR */
                                verbosity,
                                McOptionsReadDbgLevel(options),
                                McOptionsReadPrintInputs(options),
                                McOptionsReadDebugFile(options),
                                McOptionsReadUseMore(options),
                                "INV" /* driverName */
                                );
    McOptionsFree(options);
    return 0;
  }

  if (approxFlag == Fsm_Rch_PureSat_c) {

    if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) {
      McOptionsFree(options);
      fprintf(vis_stderr,
              "** inv error: Please run build_partition_maigs first\n");
      McOptionsFree(options);
      return 1;
    }

    if (timeOutPeriod > 0) {
      /* Set the static variables used by the signal handler. */
      mcTimeOut = timeOutPeriod;
      alarmLapTime = util_cpu_ctime();
      (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
      (void) alarm(timeOutPeriod);
      if (setjmp(timeOutEnv) > 0) {
        (void) fprintf(vis_stdout,
           "# INV by PURESAT: Checking Invariant using PURESAT: timeout occurred after %d seconds.\n",
                       timeOutPeriod);
        (void) fprintf(vis_stdout, "# INV by PURESAT: data may be corrupted.\n");
        alarm(0);
        return 1;
      }
    }
    PureSat_CheckInvariant(network,invarArray,
                           (int)options->verbosityLevel,
                           options->dbgLevel,McOptionsReadDebugFile(options),
                           McOptionsReadPrintInputs(options),options->incre,
                           options->sss, options->flatIP, options->IPspeed);
    McOptionsFree(options);
    return 0;
  }
  guideFile =  McOptionsReadGuideFile(options);

  if(guideFile != NIL(FILE) ){
    hintsArray = Mc_ReadHints(guideFile);
    fclose(guideFile); guideFile = NIL(FILE);
    if( hintsArray == NIL(array_t) ){
      McOptionsFree(options);
      return 1;
    }
  } /* if guided search */

  if(Img_UserSpecifiedMethod() != Img_Iwls95_c &&
     Img_UserSpecifiedMethod() != Img_Monolithic_c &&
     Img_UserSpecifiedMethod() != Img_Mlp_c &&
     guideFile != NIL(FILE)){
    fprintf(vis_stdout,
 "** inv error: The Tfm and Hybrid image methods are incompatible with -g\n");
    McOptionsFree(options);
    return 1;
  }

  if (dcLevel == McDcLevelArdc_c)
    ardc = 1;
  else
    ardc = 0;

  /* obtain the fsm and mdd manager */
  totalFsm = Fsm_NetworkReadOrCreateFsm(network);
  if (totalFsm == NIL(Fsm_Fsm_t)) {
    fprintf(vis_stderr, "%s\n", error_string());
    error_init();
    McOptionsFree(options);
    return 1;
  }

  systemVarBddIdTable = 0;
  systemFile = McOptionsReadSystemFile(options);
  if(systemFile != NIL(FILE) ){
    systemVarBddIdTable = Mc_ReadSystemVariablesFAFW(totalFsm, systemFile);
    fclose(systemFile); systemFile = NIL(FILE);
    if(systemVarBddIdTable == (st_table *)-1 ){
      McOptionsFree(options);
      return 1;
    }
  } /* if FAFW */

  if(options->FAFWFlag && systemVarBddIdTable == 0) {
    systemVarBddIdTable = Mc_SetAllInputToSystem(totalFsm);
  }

  mddMgr = Fsm_FsmReadMddManager(totalFsm);
  tautology = mdd_one(mddMgr);

  /* set time out */
  if (timeOutPeriod > 0) {
    /* Set the static variables used by the signal handler. */
    mcTimeOut = timeOutPeriod;
    alarmLapTime = util_cpu_ctime();
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout, "# INV: Checking Invariant: timeout occurred after %d seconds.\n", timeOutPeriod);
      (void) fprintf(vis_stdout, "# INV: data may be corrupted.\n");
      alarm(0);
      return 1;
    }
  }

  /* debugFlag = 1 -> need to store/compute onion shells, else not */
  debugFlag = (McOptionsReadDbgLevel(options) != McDbgLevelNone_c);

  /* use formula tree if reduce option and dont-care level is high */
  if ((McOptionsReadReduceFsm(options) == TRUE) &&
     (dcLevel != McDcLevelNone_c)) {
      McOptionsSetUseFormulaTree(options, TRUE);
  }

  /* derive the normalized array of invariant formulas */
  if (McOptionsReadUseFormulaTree(options) == TRUE) {
    invarNormalFormulaArray =
      Ctlp_FormulaArrayConvertToExistentialFormTree(invarArray);
  } else {
    array_t *temp = Ctlp_FormulaArrayConvertToDAG( invarArray );
    array_free( invarArray );
    invarArray = temp;
    invarNormalFormulaArray = Ctlp_FormulaDAGConvertToExistentialFormDAG(
      invarArray );
  }

  if (array_n(invarNormalFormulaArray) == 0) {
    array_free(invarNormalFormulaArray);
    Ctlp_FormulaArrayFree(invarArray);
    mdd_free(tautology);
    return 1;
  }
  fsmArray = array_alloc(Fsm_Fsm_t *, 0);
  sortedFormulaArray = SortFormulasByFsm(totalFsm, invarNormalFormulaArray,
                                         fsmArray, options);
  if (sortedFormulaArray == NIL(array_t)) {
    array_free(invarNormalFormulaArray);
    Ctlp_FormulaArrayFree(invarArray);
    mdd_free(tautology);
    return 1;
  }
  assert(array_n(fsmArray) == array_n(sortedFormulaArray));

  careSetArray = array_alloc(mdd_t *, 0);

  /* main loop for array of array of formulas. Each of the latter
     arrays corresponds to one reduced fsm. */
  arrayForEachItem(array_t *, sortedFormulaArray, i, formulas) {
    int *resultArray;
    int fail;
    /* initialize pass, fail array */
    resultArray = ALLOC(int, array_n(formulas));
    for (j = 0; j < array_n(formulas); j++) {
      resultArray[j] = 1;
    }
    /* get reduced fsm for this set of formulas */
    modelFsm = array_fetch(Fsm_Fsm_t *, fsmArray, i);

    /* evaluate hints for this reduced fsm, stop if the hints contain variables
     * outside this model FSM.
     */
    if (hintsArray != NIL(Ctlp_FormulaArray_t)) {
      int k;
      hintsStatesArray = Mc_EvaluateHints(modelFsm, hintsArray);
      if( hintsStatesArray == NIL(array_t)) { /* something wrong, clean up */
        int l;
        fprintf(vis_stdout, "Hints dont match the reduced FSM for this set of invariants.\n");
        fprintf(vis_stdout, "Continuing with the next set of invariants\n");
        for (k = i; k < array_n(sortedFormulaArray); k++) {
          formulas = array_fetch(array_t *, sortedFormulaArray, k);
          arrayForEachItem(Ctlp_Formula_t *, formulas, l, invarFormula) {
            Ctlp_FormulaFree(invarFormula);
          }
          array_free(formulas);
          /* get reduced fsm for this set of formulas */
          modelFsm = array_fetch(Fsm_Fsm_t *, fsmArray, k);
          /* free the Fsm if it was reduced here */
          if (modelFsm != totalFsm) Fsm_FsmFree(modelFsm);
        }
        array_free(careSetArray);
        array_free(fsmArray);
        array_free(sortedFormulaArray);
        array_free(invarNormalFormulaArray);
        (void) fprintf(vis_stdout, "\n");

        Ctlp_FormulaArrayFree(invarArray);
        McOptionsFree(options);
        mdd_free(tautology);
        return 1;
      }
    }/* hints exist */

    if(options->FAFWFlag > 1) {
      reachableStates = Fsm_FsmComputeReachableStates(
          modelFsm, 0, verbosity , 0, 0, 1, 0, 0,
          approxFlag, ardc, 0, 0, (verbosity > 1),
          hintsStatesArray);
      mdd_free(reachableStates);
    }


    invarStatesArray = array_alloc(mdd_t *, 0);
    array_insert(mdd_t *, careSetArray, 0, tautology);
    arrayForEachItem(Ctlp_Formula_t *, formulas, j, invarFormula) {
      /* compute the set of states represented by the invariant. */
      invarFormulaStates =
        Mc_FsmEvaluateFormula(modelFsm, invarFormula, tautology,
                              NIL(Fsm_Fairness_t), careSetArray,
                              MC_NO_EARLY_TERMINATION,
                              NIL(Fsm_HintsArray_t), Mc_None_c,
                              verbosity, dcLevel, buildOnionRings,
                              McGSH_EL_c);

      array_insert_last(mdd_t *, invarStatesArray, invarFormulaStates);
    }

    printStep = (verbosity == McVerbosityMax_c) && (totalFsm == modelFsm);
    /* main loop to check a set of invariants. */
    do {
      boolean compute = FALSE;
      /* check if the computed reachable set in the total FSM already violates an invariant. */
      compute = TestInvariantsInTotalFsm(totalFsm, invarStatesArray, (debugFlag ||
                                                         buildOnionRings));

      /* compute reachable set or until early failure */
      if (compute)
        reachableStates = Fsm_FsmComputeReachableStates(
          modelFsm, 0, verbosity , 0, 0, (debugFlag || buildOnionRings), 0, 0,
          approxFlag, ardc, 0, invarStatesArray, (verbosity > 1),
          hintsStatesArray);
      else if (debugFlag || buildOnionRings) {
        (void)Fsm_FsmReachabilityOnionRingsStates(totalFsm, &reachableStates);
      } else {
        reachableStates = mdd_dup(Fsm_FsmReadCurrentReachableStates(totalFsm));
      }

      ardc = 0; /* once ardc is applied, we don't need it again. */
      /* updates result array and sets fail if any formula failed.*/
      fail = UpdateResultArray(reachableStates, invarStatesArray, resultArray);
      mdd_free(reachableStates);
      someLeft = 0;
      if (fail) {
        /* some invariant failed */
        if (debugFlag) {
          assert (approxFlag != Fsm_Rch_Oa_c);
          Fsm_FsmSetFAFWFlag(modelFsm, options->FAFWFlag);
          Fsm_FsmSetSystemVariableFAFW(modelFsm, systemVarBddIdTable);
          InvarPrintDebugInformation(modelFsm, formulas, invarStatesArray,
                                     resultArray, options, hintsStatesArray);
          Fsm_FsmSetFAFWFlag(modelFsm, 0);
          Fsm_FsmSetSystemVariableFAFW(modelFsm, 0);
        } else if (approxFlag == Fsm_Rch_Oa_c) {
          assert(!buildOnionRings);
          /* May be a false negative */
          /* undo failed results in the result array, report passed formulae */
          arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
            if (invarFormulaStates == NIL(mdd_t)) continue;
            /* print all formulae that are known to have passed */
            if (resultArray[j] == 1) {
              mdd_free(invarFormulaStates);
              array_insert(mdd_t *, invarStatesArray, j, NIL(mdd_t));
              (void) fprintf(vis_stdout, "# INV: Early detection - formula passed --- ");
              invarFormula = array_fetch(Ctlp_Formula_t *, formulas, j);
              Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula));
              fprintf(vis_stdout, "\n");
            } else resultArray[j] = 1;
          }
          fprintf(vis_stdout, "# INV: Invariant violated by over-approximated reachable states\n");
          fprintf(vis_stdout, "# INV: Switching to BFS (exact computation) to resolve false negatives\n");
          /* compute reachable set or until early failure */
          reachableStates = Fsm_FsmComputeReachableStates(
            modelFsm, 0, verbosity , 0, 0, 0, 0, 0, Fsm_Rch_Bfs_c, ardc, 0,
            invarStatesArray, (verbosity > 1), hintsStatesArray);
          /* either invariant has failed or all reachable states are computed */
          /* updates result array */
          fail = UpdateResultArray(reachableStates, invarStatesArray, resultArray);
          mdd_free(reachableStates);
        }
        /* remove the failed invariants from the invariant list. */
        if (fail) {
          arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
            if (invarFormulaStates == NIL(mdd_t)) continue;
            /* free the failed invariant mdds */
            if (resultArray[j] == 0) {
              mdd_free(invarFormulaStates);
              array_insert(mdd_t *, invarStatesArray, j, NIL(mdd_t));
              if (!debugFlag) {
                (void) fprintf(vis_stdout, "# INV: Early detection - formula failed --- ");
                invarFormula = array_fetch(Ctlp_Formula_t *, formulas, j);
                Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(invarFormula));
                fprintf(vis_stdout, "\n");
              }
            } else {
              someLeft = 1;
            }
          }
        }
      } /* end of recomputation dur to over approximate computation */
    } while (someLeft);

    arrayForEachItem(mdd_t *, invarStatesArray, j, invarFormulaStates) {
      if (invarFormulaStates == NIL(mdd_t)) continue;
      /* free the passed invariant mdds */
      mdd_free(invarFormulaStates);
    }
    array_free(invarStatesArray);
    if (printStep) {
      finalTime = util_cpu_time();
      Fsm_FsmReachabilityPrintResults(modelFsm,finalTime-initTime ,approxFlag);
    }
    /* free the Fsm if it was reduced here */
    if (modelFsm != totalFsm) Fsm_FsmFree(modelFsm);


    PrintInvPassFail(formulas, resultArray);


    arrayForEachItem(Ctlp_Formula_t *, formulas, j, invarFormula) {
      Ctlp_FormulaFree(invarFormula);
    }
    array_free(formulas);
    FREE(resultArray);
  } /* end of processing the sorted array of array of invariants */

  if(hintsStatesArray != NIL(array_t))
    mdd_array_free(hintsStatesArray);
  if(hintsArray)
    Ctlp_FormulaArrayFree(hintsArray);
  array_free(careSetArray);
  array_free(fsmArray);
  array_free(sortedFormulaArray);
  array_free(invarNormalFormulaArray);
  (void) fprintf(vis_stdout, "\n");

  if (options->FAFWFlag) {
    st_free_table(systemVarBddIdTable);
  }

  Ctlp_FormulaArrayFree(invarArray);
  McOptionsFree(options);
  mdd_free(tautology);

  alarm(0);
  return 0;
}


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

  Synopsis    [Parse command line options for invar.]

  SideEffects []

******************************************************************************/
static McOptions_t *
ParseInvarOptions(
  int argc,
  char **argv)
{
  unsigned int i;
  int c;
  boolean useMore = FALSE;
  boolean reduceFsm = FALSE;
  boolean printInputs = FALSE;
  boolean useFormulaTree = FALSE;
  FILE *inputFp=NIL(FILE);
  FILE *debugOut=NIL(FILE);
  char *debugOutName=NIL(char);
  McDbgLevel dbgLevel = McDbgLevelNone_c;
  Mc_VerbosityLevel verbosityLevel = McVerbosityNone_c;
  int timeOutPeriod = 0;
  McOptions_t *options = McOptionsAlloc();
  int approxFlag = 0, ardc = 0, shellFlag = 0;
  Fsm_RchType_t rchType;
  FILE *guideFile;
  FILE *systemFile = NIL(FILE);
  boolean FAFWFlag = FALSE;
  boolean GFAFWFlag = FALSE;
  char *guideFileName = NIL(char);
  char *variablesForSystem = NIL(char);
  int incre, speed;
  /* int sss; */

  /*
   * Parse command line options.
   */

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "ifcrt:g:hmv:d:A:DO:Ww:I:SPs:")) != EOF) {
    switch(c) {
      case 'g':
        guideFileName = util_strsav(util_optarg);
        break;
      case 'h':
        goto usage;
      case 't':
        timeOutPeriod = atoi(util_optarg);
        break;
      case 'v':
        for (i = 0; i < strlen(util_optarg); i++) {
          if (!isdigit((int)util_optarg[i])) {
            goto usage;
          }
        }
        verbosityLevel = (Mc_VerbosityLevel) atoi(util_optarg);
        break;
      case 'd':
        for (i = 0; i < strlen(util_optarg); i++) {
          if (!isdigit((int)util_optarg[i])) {
            goto usage;
          }
        }
        dbgLevel = (McDbgLevel) atoi(util_optarg);
        break;
      case 'f':
        shellFlag = 1;
        break;
      case 'r' :
        reduceFsm = TRUE;
        break;
      case 'm':
        useMore = TRUE;
        break;
      case 'i' :
        printInputs = TRUE;
        break;
      case 'c' :
        useFormulaTree = TRUE;
        break;
      case 'A':
        approxFlag = atoi(util_optarg);
        if ((approxFlag > 4) || (approxFlag < 0)) {
            goto usage;
        }
        break;
      case 'D':
        ardc = 1;
        break;
      case 'O':
        debugOutName = util_strsav(util_optarg);
        break;
      case 'w':
        variablesForSystem = util_strsav(util_optarg);
      case 'W':
        FAFWFlag = 1;
        break;
      case 'G':
        GFAFWFlag = 1;
        break;
      case 'I':
        incre = atoi(util_optarg);
        options->incre = (incre==0)? FALSE:TRUE;
        break;
      case 'S':
        /*sss = atoi(util_optarg);*/
        /*options->sss = (sss==0)? FALSE:TRUE;*/
        options->sss = TRUE;
        break;
      case 'P':
        options->flatIP = TRUE;
        break;
      case 's':
        speed = atoi(util_optarg);
        options->IPspeed = speed;
        break;
      default:
        goto usage;
    }
  }

  if((FAFWFlag > 0 || GFAFWFlag > 0) &&  dbgLevel == 0) {
    fprintf(vis_stderr, "** inv warning : -w and -W options are ignored without -d option\n");
  }

  if((FAFWFlag > 0 || GFAFWFlag > 0) &&  printInputs == 0) {
    fprintf(vis_stderr, "** inv warning : -i is recommended with -w or -W option\n");
  }

  if(FAFWFlag) {
    if (bdd_get_package_name() != CUDD) {
      fprintf(vis_stderr, "** inv warning : -w and -W option is only available with CUDD\n");
      FAFWFlag = 0;
      FREE(variablesForSystem);
      variablesForSystem = NIL(char);
    }
  }


  /* translate approx flag */
  switch(approxFlag) {
  case 0: rchType = Fsm_Rch_Bfs_c; break;
  case 1: rchType = Fsm_Rch_Hd_c; break;
  case 2: rchType = Fsm_Rch_Oa_c; break;
  case 3: rchType = Fsm_Rch_Grab_c; break;
  case 4: rchType = Fsm_Rch_PureSat_c; break;
  default: rchType = Fsm_Rch_Default_c; break;
  }

  if ((approxFlag == 1) && (bdd_get_package_name() != CUDD)) {
    fprintf(vis_stderr, "** inv error: check_invariant with -A 1 option is currently supported by only CUDD.\n");
    return NIL(McOptions_t);
  }

  if (rchType == Fsm_Rch_Oa_c) {
    if (dbgLevel > 0) {
      fprintf(vis_stdout, "Over approximation and debug level 1 are incompatible\n");
      fprintf(vis_stdout, "Read check_invariant help page\n");
      goto usage;
    } else if (shellFlag == 1) {
      fprintf(vis_stdout, "Over approximation and shell flag are incompatible\n");
      fprintf(vis_stdout, "Read check_invariant help page\n");
      goto usage;
    }
  }

  if (rchType == Fsm_Rch_Grab_c) {
    if (guideFileName != NIL(char)) {
      fprintf(vis_stdout, "Abstraction refinement Grab and guided search are incompatible\n");
      fprintf(vis_stdout, "Read check_invariant help page\n");
      goto usage;
    }
  }

  if (rchType == Fsm_Rch_PureSat_c) {
    if (guideFileName != NIL(char)) {
      fprintf(vis_stdout, "Abstraction refinement PureSat and guided search are incompatible\n");
      fprintf(vis_stdout, "Read check_invariant help page\n");
      goto usage;
    }
  }

  if (guideFileName != NIL(char)) {
    guideFile = Cmd_FileOpen(guideFileName, "r", NIL(char *), 0);
    FREE(guideFileName);
    if (guideFile == NIL(FILE)) {
      McOptionsFree(options);
      return NIL(McOptions_t);
    }
    McOptionsSetGuideFile(options, guideFile);
  }

  /*
   * Open the ctl file.
   */
  if (argc - util_optind == 0) {
    (void) fprintf(vis_stderr, "** inv error: file containing invariant formulas not provided\n");
    goto usage;
  }
  else if (argc - util_optind > 1) {
    (void) fprintf(vis_stderr, "** inv error: too many arguments\n");
    goto usage;
  }

  McOptionsSetUseMore(options, useMore);
  McOptionsSetReduceFsm(options, reduceFsm);
  McOptionsSetPrintInputs(options, printInputs);
  McOptionsSetUseFormulaTree(options, useFormulaTree);
  McOptionsSetTimeOutPeriod(options, timeOutPeriod);
  McOptionsSetInvarApproxFlag(options, rchType);
  if (ardc)
    McOptionsSetDcLevel(options, McDcLevelArdc_c);
  else
    McOptionsSetDcLevel(options, McDcLevelNone_c);
  McOptionsSetInvarOnionRingsFlag(options, shellFlag);
  McOptionsSetFAFWFlag(options, FAFWFlag + GFAFWFlag);

  inputFp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
  if (inputFp == NIL(FILE)) {
    McOptionsFree(options);
    return NIL(McOptions_t);
  }
  McOptionsSetCtlFile(options, inputFp);

  if (debugOutName != NIL(char)) {
    debugOut = Cmd_FileOpen(debugOutName, "w", NIL(char *), 0);
    if (debugOut == NIL(FILE)) {
      McOptionsFree(options);
      return NIL(McOptions_t);
    }
  }
  McOptionsSetDebugFile(options, debugOut);

  if ((verbosityLevel != McVerbosityNone_c) &&
       (verbosityLevel != McVerbosityLittle_c) &&
       (verbosityLevel != McVerbositySome_c) &&
       (verbosityLevel != McVerbosityMax_c)) {
    goto usage;
  }
  else {
    McOptionsSetVerbosityLevel(options, verbosityLevel);
  }

  if ((dbgLevel != McDbgLevelNone_c) &&
       (dbgLevel != McDbgLevelMin_c)) {
    if(((rchType == Fsm_Rch_Grab_c) && (dbgLevel == McDbgLevelMinVerbose_c)))
    {
      McOptionsSetDbgLevel(options, dbgLevel);
    }
    else
    {
      if((rchType == Fsm_Rch_PureSat_c) && (options->flatIP == TRUE) && (dbgLevel == McDbgLevelMinVerbose_c))
      {
        McOptionsSetDbgLevel(options, dbgLevel);
      }
      else
      {
        if((rchType == Fsm_Rch_Bfs_c) && (dbgLevel == McDbgLevelMinVerbose_c))
        {
          McOptionsSetDbgLevel(options, dbgLevel);
        }
        else
        {
          goto usage;
        }
      }
    }
  }
  else {
    McOptionsSetDbgLevel(options, dbgLevel);
  }

  if (variablesForSystem != NIL(char)) {
    systemFile = Cmd_FileOpen(variablesForSystem, "r", NIL(char *), 0);
    if (systemFile == NIL(FILE)) {
      fprintf(vis_stderr, "** inv error: cannot open system variables file for FAFW %s.\n",
              variablesForSystem);
      FREE(variablesForSystem);
      variablesForSystem = NIL(char);
      McOptionsFree(options);
      return NIL(McOptions_t);
    }
    FREE(variablesForSystem);
    variablesForSystem = NIL(char);
  }
  McOptionsSetVariablesForSystem(options, systemFile);


  return options;

  usage:
  (void) fprintf(vis_stderr, "usage: check_invariant [-c][-d dbg_level][-f][-g <hintfile>][-h][-i][-m][-r][-v verbosity_level][-t time_out][-A <number>][-D dc_level] [-O <dbg_out>] <invar_file>\n");
  (void) fprintf(vis_stderr, "    -c  avoid sub-formula sharing between formulae\n");
  (void) fprintf(vis_stderr, "    -d  <dbg_level>");
  (void) fprintf(vis_stderr, "        dbg_level = 0 => no debug output (Default)\n");
  (void) fprintf(vis_stderr, "        dbg_level = 1 => print debug trace. (available for all options)\n ");
  (void) fprintf(vis_stderr, "        dbg_level = 2 => print debug trace in Aiger format. (available for -A0, -A3, -A4 and -A4 -P)\n");
  (void) fprintf(vis_stderr, "    -f \tStore the onion rings at each step.\n");
  (void) fprintf(vis_stderr, "    -g <hint_file> \tSpecify file for guided search.\n");
  (void) fprintf(vis_stderr, "    -i \tPrint input values in debug traces.\n");
  (void) fprintf(vis_stderr, "    -m  pipe debugger output through UNIX utility more\n");
  (void) fprintf(vis_stderr, "    -r  reduce FSM with respect to invariant being checked\n");
  (void) fprintf(vis_stderr, "    -t <period> Time out period.\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, "    -A  <number> Use Different types of reachability analysis\n");
  (void) fprintf(vis_stderr, "            0 (default) - BFS method.\n");
  (void) fprintf(vis_stderr, "            1 - HD method.\n");
  (void) fprintf(vis_stderr, "            2 - Over-approximation.\n");
  (void) fprintf(vis_stderr, "            3 - Abstraction refinement GRAB.\n");
  (void) fprintf(vis_stderr, "    -D  minimize transition relation with ARDCs\n");
  (void) fprintf(vis_stderr, "    -O <dbg_out>\n");
  (void) fprintf(vis_stderr, "        write error trace to dbg_out\n");
  (void) fprintf(vis_stderr, "    -W \tUse fate and free will algorithm when all the variables are controlled by system.\n");
  (void) fprintf(vis_stderr, "    -G \tUse general fate and free will algorithm.\n");
  (void) fprintf(vis_stderr, "    -w <node file> \tSpecify variables controlled by system.\n");
  (void) fprintf(vis_stderr, "    <invar_file> The input file containing invariants to be checked.\n");
  (void) fprintf(vis_stderr, "    -h \tPrints this usage message.\n");
  (void) fprintf(vis_stderr, "    -I \tSwitch for Incremental SAT solver in PureSAT method abstraction refinement\n");
  McOptionsFree(options);

  return NIL(McOptions_t);
}

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

  Synopsis    [Handle function for timeout.]

  Description [This function is called when the time out occurs.
  Since alarm is set with an elapsed time, this function checks if the
  CPU time corresponds to the timeout of the command.  If not, it
  reprograms the alarm to fire again later.]

  SideEffects []

******************************************************************************/
static void
TimeOutHandle(void)
{
  int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);

  if (seconds < mcTimeOut) {
    unsigned slack = (unsigned) (mcTimeOut - seconds);
    (void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
    (void) alarm(slack);
  } else {
    longjmp(timeOutEnv, 1);
  }
} /* TimeOutHandle */


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

  Synopsis [Check whether the reachable states violate the array of
  invariants.]

  Description [Check whether the reachable states violate the array of
  invariants. Return 1 if any formula failed. Update the result
  array. Entry 0 implies fail, 1 implies pass.]

  SideEffects []

******************************************************************************/
static int
UpdateResultArray(mdd_t *reachableStates,
                  array_t *invarStatesArray,
                  int *resultArray)
{
  int i;
  mdd_t *invariant;
  int fail = 0;
  arrayForEachItem(mdd_t *, invarStatesArray, i, invariant) {
    if (invariant == NIL(mdd_t)) continue;
    if (!mdd_lequal(reachableStates, invariant, 1, 1)) {
      fail = 1;
      resultArray[i] = 0;
    }
  }
  return fail;
} /* end of UpdateResultArray */


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

  Synopsis [Prints whether the set of invariants passed or failed]

  Description [Prints whether the set of invariants passed or failed.]

  SideEffects []

******************************************************************************/
static void
PrintInvPassFail(array_t *invarFormulaArray,
                 int *resultArray)
{
  int i;
  Ctlp_Formula_t *formula;
  fprintf(vis_stdout, "\n# INV: Summary of invariant pass/fail\n");
  arrayForEachItem(Ctlp_Formula_t *, invarFormulaArray, i, formula) {
    if (resultArray[i]) {
      (void) fprintf(vis_stdout, "# INV: formula passed --- ");
      Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
      fprintf(vis_stdout, "\n");
    } else {
      (void) fprintf(vis_stdout, "# INV: formula failed --- ");
      Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));
      fprintf(vis_stdout, "\n");
    }
  }
  return;
} /* end of PrintInvPassFail */