action: print promise number, not just ?

diff --git a/action.cc b/action.cc
index 130902491a97f794f13e98b917bb84522e8b0f64..81f447a5b13f9d8e3db3e352e4be49f4659559b0 100644 (file)
--- 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 38d63a2fcb9f0a45f850fc1b7bf718d1579bd234..591d42a1ab3dbbc9aae2b8ea152e252c58379fd5 100644 (file)
--- 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 9e0b34ba18b25cf642a92dea56321763c23b48ba..e92137d1c17b6222f867cd27cfdc568625dd9bd2 100644 (file)
--- 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;