From: Brian Norris <banorris@uci.edu>
Date: Wed, 8 Aug 2012 23:27:07 +0000 (-0700)
Subject: model: revert unnecessary parameter for print_summary()
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1ff648af632c0ccc8e5319a077791bd6e49011f6;p=cdsspec-compiler.git

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 71cf14a..4cbcd4f 100644
--- 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 e93c4b5..dc6ef6a 100644
--- 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();