nodestack: eliminate get_future_value_expiration()

[model-checker.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index ec72def002838b97429d3a27a99e0fd3825aecc0..708ec3d0f5fa3da43a563228ef53c4b6e72475dd 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -1,3 +1,6 @@
+#define __STDC_FORMAT_MACROS
+#include <inttypes.h>
+
 #include <string.h>
 
 #include "nodestack.h"
@@ -89,13 +92,21 @@ Node::~Node()
 void Node::print()
 {
        action->print();
-       model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty");
+       model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
        for (int i = 0; i < (int)backtrack.size(); i++)
                if (backtrack[i] == true)
                        model_print("[%d]", i);
        model_print("\n");
-       model_print("          future values: %s\n", future_value_empty() ? "empty" : "non-empty");
-       model_print("          read-from: %s\n", read_from_empty() ? "empty" : "non-empty");
+       model_print("          future values: %s", future_value_empty() ? "empty" : "non-empty ");
+       for (int i = future_index + 1; i < (int)future_values.size(); i++)
+               model_print("[%#" PRIx64 "]", future_values[i].value);
+       model_print("\n");
+
+       model_print("          read-from: %s", read_from_empty() ? "empty" : "non-empty ");
+       for (int i = read_from_index + 1; i < (int)may_read_from.size(); i++)
+               model_print("[%d]", may_read_from[i]->get_seq_number());
+       model_print("\n");
+
        model_print("          promises: %s\n", promise_empty() ? "empty" : "non-empty");
        model_print("          misc: %s\n", misc_empty() ? "empty" : "non-empty");
        model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
@@ -184,7 +195,6 @@ bool Node::promise_empty() const
        return true;
 }
 
-
 void Node::set_misc_max(int i)
 {
        misc_max = i;
@@ -205,7 +215,6 @@ bool Node::misc_empty() const
        return (misc_index + 1) >= misc_max;
 }
 
-
 /**
  * Adds a value from a weakly ordered future write to backtrack to. This
  * operation may "fail" if the future value has already been run (within some
@@ -372,23 +381,16 @@ void Node::add_read_from(const ModelAction *act)
 }
 
 /**
- * Gets the next 'future_value' value from this Node. Only valid for a node
- * where this->action is a 'read'.
+ * Gets the next 'future_value' from this Node. Only valid for a node where
+ * this->action is a 'read'.
  * @return The first element in future_values
  */
-uint64_t Node::get_future_value() const
-{
-       ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-       return future_values[future_index].value;
-}
-
-modelclock_t Node::get_future_value_expiration() const
+struct future_value Node::get_future_value() const
 {
        ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-       return future_values[future_index].expiration;
+       return future_values[future_index];
 }
 
-
 int Node::get_read_from_size() const
 {
        return may_read_from.size();