From 7cee72d776ddfbf585038f3cad3df799e353cc11 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 2 Aug 2012 11:13:46 -0700 Subject: [PATCH] model: do not call isfinalfeasible() too many times This function call incurs graph exploration, so when performing some end-of-trace bookkeeping, we should only call it once and cache the result. --- model.cc | 9 +++++---- model.h | 9 ++++++++- 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/model.cc b/model.cc index 98c6e645..4844c566 100644 --- a/model.cc +++ b/model.cc @@ -171,8 +171,9 @@ bool ModelChecker::next_execution() num_executions++; - if (isfinalfeasible() || DBG_ENABLED()) - print_summary(); + bool feasible = isfinalfeasible(); + if (feasible || DBG_ENABLED()) + print_summary(feasible); if ((diverge = model->get_next_backtrack()) == NULL) return false; @@ -704,7 +705,7 @@ static void print_list(action_list_t *list) printf("---------------------------------------------------------------------\n"); } -void ModelChecker::print_summary(void) +void ModelChecker::print_summary(bool feasible) { printf("\n"); printf("Number of executions: %d\n", num_executions); @@ -712,7 +713,7 @@ void ModelChecker::print_summary(void) scheduler->print(); - if (!isfinalfeasible()) + if (!feasible) printf("INFEASIBLE EXECUTION!\n"); print_list(action_trace); printf("\n"); diff --git a/model.h b/model.h index 4a55c52b..4e4dcf0f 100644 --- a/model.h +++ b/model.h @@ -42,7 +42,14 @@ public: ucontext_t * get_system_context(void) { return system_context; } void check_current_action(void); - void print_summary(void); + + /** + * Prints an execution summary with trace information. + * @param feasible Formats outputting according to whether or not the + * current trace is feasible. Defaults to feasible = true. + */ + void print_summary(bool feasible = true); + Thread * schedule_next_thread(); int add_thread(Thread *t); -- 2.34.1