action: print promise number, not just ?
authorBrian Norris <banorris@uci.edu>
Thu, 28 Feb 2013 19:17:42 +0000 (11:17 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 28 Feb 2013 19:19:53 +0000 (11:19 -0800)
action.cc
model.cc
model.h

index 1309024..81f447a 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());
        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) {
                        model_print("  Rf: ?  ");
        }
        if (cv) {
index 38d63a2..591d42a 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());
 }
 
        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
 /**
  * @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 (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;
        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;
 
        bool is_enabled(Thread *t) const;
        bool is_enabled(thread_id_t tid) const;