From 1d86ead1f9edde08186daf407f648fef942a93bd Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 14 Sep 2012 10:24:24 -0700 Subject: [PATCH] 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. --- model.cc | 4 ++++ model.h | 1 + 2 files changed, 5 insertions(+) diff --git a/model.cc b/model.cc index 096ebe45..cdce1028 100644 --- 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 bd879196..4f1d6eec 100644 --- 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; -- 2.34.1