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

Timestamp:

Jan 13, 2012, 6:32:51 PM (13 years ago)

Author:

cecile

Message:

Fault candidates OK

File:

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

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

@@ -191 +191 @@
 array_t          * LTLformulaArray;
 char             * ltlFileName     = NIL(char);
-
+array_t          * faultNodes = array_alloc(Ntk_Node_t*,0);
 
 /*
@@ -286 +286 @@
    
 
-        array_t           *objClause = NIL(array_t);
+        array_t *objClause = NIL(array_t);
         objClause = array_alloc(int, 0);   
         array_insert_last(int, objClause, noLoopIndex);
@@ -295 +295 @@
     st_table * nodeToMvfAigTable =  NIL(st_table);
     nodeToMvfAigTable =
-(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
-assert(nodeToMvfAigTable != NIL(st_table));
+    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
+    assert(nodeToMvfAigTable != NIL(st_table));
 
     Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);
 
-      //loop abnormal
+    //loop abnormal
     int aIndex;
     Ntk_Node_t * abnNode;
-     Dbg_ForEachAbnormal(abn,aIndex,abnNode){
-     if(aIndex<=0){
-     //set abnormal
+    Dbg_ForEachAbnormal(abn,aIndex,abnNode){
+      char * nodeName =  Ntk_NodeReadName(abnNode);
+    //set abnormal
       int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex);
       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);
-
+      
       //SAT procedure 
-      int res = Dbg_SatCheck("assig",options->cnfFileName);
-
-        array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
-        }
-     }
+      //assig assig input from cex
+      //TODO build cex correctly
+      int res = Dbg_SatCheck("assig",options->cnfFileName,options->verbosityLevel);
+      // Build set of FaultCandidates
+      if (res == SAT_SAT)
+      {
+        char * realNodeName = util_strsav(nodeName);
+        realNodeName[strlen(nodeName)-4] = '\0';
+        Ntk_Node_t * realNode =  Ntk_NetworkFindNodeByName(network,realNodeName);
+        array_insert_last(Ntk_Node_t*,faultNodes,realNode);
+      }
+
+
+      array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
+   }
 
          if(verbose)
                 (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
-                latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
-        
+                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);
+
+    
 Ctlsp_FormulaArrayFree(LTLformulaArray);    
 BmcCnfClausesFree(cnfClauses);
 BmcOptionFree(options);
+array_free(faultNodes);
 return 0;