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.

diff --git a/model.cc b/model.cc
index 98c6e645382bf2bdc32bc75e45e3a90b1de4a3cd..4844c566a0a1ba898e3a94ac126f30a26b7afc01 100644 (file)
--- 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 4a55c52b5e9f2ac637b952f12598d7374ccb561f..4e4dcf0ff702b9e825646d0dc56407b81cbed38e 100644 (file)
--- 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);