X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.h;h=6ae96be8d508d9b598ae3bb3c396760fea6047da;hp=394552ca879f7056b0002acfe1ee2e5e348580f0;hb=HEAD;hpb=5ea8e3d5d861ed363e5ac5f3b20b8181dd197efb

diff --git a/nodestack.h b/nodestack.h
index 394552c..6ae96be 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -5,7 +5,6 @@
 #ifndef __NODESTACK_H__
 #define __NODESTACK_H__
 
-#include <vector>
 #include <cstddef>
 #include <inttypes.h>
 
@@ -23,11 +22,18 @@ struct fairness_info {
 	bool priority;
 };
 
+/**
+ * @brief Types of read-from relations
+ *
+ * Our "may-read-from" set is composed of multiple types of reads, and we have
+ * to iterate through all of them in the backtracking search. This enumeration
+ * helps to identify which type of read-from we are currently observing.
+ */
 typedef enum {
-	READ_FROM_PAST,
-	READ_FROM_PROMISE,
-	READ_FROM_FUTURE,
-	READ_FROM_NONE,
+	READ_FROM_PAST, /**< @brief Read from a prior, existing store */
+	READ_FROM_PROMISE, /**< @brief Read from an existing promised future value */
+	READ_FROM_FUTURE, /**< @brief Read from a newly-asserted future value */
+	READ_FROM_NONE, /**< @brief A NULL state, which should not be reached */
 } read_from_type_t;
 
 #define YIELD_E 1
@@ -48,7 +54,8 @@ typedef enum {
  */
 class Node {
 public:
-	Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness);
+	Node(const struct model_params *params, ModelAction *act, Node *par,
+			int nthreads, Node *prevfairness);
 	~Node();
 	/* return true = thread choice has already been explored */
 	bool has_been_explored(thread_id_t tid) const;
@@ -113,6 +120,8 @@ public:
 	bool increment_relseq_break();
 	bool relseq_break_empty() const;
 
+	bool increment_behaviors();
+
 	void print() const;
 
 	MEMALLOC
@@ -126,9 +135,12 @@ private:
 	bool future_value_empty() const;
 	bool increment_future_value();
 	read_from_type_t read_from_status;
+	const struct model_params * get_params() const { return params; }
 
 	ModelAction * const action;
 
+	const struct model_params * const params;
+
 	/** @brief ATOMIC_UNINIT action which was created at this Node */
 	ModelAction *uninit_action;
 
@@ -178,11 +190,15 @@ class NodeStack {
 public:
 	NodeStack();
 	~NodeStack();
+
+	void register_engine(const ModelExecution *exec);
+
 	ModelAction * explore_action(ModelAction *act, enabled_type_t * is_enabled);
 	Node * get_head() const;
 	Node * get_next() const;
 	void reset_execution();
 	void pop_restofstack(int numAhead);
+	void full_reset();
 	int get_total_nodes() { return total_nodes; }
 
 	void print() const;
@@ -191,6 +207,11 @@ public:
 private:
 	node_list_t node_list;
 
+	const struct model_params * get_params() const;
+
+	/** @brief The model-checker execution object */
+	const ModelExecution *execution;
+
 	/**
 	 * @brief the index position of the current head Node
 	 *