From ad660ce6ce8b50abe7a380f643a5e22fb2b282df Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 25 Jun 2012 13:24:50 -0700 Subject: [PATCH] add documentation --- model.cc | 1 + nodestack.h | 17 +++++++++++++++++ 2 files changed, 18 insertions(+) diff --git a/model.cc b/model.cc index 9be04b6..f12e4d2 100644 --- a/model.cc +++ b/model.cc @@ -205,6 +205,7 @@ void ModelChecker::set_backtracking(ModelAction *act) if (node->has_been_explored(t->get_id())) return; + /* Cache the latest backtracking point */ if (!next_backtrack || *prev > *next_backtrack) next_backtrack = prev; diff --git a/nodestack.h b/nodestack.h index 974f1a9..79ab19b 100644 --- a/nodestack.h +++ b/nodestack.h @@ -16,6 +16,15 @@ class ModelAction; typedef std::set< ModelAction *, std::less< ModelAction *>, MyAlloc< ModelAction * > > action_set_t; +/** + * @brief A single node in a NodeStack + * + * Represents a single node in the NodeStack. Each Node is associated with up + * to one action and up to one parent node. A node holds information + * regarding the last action performed (the "associated action"), the thread + * choices that have been explored (explored_children) and should be explored + * (backtrack), and the actions that the last action may read from. + */ class Node { public: Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1); @@ -57,6 +66,14 @@ private: typedef std::list > node_list_t; +/** + * @brief A stack of nodes + * + * Holds a Node linked-list that can be used for holding backtracking, + * may-read-from, and replay information. It is used primarily as a + * stack-like structure, in that backtracking points and replay nodes are + * only removed from the top (most recent). + */ class NodeStack { public: NodeStack(); -- 2.34.1