From f5029d07e4fad5921f60108f5632fb2a5e4a52fb Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 28 Feb 2013 11:17:42 -0800
Subject: [PATCH] action: print promise number, not just ?
---
action.cc | 8 +++++++-
model.cc | 20 ++++++++++++++++++++
model.h | 1 +
3 files changed, 28 insertions(+), 1 deletion(-)
diff --git a/action.cc b/action.cc
index 1309024..81f447a 100644
--- a/action.cc
+++ b/action.cc
@@ -543,7 +543,13 @@ void ModelAction::print() const
if (is_read()) {
if (reads_from)
model_print(" Rf: %-3d", reads_from->get_seq_number());
- else
+ else if (reads_from_promise) {
+ int idx = model->get_promise_number(reads_from_promise);
+ if (idx >= 0)
+ model_print(" Rf: P%-2d", idx);
+ else
+ model_print(" RF: P? ");
+ } else
model_print(" Rf: ? ");
}
if (cv) {
diff --git a/model.cc b/model.cc
index 38d63a2..591d42a 100644
--- a/model.cc
+++ b/model.cc
@@ -2840,6 +2840,26 @@ Thread * ModelChecker::get_thread(const ModelAction *act) const
return get_thread(act->get_tid());
}
+/**
+ * @brief Get a Promise's "promise number"
+ *
+ * A "promise number" is an index number that is unique to a promise, valid
+ * only for a specific snapshot of an execution trace. Promises may come and go
+ * as they are generated an resolved, so an index only retains meaning for the
+ * current snapshot.
+ *
+ * @param promise The Promise to check
+ * @return The promise index, if the promise still is valid; otherwise -1
+ */
+int ModelChecker::get_promise_number(const Promise *promise) const
+{
+ for (unsigned int i = 0; i < promises->size(); i++)
+ if ((*promises)[i] == promise)
+ return i;
+ /* Not found */
+ return -1;
+}
+
/**
* @brief Check if a Thread is currently enabled
* @param t The Thread to check
diff --git a/model.h b/model.h
index 9e0b34b..e92137d 100644
--- a/model.h
+++ b/model.h
@@ -113,6 +113,7 @@ public:
void remove_thread(Thread *t);
Thread * get_thread(thread_id_t tid) const;
Thread * get_thread(const ModelAction *act) const;
+ int get_promise_number(const Promise *promise) const;
bool is_enabled(Thread *t) const;
bool is_enabled(thread_id_t tid) const;
--
2.34.1