Changeset 44 for vis_dev/vis-2.3/src/debug/debug.c

Timestamp:

Jan 24, 2012, 3:41:23 PM (13 years ago)

Author:

cecile

Message:

abnormal predicate done

File:

• vis_dev/vis-2.3/src/debug/debug.c (modified) (10 diffs)

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

@@ -132 +132 @@
 {
   Ntk_Network_t * ntk;
-  int c,verbose;
+  int c,verbose = 0;
+  array_t * excludes = NIL(array_t);
   Dbg_Abnormal_t * abnormal;
   ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+  char * subs;
   if (ntk == NIL(Ntk_Network_t)) {
         (void) fprintf(vis_stdout, "** abn error: No network\n");
         return 1;
   }
-  while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
+  while ((c = util_getopt(argc, argv, "vhs:")) != EOF) {
         switch(c) {
+        case 'h':
+          goto usage;
                 case 'v':
                         verbose = 1;
                         break;
+        case 's':
+            subs =  util_strsav(util_optarg);
+            excludes = array_alloc(char*,0);
+            array_insert_last(char*,excludes,subs);
+            break;
+        default :
+          goto usage;
                 }
  }
   abnormal = Dbg_DebugAbnormalAlloc(ntk);
   abnormal->verbose = verbose;
-  Dbg_AddAbnormalPredicatetoNetwork(abnormal);
-}
+    printf("SUBS %s \n",subs);
+  Dbg_AddAbnormalPredicatetoNetwork(abnormal,excludes);
+  printf("\t # Abnormal predicate created  %d\n", array_n(abnormal->abnormal));
+    return 0;
+  usage : 
+   (void) fprintf(vis_stderr, "usage: _createAbn [-h] [-v verboseLevel] [-s substystem excludes\n");
+  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
+  (void) fprintf(vis_stderr, "   -v  \t verbosity\n");
+  (void) fprintf(vis_stderr, "   -s <subsystemName> \texclude the abnormal predicate\
+  for this subssytem\n");
+  return 1;
+}
+
 /**Function********************************************************************
 
@@ -190 +212 @@
 array_t          * formulaArray;
 array_t          * LTLformulaArray;
-char             * ltlFileName     = NIL(char);
 array_t          * faultNodes = array_alloc(Ntk_Node_t*,0);
 
@@ -201 +222 @@
 
 
-printf("MAX K %d", options->maxK);
 
 if (verbose) {
@@ -252 +272 @@
 }
 Ctlsp_Formula_t *ltlFormula  = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
-
 
 
@@ -283 +302 @@
     int l;
     // return the clause number
-    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
+    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);    printf("LTL %d  \n",noLoopIndex);
    
 
@@ -298 +317 @@
     assert(nodeToMvfAigTable != NIL(st_table));
 
-    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);
+    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,k,cnfClauses);
 
     //loop abnormal
@@ -305 +324 @@
     Dbg_ForEachAbnormal(abn,aIndex,abnNode){
       char * nodeName =  Ntk_NodeReadName(abnNode);
-    //set abnormal
-      int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex);
+    //set abnormal for each step
+      array_t * cnfIndexArray = array_fetch(array_t*,abn->abnCnfIndexArray,aIndex);
+      int cnfIndex;
+      int step;
       bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
-      int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses);
-      array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
-      FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
-      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
-      fclose(cnfFile);
-      
+      array_t * cnfVal = array_alloc(int,0);
+      arrayForEachItem(int, cnfIndexArray, step, cnfIndex){
+        int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],step,cnfClauses);
+        array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
+        array_insert_last(int,cnfVal,abnIndex);
+        FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
+        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
+        fclose(cnfFile);
+        printf("AINDEX %d\n",aIndex);
+        if(aIndex == 0)
+        {
+        FILE *cnfFile = Cmd_FileOpen("test_aks.cnf", "w", NIL(char *), 0);
+        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
+        fclose(cnfFile);
+          
+        }
+      }//end for each step
+
       //SAT procedure 
       //assig assig input from cex
       //TODO build cex correctly
-      int res = Dbg_SatCheck("assig",options->cnfFileName,options->verbosityLevel);
+      int res = Dbg_SatCheck("assig",options->satInFile,options->verbosityLevel);
       // Build set of FaultCandidates
       if (res == SAT_SAT)
       {
         char * realNodeName = util_strsav(nodeName);
-        realNodeName[strlen(nodeName)-4] = '\0';
+        realNodeName[strlen(nodeName)-3] = '\0';
+        printf("Real = %s\n", realNodeName);
         Ntk_Node_t * realNode =  Ntk_NetworkFindNodeByName(network,realNodeName);
         array_insert_last(Ntk_Node_t*,faultNodes,realNode);
       }
 
-
-      array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
+      arrayForEachItem(int, cnfIndexArray, step, cnfIndex){
+        int abnIndex = array_fetch(int,cnfVal,step);        
+        array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
+      }
    }
 
@@ -335 +371 @@
                 latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable));
   
+    
         (void) fprintf(vis_stdout,"Number of Fault candidates %d\n",
     array_n(faultNodes));
         (void) fprintf(vis_stdout,"gates : \n");
+
+
     printNodeArray(faultNodes);
 
@@ -346 +385 @@
 array_free(faultNodes);
 return 0;
- 
-}
+}
+
 /**Function********************************************************************
 
@@ -420 +459 @@
    if (argc - util_optind != 0)
    {
-      outName  = util_strsav(argv[util_optind]);
-      /* create SAT Solver input file */
+     outName  = util_strsav(argv[util_optind]);
+     /* create SAT Solver input file */
      options->cnfFileName= outName;
-    options->satInFile = options->cnfFileName;
-    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
+     options->satInFile = options->cnfFileName;
+     cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
   }