src/imc/imcCmd.c

Go to the documentation of this file.

#include "imcInt.h"
#include "fsm.h"

static char rcsid[] UNUSED = "$Id: imcCmd.c,v 1.24 2002/09/10 04:07:38 fabio Exp $";


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

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

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

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

static jmp_buf timeOutEnv;

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

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

static int CommandImc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static void IterativeModelCheckUsage(void);
static void TimeOutHandle(void);

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

void
Imc_Init(void)
{
  Cmd_CommandAdd("iterative_model_check", CommandImc, 0);
}


void
Imc_End(void)
{
}


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


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

static int
CommandImc(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  static int          timeOutPeriod;      /* CPU seconds allowed */
  char                *ctlFileName;       /* Name of file containing formulas */
  FILE                *ctlFile;           /* File to read the formulas from */
  Ntk_Network_t       *network;           /* Pointer to the current network */
  array_t             *ctlFormulaArray;   /* Array of read ctl formulas */
  array_t             *ctlNormalForm;     /* Array of normal ctl formulas */
  Ctlp_Formula_t      *formula;           /* Formula being verified */
  Ctlp_Formula_t      *orgFormula; 
  Ctlp_Formula_t      *currentFormula; 
  char                *modelName;
  Hrc_Node_t          *currentNode;
  int                 c, i;
  array_t             *dagFormula;
  Imc_RefineMethod    refine;             /* Refine Method */
  mdd_t               *careStates;        /* Care States */
  Imc_DcLevel         dcLevel;            /* Don't Care Level */
  Imc_VerbosityLevel  verbosity;          /* Verbosity level */
  Fsm_Fsm_t           *reducedFsm;
  Fsm_Fsm_t           *exactFsm;
  int                 incrementalSize;
  int                 option;
  Fsm_ArdcOptions_t   *ardcOptions;
  Imc_GraphType       graphType;
  Imc_LowerMethod     lowerMethod;
  Imc_UpperMethod     upperMethod;
  boolean             needLower, needUpper;
  boolean             computeExact;
  Imc_PartMethod      partMethod;
  graph_t             *partition;

  long globalTimeStart;
  long globalTimeEnd;
  long initialTime;
  long finalTime;


  /* Initialize Default Values */
  timeOutPeriod    = 0;
  ctlFileName      = NIL(char);
  verbosity        = Imc_VerbosityNone_c;
  dcLevel          = Imc_DcLevelNone_c;
  incrementalSize  = 4;
  lowerMethod      = Imc_LowerUniversalQuantification_c;
  upperMethod      = Imc_UpperExistentialQuantification_c;
  computeExact     = FALSE;
  partMethod       = Imc_PartAll_c;
  refine           = Imc_RefineLatchRelation_c;
  graphType        = Imc_GraphMOG_c;

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hxt:r:i:l:p:v:D:g:")) != EOF) {
    switch(c) {
      case 'h':
        IterativeModelCheckUsage();
        return 1;
      case 'x':
        computeExact = TRUE;
        break;
      case 't':
        timeOutPeriod = atoi(util_optarg);
        if (timeOutPeriod < 0){
          fprintf(vis_stdout,"** imc warning : Timeout Option -t %s is not defined.\n",
                  util_optarg);
          IterativeModelCheckUsage();
          return 1;
        }
              break;
      case 'r':
        option = atoi(util_optarg);
        if (option == 0) refine = Imc_RefineSort_c;
        else if (option == 1) refine = Imc_RefineLatchRelation_c;
        else{
          fprintf(vis_stdout,"** imc warning : Refine option -r %d is not defined.\n",
                  option);
          IterativeModelCheckUsage();
          return 1;
        }
        break;
      case 'i':
        incrementalSize = atoi(util_optarg);
        if (incrementalSize<1){
          fprintf(vis_stdout,"** imc warning : Incremental size option -i %d",
                  incrementalSize);
          fprintf(vis_stdout," is not defined.\n");
          IterativeModelCheckUsage();
          return 1;
        }
        break;
      case 'l':
        option = atoi(util_optarg);
        if (option==0){
          lowerMethod = Imc_LowerSubsetTR_c;
        }else if (option==1){
          lowerMethod = Imc_LowerUniversalQuantification_c;
        }else{
          fprintf(vis_stdout,"** imc warning : Lower bound option option -l %d",
                  option);
          fprintf(vis_stdout," is not defined.\n");
          IterativeModelCheckUsage();
          return 1;
        }
        break;
      case 'p':
        option = atoi(util_optarg);
        if (option==0){
          partMethod = Imc_PartAll_c;
        }else if (option==1){
          partMethod = Imc_PartDepend_c;
        }else if (option==2){
          partMethod = Imc_PartInc_c;
        }else{
          fprintf(vis_stdout,"** imc warning : Partition option -p %d",
                  option);
          fprintf(vis_stdout," is not defined.\n");
          IterativeModelCheckUsage();
          return 1;
        }
        break;
      case 'v':
        option = atoi(util_optarg);
        if (option == 0) verbosity = Imc_VerbosityNone_c;
        else if (option == 1) verbosity = Imc_VerbosityMin_c;
              else if (option == 2) verbosity = Imc_VerbosityMax_c;
        else{
                fprintf(vis_stdout,"** imc warning : Verbosity option -v %d",
                        option);
                fprintf(vis_stdout, " is not defined.\n");
          IterativeModelCheckUsage();
          return 1;
              }
        break;
      case 'D':
        option = atoi(util_optarg);
              if (option == 0) dcLevel = Imc_DcLevelNone_c;
        else if (option == 1) dcLevel = Imc_DcLevelRch_c;
              else if (option == 2) dcLevel = Imc_DcLevelMax_c;
              else if (option == 3) dcLevel = Imc_DcLevelArdc_c;
        else{
                fprintf(vis_stdout,"** imc warning : Don't care option -D %d",
                        option);
                fprintf(vis_stdout, " is not defined.\n");
          IterativeModelCheckUsage();
          return 1;
              }
        break;
      case 'g':
        option = atoi(util_optarg);
        if (option == 0) graphType = Imc_GraphNDOG_c;
        else if (option == 1) graphType = Imc_GraphPDOG_c;
        else if (option == 2) graphType = Imc_GraphMOG_c;
        else{
                fprintf(vis_stdout,"** imc warning : Graph type option -g %d",
                        option);
                fprintf(vis_stdout," is not defined.\n");
          IterativeModelCheckUsage();
          return 1;
              }
        break;    
      default:
              IterativeModelCheckUsage();
              return 1;
    }
  }

  /* Make sure the CTL file has been provided */
  if (argc == util_optind) {
    IterativeModelCheckUsage();
    return 1;
  }
  else {
    ctlFileName = argv[util_optind];
  }

  /* 
   * Obtain the network from the hierarchy manager 
   */
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  /* 
   * Read in the array of CTL formulas provided in ctlFileName 
   */
  ctlFile = Cmd_FileOpen(ctlFileName, "r", NIL(char *), 0);
  if (ctlFile == NIL(FILE)) {
    return 1;
  }
  ctlFormulaArray = Ctlp_FileParseFormulaArray(ctlFile);
  fclose(ctlFile);

  if (ctlFormulaArray == NIL(array_t)) {
    fprintf(vis_stderr, "** imc error: Error while parsing ctl formulas in file.\n");
    return 1;
  } 

  /* 
   * Start the timer. 
   */
  if (timeOutPeriod > 0) {
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);

    /* The second time setjmp is called, it returns here !!*/
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout, "IMC: Timeout occurred after %d seconds.\n",
                     timeOutPeriod);
      alarm(0);

      /* Note that there is a huge memory leak here. */
      Ctlp_FormulaArrayFree(ctlFormulaArray);
      return 1;
    } 
  }

  currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
  modelName = Hrc_NodeReadModelName(currentNode);
  partition = Part_NetworkReadPartition(network);

  exactFsm = NIL(Fsm_Fsm_t);
  reducedFsm = NIL(Fsm_Fsm_t);
  careStates = NIL(mdd_t);

  if ((computeExact)&&(partMethod == Imc_PartInc_c)){
    partMethod = Imc_PartDepend_c;
  }

  if ((dcLevel != Imc_DcLevelNone_c) && (partMethod == Imc_PartInc_c)){
    partMethod = Imc_PartDepend_c;
  }

  if (partition == NIL(graph_t) && (partMethod != Imc_PartInc_c)){
    if (partMethod == Imc_PartAll_c){

      partition = Part_NetworkCreatePartition(network, currentNode, modelName,
                                          (lsList)0, (lsList)0, NIL(mdd_t),
                                          Part_InOut_c, (lsList)0, FALSE,
                                          verbosity, 0);
      Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                          (void *) partition);

    }else if (partMethod == Imc_PartDepend_c){
      partition = Part_PartCreatePartitionWithCTL(hmgr, Part_InOut_c, verbosity, 
                                      0, FALSE, ctlFormulaArray, NIL(array_t));
      /* Register the partition in the network if any */
      Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY,
                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                          (void *) partition);
    }
  }
 
  if (partition != NIL(graph_t)){ 
    exactFsm = Fsm_NetworkReadOrCreateFsm(network); 
    reducedFsm = Mc_ConstructReducedFsm(network, ctlFormulaArray);
    if (reducedFsm==NIL(Fsm_Fsm_t)){
      reducedFsm = exactFsm;
    }

    /*
     * Check whether the fairness was read. Fairnedd is ignored.
     */
    {
      Fsm_Fairness_t *fairCons =  Fsm_FsmReadFairnessConstraint(exactFsm);
      int numOfConj     = Fsm_FairnessReadNumConjunctsOfDisjunct(fairCons, 0);
      if (numOfConj > 1) {
        /* Buchi */
        fprintf(vis_stdout, "** imc warning : Fairness Constraint is not supported.");
        fprintf(vis_stdout, " Fairness Constraint is ignored.\n");
      }else if (numOfConj == 1){
        /* check if fairness is simply default fairness formula, which is TRUE */
        Ctlp_Formula_t *formula = Fsm_FairnessReadFinallyInfFormula(fairCons, 0, 0);
        if (Ctlp_FormulaReadType(formula) != Ctlp_TRUE_c){
          fprintf(vis_stdout, "** imc warning : Fairness Constraint is not supported.");
          fprintf(vis_stdout, " Fairness Constraint is ignored.\n");
        }
      }
    }
  } 

  globalTimeStart = util_cpu_time();

  if (partition != NIL(graph_t)){

    if (dcLevel == Imc_DcLevelArdc_c){
      if (verbosity != Imc_VerbosityNone_c){
        fprintf(vis_stdout, "IMC: Computing approximate reachable states.\n");
      }
      ardcOptions = Fsm_ArdcAllocOptionsStruct();
      Fsm_ArdcGetDefaultOptions(ardcOptions); 
      initialTime = util_cpu_time();
      (void) Fsm_ArdcComputeOverApproximateReachableStates(
        reducedFsm, 0, verbosity, 0, 0, 0, 0, 0, 0, ardcOptions);
      finalTime = util_cpu_time();
      if (verbosity != Imc_VerbosityNone_c) {
        Fsm_ArdcPrintReachabilityResults(reducedFsm, finalTime - initialTime);
      }
      /* CW::user is responsible to free Fsm_ArdcGetMdd...
      careStates
        = mdd_dup(Fsm_ArdcGetMddOfOverApproximateReachableStates(reducedFsm));
      */
      careStates
        = Fsm_ArdcGetMddOfOverApproximateReachableStates(reducedFsm);
      
    }else if (dcLevel >= Imc_DcLevelRch_c){
      if (verbosity != Imc_VerbosityNone_c){
         fprintf(vis_stdout, "IMC: Computing exact reachable states.\n");
      }
      initialTime = util_cpu_time();
      careStates = Fsm_FsmComputeReachableStates(reducedFsm,
                                         0, 1, 0, 0, 0, 0, 0,
                                         Fsm_Rch_Default_c, 0, 0,
                                         NIL(array_t), FALSE, NIL(array_t));
      finalTime = util_cpu_time();
      if (verbosity != Imc_VerbosityNone_c) {
        Fsm_FsmReachabilityPrintResults(reducedFsm, finalTime - initialTime,
                                      Fsm_Rch_Default_c);
      }
    }else{
      careStates = NIL(mdd_t);
    }
  
    if (reducedFsm != NIL(Fsm_Fsm_t) && 
        Fsm_FsmReadImageInfo(reducedFsm) != NIL(Img_ImageInfo_t)) {
      Fsm_FsmFreeImageInfo(reducedFsm);
    }
  }

  ctlNormalForm = Ctlp_FormulaArrayConvertToSimpleExistentialFormTree(
                  ctlFormulaArray);

  /* 
   * Loop over every CTL formula in the array 
   */
  arrayForEachItem(Ctlp_Formula_t *, ctlNormalForm, i, currentFormula) {
    Ctlp_FormulaClass formulaClass;    
    array_t * singleFormulaArray = array_alloc(Ctlp_Formula_t *, 1);

    array_insert(Ctlp_Formula_t *, singleFormulaArray, 0, currentFormula);
    dagFormula = Ctlp_FormulaArrayConvertToDAG(singleFormulaArray);
    array_free(singleFormulaArray);
    formula = array_fetch(Ctlp_Formula_t *, dagFormula, 0);
    array_free(dagFormula);

    formulaClass = Ctlp_CheckClassOfExistentialFormula(formula);

    /*
     * Type of approximation needed for verification
     *
     *       pDOG  nDOG  MOG
     * ---------------------
     * ACTL    L     U    B
     * ECTL    U     L    B
     * Mixed   B     B    B
     */

    if ((formulaClass == Ctlp_Mixed_c) || (graphType == Imc_GraphMOG_c)){
      needLower = TRUE;
      needUpper = TRUE;

    }else if (((formulaClass == Ctlp_ACTL_c) && (graphType == Imc_GraphPDOG_c)) ||
        ((formulaClass == Ctlp_ECTL_c) && (graphType == Imc_GraphNDOG_c))){
      needLower = TRUE;
      needUpper = FALSE;      

    }else{
      needLower = FALSE;
      needUpper = TRUE;
    }            

    if (!Mc_FormulaStaticSemanticCheckOnNetwork(formula,network,FALSE)){
      (void) fprintf(vis_stdout, "\n** imc error: Error in parsing formula:\n%s\n", 
                     error_string());
      error_init();
      continue;
    }

    error_init();
    initialTime = util_cpu_time();
   
    orgFormula = array_fetch(Ctlp_Formula_t *, ctlFormulaArray, i);

    Imc_ImcEvaluateFormulaLinearRefine(network, orgFormula, formula, 
      formulaClass, incrementalSize, verbosity, refine, careStates, reducedFsm,
      dcLevel, graphType, lowerMethod, upperMethod, computeExact, needLower, 
      needUpper, partMethod, currentNode, modelName);

    finalTime = util_cpu_time();
    if(verbosity != Imc_VerbosityNone_c) {
      (void) fprintf(vis_stdout, "%-20s%10ld\n\n",
                     "IMC: Verification time for this formula =",
                     (finalTime - initialTime) / 1000);
    }
    fprintf(vis_stdout, "\n");
    
  } /* End of arrayForEachItem in ctlFormulaArray */

  if (careStates)
    mdd_free(careStates); /* FIXED */

  globalTimeEnd = util_cpu_time();

  if (verbosity != Imc_VerbosityNone_c) {
     (void) fprintf(vis_stdout, "%-20s%10ld\n\n",
                    "IMC: Total verification time =",
                    (globalTimeEnd - globalTimeStart) / 1000);
  } 
  
  /* Deactivate the alarm */
  alarm(0);

  if ((reducedFsm != NIL(Fsm_Fsm_t)) && (exactFsm != reducedFsm)){
    Fsm_FsmFree(reducedFsm);
  }

  Ctlp_FormulaArrayFree(ctlFormulaArray);
  Ctlp_FormulaArrayFree(ctlNormalForm);
  error_cleanup();

  /* normal exit */
  return 0;
}

static void
IterativeModelCheckUsage(void)
{
  fprintf(vis_stderr, "usage: iterative_model_check [-h] [-x]");
  fprintf(vis_stderr, "[-t <secs>] [-v <number>] [-D <number>] [-r <number>]");
  fprintf(vis_stderr, "[-i <number] [-l <number] [-p <number] [-g <number] ctlfile\n");
  fprintf(vis_stderr, "   -h        print the command usage\n");
  fprintf(vis_stderr, "   -x        Exact verification\n");
  fprintf(vis_stderr, "   -t secs   Seconds allowed for computation\n");
  fprintf(vis_stderr, "   -v number verbosity level (0:none, 1:mid, 2:max)\n");
  fprintf(vis_stderr, "   -D number Don't care level. DC's are used to\n");
  fprintf(vis_stderr, "             reduce transition relation\n");
  fprintf(vis_stderr, "        0    No don't care (default)\n");
  fprintf(vis_stderr, "        1    Exact reachable states\n");
  fprintf(vis_stderr, "        2    Aggressively use DC's\n");
  fprintf(vis_stderr, "        3    Approximate reachable states\n");
  fprintf(vis_stderr, "   -r number Refinement method\n");
  fprintf(vis_stderr, "        0    Static scheduling by name sorting\n");
  fprintf(vis_stderr, "        1    Static scheduling by latch affinity (defualt)\n");
  fprintf(vis_stderr, "   -i number Incremental size (default = 4)\n");
  fprintf(vis_stderr, "   -l number Type of lower-bound approximation method\n");
  fprintf(vis_stderr, "        0    Take a subset of each transition sub-relation\n");
  fprintf(vis_stderr, "        1    Take a subset by universal quantification (default)\n");
  fprintf(vis_stderr, "   -p number Type of partition method\n");
  fprintf(vis_stderr, "        0    Build all next state functions (default)\n");
  fprintf(vis_stderr, "        1    Build the next state functions related to formulas\n");
  fprintf(vis_stderr, "        2    Build the next state functions incrementally\n");
  fprintf(vis_stderr, "   -g number Type of operational graph\n");
  fprintf(vis_stderr, "        0    Negative Operational Graph\n");
  fprintf(vis_stderr, "        1    Positive Operational Graph\n");
  fprintf(vis_stderr, "        2    Mixed Operational Graph (default)\n");  
  fprintf(vis_stderr, "   ctlfile   File containing the ctl formulas\n");

  return;
} /* End of IterativeModelCheckUsage */


static void
TimeOutHandle(void)
{
  longjmp(timeOutEnv, 1);
} /* End of TimeOutHandle */