From: Brian Norris <banorris@uci.edu>
Date: Thu, 10 Jan 2013 18:54:02 +0000 (-0800)
Subject: model: reformat execution trace prints
X-Git-Tag: oopsla2013~361
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=65e1c44cb1a70d7d19bc32b07bf41a7a6fa722d0;p=model-checker.git

model: reformat execution trace prints

Bring the "INFEASIBLE" message together with the "Execution #" message,
to make the log more compact and readable (e.g., grep for "Execution"
will give you some regularly-patterned, useful information).
---

diff --git a/model.cc b/model.cc
index c63d9d9..9c34884 100644
--- a/model.cc
+++ b/model.cc
@@ -2576,13 +2576,11 @@ ModelAction * ModelChecker::new_uninitialized_action(void *location) const
 	return act;
 }
 
-static void print_list(action_list_t *list, int exec_num = -1)
+static void print_list(action_list_t *list)
 {
 	action_list_t::iterator it;
 
 	model_print("---------------------------------------------------------------------\n");
-	if (exec_num >= 0)
-		model_print("Execution %d:\n", exec_num);
 
 	unsigned int hash = 0;
 
@@ -2635,9 +2633,12 @@ void ModelChecker::print_summary() const
 	dumpGraph(buffername);
 #endif
 
-	if (!isfeasibleprefix())
-		print_infeasibility("INFEASIBLE EXECUTION");
-	print_list(action_trace, stats.num_total);
+	model_print("Execution %d:", stats.num_total);
+	if (isfeasibleprefix())
+		model_print("\n");
+	else
+		print_infeasibility(" INFEASIBLE");
+	print_list(action_trace);
 	model_print("\n");
 }