nodestack: register ModelExecution class w/in NodeStack

[c11tester.git] / nodestack.h

diff --git a/nodestack.h b/nodestack.h
index 394552ca879f7056b0002acfe1ee2e5e348580f0..1a8bbbe9f371cc2bef422ec2218e96f989fb28a8 100644 (file)
--- 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
@@ -113,6 +119,8 @@ public:
        bool increment_relseq_break();
        bool relseq_break_empty() const;
 
+       bool increment_behaviors();
+
        void print() const;
 
        MEMALLOC
@@ -178,6 +186,9 @@ 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;
@@ -191,6 +202,9 @@ public:
 private:
        node_list_t node_list;
 
+       /** @brief The model-checker execution object */
+       const ModelExecution *execution;
+
        /**
         * @brief the index position of the current head Node
         *