model: record the number of feasible executions

The 'num_executions' statistic isn't quite as useful now. We want to compare
total executions to the number of feasible executions.

diff --git a/model.cc b/model.cc
index 096ebe450e5db5221afe80f55ae0aa498da2021e..cdce1028c141b914dcf4f0d7623df3c452eeb461 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -21,6 +21,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        /* Initialize default scheduler */
        scheduler(new Scheduler()),
        num_executions(0),
+       num_feasible_executions(0),
        params(params),
        diverge(NULL),
        action_trace(new action_list_t()),
@@ -174,6 +175,8 @@ bool ModelChecker::next_execution()
        DBG();
 
        num_executions++;
+       if (isfinalfeasible())
+               num_feasible_executions++;
 
        if (isfinalfeasible() || DBG_ENABLED())
                print_summary();
@@ -1229,6 +1232,7 @@ void ModelChecker::print_summary()
 {
        printf("\n");
        printf("Number of executions: %d\n", num_executions);
+       printf("Number of feasible executions: %d\n", num_feasible_executions);
        printf("Total nodes created: %d\n", node_stack->get_total_nodes());
 
 #if SUPPORT_MOD_ORDER_DUMP

diff --git a/model.h b/model.h
index bd8791964baee4982c058c05c42d3678a7f621da..4f1d6eece463e4e0da4e59d8b09816aa4772d6a9 100644 (file)
--- a/model.h
+++ b/model.h
@@ -99,6 +99,7 @@ private:
        bool has_asserted() {return asserted;}
        void reset_asserted() {asserted=false;}
        int num_executions;
+       int num_feasible_executions;
        bool promises_expired();
        const model_params params;