Ignore:
Timestamp:
Jan 10, 2012, 6:51:23 PM (12 years ago)
Author:
cecile
Message:

new command generate cnf from network

File:
1 edited

Legend:

Unmodified
Added
Removed

  • vis_dev/vis-2.3/src/debug/debug.c

    r40 r41  
    6565static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
    6666static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
     67static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
    6768
    6869
    … …  
    9495  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
    9596  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
     97  Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 0);
    9698
    9799}
    … …  
    176178
    177179******************************************************************************/
    178 static int
    179 checkIndex(
    180   int             index,
    181   BmcCnfClauses_t *cnfClauses)
    182 {
    183   int     rtnValue = -1; /* it is not TRUE or FALSE*/
    184 
    185   if (index == 0){ /* TRUE or FALSE*/
    186     if (cnfClauses->emptyClause){   /* last added clause was empty = FALSE*/
    187       rtnValue = 0; /* FALSE */
    188     } else {
    189       /*
    190         if (cnfClauses->noOfClauses == 0)
    191         rtnValue = 1;
    192         }
    193       */
    194       rtnValue = 1; /* TRUE */
    195     }
    196   }
    197   return rtnValue;
    198 }
    199 
    200 
    201180static int
    202181CommandSatDebug(
    … …  
    206185int            c,i;
    207186int            verbose = 0;              /* default value */
    208 BmcOption_t  *options = BmcOptionAlloc();
    209 Ntk_Network_t * network;
    210 bAig_Manager_t    *manager;
    211 array_t           *formulaArray;
    212 array_t           *LTLformulaArray;
    213 char *ltlFileName     = NIL(char);
     187BmcOption_t      * options = BmcOptionAlloc();
     188Ntk_Network_t    * network;
     189bAig_Manager_t   * manager;
     190array_t          * formulaArray;
     191array_t          * LTLformulaArray;
     192char             * ltlFileName     = NIL(char);
     193
    214194
    215195/*
    216196 * Parse command line options.
    217197 */
    218 util_getopt_reset();
    219 while ((c = util_getopt(argc, argv, "vhp:m:k:o:")) != EOF) {
    220   switch(c) {
    221     case 'v':
    222       verbose = 1;
    223           options->verbosityLevel =  verbose;
    224       break;
    225     case 'h':
    226       goto usage;
    227         case 'm':
    228       for (i = 0; i < strlen(util_optarg); i++) {
    229                 if (!isdigit((int)util_optarg[i])) {
    230                         goto usage;
    231                 }
    232       }
    233       options->minK = atoi(util_optarg);
    234       break;
    235     case 'k':
    236       for (i = 0; i < strlen(util_optarg); i++) {
    237                 if (!isdigit((int)util_optarg[i])) {
    238                         goto usage;
    239                 }
    240       }
    241           options->maxK = atoi(util_optarg);
    242           break;
    243         case 'o':
    244       options->cnfFileName = util_strsav(util_optarg);
    245       break;
    246     case 'p':
    247       ltlFileName     = util_strsav(util_optarg);
    248     break;
    249 
    250     default:
    251       goto usage;
    252   }
    253 }
     198if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
     199     return 1;
     200}
     201
     202
    254203printf("MAX K %d", options->maxK);
    255  if (options->minK > options->maxK){
    256     (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");   
    257     goto usage;
    258   }
    259204
    260205if (verbose) {
    261206  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
    262207}
    263  /* create SAT Solver input file */
    264  if (options->cnfFileName == NIL(char)) {
    265     options->satInFile = BmcCreateTmpFile();
    266 }
    267  else {
    268     options->satInFile = options->cnfFileName;
    269  }
    270 
    271 /* create SAT Solver output file */
    272 options->satOutFile = BmcCreateTmpFile();
    273 if (options->satOutFile == NIL(char)){
     208/*
     209 *  Read the network
     210 */
     211network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
     212if (network == NIL(Ntk_Network_t)) {
     213  (void) fprintf(vis_stdout, "** _sat_debug error: No network\n");
    274214  BmcOptionFree(options);
    275  (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
    276215  return 1;
    277216}
    278 
    279 options->verbosityLevel =  1;
    280 //options->satSolver
    281 //options->clauses
    282 
    283  /*
    284    * Read the network
    285    */
    286   network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
    287   if (network == NIL(Ntk_Network_t)) {
    288     (void) fprintf(vis_stdout, "** bmc error: No network\n");
    289     BmcOptionFree(options);
    290     return 1;
    291   }
    292   manager = Ntk_NetworkReadMAigManager(network);
    293   if (manager == NIL(mAig_Manager_t)) {
    294     (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
    295     BmcOptionFree(options);
    296     return 1;
    297   }
    298 
    299   /*
    300     We need the bdd when building the transition relation of the automaton
    301   */
    302   if(options->inductiveStep !=0){
    303     Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
    304  
    305     designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
    306     if (designFsm == NIL(Fsm_Fsm_t)) {
    307          (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
    308       return 1;
    309     }
    310   }
     217manager = Ntk_NetworkReadMAigManager(network);
     218if (manager == NIL(mAig_Manager_t)) {
     219  (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n");
     220  BmcOptionFree(options);
     221  return 1;
     222}
     223
    311224Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
    312 printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
    313 /*
    314  * Read the formula
    315  */
    316  /* Read LTL Formulae */
    317   if (!ltlFileName)
    318       goto usage;
    319 
    320   options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
    321   if (options->ltlFile == NIL(FILE)) {
    322     (void) fprintf(vis_stdout,"** _sat_debug error: Cannot open the file %s\n", ltlFileName);
    323     FREE(ltlFileName);
    324     BmcOptionFree(options);
    325   }
    326   FREE(ltlFileName);
    327 
    328  formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
    329   if (formulaArray == NIL(array_t)) {
    330     (void) fprintf(vis_stderr,
    331                    "** bmc error: error in parsing CTL* Fromula from file\n");
    332     BmcOptionFree(options);
    333     return 1;
    334   }
    335   if (array_n(formulaArray) == 0) {
    336     (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
    337     BmcOptionFree(options);
    338     Ctlsp_FormulaArrayFree(formulaArray);
    339     return 1;
    340   }
    341   LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
     225if(abn == NIL(Dbg_Abnormal_t)){
     226  (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n");
     227  return 1;
     228}
     229if(verbose)
     230  printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
     231
     232
     233formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
     234if (formulaArray == NIL(array_t)) {
     235  (void) fprintf(vis_stderr,
     236           "** bmc error: error in parsing CTL* Fromula from file\n");
     237  BmcOptionFree(options);
     238  return 1;
     239}
     240if (array_n(formulaArray) == 0) {
     241  (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
     242  BmcOptionFree(options);
    342243  Ctlsp_FormulaArrayFree(formulaArray);
    343   if (LTLformulaArray ==  NIL(array_t)){
    344     (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
    345     BmcOptionFree(options);
    346     return 1;
    347   }
    348     Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
     244  return 1;
     245}
     246LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
     247Ctlsp_FormulaArrayFree(formulaArray);
     248if (LTLformulaArray ==  NIL(array_t)){
     249  (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
     250  BmcOptionFree(options);
     251  return 1;
     252}
     253Ctlsp_Formula_t *ltlFormula  = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
    349254
    350255
    … …  
    353258    Compute the cone of influence
    354259        here : a list of state variables (latches)
     260    TODO refine to COI of the property
    355261  */
    356262        st_table        *CoiTable =  generateAllLatches(network);
    … …  
    359265      clauses in BMC.
    360266    */
    361     st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
    362         BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
    363     FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
    364         /*
    365     nodeToMvfAigTable maps each node to its multi-function And/Inv graph
    366     */
    367         nodeToMvfAigTable =
    368         (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
    369         assert(nodeToMvfAigTable != NIL(st_table));
    370 
    371         if(verbose)
     267        if(verbose)
    372268        {       
    373                 (void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
    374                 printLatch(nodeToMvfAigTable);
    375269                (void) fprintf(vis_stdout, "------      COI       ----\n");
    376270                printLatch(CoiTable);
    377271                (void) fprintf(vis_stdout, "--------------------------\n");
    378272    }
    379     /*
    380       Create a clause database
    381      */
    382     cnfClauses = BmcCnfClausesAlloc();
    383     /*
    384       Generate clauses for an initialized path of length k
    385      */
    386     Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
    387      fprintf(vis_stdout, "\n");
    388     BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
    389                                  cnfClauses, nodeToMvfAigTable, CoiTable);
     273    BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
     274
    390275
    391276    //Generate ltl CNF
    … …  
    393278    // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
    394279    // cf. BmcLtlVerifyGeneralLtl
     280    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
     281    fprintf(vis_stdout, "\n");
    395282    int k = options->maxK;
    396283    int l;
    … …  
    398285    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
    399286   
    400     int leftValue   = checkIndex(noLoopIndex, cnfClauses);
    401     printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue);
     287
    402288        array_t           *objClause = NIL(array_t);
    403289        objClause = array_alloc(int, 0);   
    … …  
    406292    array_free(objClause);
    407293
    408        
    409 //TODO Add abnormal formula
    410 
    411 
    412 
    413 
     294        //Add Abnormal
     295    st_table * nodeToMvfAigTable =  NIL(st_table);
     296    nodeToMvfAigTable =
     297(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
     298assert(nodeToMvfAigTable != NIL(st_table));
     299
     300    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);
     301
     302      //loop abnormal
     303    int aIndex;
     304    Ntk_Node_t * abnNode;
     305     Dbg_ForEachAbnormal(abn,aIndex,abnNode){
     306     if(aIndex<=0){
     307     //set abnormal
     308      int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex);
     309      bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
     310      int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses);
     311      array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
     312
     313      FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
     314      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
     315      fclose(cnfFile);
     316
     317      //SAT procedure
     318      int res = Dbg_SatCheck("assig",options->cnfFileName);
     319
     320        array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
     321        }
     322     }
    414323
    415324         if(verbose)
    … …  
    417326                latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
    418327       
    419  Ctlsp_FormulaArrayFree(LTLformulaArray);   
    420         BmcWriteClauses(manager, cnfFile, cnfClauses, options);
    421 fclose(cnfFile);
     328Ctlsp_FormulaArrayFree(LTLformulaArray);   
    422329BmcCnfClausesFree(cnfClauses);
    423330BmcOptionFree(options);
    424331return 0;
    425   usage:
    426   (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
    427   minimum length] [-o cnf_file] [-p ltl_file]\n");
    428   (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
    429   (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
    430   (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n"); 
     332 
     333}
     334/**Function********************************************************************
     335
     336  Synopsis    [Implements the generate_network_cnf.]
     337
     338  CommandName [generate_network_cnf]
     339
     340  CommandSynopsis [generate a CNF view of the network]
     341
     342  CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
     343 
     344  CommandDescription [This command geerate a CNF of the network in DMACS form.
     345  The network may be unroll within k steps.
     346  <p>
     347
     348  Command options:<p> 
     349
     350  <dl>
     351  <dt> -h
     352  <dd> Print the command usage.
     353  </dl>
     354
     355  <dt> -v
     356  <dd> Verbose mode.
     357  </dl>
     358
     359  <dt> -k
     360  <dd> number of steps (default 1).
     361  </dl>
     362  ]
     363
     364  SideEffects []
     365
     366******************************************************************************/
     367
     368static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
     369{
     370  BmcOption_t  *options = BmcOptionAlloc();
     371  int c;
     372  unsigned int i;
     373  Ntk_Network_t * network;
     374  bAig_Manager_t   * manager;
     375  char *  outName = NIL(char);
     376   FILE *cnfFile;
     377  if (!options){
     378    return 1;
     379  }
     380  options->dbgOut = 0;
     381  /*
     382   * Parse command line options.
     383   */
     384  util_getopt_reset();
     385  while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
     386    switch(c) {
     387    case 'h':
     388      goto usage;
     389    case 'k':
     390      options->maxK = atoi(util_optarg);
     391      break;
     392    case 'v':
     393      for (i = 0; i < strlen(util_optarg); i++) {
     394        if (!isdigit((int)util_optarg[i])) {
     395          goto usage;
     396        }
     397      }
     398      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
     399      break;
     400    default:
     401      goto usage;
     402    }
     403  }
     404   if (argc - util_optind != 0)
     405   {
     406      outName  = util_strsav(argv[util_optind]);
     407      /* create SAT Solver input file */
     408     options->cnfFileName= outName;
     409    options->satInFile = options->cnfFileName;
     410    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
     411  }
     412 
     413 
     414/*
     415 *  Read the network
     416 */
     417network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
     418if (network == NIL(Ntk_Network_t)) {
     419  (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
     420  BmcOptionFree(options);
     421  return 1;
     422}
     423manager = Ntk_NetworkReadMAigManager(network);
     424if (manager == NIL(mAig_Manager_t)) {
     425  (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
     426  BmcOptionFree(options);
     427  return 1;
     428}
     429
     430 /*
     431    Compute the cone of influence
     432        here : a list of state variables (latches)
     433  */
     434st_table        *CoiTable =  generateAllLatches(network);
     435
     436if(options->verbosityLevel)
     437{       
     438        (void) fprintf(vis_stdout, "------      COI       ----\n");
     439        printLatch(CoiTable);
     440        (void) fprintf(vis_stdout, "--------------------------\n");
     441}
     442BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
     443  if(outName != NIL(char))
     444  {
     445    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
     446    fclose(cnfFile);
     447  }
     448  else
     449     BmcWriteClauses(manager, vis_stdout, cnfClauses, options);
     450
     451if(options->verbosityLevel)
     452{       
     453        (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
     454    (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
     455    st_count(CoiTable));
     456}
     457   
     458BmcOptionFree(options);
     459 return 0;
     460 usage:
     461  (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n");
     462  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
    431463  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
    432   (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the debug instance\n"); 
    433   (void) fprintf(vis_stderr, "   -p <ltl_file> contains the ltl formula\n"); 
    434   return 1;             /* error exit */
    435 
    436 }
     464  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
     465  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
     466  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
     467  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
     468  (void) fprintf(vis_stderr, "   <cnf_file> The output file containing CNF of the network.\n");
     469
     470  BmcOptionFree(options);
     471  return 1;
     472}
     473
    437474/**Function********************************************************************
    438475
Note: See TracChangeset for help on using the changeset viewer.