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

  FileName    [absCmd.c]

  PackageName [abs]

  Synopsis    [Encapsulation for the incremental_ctl_verification command.]

  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]

  Copyright [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

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

#include "absInt.h"

static char rcsid[] UNUSED = "$Id: absCmd.c,v 1.37 2002/09/08 22:13:50 fabio Exp $";

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

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

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

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static jmp_buf timeOutEnv;
static int absTimeOut;
static long alarmLap;

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

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

static int CommandAbsCtl(Hrc_Manager_t **hmgr, int argc, char **argv);
static AbsOptions_t * ParseAbsCtlOptions(int argc, char **argv);
static void TimeOutHandle(int sigType);

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


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


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

  Synopsis [Initialize abs package]

  SideEffects []

******************************************************************************/
void
Abs_Init(void)
{
  Cmd_CommandAdd("incremental_ctl_verification", CommandAbsCtl, 0);
}


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

  Synopsis [End abs package]

  SideEffects []

******************************************************************************/
void
Abs_End(void)
{
}


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

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

  Synopsis [Encapsulation of the incremental_ctl_verification command.]

  Description [The function starts by parsing the options. After that it checks
  for the network structure. The ctl formulas are read and check for
  correctness. Once the formulas have been read, they need to be translated
  from the CTL representation to the operational graph representation required
  for the incremental algorithm. The function AbsCtlFormulaArrayTranslate
  performs this task. After all these points have been cleared, the timeout is
  programmed and the verification process starts.
  
  Once the result has been obtained, the function prints the result as well as
  some execution statistics, de-allocates all the required data structures and
  returns.]

  SideEffects        []

  CommandName        [incremental_ctl_verification] 	   

  CommandSynopsis [Verify a set of CTL formulas by means of an incremental
  model checking algorithm.]

  CommandArguments [\[-D &lt;number&gt;\] \[-e\] \[-h\]  \[-n\] \
  \[-s\] \[-t &lt;seconds&gt;\] \[-v &lt;number&gt;\] \[-V &lt;number&gt;\] 
  \[-x\] &lt;ctlfile&gt;]]

  CommandDescription [
  Like model_check, incremental_ctl_verification verifies a set of CTL
  formulas.  It uses a system of abstraction and incremental
  refinement 
  that works for all of (fair)CTL, using over and underapproximations as
  appropriate. See \[1,2\] for details.
  
  <p> Incremental_ctl_verification (also known as Abs or Trasgo) 
  works especially well on large systems on which mc is too slow or
  runs out of memory.  
  Unlike amc, it can handle full CTL, not just the universal or
  existential subsets of it. Also, fairness is supported with this
  command, although it tends to be inefficient.  
  Support for the mu-calculus is not yet implemented.

  <p>Before using incremental_ctl_verification, a flattened hierarchy
  should be present. See `help init`. Using dynamic variable reordering
  may be beneficial on large systems. See `help
  dynamic_var_ordering`. 

  <p>Fairness constraints can be applied using
  `read_fairness', as with mc.  When using incremental verification
  with fairness, there is no check for unfair initial states. Please
  be aware that if there are no fair initial states, all formulas
  starting with "A" will be trivially true. Mc will tell you whether
  you have fair initial states.

  <p>A typical use would be
  <br>incremental_ctl_verification -D2 &lt;ctl_file&gt;

  <p>For every formula, incremental verification will report whether
  it is valid or invalid, or it returns an inconclusive result. A formula is
  valid iff it holds for all initial states. An error trace is not provided.

  For the people who are used to mc: The -r option is not supported,
  incremental verification always reduces the fsm with respect to
  individual formulas. The -c option is not supported either. There is
  no sharing of subformulas between different formulas.

  <p>Command options:<p>

  <dl>

  <dt> -D &lt;number&gt;
  <dd> Specify extent to which don't cares are used to simplify the
  MDDs.
  <ul> 
  <li>0: No Don't Cares used.
  <li>1: Use reachability information to compute the don't-care
     set. Reachability is performed by formula. This is different from
     mc, where reachability is performed only once.
  <li>2: Use reachability information, and minimize the transition relation
     with respect to the `frontier set' (aggresive minimization).
  </ul>
  The equivalent of mc -D3 is not implemented.

  <dt> -e
  <dd>Compute the set of fair states (those satisfying the formula EGfair TRUE)
  before the verification process and use the result as care set. In certain
  cases this will speed up computation when fairness constraints are
  present. In other cases it will slow it down.

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

  <dt> -n
  <dd> Try to prove the negation of every formula. In some cases it
  may be easier to prove the negation of a formula than the formula
  itself. For systems with only one initial state, a formula is true
  iff its negation is false. Note that for systems with multiple
  initial states a formula and its negation can both be false.

  <dt> -s
  <dd> Print a summary of statistics after the verification.

  <dt> -t &lt;secs&gt;
  <dd> Time in seconds allowed to spend in the verification.  The default is
  infinity.

  <dt> -v &lt;number&gt;
  <dd>Specify verbosity level. Use 0 for no feedback (default), 1
  for more and 2 for maximum feedback. This option can not be used in
  conjunction with -V.

  <dt> -V &lt;number&gt;
  <dd> Mask specifying type of information to be printed out while
  verifying the formulas. This allows for a finer control than -v. -V
  and -v cannot be used simultaneously.
  The mask is given as a binary number, by taking the
  logical or of the following binary values. One does not have to
  convert these numbers to decimal.<p> 
  
                        1  number of primary inputs and flip-flops <p>
                       10  labeled operational graph of the formulas <p>
                      100  cpu-time for the computation in each vertex <p> 
                     1000  cubes of the function sat for each vertex <p> 
                    10000  cubes of the function goalSet for each vertex <p> 
                   100000  vertex data structure contents after evaluation <p>
                  1000000  cubes in the care set for every evaluation <p> 
                 10000000  size of care set for every evaluation <p> 
                100000000  number of states that satisfy every sub-formula <p> 
               1000000000  number of overall reachable states <p> 
              10000000000  cubes for every iteration of a fixed point <p> 
             100000000000  size of the BDD in each iteration in a fix-point <p> 
            1000000000000  labeled operational graph in dot format <p> 
           10000000000000  number of envelope states <p> 
          100000000000000  number of states to be refined <p> 
         1000000000000000  size of the refinement operands <p> 
        10000000000000000  cubes of the refinement operands <p> 
       100000000000000000  Number of latches before and after simplification <p>
      1000000000000000000  report partial progress (i.e. reach, EG(true),...)<p>
     10000000000000000000  Begin/End refinement process <p> 
    100000000000000000000  Size of goal set <p> 
   1000000000000000000000  cubes of the goal set <p> 
  10000000000000000000000  Contents of vertex after refinement <p> 

  <dt> -x
  <dd> Perform the verification exactly. No approximation is done.

  <dt> &lt;ctlfile&gt; 
  <dd> File containing the CTL formulas to be verified.

  <dt> Related "set" options: <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 commands : model_check, incremental_ctl_verification <p>

  </dl>

  <p>1. A. Pardo and G. Hachtel. Automatic abstraction techniques for
  propositional mu-calculus model checking. In <I>9th Conference on
  Computer Aided Verification (CAV'97)</I>. Springer-Verlag. Pages
  12-23, 1997.
  <p>2. A. Pardo and G. Hachtel. Incremental CTL model checking using BDD
  subsetting.  In <I>35th Design Automation Conference
  (DAC'98)</I>. pages 457-462, 1998.   
  ]

******************************************************************************/
static int
CommandAbsCtl(
  Hrc_Manager_t **hmgr,
  int argc,
  char **argv)
{
  AbsVerificationResult_t formulaResult;
  Abs_VerificationInfo_t  *absInfo;
  AbsVertexInfo_t         *formulaPtr;
  Ctlp_Formula_t          *ctlFormula;
  AbsOptions_t            *options;
  Ntk_Network_t           *network;
  array_t                 *ctlArray;
  array_t                 *existCtlArray;
  array_t                 *fairArray;
  array_t                 *existFairArray;
  array_t                 *graphArray;
  array_t                 *resultArray;
  FILE                    *formulaFile;
  boolean                 correctSemantics;
  Fsm_Fsm_t               *fsm;
  Fsm_Fairness_t          *fairness;
  long                    cpuTime;
  int                     status;
  int                     i;
  int                     numConjuncts;

  /* Initialize some variables */
  graphArray = NIL(array_t);
  resultArray = NIL(array_t);
  options = NIL(AbsOptions_t);
  ctlArray = NIL(array_t);
  existCtlArray = NIL(array_t);
  fairArray = NIL(array_t);
  existFairArray = NIL(array_t);
  absInfo = NIL(Abs_VerificationInfo_t);

  if (bdd_get_package_name() != CUDD) {
    fprintf(vis_stderr, "** abs error : incremental_ctl_verification ");
    fprintf(vis_stderr, "is currently supported by only CUDD.\n");
    status = 1;
    goto cleanup;
  }

  error_init();

  /* Parse the options */
  options = ParseAbsCtlOptions(argc, argv);

  /* Check if there has been any error parsing the options */
  if (!options) {
    status = 1;
    goto cleanup;
  }

  /* Obtain the network */
  network = Ntk_HrcManagerReadCurrentNetwork( *hmgr );
  if ( network == NIL( Ntk_Network_t)) {
    (void) fprintf(vis_stdout, "%s\n", error_string());
    error_init();
    status = 1;
    goto cleanup;
  }

  /* Open the file with the ctl formulas */
  formulaFile = Cmd_FileOpen(AbsOptionsReadFileName(options), "r", 
			     NIL(char *), 0);
  if (formulaFile == NIL(FILE)) {
    status = 1;
    goto cleanup;
  }

  /* Parse the formulas and close the file */
  ctlArray = Ctlp_FileParseFormulaArray(formulaFile);
  fclose(formulaFile);

  if (ctlArray == NIL(array_t)) {
    (void) fprintf(vis_stderr, 
		   "** abs error: Error while parsing CTL formulas\n");
    status = 1;
    goto cleanup;
  }

  /* Read the fairness constraints */
  fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  if (fsm != NIL(Fsm_Fsm_t)){
    fairness = Fsm_FsmReadFairnessConstraint(fsm);
    if (fairness != NIL(Fsm_Fairness_t)){
      fairArray = array_alloc(Ctlp_Formula_t *,0);
      numConjuncts = Fsm_FairnessReadNumConjunctsOfDisjunct(fairness, 0);
      for (i = 0; i < numConjuncts; i++) {
        ctlFormula = Fsm_FairnessReadFinallyInfFormula(fairness, 0, i);
        if ((Ctlp_FormulaReadType(ctlFormula) != Ctlp_TRUE_c) &&
            (Ctlp_FormulaReadType(ctlFormula) != Ctlp_FALSE_c)){
	  array_insert_last(Ctlp_Formula_t *, fairArray, 
			    Ctlp_FormulaDup(ctlFormula));
        }
      }
      if (array_n(fairArray) == 0){
        array_free(fairArray);
        fairArray = NIL(array_t);
      }
    }
  }

  /* Verify that the formulas are semantically correct */
  correctSemantics = TRUE;

  /* Check the semantics of the temporal formulas */
  arrayForEachItem(Ctlp_Formula_t *, ctlArray, i, ctlFormula) {
    if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
      (void) fprintf(vis_stdout, 
		 "** abs error: Inconsistency detected in formula number %d.\n",
		     i);
      (void) fprintf(vis_stdout, "ABS: %s\n", error_string());
      error_init();
      correctSemantics = FALSE;
    }
  }

  /* Check the fairness constraints */
  if (fairArray != NIL(array_t)) {
    arrayForEachItem(Ctlp_Formula_t *, fairArray, i, ctlFormula) {
      if (!Mc_FormulaStaticSemanticCheckOnNetwork(ctlFormula, network, FALSE)) {
	(void) fprintf(vis_stdout, 
		       "** abs error: Inconsistency detected in fairness ");
	(void) fprintf(vis_stdout, "constraint number %d.\n", i);
	(void) fprintf(vis_stdout, "ABS: %s\n", error_string());
	error_init();
	correctSemantics = FALSE;
      }
    }
  }

  /* If there is any inconsistency, do not execute the command */
  if (!correctSemantics) {
    status = 1;
    goto cleanup;
  }

  /* Replace XORs and EQs with equivalent subtrees. We insist on having
   * only monotonic operators. */
  Ctlp_FormulaArrayMakeMonotonic(ctlArray);
  Ctlp_FormulaArrayMakeMonotonic(fairArray);

  /* Translate the ctl formulas and fairness constraints to existential form */
  existCtlArray = Ctlp_FormulaArrayConvertToExistentialFormTree(ctlArray);
  if (fairArray != NIL(array_t)) {
    existFairArray = Ctlp_FormulaArrayConvertToExistentialFormTree(fairArray);
  }

  /* Compute the information related to the system being verified */
  absInfo = Abs_VerificationComputeInfo(network);
  if (absInfo == NIL(Abs_VerificationInfo_t)) {
    (void) fprintf(vis_stdout, "** abs error: Error computing the information required ");
    (void) fprintf(vis_stdout, "for verification.\n");
    status = 1;
    goto cleanup;
  }

  /* Store the options */
  AbsVerificationInfoSetOptions(absInfo, options);

  /* Translate the array of CTL formulas to operational graphs */
  graphArray = AbsCtlFormulaArrayTranslate(absInfo, existCtlArray, 
					   existFairArray);

  if (graphArray == NIL(array_t)) {
    (void) fprintf(vis_stderr, 
		   "** abs error: Error translating CTL formulas.\n");
    (void) fprintf(vis_stderr, "** abs error: Aborting command.\n");
    status = 1;
    goto cleanup;
  }

  /* Program the timeOut if pertinent */
  if (AbsOptionsReadTimeOut(options) > 0) {
    /* Set the static variables */
    absTimeOut = AbsOptionsReadTimeOut(options);
    alarmLap = util_cpu_time();

    /* Set the handler */
    (void) signal(SIGALRM, TimeOutHandle);
    (void) alarm(AbsOptionsReadTimeOut(options));
    
    /* Set the jump for the timeout */
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout,
		     "# ABS: Timeout occurred after %7.1f CPU seconds\n",
		     (util_cpu_time() - alarmLap)/1000.0);
      (void) fprintf(vis_stdout, "# ABS: data may be corrupted.\n");
      alarm(0);
      return 1;
    }
  }

  /* Print the graph in DOT format */
  if (AbsOptionsReadVerbosity(options) & ABS_VB_PRDOT) {
      AbsVertexPrintDot(vis_stdout, graphArray);
  }

  /* Set the cpu-time lap */
  cpuTime = util_cpu_time();

  /* Verify every formula */
  resultArray = AbsFormulaArrayVerify(absInfo, graphArray);

  /* Print out the execution time*/
  (void) fprintf(vis_stdout, "ABS: Total Verification Time: %7.1f secs\n",
		 (util_cpu_time() - cpuTime)/1000.0);
  
  /* Print out the results */
  /* RB changed this to take into account multiple initial states in negtd
     formulas */
  arrayForEachItem(AbsVerificationResult_t, resultArray, i, formulaResult) {
    (void) fprintf(vis_stdout, "# ABS: formula ");
    switch (formulaResult) {
    case trueVerification_c:
      (void) fprintf(vis_stdout, "passed --- ");
      break;
    case falseVerification_c:
      (void) fprintf(vis_stdout, "failed --- ");
      break;
    case inconclusiveVerification_c:
      (void) fprintf(vis_stdout, "undecided --- ");
    }
    if (AbsOptionsReadNegateFormula(options))
      fprintf(vis_stdout, "NOT[ ");
    Ctlp_FormulaPrint(vis_stdout, 
		      array_fetch(Ctlp_Formula_t *, ctlArray, i));
    if (AbsOptionsReadNegateFormula(options))
      fprintf(vis_stdout, " ]\n");
    else
      fprintf(vis_stdout, "\n");
  }
  
  /* Print the stats if selected by command line option */
  if (AbsOptionsReadPrintStats(options)) {
    int i;
    
    AbsStatsPrintReport(vis_stdout, AbsVerificationInfoReadStats(absInfo));
    
    (void) fprintf(vis_stdout, "# ABS: -- Command Line Options --\n");
    (void) fprintf(vis_stdout, "# ABS: ");
    for (i=0; i<argc; i++) {
      (void) fprintf(vis_stdout, "%s ", argv[i]);
    }
    (void) fprintf(vis_stdout, "\n");
  }
  
  /* Disconnect the alarm */
  alarm(0);
  
  status = 0;
  
  /* Clean up the memory and return */
  cleanup:
  if (graphArray != NIL(array_t)) {
    arrayForEachItem(AbsVertexInfo_t *, graphArray, i, formulaPtr) {
      AbsVertexFree(AbsVerificationInfoReadCatalog(absInfo), formulaPtr,
		    NIL(AbsVertexInfo_t));
    }
    array_free(graphArray);
  }
  if (resultArray != NIL(array_t)) {
    array_free(resultArray);
  }
  if (options != NIL(AbsOptions_t)) {
    AbsOptionsFree(options);
  }
  if (ctlArray != NIL(array_t)) {
    Ctlp_FormulaArrayFree(ctlArray);
  }
  if (existCtlArray != NIL(array_t)) {
    Ctlp_FormulaArrayFree(existCtlArray);
  }
  if (fairArray != NIL(array_t)) {
    Ctlp_FormulaArrayFree(fairArray);
  }
  if (existFairArray != NIL(array_t)) {
    Ctlp_FormulaArrayFree(existFairArray);
  }
  if (absInfo != NIL(Abs_VerificationInfo_t)) {
    AbsVerificationInfoFree(absInfo);
  }
  
  return status;
} /* End of CommandAbsCtl */

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

  Synopsis [Parses the options given to the incremental_ctl_verification command
  and stores them into a structure.]

  SideEffects        []

  SeeAlso            [CommandAbsCtl]

******************************************************************************/
static AbsOptions_t *
ParseAbsCtlOptions(
  int argc,
  char **argv)
{
  AbsOptions_t *result;
  char *fileName;
  boolean reachability;
  boolean envelope;
  boolean exact;
  boolean printStats;
  boolean minimizeIterate;
  boolean negateFormula;
  boolean partApprox;
  boolean DFlag, eFlag, nFlag, pFlag, sFlag, tFlag, vFlag, xFlag;
  long verbosity;
  int intVerbosity;
  int timeOut;
  int dcValue;
  int c;
  unsigned int i;

  /* Default Options */
  DFlag = eFlag = nFlag = pFlag = sFlag = tFlag = FALSE;
  vFlag = xFlag = FALSE;
  reachability = FALSE;
  envelope = FALSE;
  exact = FALSE;
  printStats = FALSE;
  minimizeIterate = FALSE;
  negateFormula = FALSE;
  partApprox = FALSE;
  verbosity = 0;
  intVerbosity = 0;
  timeOut = -1;
  dcValue = 0;

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "D:ehnpst:v:V:x")) != EOF) {
    switch(c) {
      case 'D':
	dcValue = atoi(util_optarg);
	if (DFlag || (dcValue < 0) || (dcValue > 2)) {
	  goto usage;
	}
	if (dcValue > 0) {
	  reachability = TRUE;
	}
	if (dcValue > 1) {
	  minimizeIterate = TRUE;
	}
	DFlag = TRUE;
	break;
      case 'e':
	if (eFlag) {
	  goto usage;
	}
	envelope = TRUE;
	eFlag = TRUE;
	break;
      case 'h':
        goto usage;
      case 'n':
	if (nFlag) {
	  goto usage;
	}
	negateFormula = TRUE;
	nFlag = TRUE;
	break;
      case 'p':
	if (pFlag) {
	  goto usage;
	}
	partApprox = TRUE;
	pFlag = TRUE;
        break;
      case 's':
	if (sFlag) {
	  goto usage;
	}
	printStats = TRUE;
	sFlag = TRUE;
        break;
      case 't':
	if (tFlag) {
	  goto usage;
	}
	timeOut = atoi(util_optarg);
	tFlag = TRUE;
        break;
      case 'v':
	if (vFlag) {
	  goto usage;
	}
	intVerbosity =  atoi(util_optarg);
        if (intVerbosity == 1){
	  verbosity = 131849;
	}else if (intVerbosity == 2){
	  verbosity = 8388607;
	}else{
	  verbosity = 0;
        }
        vFlag = TRUE;
	break;
      case 'V':
	if (vFlag) {
	  goto usage;
	}
	for(i=0;i<strlen(util_optarg)-1;i++){
          if (util_optarg[i] != '0' && util_optarg[i] != '1'){
	     goto usage;
	  }
	}
	verbosity =  strtol(util_optarg, NIL(char *), 2);
	vFlag = TRUE;
        break;
      case 'x':
	if (xFlag) {
	  goto usage;
	}
	exact = TRUE;
	xFlag = TRUE;
	break;
      default:
	goto usage;
    }
  }

  /* Check if there is still one parameter left */
  if (argc - util_optind != 1) {
    goto usage;
  }

  /* Obtain the filename from the end of the command line */
  fileName = util_strsav(argv[util_optind]);
  
  /* Store the options  */
  result = AbsOptionsInitialize();
  
  AbsOptionsSetVerbosity(result, verbosity);
  AbsOptionsSetTimeOut(result, timeOut);
  AbsOptionsSetReachability(result, reachability);
  AbsOptionsSetEnvelope(result, envelope);
  AbsOptionsSetFileName(result, fileName);
  AbsOptionsSetExact(result, exact);
  AbsOptionsSetPrintStats(result, printStats);
  AbsOptionsSetMinimizeIterate(result, minimizeIterate);
  AbsOptionsSetNegateFormula(result, negateFormula);
  AbsOptionsSetPartApprox(result, partApprox);

  return result;

 usage:
  fprintf(vis_stderr,"usage: incremental_ctl_verification [-D <number>] [-e] [-h] [-n] [-s]\n");
  fprintf(vis_stderr,"[-t <seconds>] [-v <number>] [-V <number>] [-x] <ctlfile>\n");
  fprintf(vis_stderr,"\n");
  fprintf(vis_stderr,"Command options:\n");
  fprintf(vis_stderr,"-D <number>\n");
  fprintf(vis_stderr,"   Specify extent to which don't cares are used to simplify\n");
  fprintf(vis_stderr,"   the MDDs.\n");
  fprintf(vis_stderr,"   0: No Don't Cares used.\n");
  fprintf(vis_stderr,"   1: Use reachability information to compute the don't-care\n");
  fprintf(vis_stderr,"     set. Reachability is performed by formula. This is different from\n");
  fprintf(vis_stderr,"     mc, where reachability is performed only once.\n");
  fprintf(vis_stderr,"   2: Use reachability information, and minimize the transition relation\n");
  fprintf(vis_stderr,"     with respect to the `frontier set' (aggresive minimization).\n");
  fprintf(vis_stderr,"-e\n");
  fprintf(vis_stderr,"   Compute the set of fair states (those satisfying the formula\n");
  fprintf(vis_stderr,"   EGfair TRUE) before the verification process and use the result\n");
  fprintf(vis_stderr,"   as care set.\n");
  fprintf(vis_stderr,"-h\n");
  fprintf(vis_stderr,"   Print the command usage.\n");
  fprintf(vis_stderr,"-n\n");
  fprintf(vis_stderr,"   Try to prove the negation of every formula\n");
  fprintf(vis_stderr,"-s\n");
  fprintf(vis_stderr,"   Print a summary of statistics after the verification.\n");
  fprintf(vis_stderr,"-t <secs>\n");
  fprintf(vis_stderr,"   Time in seconds allowed to spend in the verification.\n");
  fprintf(vis_stderr,"-v <number>\n");
  fprintf(vis_stderr,"   Specify verbosity level. Use 0 for no feedback (default), 1 for\n");
  fprintf(vis_stderr,"   more and 2 for maximum feedback. This option can not be used\n");
  fprintf(vis_stderr,"   in conjunction with -V.\n");
  fprintf(vis_stderr,"-V <number>\n");
  fprintf(vis_stderr,"   Mask specifying type of information to be printed out while\n");
  fprintf(vis_stderr,"   verifying the formulas. See the help page.\n");
  fprintf(vis_stderr,"-x\n");
  fprintf(vis_stderr,"   Perform the verification exactly. No approximation is done.\n");
  fprintf(vis_stderr,"<ctlfile>\n");
  fprintf(vis_stderr,"   File containing the CTL formulas to be verified.\n");
  return NIL(AbsOptions_t);
} /* End of ParseAbsCtlOptions */

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

  Synopsis    [Handle function for timeout.]

  Description [This function is called when the process receives a signal of
  type alarm. Since alarm is set with elapsed time, this function checks if the
  CPU time corresponds to the timeout of the command. If not, it reprograms the
  alarm to fire later and check if the CPU limit has been reached.]

  SideEffects []

******************************************************************************/
static void
TimeOutHandle(
  int sigType)
{
  long seconds;

  seconds = (util_cpu_time() - alarmLap) / 1000;
  
  if (seconds < absTimeOut) {
    unsigned slack;

    slack = absTimeOut - seconds;
    (void) signal(SIGALRM, TimeOutHandle);
    (void) alarm(slack);
  }
  else {
    longjmp(timeOutEnv, 1);
  }
} /* End of TimeOutHandle */