Changeset 38 for vis_dev/vis-2.3


Ignore:
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:
3 edited

Legend:

Unmodified
Added
Removed
  • vis_dev/vis-2.3/models/debug/test.script

    r33 r38  
    1 rlmv %:2.mv
     1rlmv and2.mv
    22init
    3 _createAbn
    4 #aig
    5 #_sat_debug -v 1 -k 1 -o %:2.cnf
    6 
     3#_createAbn
     4aig
     5_sat_debug  -k 1 -p and2.ltl -o and2_prop.cnf -v 1 
  • vis_dev/vis-2.3/src/bmc/bmcBmc.c

    r14 r38  
    18171817        if (rightValue == 0){
    18181818          break;
    1819         }
     1819         }
    18201820        if(fairness){
    18211821          Ctlsp_Formula_t *formula;
  • vis_dev/vis-2.3/src/debug/debug.c

    r37 r38  
    176176
    177177******************************************************************************/
     178static int
     179checkIndex(
     180  int             index,
     181  BmcCnfClauses_t *cnfClauses)
     182{
     183  int     rtnValue = -1; /* it is not TRUE or FALSE*/
     184
     185  if (index == 0){ /* TRUE or FALSE*/
     186    if (cnfClauses->emptyClause){   /* last added clause was empty = FALSE*/
     187      rtnValue = 0; /* FALSE */
     188    } else {
     189      /*
     190        if (cnfClauses->noOfClauses == 0)
     191        rtnValue = 1;
     192        }
     193      */
     194      rtnValue = 1; /* TRUE */
     195    }
     196  }
     197  return rtnValue;
     198}
    178199
    179200
     
    188209Ntk_Network_t * network;
    189210bAig_Manager_t    *manager;
    190 
     211array_t           *formulaArray;
     212array_t           *LTLformulaArray;
     213char *ltlFileName     = NIL(char);
    191214
    192215/*
     
    194217 */
    195218util_getopt_reset();
    196 while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
     219while ((c = util_getopt(argc, argv, "vhp:m:k:o:")) != EOF) {
    197220  switch(c) {
    198221    case 'v':
     
    220243        case 'o':
    221244      options->cnfFileName = util_strsav(util_optarg);
    222       break;   
     245      break;
     246    case 'p':
     247      ltlFileName     = util_strsav(util_optarg);
     248    break;
    223249
    224250    default:
     
    226252  }
    227253}
     254printf("MAX K %d", options->maxK);
    228255 if (options->minK > options->maxK){
    229256    (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");   
     
    282309  }
    283310
     311/*
     312 * Read the formula
     313 */
     314 /* Read LTL Formulae */
     315  if (!ltlFileName)
     316      goto usage;
     317
     318  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
     319  if (options->ltlFile == NIL(FILE)) {
     320    (void) fprintf(vis_stdout,"** _sat_debug error: Cannot open the file %s\n", ltlFileName);
     321    FREE(ltlFileName);
     322    BmcOptionFree(options);
     323  }
     324  FREE(ltlFileName);
     325
     326 formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
     327  if (formulaArray == NIL(array_t)) {
     328    (void) fprintf(vis_stderr,
     329                   "** bmc error: error in parsing CTL* Fromula from file\n");
     330    BmcOptionFree(options);
     331    return 1;
     332  }
     333  if (array_n(formulaArray) == 0) {
     334    (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
     335    BmcOptionFree(options);
     336    Ctlsp_FormulaArrayFree(formulaArray);
     337    return 1;
     338  }
     339  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
     340  Ctlsp_FormulaArrayFree(formulaArray);
     341  if (LTLformulaArray ==  NIL(array_t)){
     342    (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
     343    BmcOptionFree(options);
     344    return 1;
     345  }
     346    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
     347
     348
     349
    284350 /*
    285351    Compute the cone of influence
    286         here a list of state variables (latches)
     352        here : a list of state variables (latches)
    287353  */
    288354        st_table        *CoiTable =  generateAllLatches(network);
     
    316382      Generate clauses for an initialized path of length k
    317383     */
     384    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
     385     fprintf(vis_stdout, "\n");
    318386    BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
    319387                                 cnfClauses, nodeToMvfAigTable, CoiTable);
     388
     389    //Generate ltl CNF
     390    // BmcGenerateCnfForLtl Génére la formule borné et retourne un index
     391    // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
     392    // cf. BmcLtlVerifyGeneralLtl
     393    int k = options->maxK;
     394    int l;
     395    // return the clause number
     396    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
     397   
     398    int leftValue   = checkIndex(noLoopIndex, cnfClauses);
     399    printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue);
     400    int rightValue,loop,andIndex;
     401    array_t           *orClause = NIL(array_t);
     402    array_t           *loopClause, *tmpclause;
     403
     404    if (leftValue != 1) {
     405      orClause = array_alloc(int, 0);   
     406      if (leftValue == -1){
     407            array_insert_last(int, orClause, noLoopIndex);
     408      }
     409      loopClause = array_alloc(int, k+1);
     410      for(l=0; l<=k; l++){
     411            int loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, l, cnfClauses);
     412            rightValue = checkIndex(loopIndex, cnfClauses);
     413          if (rightValue == 0){
     414            break;
     415          }
     416      if (rightValue !=0){
     417            loop = cnfClauses->cnfGlobalIndex++;
     418            BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
     419                                                nodeToMvfAigTable, CoiTable, loop);
     420          array_insert(int, loopClause, l, loop);
     421          if(rightValue == -1){
     422           
     423            andIndex   = cnfClauses->cnfGlobalIndex++;
     424            tmpclause  = array_alloc(int, 2);
     425            array_insert(int, tmpclause, 0, loop);
     426            array_insert(int, tmpclause, 1, -andIndex);
     427            BmcCnfInsertClause(cnfClauses, tmpclause);
     428
     429            array_insert(int, tmpclause, 0, loopIndex);
     430            array_insert(int, tmpclause, 1, -andIndex);
     431            BmcCnfInsertClause(cnfClauses, tmpclause);
     432        array_free(tmpclause);
     433            array_insert_last(int, orClause, andIndex);
     434      }
     435      else {
     436            array_insert_last(int, orClause, loop);
     437          }
     438      }} // for l loop
     439      }
     440       BmcCnfInsertClause(cnfClauses, orClause);
     441        array_free(orClause);
     442
     443
     444
     445
     446
     447
     448
    320449         if(verbose)
    321450                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
    322451                latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
    323452       
    324     
     453 Ctlsp_FormulaArrayFree(LTLformulaArray);    
    325454        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
    326455fclose(cnfFile);
     
    330459  usage:
    331460  (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
    332   minimum length] [-o cnf_file]\n");
     461  minimum length] [-o cnf_file] [-p ltl_file]\n");
    333462  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
    334463  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
    335464  (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n"); 
    336465  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
    337   (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the counterexample\n"); 
     466  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the debug instance\n"); 
     467  (void) fprintf(vis_stderr, "   -p <ltl_file> contains the ltl formula\n"); 
    338468  return 1;             /* error exit */
    339469
Note: See TracChangeset for help on using the changeset viewer.