model: add "# redundant" stat
authorBrian Norris <banorris@uci.edu>
Sat, 17 Nov 2012 08:01:18 +0000 (00:01 -0800)
committerBrian Norris <banorris@uci.edu>
Sat, 17 Nov 2012 08:01:18 +0000 (00:01 -0800)
model.cc
model.h

index eb5cd34..df06760 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -401,12 +401,15 @@ void ModelChecker::record_stats()
                stats.num_buggy_executions++;
        else if (is_complete_execution())
                stats.num_complete++;
                stats.num_buggy_executions++;
        else if (is_complete_execution())
                stats.num_complete++;
+       else
+               stats.num_redundant++;
 }
 
 /** @brief Print execution stats */
 void ModelChecker::print_stats() const
 {
        model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
 }
 
 /** @brief Print execution stats */
 void ModelChecker::print_stats() const
 {
        model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+       model_print("Number of redundant executions: %d\n", stats.num_redundant);
        model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
        model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
        model_print("Total executions: %d\n", stats.num_total);
        model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
        model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
        model_print("Total executions: %d\n", stats.num_total);
diff --git a/model.h b/model.h
index 0d27d5a..15516e2 100644 (file)
--- a/model.h
+++ b/model.h
@@ -58,6 +58,7 @@ struct execution_stats {
        int num_infeasible; /**< @brief Number of infeasible executions */
        int num_buggy_executions; /** @brief Number of buggy executions */
        int num_complete; /**< @brief Number of feasible, non-buggy, complete executions */
        int num_infeasible; /**< @brief Number of infeasible executions */
        int num_buggy_executions; /** @brief Number of buggy executions */
        int num_complete; /**< @brief Number of feasible, non-buggy, complete executions */
+       int num_redundant; /**< @brief Number of redundant, aborted executions */
 };
 
 struct PendingFutureValue {
 };
 
 struct PendingFutureValue {