Index: src/bmc/bmcDump.c =================================================================== --- src/bmc/bmcDump.c (revision 1) +++ src/bmc/bmcDump.c (revision 27) @@ -74,13 +74,6 @@ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static void -bmc_dump_expandFilename ARGS((const int k, const int l, - const int prop_idx, - const char* filename_to_be_expanded, - char* filename_expanded, - const size_t filename_expanded_maxlen)); - static int bmc_dump_openDimacsFile ARGS((const char* filename, FILE** file_ref)); @@ -114,7 +107,7 @@ nusmv_assert(dump_fname_template != (char*) NULL); /* 10 here is the maximum length of extension */ - bmc_dump_expandFilename(k, loop, + Bmc_Dump_ExpandFilename(k, loop, PropDb_get_prop_index(prop), dump_fname_template, dumpFilenameExpanded, @@ -404,52 +397,8 @@ } } - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - /**Function******************************************************************** - Synopsis [Open a file named filename and returns its descriptor] - - Description [The file is opened with the writable attribute. The - file descriptor is returned via the file_ref parameter. Returns 0 if the - function succedeed, otherwise the function prints out a warning in the - standard output and returns 1.] - - SideEffects [file_ref will change] - - SeeAlso [] - -******************************************************************************/ -static int bmc_dump_openDimacsFile(const char* filename, FILE** file_ref) -{ - int ret = 0; - if (opt_verbose_level_gt(options, 1)) { - fprintf(stderr, "\nOpening file '%s' for writing...\n", filename); - } - - *file_ref = fopen(filename, "w"); - if ((*file_ref) == NULL) { - fprintf(nusmv_stdout, - "\n************* WARNING *************\ - \n An error has occurred when writing the file \"%s\".\ - \n DIMACS dumping is not allowed.\ - \n************* END WARNING *************\n\n", filename); - ret = 1; - } - - return ret; -} - - -/**Function******************************************************************** - Synopsis [This is only a useful wrapper for easily call Bmc_Utils_ExpandMacrosInFilename] @@ -460,12 +409,15 @@ SeeAlso [] ******************************************************************************/ -static void -bmc_dump_expandFilename(const int k, const int l, - const int prop_idx, - const char* filename_to_be_expanded, - char* filename_expanded, - const size_t filename_expanded_maxlen) + +/* SW090820 This used to be a static function and its name was in all + lower case letters. As its now used also for my sbmc iCNF + dumping code it has now become a "public member function" */ +void Bmc_Dump_ExpandFilename(const int k, const int l, + const int prop_idx, + const char* filename_to_be_expanded, + char* filename_expanded, + const size_t filename_expanded_maxlen) { char szBuffer[1024]; char szLoopback[16]; @@ -508,3 +460,45 @@ filename_expanded, filename_expanded_maxlen); } + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Open a file named filename and returns its descriptor] + + Description [The file is opened with the writable attribute. The + file descriptor is returned via the file_ref parameter. Returns 0 if the + function succedeed, otherwise the function prints out a warning in the + standard output and returns 1.] + + SideEffects [file_ref will change] + + SeeAlso [] + +******************************************************************************/ +static int bmc_dump_openDimacsFile(const char* filename, FILE** file_ref) +{ + int ret = 0; + if (opt_verbose_level_gt(options, 1)) { + fprintf(stderr, "\nOpening file '%s' for writing...\n", filename); + } + + *file_ref = fopen(filename, "w"); + if ((*file_ref) == NULL) { + fprintf(nusmv_stdout, + "\n************* WARNING *************\ + \n An error has occurred when writing the file \"%s\".\ + \n DIMACS dumping is not allowed.\ + \n************* END WARNING *************\n\n", filename); + ret = 1; + } + + return ret; +} Index: src/bmc/bmcDump.h =================================================================== --- src/bmc/bmcDump.h (revision 1) +++ src/bmc/bmcDump.h (revision 27) @@ -70,7 +70,7 @@ BMC_DUMP_NONE, BMC_DUMP_DIMACS, BMC_DUMP_DA_VINCI, - BMC_DUMP_GDL + BMC_DUMP_GDL } Bmc_DumpType; /*---------------------------------------------------------------------------*/ @@ -122,6 +122,15 @@ const Be_Cnf_ptr cnf, const int k, FILE* dimacsfile)); +/* SW090820 This was a static function in bmcDump.c, now visible to + the outside for use in the sbmc iCNF dumping code */ +EXTERN void +Bmc_Dump_ExpandFilename ARGS((const int k, const int l, + const int prop_idx, + const char* filename_to_be_expanded, + char* filename_expanded, + const size_t filename_expanded_maxlen)); + /**AutomaticEnd***************************************************************/ #endif /* _BMC_DIMACS_H */ Index: src/bmc/sbmc/sbmcBmcInc.c =================================================================== --- src/bmc/sbmc/sbmcBmcInc.c (revision 1) +++ src/bmc/sbmc/sbmcBmcInc.c (revision 27) @@ -155,15 +155,35 @@ SeeAlso [optional] ******************************************************************************/ -int Sbmc_zigzag_incr(Prop_ptr ltlprop, const int max_k, +int Sbmc_zigzag_incr(Prop_ptr ltlprop, + const int max_k, + const int loop, /* SW090119 */ const int opt_do_virtual_unrolling, - const int opt_do_completeness_check) + const int opt_do_completeness_check, + const boolean must_solve, + char* const pipeProgArgs[], + const char* dump_fname_template) { + const char *pFilename = NULL; + char dumpFilenameExpanded[BMC_DUMP_FILENAME_MAXLEN]; + nusmv_assert( Bmc_Utils_IsNoLoopback(loop) || Bmc_Utils_IsAllLoopbacks(loop) ); /* SW090119 */ + node_ptr bltlspec; /* Its booleanization */ BeFsm_ptr be_fsm; /* The corresponding be fsm */ BeEnc_ptr be_enc; Be_Manager_ptr be_mgr; + if ( dump_fname_template != NULL ) { + /* 10 here is the maximum length of extension */ + Bmc_Dump_ExpandFilename(max_k, loop, + PropDb_get_prop_index(ltlprop), + dump_fname_template, + dumpFilenameExpanded, + sizeof(dumpFilenameExpanded)-10); + pFilename = dumpFilenameExpanded; + } + + /* Structure for holding state variable information */ state_vars_struct *state_vars = (state_vars_struct *)NULL; @@ -230,7 +250,7 @@ /* * Incremental SAT solver construction */ - zolver = sbmc_MS_create(be_enc); + zolver = sbmc_MS_create_ext(be_enc, must_solve, pipeProgArgs, pFilename); if ((sbmc_MetaSolver *)NULL == zolver) { /* Something went wrong */ return 1; @@ -365,6 +385,7 @@ current_k); } + /******************************************************************** * * The k-invariant part of the translation @@ -416,11 +437,13 @@ sbmc_state_vars_get_l_var(state_vars), sbmc_real_k(i)); - if (i == 0) { - /* l_0 <=> FALSE */ + if (i == 0 + || Bmc_Utils_IsNoLoopback(loop) // SW090119 + ) { + /* l_i <=> FALSE */ be_constraint = Be_Iff(be_mgr, be_l_i, Be_Falsity(be_mgr)); if (opt_verbose_level_ge(options, 6)) { - fprintf(nusmv_stderr, "Created (l_0 <=> false): "); + fprintf(nusmv_stderr, "Created (l_%d <=> false): ", i); // SW090119 (modified) Be_DumpSexpr(be_mgr, be_constraint, nusmv_stderr); fprintf(nusmv_stderr, "\n"); } @@ -576,7 +599,9 @@ /* * Actually solve the problem */ - satResult = sbmc_MS_solve(zolver); + if ( must_solve ) + satResult = sbmc_MS_solve(zolver); + #ifdef BENCHMARKING { @@ -693,73 +718,77 @@ times(&time_solver_start); #endif - /* - * Actually solve the problem - */ - satResult = sbmc_MS_solve(zolver); - + if ( must_solve ) { /* SW090819 */ + /* + * Actually solve the problem + */ + satResult = sbmc_MS_solve(zolver); + #ifdef BENCHMARKING - { - times(&time_temp); - fprintf(nusmv_stderr, ":UTIME = %.4f secs.\n", - time_diff(&time_solver_start, &time_temp)); - fprintf(nusmv_stderr, ":STOP:benchmarking Solving\n"); - fprintf(nusmv_stderr, - "counterexample, k=%d, solver time=%.4f, cumulative time=%.4f.\n", - current_k, - time_diff(&time_solver_start, &time_temp), - time_diff(&time_bmc_start, &time_temp)); - } + { + times(&time_temp); + fprintf(nusmv_stderr, ":UTIME = %.4f secs.\n", + time_diff(&time_solver_start, &time_temp)); + fprintf(nusmv_stderr, ":STOP:benchmarking Solving\n"); + fprintf(nusmv_stderr, + "counterexample, k=%d, solver time=%.4f, cumulative time=%.4f.\n", + current_k, + time_diff(&time_solver_start, &time_temp), + time_diff(&time_bmc_start, &time_temp)); + } #endif - - /* Processes the result: */ - switch (satResult) { - case SAT_SOLVER_UNSATISFIABLE_PROBLEM: { - fprintf(nusmv_stdout, - "-- no counterexample found with bound %d", - current_k); - if (opt_verbose_level_gt(options, 2)) { - fprintf(nusmv_stdout, " for "); - print_spec(nusmv_stdout, ltlprop); + + /* Processes the result: */ + switch (satResult) { + case SAT_SOLVER_UNSATISFIABLE_PROBLEM: { + fprintf(nusmv_stdout, + "-- no counterexample found with bound %d", + current_k); + if (opt_verbose_level_gt(options, 2)) { + fprintf(nusmv_stdout, " for "); + print_spec(nusmv_stdout, ltlprop); + } + fprintf(nusmv_stdout, "\n"); + break; } - fprintf(nusmv_stdout, "\n"); - break; - } - case SAT_SOLVER_SATISFIABLE_PROBLEM: - fprintf(nusmv_stdout, "-- "); - print_spec(nusmv_stdout, ltlprop); - fprintf(nusmv_stdout, " is false\n"); - Prop_set_status(ltlprop, Prop_False); + case SAT_SOLVER_SATISFIABLE_PROBLEM: + fprintf(nusmv_stdout, "-- "); + print_spec(nusmv_stdout, ltlprop); + fprintf(nusmv_stdout, " is false\n"); + Prop_set_status(ltlprop, Prop_False); - found_solution = true; + found_solution = true; + if (opt_counter_examples(options)) { + Trace_ptr trace = + Sbmc_Utils_generate_and_print_cntexample(be_enc, + zolver, + Enc_get_bdd_encoding(), + sbmc_state_vars_get_l_var(state_vars), + current_k, + "BMC Counterexample"); + Prop_set_trace(ltlprop, Trace_get_id(trace)); + } - if (opt_counter_examples(options)) { - Trace_ptr trace = - Sbmc_Utils_generate_and_print_cntexample(be_enc, - zolver, - Enc_get_bdd_encoding(), - sbmc_state_vars_get_l_var(state_vars), - current_k, - "BMC Counterexample"); - Prop_set_trace(ltlprop, Trace_get_id(trace)); - } - break; + break; + + case SAT_SOLVER_INTERNAL_ERROR: + internal_error("Sorry, solver answered with a fatal Internal " + "Failure during problem solving.\n"); + break; + + case SAT_SOLVER_TIMEOUT: + case SAT_SOLVER_MEMOUT: + internal_error("Sorry, solver ran out of resources and aborted " + "the execution.\n"); + break; + + default: + internal_error("Sbmc_zigzag_incr: Unexpected value in satResult"); + } /* switch */ + } - case SAT_SOLVER_INTERNAL_ERROR: - internal_error("Sorry, solver answered with a fatal Internal " - "Failure during problem solving.\n"); - break; + if ( !sbmc_MS_isActive(zolver) ) break; - case SAT_SOLVER_TIMEOUT: - case SAT_SOLVER_MEMOUT: - internal_error("Sorry, solver ran out of resources and aborted " - "the execution.\n"); - break; - - default: - internal_error("Sbmc_zigzag_incr: Unexpected value in satResult"); - } /* switch */ - if (opt_verbose_level_gt(options, 1)) fprintf(nusmv_stderr, "Deleting k-dependent stuff\n"); @@ -786,6 +815,7 @@ if (state_vars != (state_vars_struct*) NULL) { sbmc_state_vars_destroy(state_vars); } + return 0; } Index: src/bmc/sbmc/sbmcCmd.c =================================================================== --- src/bmc/sbmc/sbmcCmd.c (revision 1) +++ src/bmc/sbmc/sbmcCmd.c (revision 27) @@ -92,6 +92,9 @@ static int UsageSBMCCheckLtlSpec ARGS((void)); static int UsageSBMCGenLtlSpec ARGS((void)); static int UsageSBMCIncCheck ARGS((void)); +static int UsageSBMCIncGen ARGS((void)); /* SW090824 */ +static int UsageSBMCIncPipe ARGS((void)); /* SW090824 */ +static void freePipeProgArgs( char* ppa[]); /* SW090825 */ static outcome sbmc_cmd_options_handling ARGS((int argc, char** argv, @@ -102,6 +105,7 @@ int* res_k, int* res_l, char** res_o, + char*** pipeProgArgs, /* SW090825 */ boolean* res_N, boolean* res_c, boolean* res_1)); @@ -216,8 +220,9 @@ Prop_Ltl, <lprop, &k, &relative_loop, &fname, + NULL, /* SW090825 pipeProgArgs */ NULL, /* -N */ - NULL /* -c */, + NULL, /* -c */ &single_prob); if (opt_handling_res == SUCCESS_REQUIRED_HELP) { @@ -401,6 +406,7 @@ <lprop, &k, &relative_loop, &fname, + NULL, /* SW090825 pipeProgArgs */ NULL, NULL /* -N -c */, &single_prob); @@ -504,34 +510,52 @@ CommandDescription [optional] ******************************************************************************/ -int Sbmc_CommandLTLCheckZigzagInc(int argc, char** argv) +static outcome commandLTLZigzagInc(int argc, char** argv, boolean mustSolve, boolean mustPipe) { Prop_ptr ltlprop = PROP(NULL); /* The property being processed */ outcome opt_handling_res; int k = get_bmc_pb_length(options); boolean do_virtual_unrolling = true; boolean do_completeness_check = false; + int loop = Bmc_Utils_ConvertLoopFromString(get_bmc_pb_loop(options), NULL); /* SW090119 */ + char* fname = (char*) NULL; /* SW090819 */ + char** pipeProgArgs = (char**) NULL; + assert( !mustSolve || !mustPipe ); + /* ----------------------------------------------------------------------- */ /* Options handling: */ opt_handling_res = sbmc_cmd_options_handling(argc, argv, Prop_Ltl, <lprop, &k, - NULL, NULL, /* l, o */ + &loop, /* SW090119 */ + mustPipe ? NULL : &fname, /* SW090819 */ + mustPipe ? &pipeProgArgs : NULL, /* SW090825 */ &do_virtual_unrolling, - &do_completeness_check, + mustSolve ? &do_completeness_check : NULL, NULL /* single problem */ ); - if (opt_handling_res == SUCCESS_REQUIRED_HELP) { - return UsageSBMCIncCheck(); + if (opt_handling_res == SUCCESS_REQUIRED_HELP ) { + if (fname != (char*) NULL) FREE(fname); + if (pipeProgArgs != NULL) freePipeProgArgs(pipeProgArgs); + return SUCCESS_REQUIRED_HELP; } - if (opt_handling_res != SUCCESS) return 1; /* makes sure bmc has been set up */ - if (Bmc_check_if_model_was_built(nusmv_stderr, false)) { - return 1; + if ((opt_handling_res != SUCCESS) || (Bmc_check_if_model_was_built(nusmv_stderr, false))) { + if (fname != (char*) NULL) FREE(fname); + if (pipeProgArgs != NULL) freePipeProgArgs(pipeProgArgs); + return GENERIC_ERROR; } + + /* SW090819 */ + if ( !mustSolve && !mustPipe && ( fname == (char*) NULL ) ) { + fname = util_strsav(get_bmc_inccnf_filename(options)); + } + + nusmv_assert( !mustPipe || (pipeProgArgs[0] != NULL) ); + /* ----------------------------------------------------------------------- */ /* prepares the list of properties if no property was selected: */ @@ -543,26 +567,77 @@ nusmv_assert(props != LS_NIL); lsForEachItem(props, iterator, prop) { - if (Sbmc_zigzag_incr(prop, k, do_virtual_unrolling, - do_completeness_check) != 0) - return 1; + if (Sbmc_zigzag_incr(prop, k, loop, do_virtual_unrolling, + do_completeness_check, + /* SW090819 */ + mustSolve, + pipeProgArgs, + fname) != 0) { + if (fname != (char*) NULL) FREE(fname); + if (pipeProgArgs != NULL) freePipeProgArgs(pipeProgArgs); + return GENERIC_ERROR; + } } lsDestroy(props, NULL); /* the list is no longer needed */ } else { /* its time to solve (a single property): */ - if (Sbmc_zigzag_incr(ltlprop, k, do_virtual_unrolling, - do_completeness_check) != 0) - return 1; + if (Sbmc_zigzag_incr(ltlprop, k, loop, do_virtual_unrolling, + do_completeness_check, + /* SW090819 */ + mustSolve, + pipeProgArgs, + fname) != 0) { + if (fname != (char*) NULL) FREE(fname); + if (pipeProgArgs != NULL) freePipeProgArgs(pipeProgArgs); + return GENERIC_ERROR; + } } - return 0; + if (fname != (char*) NULL) FREE(fname); + if (pipeProgArgs != NULL) freePipeProgArgs(pipeProgArgs); + return SUCCESS; } +int Sbmc_CommandLTLCheckZigzagInc(int argc, char** argv) { + outcome res = commandLTLZigzagInc(argc, argv, true, false); + + if ( res == SUCCESS_REQUIRED_HELP ) + return UsageSBMCIncCheck(); + else if ( res != SUCCESS ) + return 1; + else + return 0; +} + +/* SW090824 */ +int Sbmc_CommandLTLGenZigzagInc(int argc, char** argv) { + outcome res = commandLTLZigzagInc(argc, argv, false, false); + + if ( res == SUCCESS_REQUIRED_HELP ) + return UsageSBMCIncGen(); + else if ( res != SUCCESS ) + return 1; + else + return 0; +} + +/* SW090824 */ +int Sbmc_CommandLTLPipeZigzagInc(int argc, char** argv) { + outcome res = commandLTLZigzagInc(argc, argv, false, true); + + if ( res == SUCCESS_REQUIRED_HELP ) + return UsageSBMCIncPipe(); + else if ( res != SUCCESS ) + return 1; + else + return 0; +} + + static int UsageSBMCIncCheck(void) { - fprintf(nusmv_stderr, "\nUsage: check_ltlspec_sbmc_inc [-h | -n idx | -p \"formula\"] [-k max_length] [-N] [-c] [-1]\n"); - fprintf(nusmv_stderr, " [-o ] [-N] [-c]\n"); + fprintf(nusmv_stderr, "\nUsage: check_ltlspec_sbmc_inc [-h | -n idx | -p \"formula\"] [-k max_length]\n\t[-N] [-c] [-o ]\n"); fprintf(nusmv_stderr, " -h \t\tPrints the command usage.\n"); fprintf(nusmv_stderr, " -n idx\tChecks the LTL property specified with \n" " \t(using incremental algorithms).\n"); @@ -570,17 +645,45 @@ fprintf(nusmv_stderr, "\t\tIf no property is specified, checks all LTL properties (using \n" "\t\tincremental algorithms).\n"); fprintf(nusmv_stderr, " -k max_length\tChecks the property using value instead of using \n\t\tthe variable value.\n"); - fprintf(nusmv_stderr, " -o filename\tGenerates dimacs output file too. may contain patterns\n\n"); fprintf(nusmv_stderr, " -N \t\tDoes not perform virtual unrolling.\n"); - fprintf(nusmv_stderr, " -c \t\tPerforms completeness check.\n"); - fprintf(nusmv_stderr, " -1 \t\tGenerates and solves a single problem.\n"); + fprintf(nusmv_stderr, " -c \t\tPerforms completeness check.\n"); + fprintf(nusmv_stderr, " -o filename\tGenerates iCNF output file too. may contain patterns\n\n"); return 1; } +static int UsageSBMCIncGen(void) +{ + fprintf(nusmv_stderr, "\nUsage: gen_ltlspec_sbmc_inc [-h | -n idx | -p \"formula\"] [-k max_length]\n\t[-N] [-o ]\n"); + fprintf(nusmv_stderr, " -h \t\tPrints the command usage.\n"); + fprintf(nusmv_stderr, " -n idx\tEncodes the LTL property specified with \n"); + fprintf(nusmv_stderr, " -p \"formula\"\tEncodes the specified LTL property\n"); + fprintf(nusmv_stderr, "\t\tIf no property is specified, encodes all LTL properties\n"); + fprintf(nusmv_stderr, " -k max_length\tEncodes the property using value instead of using \n\t\tthe variable value.\n"); + fprintf(nusmv_stderr, " -N \t\tDoes not encode virtual unrolling.\n"); + fprintf(nusmv_stderr, " -o filename\tiCNF output filename. may contain patterns\n\n"); + return 1; +} +static int UsageSBMCIncPipe(void) +{ + fprintf(nusmv_stderr, "\nUsage: pipe_ltlspec_sbmc_inc [-h | -n idx | -p \"formula\"] [-k max_length]\n\t[-N] -s \n"); + fprintf(nusmv_stderr, " -h \t\tPrints the command usage.\n"); + fprintf(nusmv_stderr, " -n idx\tEncodes the LTL property specified with \n"); + fprintf(nusmv_stderr, " -p \"formula\"\tEncodes the specified LTL property\n"); + fprintf(nusmv_stderr, "\t\tIf no property is specified, encodes all LTL properties\n"); + fprintf(nusmv_stderr, " -k max_length\tEncodes the property using value instead of using \n\t\tthe variable value.\n"); + fprintf(nusmv_stderr, " -N \t\tDoes not encode virtual unrolling.\n"); + fprintf(nusmv_stderr, " -s \t\tEverything trailing -s will be treated as a command\n"); + fprintf(nusmv_stderr, "\t\twith parameters that is executed in the shell. The iCNF\n"); + fprintf(nusmv_stderr, "\t\tencoding is piped to that command's stdin\n"); + return 1; +} + + + /**Function******************************************************************** Synopsis [Top-level function for bmc of PSL properties] @@ -636,23 +739,23 @@ "solvers is an unsupported feature of SBMC.\n"); return 1; } - - if (dump_prob && inc_sat) { - fprintf(nusmv_stderr, - "Error: problem cannot be dumped when incremental sat solving is used.\n"); - return 1; - } if (inc_sat) { - if (Sbmc_zigzag_incr(prop, k, do_virtual_unrolling, - do_completeness_check) != 0) + if (Sbmc_zigzag_incr(prop, k, + rel_loop, /* SW090819 */ + do_virtual_unrolling, + do_completeness_check, + /* SW090819 */ + true, + false, + get_bmc_inccnf_filename(options)) != 0) return 1; } else { if (Bmc_SBMCGenSolveLtl(prop, k, rel_loop, !single_prob, /* iterate on k */ true, /* solve */ - (dump_prob) ? BMC_DUMP_DIMACS : BMC_DUMP_NONE, + false, get_bmc_dimacs_filename(options)) != 0) { return 1; } @@ -720,10 +823,12 @@ int* res_k, int* res_l, char** res_o, + char*** pipeProgArgs, boolean* res_N, - boolean* res_c, + boolean* res_c, boolean* res_1) { + int argCnt = 0; int c; int prop_idx; char* str_formula = (char*) NULL; @@ -754,12 +859,14 @@ *res_o = (char*) NULL; strcat(opt_string, "o:"); } + if (pipeProgArgs != NULL) { + strcat(opt_string,"s:"); + } if (res_N != (boolean*) NULL) strcat(opt_string, "N"); if (res_c != (boolean*) NULL) strcat(opt_string, "c"); if (res_1 != (boolean*) NULL) strcat(opt_string, "1"); - util_getopt_reset(); while ((c = util_getopt((int)argc, (char**) argv, opt_string)) != EOF) { switch (c) { @@ -866,6 +973,20 @@ *res_o = util_strsav(util_optarg); break; + case 's': + { + int i=0; + + *pipeProgArgs = (char**) malloc( (2+argc-util_optind) * sizeof(char*) ); + nusmv_assert( *pipeProgArgs != NULL ); + + util_optind--; + while( util_optind < argc ) + (*pipeProgArgs)[i++] = util_strsav(argv[util_optind++]); + (*pipeProgArgs)[i] = NULL; + } + break; + case 'N': nusmv_assert(res_N != (boolean*) NULL); *res_N = false; @@ -891,7 +1012,7 @@ return GENERIC_ERROR; } - /* Checking of k,l constrains: */ + /* Checking of l constraint: */ if (str_loop != (char*) NULL) { outcome res; int rel_loop; @@ -905,15 +1026,14 @@ } FREE(str_loop); - if (Bmc_Utils_Check_k_l(*res_k, - Bmc_Utils_RelLoop2AbsLoop(rel_loop, *res_k)) - != SUCCESS) { - error_bmc_invalid_k_l(*res_k, rel_loop); + /* SW090821 */ + if ( !Bmc_Utils_IsAllLoopbacks(rel_loop) && !Bmc_Utils_IsNoLoopback(rel_loop) ) { + fprintf(nusmv_stderr, "sbmc encoding can only be used with all (*) or no (X) loopbacks\n"); return GENERIC_ERROR; } *res_l = rel_loop; - } /* k,l consistency check */ + } /* Formula checking and commitment: */ @@ -940,5 +1060,25 @@ FREE(str_formula); } /* formula checking and commit */ + /* SW090825 */ + if ( pipeProgArgs != NULL && *pipeProgArgs == NULL ) { + fprintf(nusmv_stderr, "Parameter -s is obligatory\n"); + return GENERIC_ERROR; + } + if ( (res_c != NULL) && (*res_c == true) && (res_o != NULL) && (*res_o != NULL) ) { + fprintf(nusmv_stderr, "Can not do completeness check AND generate iCNF output\n"); + return GENERIC_ERROR; + } + + return SUCCESS; } + + +/* SW090825 */ +static void freePipeProgArgs( char* ppa[]) { + int i=0; + while( ppa[i] != NULL ) + free( ppa[i++] ); + free(ppa); +} Index: src/bmc/sbmc/sbmcPkg.c =================================================================== --- src/bmc/sbmc/sbmcPkg.c (revision 1) +++ src/bmc/sbmc/sbmcPkg.c (revision 27) @@ -152,8 +152,9 @@ /* These commands are re-entrant wrt Ctrl+C */ Cmd_CommandAdd("check_ltlspec_sbmc", Sbmc_CommandCheckLtlSpecSBmc, 0, true); Cmd_CommandAdd("gen_ltlspec_sbmc", Sbmc_CommandGenLtlSpecSBmc, 0, true); - Cmd_CommandAdd("check_ltlspec_sbmc_inc", Sbmc_CommandLTLCheckZigzagInc, - 0, true); + Cmd_CommandAdd("check_ltlspec_sbmc_inc", Sbmc_CommandLTLCheckZigzagInc, 0, true); + Cmd_CommandAdd("gen_ltlspec_sbmc_inc", Sbmc_CommandLTLGenZigzagInc, 0, true); + Cmd_CommandAdd("pipe_ltlspec_sbmc_inc", Sbmc_CommandLTLPipeZigzagInc, 0, true); } Index: src/bmc/sbmc/sbmcUtils.c =================================================================== --- src/bmc/sbmc/sbmcUtils.c (revision 1) +++ src/bmc/sbmc/sbmcUtils.c (revision 27) @@ -41,6 +41,7 @@ #include #include +#include #if HAVE_CONFIG_H # include "config.h" @@ -99,6 +100,13 @@ SatIncSolver_ptr solver; SatSolverGroup permanent_group; SatSolverGroup volatile_group; + /* SW090821 Additional data for dumping iCNF files */ + FILE* iCnfDumpFile; + hash_ptr cnfVar2dumpVar; + int dumpVarCnt; + int volatile_dump_group; + int outPipe; + pid_t pipeThreadPid; }; /*---------------------------------------------------------------------------*/ @@ -138,15 +146,28 @@ #define METASOLVERCHECK( ms ) \ nusmv_assert((sbmc_MetaSolver *)NULL != ms); \ nusmv_assert((BeEnc_ptr)NULL != ms->be_enc); \ - nusmv_assert((SatIncSolver_ptr)NULL != ms->solver); - + nusmv_assert((SatIncSolver_ptr)NULL != ms->solver); +/* SW090820 Using the MS_create_ext function a metasolver can be created + for dumping iCNFs that is NOT an interface to an actual solver */ +#define EXTMETASOLVERCHECK( ms ) \ + nusmv_assert((sbmc_MetaSolver *)NULL != ms); \ + nusmv_assert((BeEnc_ptr)NULL != ms->be_enc); + /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ +/* SW090820 */ +static void sbmc_dump_volatileframe_end(sbmc_MetaSolver *ms); +static void sbmc_dump_inc(sbmc_MetaSolver *ms, Be_Cnf_ptr cnf); +static void sbmc_dump_problemline(sbmc_MetaSolver *ms); +static boolean sbmc_openpipe(sbmc_MetaSolver *ms, char *const progargs[]); +static void sbmc_dump_int(sbmc_MetaSolver *ms, int i); +static void sbmc_dump_str(sbmc_MetaSolver *ms, const char *str); + /**AutomaticEnd***************************************************************/ @@ -913,31 +934,75 @@ SideEffects [None] ******************************************************************************/ -sbmc_MetaSolver * sbmc_MS_create(BeEnc_ptr be_enc) +boolean volatile stopPipe; +void sigh( int sig ) { + stopPipe = true; +} +sbmc_MetaSolver * sbmc_MS_create_ext(BeEnc_ptr be_enc, boolean must_solve, + char *const pipeProgArgs[], const char *dumpFilename) { - nusmv_assert((BeEnc_ptr)NULL != be_enc); sbmc_MetaSolver * ms = ALLOC(sbmc_MetaSolver, 1); nusmv_assert((sbmc_MetaSolver *)NULL != ms); + stopPipe = false; + signal( SIGCHLD, sigh ); + ms->be_enc = be_enc; ms->using_volatile_group = false; ms->solver = SAT_INC_SOLVER(NULL); - ms->solver = Sat_CreateIncSolver(get_sat_solver(options)); + ms->iCnfDumpFile = NULL; + ms->outPipe = -1; + ms->cnfVar2dumpVar = ( dumpFilename != NULL || pipeProgArgs != NULL ) ? new_assoc() : NULL; + ms->dumpVarCnt = 0; + + if ( must_solve ) { + ms->solver = Sat_CreateIncSolver(get_sat_solver(options)); + + if (ms->solver == SAT_INC_SOLVER(NULL)) { + fprintf(nusmv_stderr, "Incremental sat solver '%s' is not available.\n", + get_sat_solver(options)); + FREE(ms); + return (sbmc_MetaSolver *)NULL; + } + ms->permanent_group = SatSolver_get_permanent_group(SAT_SOLVER(ms->solver)); + } + else nusmv_assert( dumpFilename != NULL || pipeProgArgs != NULL ); - if (ms->solver == SAT_INC_SOLVER(NULL)) { - fprintf(nusmv_stderr, "Incremental sat solver '%s' is not available.\n", - get_sat_solver(options)); + if ( pipeProgArgs != NULL && !sbmc_openpipe( ms, pipeProgArgs ) ) { FREE(ms); return (sbmc_MetaSolver *)NULL; } - ms->permanent_group = SatSolver_get_permanent_group(SAT_SOLVER(ms->solver)); + + if ( dumpFilename != NULL ) { + ms->iCnfDumpFile = fopen( dumpFilename, "wt" ); + if ( ms->iCnfDumpFile == NULL ) { + fprintf(nusmv_stderr, "Could not open file '%s' for writing.\n", dumpFilename); + FREE(ms); + return (sbmc_MetaSolver *)NULL; + } + } + + sbmc_dump_problemline(ms); + return ms; } +sbmc_MetaSolver * sbmc_MS_create(BeEnc_ptr be_enc) +{ + sbmc_MS_create_ext(be_enc, true, false, NULL); +} + +/* SW090825 Returns false if this meta solver doesn't do anything at all + this may happen if we were piping to an application which terminated. + */ +boolean sbmc_MS_isActive(sbmc_MetaSolver *ms) { + return ( ms->iCnfDumpFile != NULL ) || ( ms->outPipe >= 0 ) || ( ms->solver != NULL ); +} + /**Function******************************************************************** Synopsis [Destroy a meta solver wrapper] @@ -949,9 +1014,19 @@ ******************************************************************************/ void sbmc_MS_destroy(sbmc_MetaSolver *ms) { - METASOLVERCHECK(ms); - SatIncSolver_destroy(ms->solver); - ms->solver = SAT_INC_SOLVER(NULL); + EXTMETASOLVERCHECK(ms); + + if ( ms->solver != NULL ) { + SatIncSolver_destroy(ms->solver); + ms->solver = SAT_INC_SOLVER(NULL); + } + + if ( ms->cnfVar2dumpVar != NULL ) free_assoc(ms->cnfVar2dumpVar); + if ( ms->iCnfDumpFile != NULL ) fclose(ms->iCnfDumpFile); + if ( ms->outPipe >= 0 ) { + close( ms->outPipe ); + waitpid(ms->pipeThreadPid, NULL, 0); + } } /**Function******************************************************************** @@ -1036,9 +1111,13 @@ ******************************************************************************/ void sbmc_MS_goto_permanent_group(sbmc_MetaSolver *ms) { - METASOLVERCHECK(ms); + EXTMETASOLVERCHECK(ms); nusmv_assert(ms->using_volatile_group); - SatIncSolver_destroy_group(ms->solver, ms->volatile_group); + + sbmc_dump_volatileframe_end(ms); + + if ( ms->solver != NULL ) + SatIncSolver_destroy_group(ms->solver, ms->volatile_group); ms->using_volatile_group = false; } @@ -1055,9 +1134,12 @@ ******************************************************************************/ void sbmc_MS_goto_volatile_group(sbmc_MetaSolver *ms) { - METASOLVERCHECK(ms); + EXTMETASOLVERCHECK(ms); nusmv_assert(!ms->using_volatile_group); - ms->volatile_group = SatIncSolver_create_group(ms->solver); + if ( ms->solver != NULL ) + ms->volatile_group = SatIncSolver_create_group(ms->solver); + + ms->volatile_dump_group = ++ms->dumpVarCnt; ms->using_volatile_group = true; } @@ -1078,22 +1160,26 @@ Be_Cnf_ptr cnf; be_ptr inconstr; - METASOLVERCHECK(ms); + EXTMETASOLVERCHECK(ms); be_mgr = BeEnc_get_be_manager(ms->be_enc); - SatSolver_ptr solver = SAT_SOLVER(ms->solver); - inconstr = Bmc_Utils_apply_inlining(be_mgr, be_constraint); cnf = Be_ConvertToCnf(be_mgr, inconstr, 1); - if (ms->using_volatile_group) { - SatSolver_add(solver, cnf, ms->volatile_group); - SatSolver_set_polarity(solver, cnf, 1, ms->volatile_group); + if ( ms->solver != (SatIncSolver_ptr) NULL ) { + SatSolver_ptr solver = SAT_SOLVER(ms->solver); + if (ms->using_volatile_group) { + SatSolver_add(solver, cnf, ms->volatile_group); + SatSolver_set_polarity(solver, cnf, 1, ms->volatile_group); + } + else { + SatSolver_add(solver, cnf, ms->permanent_group); + SatSolver_set_polarity(solver, cnf, 1, ms->permanent_group); + } } - else { - SatSolver_add(solver, cnf, ms->permanent_group); - SatSolver_set_polarity(solver, cnf, 1, ms->permanent_group); - } + + sbmc_dump_inc(ms, cnf); + Be_Cnf_Delete(cnf); } @@ -1301,6 +1387,24 @@ return _sbmc_loopvar_name; } +int sbmc_cnfVar2dumpVar(sbmc_MetaSolver *ms, int lit) { + int cnfVar = abs(lit); + int dumpVar; + + nusmv_assert(cnfVar > 0); + + dumpVar = NODE_TO_INT(find_assoc(ms->cnfVar2dumpVar, + NODE_FROM_INT(cnfVar))); + + if ((int)Nil == dumpVar) { + dumpVar = ++ms->dumpVarCnt; + insert_assoc(ms->cnfVar2dumpVar, + NODE_FROM_INT(cnfVar), NODE_FROM_INT(dumpVar)); + } + + return lit > 0 ? dumpVar : - dumpVar; +} + /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ @@ -1310,4 +1414,130 @@ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ +/* SW090820 */ +static void sbmc_dump_volatileframe_end(sbmc_MetaSolver *ms) { + sbmc_dump_str( ms, "a "); + sbmc_dump_int( ms, -ms->volatile_dump_group ); + sbmc_dump_str( ms, "0\n"); +} +/* SW090820 */ +static void sbmc_dump_inc(sbmc_MetaSolver *ms, Be_Cnf_ptr cnf) { + int time; + Be_Manager_ptr be_mgr = BeEnc_get_be_manager(ms->be_enc); + + if ( ms->iCnfDumpFile != NULL || ms->outPipe >= 0 ) + { + lsList cl = LS_NIL; + lsGen genCl, genLit; + nusmv_ptrint lit = 0; + + // If a Boolean constant is to be encoded + if (Be_Cnf_GetFormulaLiteral(cnf) == INT_MAX) { + // If the Boolean constant is FALSE + if (0 != lsLength(Be_Cnf_GetClausesList(cnf))) { + if ( ms->using_volatile_group ) { + sbmc_dump_int(ms, ms->volatile_dump_group ); + sbmc_dump_str(ms,"0\n" ); + } + else { + sbmc_dump_str(ms,"1 0\n-1 0\n"); /* this is always false */ + } + } + } else { + /* Prints the clauses. */ + genCl = lsStart(Be_Cnf_GetClausesList(cnf)); + while (lsNext(genCl, (lsGeneric*) &cl, LS_NH) == LS_OK) { + genLit = lsStart(cl); + while (lsNext(genLit, (lsGeneric*) &lit, LS_NH) == LS_OK) { + sbmc_dump_int(ms, sbmc_cnfVar2dumpVar(ms, lit)); + } + lsFinish(genLit); + + if ( ms->using_volatile_group ) + sbmc_dump_int(ms, ms->volatile_dump_group); + + sbmc_dump_str(ms, "0\n"); + } + lsFinish(genCl); + + sbmc_dump_int(ms, sbmc_cnfVar2dumpVar(ms, Be_Cnf_GetFormulaLiteral(cnf))); + if ( ms->using_volatile_group ) + sbmc_dump_int(ms, ms->volatile_dump_group); + sbmc_dump_str(ms, "0\n"); + } + } +} + +/* SW090820 */ +static void sbmc_dump_problemline(sbmc_MetaSolver *ms) { + sbmc_dump_str( ms, "p inccnf\n" ); +} + +/* SW090824 */ +static boolean sbmc_openpipe(sbmc_MetaSolver *ms, char *const progargs[]) { + int writePipe[2]; + pid_t pid, ppid=getpid(); + + nusmv_assert(progargs); + nusmv_assert(progargs[0]); + + if ( pipe(writePipe) < 0 || (pid = fork()) < 0 ) { + fprintf(nusmv_stderr,"Error opening pipe or forking thread\n"); + return false; + } + else if ( pid == 0 ) { + signal( SIGCHLD, SIG_IGN ); + + dup2( writePipe[0], 0 ); /* Redirect pipe to stdin */ + close( writePipe[0] ); + close( writePipe[1] ); + + /* This child is forked again to handle finished execution of "args[0]" */ + if ( (pid = fork()) < 0 ) { + fprintf(nusmv_stderr,"Error opening pipe or forking thread\n"); + _exit(1); + } + else if ( pid == 0 ) { + execvp( progargs[0], progargs ); + fprintf(nusmv_stderr,"Error executing '%s'\n", progargs[0]); + } + else { + char buf[32]; + waitpid(pid, NULL, 0); /* Wait for external program to finish */ + + kill( ppid, SIGCHLD ); /* Signal parent we're about to die */ + while(read(0,buf,32)>0) {} /* Allow parent to finish its pending writes */ + } + + _exit(0); + } + + ms->pipeThreadPid = pid; + ms->outPipe = writePipe[1]; + close( writePipe[0] ); + + return true; +} + +static void sbmc_dump_int(sbmc_MetaSolver *ms, int i) { + char str[20]; + sprintf( str, "%d ", i ); + sbmc_dump_str(ms, str); +} + +static void sbmc_dump_str(sbmc_MetaSolver *ms, const char *str) { + if ( ms->iCnfDumpFile != NULL ) + fprintf( ms->iCnfDumpFile, str ); + + if ( ms->outPipe >= 0 ) { + write( ms->outPipe, str, strlen(str) ); + + /* If we have been signalled that the external program + has terminated close the pipe */ + if ( stopPipe ) { + close( ms->outPipe ); + ms->outPipe = -1; + } + } +} Index: src/bmc/sbmc/sbmcBmcInc.h =================================================================== --- src/bmc/sbmc/sbmcBmcInc.h (revision 1) +++ src/bmc/sbmc/sbmcBmcInc.h (revision 27) @@ -80,8 +80,13 @@ EXTERN int Sbmc_zigzag_incr ARGS((Prop_ptr ltlprop, const int max_k, + const int loop, /* SW090119 */ const int opt_do_virtual_unrolling, - const int opt_do_completeness_check)); + const int opt_do_completeness_check, + /* SW090819 */ + const boolean must_solve, + char* const pipeProgArgs[], + const char* dump_fname_template)); /**AutomaticEnd***************************************************************/ Index: src/bmc/sbmc/sbmcCmd.h =================================================================== --- src/bmc/sbmc/sbmcCmd.h (revision 1) +++ src/bmc/sbmc/sbmcCmd.h (revision 27) @@ -58,8 +58,11 @@ EXTERN int Sbmc_CommandCheckLtlSpecSBmc ARGS((int argc, char** argv)); EXTERN int Sbmc_CommandGenLtlSpecSBmc ARGS((int argc, char** argv)); -EXTERN int Sbmc_CommandLTLCheckZigzagInc ARGS((int argc, char** argv)); +EXTERN int Sbmc_CommandLTLCheckZigzagInc ARGS((int argc, char** argv)); +EXTERN int Sbmc_CommandLTLGenZigzagInc ARGS((int argc, char** argv)); /* SW090824 */ +EXTERN int Sbmc_CommandLTLPipeZigzagInc ARGS((int argc, char** argv)); /* SW090824 */ + EXTERN int Sbmc_check_psl_property ARGS((Prop_ptr prop, boolean dump_prob, boolean inc_sat, Index: src/bmc/sbmc/sbmcUtils.h =================================================================== --- src/bmc/sbmc/sbmcUtils.h (revision 1) +++ src/bmc/sbmc/sbmcUtils.h (revision 27) @@ -137,7 +137,10 @@ EXTERN void sbmc_loop_var_name_set ARGS((node_ptr n)); EXTERN node_ptr sbmc_loop_var_name_get ARGS((void)); - +/* SW090820 */ +EXTERN sbmc_MetaSolver * sbmc_MS_create_ext ARGS((BeEnc_ptr be_enc, boolean must_solve, + char *const pipeProgArgs[], const char *dumpFilename)); +EXTERN boolean sbmc_MS_isActive ARGS((sbmc_MetaSolver *ms)); /**AutomaticEnd***************************************************************/ #endif /* _SBMC_UTILS */ Index: src/opt/optCmd.c =================================================================== --- src/opt/optCmd.c (revision 1) +++ src/opt/optCmd.c (revision 27) @@ -161,6 +161,7 @@ /* BMC Stuff */ opt->bmc_mode = false; opt->bmc_dimacs_filename = DEFAULT_DIMACS_FILENAME ; + opt->bmc_inccnf_filename = DEFAULT_INCCNF_FILENAME ; /* SW090821 */ opt->bmc_invar_dimacs_filename = DEFAULT_INVAR_DIMACS_FILENAME ; opt->bmc_pb_length = DEFAULT_BMC_PB_LENGTH; opt->bmc_pb_loop = NULL; set_bmc_pb_loop(opt, DEFAULT_BMC_PB_LOOP); @@ -897,6 +898,19 @@ OPT_SET_DYN_STR(opt->bmc_dimacs_filename, str, DEFAULT_DIMACS_FILENAME); } +/* SW090821 */ +char* get_bmc_inccnf_filename(options_ptr opt) +{ + nusmv_assert(opt != NULL); + return (opt->bmc_inccnf_filename); +} +/* SW090821 */ +void set_bmc_inccnf_filename(options_ptr opt, char* str) +{ + nusmv_assert(opt != NULL); + OPT_SET_DYN_STR(opt->bmc_inccnf_filename, str, + DEFAULT_INCCNF_FILENAME); +} char* get_bmc_invar_dimacs_filename(options_ptr opt) { nusmv_assert(opt != NULL); @@ -1940,6 +1954,10 @@ set_bmc_dimacs_filename(options, util_strsav(flag_value)); return 0; } + if (strcmp(argv[1], BMC_INCCNF_FILENAME) == 0) { /* SW090821 */ + set_bmc_inccnf_filename(options, util_strsav(flag_value)); + return 0; + } if (strcmp(argv[1], BMC_INVAR_DIMACS_FILENAME) == 0) { set_bmc_invar_dimacs_filename(options, util_strsav(flag_value)); return 0; @@ -2633,6 +2651,9 @@ fprintf(fn, "%s\t\t\"%s\"\n", BMC_DIMACS_FILENAME, (opt->bmc_dimacs_filename != (char*) NULL) ? opt->bmc_dimacs_filename : OPT_USER_POV_NULL_STRING); + fprintf(fn, "%s\t\t\"%s\"\n", BMC_INCCNF_FILENAME, /* SW090821 */ + (opt->bmc_inccnf_filename != (char*) NULL) + ? opt->bmc_inccnf_filename : OPT_USER_POV_NULL_STRING); fprintf(fn, "%s\t\"%s\"\n", BMC_INVAR_DIMACS_FILENAME, (opt->bmc_invar_dimacs_filename != (char*) NULL) ? opt->bmc_invar_dimacs_filename : OPT_USER_POV_NULL_STRING); Index: src/opt/opt.h =================================================================== --- src/opt/opt.h (revision 1) +++ src/opt/opt.h (revision 27) @@ -74,6 +74,7 @@ /* BMC stuff */ #define DEFAULT_DIMACS_FILENAME "@f_k@k_l@l_n@n" #define DEFAULT_INVAR_DIMACS_FILENAME "@f_invar_n@n" +#define DEFAULT_INCCNF_FILENAME "@f_kmax@k_l@l_n@n" /* SW090821 */ #define DEFAULT_BMC_PB_LENGTH 10 #define DEFAULT_BMC_PB_LOOP Bmc_Utils_GetAllLoopbacksString() #define DEFAULT_BMC_INVAR_ALG "classic" @@ -239,6 +240,8 @@ EXTERN void print_partition_method ARGS((FILE *)); EXTERN char* get_bmc_dimacs_filename ARGS((options_ptr)); EXTERN void set_bmc_dimacs_filename ARGS((options_ptr, char *)); +EXTERN char* get_bmc_inccnf_filename ARGS((options_ptr)); /* SW090821 */ +EXTERN void set_bmc_inccnf_filename ARGS((options_ptr, char *)); /* SW090821 */ EXTERN char* get_bmc_invar_dimacs_filename ARGS((options_ptr)); EXTERN void set_bmc_invar_dimacs_filename ARGS((options_ptr, char *)); EXTERN void set_bmc_pb_length ARGS((options_ptr opt, const int k)); Index: src/opt/optInt.h =================================================================== --- src/opt/optInt.h (revision 1) +++ src/opt/optInt.h (revision 27) @@ -207,6 +207,8 @@ #define BMC_MODE "bmc_mode" char* bmc_dimacs_filename; #define BMC_DIMACS_FILENAME "bmc_dimacs_filename" + char* bmc_inccnf_filename; /* SW090821 */ +#define BMC_INCCNF_FILENAME "bmc_inccnf_filename" char* bmc_invar_dimacs_filename; #define BMC_INVAR_DIMACS_FILENAME "bmc_invar_dimacs_filename" int bmc_pb_length;