X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.h;h=a857084ba1fe8676b0b2c5b8e57fc8a873a77bc0;hb=ab9a8cb068ff8fbc2f913c2c4be0fb4cede98743;hp=6200887a0e624c945fee33f09546ee87cd7109c1;hpb=ee296f053997ba5914f29334960dade61b1654e3;p=model-checker.git

diff --git a/nodestack.h b/nodestack.h
index 6200887..a857084 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -38,6 +38,12 @@ struct fairness_info {
 	bool priority;
 };
 
+typedef enum {
+	READ_FROM_PAST,
+	READ_FROM_FUTURE,
+	READ_FROM_NONE,
+} read_from_type_t;
+
 /**
  * @brief A single node in a NodeStack
  *
@@ -72,17 +78,19 @@ public:
 	 * occurred previously in the stack. */
 	Node * get_parent() const { return parent; }
 
-	bool add_future_value(struct future_value fv);
-	struct future_value get_future_value() const;
-	bool increment_future_value();
-	bool future_value_empty() const;
+	read_from_type_t get_read_from_status();
+	bool increment_read_from();
+	bool read_from_empty() const;
+	unsigned int read_from_size() const;
 
+	void print_read_from_past();
 	void add_read_from_past(const ModelAction *act);
 	const ModelAction * get_read_from_past() const;
-	bool increment_read_from_past();
-	bool read_from_past_empty() const;
-	int get_read_from_past_size() const;
 	const ModelAction * get_read_from_past(int i) const;
+	int get_read_from_past_size() const;
+
+	bool add_future_value(struct future_value fv);
+	struct future_value get_future_value() const;
 
 	void set_promise(unsigned int i, bool is_rmw);
 	bool get_promise(unsigned int i) const;
@@ -101,12 +109,17 @@ public:
 	bool relseq_break_empty() const;
 
 	void print() const;
-	void print_read_from_past();
 
 	MEMALLOC
 private:
 	void explore(thread_id_t tid);
 
+	bool read_from_past_empty() const;
+	bool increment_read_from_past();
+	bool future_value_empty() const;
+	bool increment_future_value();
+	read_from_type_t read_from_status;
+
 	ModelAction * const action;
 	Node * const parent;
 	const int num_threads;