src/abs/absCmd.c

Go to the documentation of this file.

#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;

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

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


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


void
Abs_End(void)
{
}


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

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/
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 */

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

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