Index: vis_dev/vis-2.3/models/debug/test.script =================================================================== --- vis_dev/vis-2.3/models/debug/test.script (revision 37) +++ vis_dev/vis-2.3/models/debug/test.script (revision 38) @@ -1,6 +1,5 @@ -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 Index: vis_dev/vis-2.3/src/bmc/bmcBmc.c =================================================================== --- vis_dev/vis-2.3/src/bmc/bmcBmc.c (revision 37) +++ vis_dev/vis-2.3/src/bmc/bmcBmc.c (revision 38) @@ -1817,5 +1817,5 @@ if (rightValue == 0){ break; - } + } if(fairness){ Ctlsp_Formula_t *formula; Index: vis_dev/vis-2.3/src/debug/debug.c =================================================================== --- vis_dev/vis-2.3/src/debug/debug.c (revision 37) +++ vis_dev/vis-2.3/src/debug/debug.c (revision 38) @@ -176,4 +176,25 @@ ******************************************************************************/ +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,5 +209,7 @@ Ntk_Network_t * network; bAig_Manager_t *manager; - +array_t *formulaArray; +array_t *LTLformulaArray; +char *ltlFileName = NIL(char); /* @@ -194,5 +217,5 @@ */ 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,5 +243,8 @@ case 'o': options->cnfFileName = util_strsav(util_optarg); - break; + break; + case 'p': + ltlFileName = util_strsav(util_optarg); + break; default: @@ -226,4 +252,5 @@ } } +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,7 +309,46 @@ } +/* + * 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,11 +382,74 @@ 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,10 +459,11 @@ 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 contains CNF of the counterexample\n"); + (void) fprintf(vis_stderr, " -o contains CNF of the debug instance\n"); + (void) fprintf(vis_stderr, " -p contains the ltl formula\n"); return 1; /* error exit */