From: Brian Norris <banorris@uci.edu>
Date: Mon, 4 Mar 2013 03:50:47 +0000 (-0800)
Subject: nodestack: print thread status info in Node::print
X-Git-Tag: oopsla2013~165
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=6153172f6df36b35080456c47ca7178fcb49bbb4

nodestack: print thread status info in Node::print

It's useful to have sleep-set information for debugging.
---

diff --git a/nodestack.cc b/nodestack.cc
index 0127347..8ffdc33 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -98,6 +98,16 @@ Node::~Node()
 void Node::print() const
 {
 	action->print();
+	model_print("          thread status: ");
+	if (enabled_array) {
+		for (int i = 0; i < num_threads; i++) {
+			char str[20];
+			enabled_type_to_string(enabled_array[i], str);
+			model_print("[%d: %s]", i, str);
+		}
+		model_print("\n");
+	} else
+		model_print("(info not available)\n");
 	model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
 	for (int i = 0; i < (int)backtrack.size(); i++)
 		if (backtrack[i] == true)
diff --git a/schedule.cc b/schedule.cc
index a2eb4cf..f65d1e9 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -12,7 +12,7 @@
  * @param e The type to format
  * @param str The output character array
  */
-static void enabled_type_to_string(enabled_type_t e, char *str)
+void enabled_type_to_string(enabled_type_t e, char *str)
 {
 	const char *res;
 	switch (e) {
diff --git a/schedule.h b/schedule.h
index c8555b6..c18953d 100644
--- a/schedule.h
+++ b/schedule.h
@@ -18,6 +18,8 @@ typedef enum enabled_type {
 	THREAD_SLEEP_SET
 } enabled_type_t;
 
+void enabled_type_to_string(enabled_type_t e, char *str);
+
 /** @brief The Scheduler class performs the mechanics of Thread execution
  * scheduling. */
 class Scheduler {