X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=bf54ecc10aadf02a1807dec87dd7c013f998a81d;hb=9a9c5146d0bb00385367066ae9d657adb3edc50d;hp=8dcb6f3ad8e69a0e82ad3991c4425a35f1a24640;hpb=adf77053d498af32ab4c6764b50d4265bed5996c;p=model-checker.git

diff --git a/model.cc b/model.cc
index 8dcb6f3..bf54ecc 100644
--- a/model.cc
+++ b/model.cc
@@ -419,8 +419,6 @@ bool ModelChecker::next_execution()
 {
 	DBG();
 
-	record_stats();
-
 	if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
 		model_print("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
@@ -436,13 +434,14 @@ bool ModelChecker::next_execution()
 		checkDataRaces();
 		print_bugs();
 		model_print("\n");
-		print_stats();
 		print_summary();
 	} else if (DBG_ENABLED()) {
 		model_print("\n");
 		print_summary();
 	}
 
+	record_stats();
+
 	if ((diverge = get_next_backtrack()) == NULL)
 		return false;
 
@@ -2222,12 +2221,14 @@ bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *wr
 	}
 }
 
-static void print_list(action_list_t *list)
+static void print_list(action_list_t *list, int exec_num = -1)
 {
 	action_list_t::iterator it;
 
 	model_print("---------------------------------------------------------------------\n");
-	model_print("Trace:\n");
+	if (exec_num >= 0)
+		model_print("Execution %d:\n", exec_num);
+
 	unsigned int hash=0;
 
 	for (it = list->begin(); it != list->end(); it++) {
@@ -2279,7 +2280,7 @@ void ModelChecker::print_summary()
 
 	if (!isfinalfeasible())
 		model_print("INFEASIBLE EXECUTION!\n");
-	print_list(action_trace);
+	print_list(action_trace, stats.num_total);
 	model_print("\n");
 }