model: revert unnecessary parameter for print_summary()

CycleGraph::checkForCycles() is a cheap function; it only checks a flag status.
So we don't need to make code more complicated just to avoid calling this
function.

Effectively a revert of:
commit 7cee72d776ddfbf585038f3cad3df799e353cc11

diff --git a/model.cc b/model.cc
index 71cf14a3ce136202276e941372ae412787848bac..4cbcd4fd96b215ddf1440b9a20212b01fb4579d5 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -172,9 +172,8 @@ bool ModelChecker::next_execution()
 
        num_executions++;
 
-       bool feasible = isfinalfeasible();
-       if (feasible || DBG_ENABLED())
-               print_summary(feasible);
+       if (isfinalfeasible() || DBG_ENABLED())
+               print_summary();
 
        if ((diverge = model->get_next_backtrack()) == NULL)
                return false;
@@ -704,7 +703,7 @@ static void print_list(action_list_t *list)
        printf("---------------------------------------------------------------------\n");
 }
 
-void ModelChecker::print_summary(bool feasible)
+void ModelChecker::print_summary()
 {
        printf("\n");
        printf("Number of executions: %d\n", num_executions);
@@ -712,7 +711,7 @@ void ModelChecker::print_summary(bool feasible)
 
        scheduler->print();
 
-       if (!feasible)
+       if (!isfinalfeasible())
                printf("INFEASIBLE EXECUTION!\n");
        print_list(action_trace);
        printf("\n");

diff --git a/model.h b/model.h
index e93c4b51f6aa0cf9c12529c6f1220823f63cb380..dc6ef6add21045042ed42a29882e3ad9a38ac34e 100644 (file)
--- a/model.h
+++ b/model.h
@@ -50,12 +50,8 @@ public:
 
        void check_current_action(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);
+       /** Prints an execution summary with trace information. */
+       void print_summary();
 
        Thread * schedule_next_thread();