X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.h;h=94bb58ee1e64d235e4daf0801ee6861491c6b292;hb=d70f6f259c9850e5fceb527e3a9541c440c0146b;hp=f6d3e4e36be07a0ffa0feec975181faacd283f4f;hpb=17a0e8e736bf745dffec039a5eacc404349e04e5;p=model-checker.git diff --git a/nodestack.h b/nodestack.h index f6d3e4e..94bb58e 100644 --- a/nodestack.h +++ b/nodestack.h @@ -56,7 +56,7 @@ struct fairness_info { */ class Node { public: - Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 2, Node *prevfairness = NULL); + Node(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; @@ -89,7 +89,7 @@ public: bool increment_read_from(); bool read_from_empty() const; int get_read_from_size() const; - const ModelAction * get_read_from_at(int i); + const ModelAction * get_read_from_at(int i) const; void set_promise(unsigned int i, bool is_rmw); bool get_promise(unsigned int i) const; @@ -114,9 +114,9 @@ public: private: void explore(thread_id_t tid); - ModelAction *action; - Node *parent; - int num_threads; + ModelAction * const action; + Node * const parent; + const int num_threads; std::vector< bool, ModelAlloc > explored_children; std::vector< bool, ModelAlloc > backtrack; std::vector< struct fairness_info, ModelAlloc< struct fairness_info> > fairness; @@ -171,7 +171,7 @@ private: * @brief the index position of the current head Node * * This index is relative to node_list. The index should point to the - * current head Node. + * current head Node. It is negative when the list is empty. */ int head_idx;