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

Timestamp:

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

Author:

cecile

Message:

abnormal structure in network

File:

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

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