source: vis_dev/vis-2.3/models/transition/mc.html

/**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);

    /* 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;
}