model: record the number of feasible executions
authorBrian Norris <banorris@uci.edu>
Fri, 14 Sep 2012 17:24:24 +0000 (10:24 -0700)
committerBrian Norris <banorris@uci.edu>
Fri, 14 Sep 2012 17:30:34 +0000 (10:30 -0700)
The 'num_executions' statistic isn't quite as useful now. We want to compare
total executions to the number of feasible executions.

model.cc
model.h

index 096ebe4..cdce102 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 bd87919..4f1d6ee 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;