Changeset 40 for vis_dev/vis-2.3

Timestamp:

Jan 8, 2012, 5:12:00 PM (13 years ago)

Author:

cecile

Message:

abnormal structure in network

Location:

vis_dev/vis-2.3

Files:

• models/debug/test.script (modified) (1 diff)
• models/transition/f.ctl (modified) (1 diff)
• models/transition/script (modified) (1 diff)
• src/debug/debug.c (modified) (3 diffs)
• src/debug/debug.h (modified) (3 diffs)
• src/debug/debugAbnormal.c (modified) (3 diffs)
• src/ntk/ntkNtk.c (modified) (1 diff)

vis_dev/vis-2.3/models/debug/test.script

@@ -1 +1 @@
 rlmv and2.mv
 init
-#_createAbn
+_createAbn
 aig
 _sat_debug  -k 1 -p and2.ltl -o and2_prop.cnf -v 1  

vis_dev/vis-2.3/models/transition/f.ctl

@@ -1 +1 @@
 !EX(state[1:0] = 1);
+EX(state[1:0] = 3);

vis_dev/vis-2.3/models/transition/script

@@ -2 +2 @@
 init
 compute_reach -v 1 
-_transition
+_transition -v 1

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

@@ -296 +296 @@
     return 1;
   }
+
   /*
     We need the bdd when building the transition relation of the automaton
@@ -308 +309 @@
     }
   }
-
+Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
+printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
 /*
  * Read the formula
@@ -394 +396 @@
     int l;
     // return the clause number
-    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
+    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
    
     int leftValue   = checkIndex(noLoopIndex, cnfClauses);
     printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue); 
-    int rightValue,loop,andIndex;
-    array_t           *orClause = NIL(array_t);
-    array_t           *loopClause, *tmpclause;
-
-    if (leftValue != 1) {
-      orClause = array_alloc(int, 0);   
-      if (leftValue == -1){
-            array_insert_last(int, orClause, noLoopIndex);
-      }
-      loopClause = array_alloc(int, k+1);
-      for(l=0; l<=k; l++){
-            int loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, l, cnfClauses);
-            rightValue = checkIndex(loopIndex, cnfClauses);
-          if (rightValue == 0){
-            break;
-          }
-      if (rightValue !=0){
-            loop = cnfClauses->cnfGlobalIndex++;
-            BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
-                                                nodeToMvfAigTable, CoiTable, loop);
-          array_insert(int, loopClause, l, loop);
-          if(rightValue == -1){
-            
-            andIndex   = cnfClauses->cnfGlobalIndex++;
-            tmpclause  = array_alloc(int, 2);
-            array_insert(int, tmpclause, 0, loop);
-            array_insert(int, tmpclause, 1, -andIndex);
-            BmcCnfInsertClause(cnfClauses, tmpclause);
-
-            array_insert(int, tmpclause, 0, loopIndex);
-            array_insert(int, tmpclause, 1, -andIndex);
-            BmcCnfInsertClause(cnfClauses, tmpclause);
-        array_free(tmpclause);
-            array_insert_last(int, orClause, andIndex);
-      }
-      else {
-            array_insert_last(int, orClause, loop);
-          }
-      }} // for l loop 
-      }
-       BmcCnfInsertClause(cnfClauses, orClause);
-        array_free(orClause);
-
-
+        array_t           *objClause = NIL(array_t);
+        objClause = array_alloc(int, 0);   
+        array_insert_last(int, objClause, noLoopIndex);
+        BmcCnfInsertClause(cnfClauses, objClause);
+    array_free(objClause);
+
+        
+//TODO Add abnormal formula 
 
 

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

@@ -55 +55 @@
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
-
+#define DBG_NETWORK_APPL_KEY "Dbg_NetworkApplKey"
 
 /*---------------------------------------------------------------------------*/
@@ -124 +124 @@
 EXTERN void Debug_End(void);
 EXTERN Dbg_Abnormal_t * Dbg_DebugAbnormalAlloc(Ntk_Network_t * network);
-EXTERN void  Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn);
+EXTERN void Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn);
+EXTERN void Dbg_AbnormalFreeCallback(void *data);
 EXTERN void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal);
 EXTERN void Dbg_AddAbnormalPredicate(Dbg_Abnormal_t * abn, Ntk_Node_t* abnNode);
@@ -130 +131 @@
 EXTERN array_t* Dbg_ReadFreeInputs(Dbg_Abnormal_t *abnormal);
 EXTERN array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal);
+EXTERN Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network);
 /**AutomaticEnd***************************************************************/
 

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

@@ -114 +114 @@
         }
 }
+ Ntk_NetworkAddApplInfo(ntk, DBG_NETWORK_APPL_KEY,
+ (Ntk_ApplInfoFreeFn) Dbg_AbnormalFreeCallback,
+ (void *) abnormal);
 }
 /**Function********************************************************************
@@ -157 +160 @@
          FREE(abn);
 }       
+/**Function********************************************************************
+
+  Synopsis    [Call-back function to free an abnormal structure.]
+
+  Description [This function will be stored in the network together with the
+  pointer to the structure. Whenever the network deletes the partitioning
+  information, this function is called and it will deallocate the abnormal and
+  the information attached to it.]
+
+  SideEffects []
+
+  SeeAlso     [Ntk_NetworkAddApplInfo]
+
+******************************************************************************/
+void
+Dbg_AbnormalFreeCallback(
+   void *data)
+{
+  Dbg_DebugAbnormalFree((Dbg_Abnormal_t *) data);
+} /* End of Part_PartitionFreeCallback */
 
 
@@ -227 +250 @@
         return abnormal->abnormal;
 }
-
+/**Function********************************************************************
+ 
+  Synopsis    [returns the abnormal structure]
+
+  Description [returns the abnormal structure associated to the network]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network)
+{
+        Dbg_Abnormal_t * abn = (Dbg_Abnormal_t *) Ntk_NetworkReadApplInfo(network, DBG_NETWORK_APPL_KEY);
+
+        return abn;
+}

vis_dev/vis-2.3/src/ntk/ntkNtk.c

@@ -1039 +1039 @@
     mAig_quit(network->mAigManager);
   }
-
   FREE(network);
 }