Changeset 38 for vis_dev/vis-2.3

Timestamp:

Jan 8, 2012, 3:30:01 PM (13 years ago)

Author:

cecile

Message:

first attempt debug with ltl formula

Location:

vis_dev/vis-2.3

Files:

• models/debug/test.script (modified) (1 diff)
• src/bmc/bmcBmc.c (modified) (1 diff)
• src/debug/debug.c (modified) (8 diffs)

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

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

vis_dev/vis-2.3/src/bmc/bmcBmc.c

@@ -1817 +1817 @@
         if (rightValue == 0){
           break;
-        }
+         }
         if(fairness){
           Ctlsp_Formula_t *formula;

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

@@ -176 +176 @@
 
 ******************************************************************************/
+static int
+checkIndex(
+  int             index,
+  BmcCnfClauses_t *cnfClauses)
+{
+  int     rtnValue = -1; /* it is not TRUE or FALSE*/
+
+  if (index == 0){ /* TRUE or FALSE*/
+    if (cnfClauses->emptyClause){   /* last added clause was empty = FALSE*/
+      rtnValue = 0; /* FALSE */
+    } else {
+      /*
+        if (cnfClauses->noOfClauses == 0)
+        rtnValue = 1;
+        }
+      */
+      rtnValue = 1; /* TRUE */
+    }
+  }
+  return rtnValue;
+}
 
 
@@ -188 +209 @@
 Ntk_Network_t * network;
 bAig_Manager_t    *manager;
-
+array_t           *formulaArray;
+array_t           *LTLformulaArray;
+char *ltlFileName     = NIL(char);
 
 /*
@@ -194 +217 @@
  */
 util_getopt_reset();
-while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
+while ((c = util_getopt(argc, argv, "vhp:m:k:o:")) != EOF) {
   switch(c) {
     case 'v':
@@ -220 +243 @@
         case 'o':
       options->cnfFileName = util_strsav(util_optarg);
-      break;    
+      break;
+    case 'p':
+      ltlFileName     = util_strsav(util_optarg);
+    break;
 
     default:
@@ -226 +252 @@
   }
 }
+printf("MAX K %d", options->maxK);
  if (options->minK > options->maxK){
     (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");    
@@ -282 +309 @@
   }
 
+/*
+ * Read the formula
+ */
+ /* Read LTL Formulae */
+  if (!ltlFileName) 
+      goto usage;
+
+  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
+  if (options->ltlFile == NIL(FILE)) {
+    (void) fprintf(vis_stdout,"** _sat_debug error: Cannot open the file %s\n", ltlFileName);
+    FREE(ltlFileName);
+    BmcOptionFree(options);
+  }
+  FREE(ltlFileName);
+
+ formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
+  if (formulaArray == NIL(array_t)) {
+    (void) fprintf(vis_stderr,
+                   "** bmc error: error in parsing CTL* Fromula from file\n");
+    BmcOptionFree(options);
+    return 1;
+  }
+  if (array_n(formulaArray) == 0) {
+    (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
+    BmcOptionFree(options);
+    Ctlsp_FormulaArrayFree(formulaArray);
+    return 1;
+  }
+  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
+  Ctlsp_FormulaArrayFree(formulaArray);
+  if (LTLformulaArray ==  NIL(array_t)){
+    (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
+    BmcOptionFree(options);
+    return 1;
+  }
+    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
+
+
+
  /*
     Compute the cone of influence 
-        here a list of state variables (latches)
+        here : a list of state variables (latches)
   */
         st_table        *CoiTable =  generateAllLatches(network);
@@ -316 +382 @@
       Generate clauses for an initialized path of length k
      */
+    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
+     fprintf(vis_stdout, "\n");
     BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
                                  cnfClauses, nodeToMvfAigTable, CoiTable);
+
+    //Generate ltl CNF
+    // BmcGenerateCnfForLtl Génére la formule borné et retourne un index 
+    // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
+    // cf. BmcLtlVerifyGeneralLtl
+    int k = options->maxK;
+    int l;
+    // return the clause number
+    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, 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);
+
+
+
+
+
+
+
          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));
         
-    
+ Ctlsp_FormulaArrayFree(LTLformulaArray);    
         BmcWriteClauses(manager, cnfFile, cnfClauses, options);
 fclose(cnfFile);
@@ -330 +459 @@
   usage:
   (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
-  minimum length] [-o cnf_file]\n");
+  minimum length] [-o cnf_file] [-p ltl_file]\n");
   (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
   (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
   (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n");  
   (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
-  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the counterexample\n");  
+  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the debug instance\n");  
+  (void) fprintf(vis_stderr, "   -p <ltl_file> contains the ltl formula\n");  
   return 1;             /* error exit */