+/**
+ * Get the total size of the may-read-from set, including both past and future
+ * values
+ * @return The size of may-read-from
+ */
+unsigned int Node::read_from_size() const
+{
+ return read_from_past.size() +
+ read_from_promises.size() +
+ future_values.size();
+}
+
+/******************************* end read from ********************************/
+
+/****************************** read from past ********************************/
+
+/** @brief Prints info about read_from_past set */
+void Node::print_read_from_past()
+{
+ for (unsigned int i = 0; i < read_from_past.size(); i++)
+ read_from_past[i]->print();
+}
+
+/**
+ * Add an action to the read_from_past set.
+ * @param act is the action to add
+ */
+void Node::add_read_from_past(const ModelAction *act)
+{
+ read_from_past.push_back(act);
+}
+
+/**
+ * Gets the next 'read_from_past' action from this Node. Only valid for a node
+ * where this->action is a 'read'.
+ * @return The first element in read_from_past
+ */
+const ModelAction * Node::get_read_from_past() const
+{
+ if (read_from_past_idx < read_from_past.size())
+ return read_from_past[read_from_past_idx];
+ else
+ return NULL;
+}
+
+const ModelAction * Node::get_read_from_past(int i) const
+{
+ return read_from_past[i];
+}
+
+int Node::get_read_from_past_size() const
+{
+ return read_from_past.size();
+}
+
+/**
+ * Checks whether the readsfrom set for this node is empty.
+ * @return true if the readsfrom set is empty.
+ */
+bool Node::read_from_past_empty() const
+{
+ return ((read_from_past_idx + 1) >= read_from_past.size());
+}
+
+/**
+ * Increments the index into the readsfrom set to explore the next item.
+ * @return Returns false if we have explored all items.
+ */
+bool Node::increment_read_from_past()
+{
+ DBG();
+ if (read_from_past_idx < read_from_past.size()) {
+ read_from_past_idx++;
+ return read_from_past_idx < read_from_past.size();
+ }
+ return false;
+}
+
+/************************** end read from past ********************************/
+
+/***************************** read_from_promises *****************************/
+
+/**
+ * Add an action to the read_from_promises set.
+ * @param reader The read which generated the Promise; we use the ModelAction
+ * instead of the Promise because the Promise does not last across executions
+ */
+void Node::add_read_from_promise(const ModelAction *reader)
+{
+ read_from_promises.push_back(reader);
+}
+
+/**
+ * Gets the next 'read-from-promise' from this Node. Only valid for a node
+ * where this->action is a 'read'.
+ * @return The current element in read_from_promises
+ */
+Promise * Node::get_read_from_promise() const
+{
+ ASSERT(read_from_promise_idx >= 0 && read_from_promise_idx < ((int)read_from_promises.size()));
+ return read_from_promises[read_from_promise_idx]->get_reads_from_promise();
+}
+
+/**
+ * Gets a particular 'read-from-promise' form this Node. Only vlaid for a node
+ * where this->action is a 'read'.
+ * @param i The index of the Promise to get
+ * @return The Promise at index i, if the Promise is still available; NULL
+ * otherwise
+ */
+Promise * Node::get_read_from_promise(int i) const
+{
+ return read_from_promises[i]->get_reads_from_promise();
+}
+
+/** @return The size of the read-from-promise set */
+int Node::get_read_from_promise_size() const
+{
+ return read_from_promises.size();
+}
+
+/**
+ * Checks whether the read_from_promises set for this node is empty.
+ * @return true if the read_from_promises set is empty.
+ */
+bool Node::read_from_promise_empty() const
+{
+ return ((read_from_promise_idx + 1) >= ((int)read_from_promises.size()));
+}
+
+/**
+ * Increments the index into the read_from_promises set to explore the next item.
+ * @return Returns false if we have explored all promises.
+ */
+bool Node::increment_read_from_promise()