Fix snapshot code

[model-checker.git] / nodestack.h

diff --git a/nodestack.h b/nodestack.h
index e260f083c80a9455cabf4f0c23c3d30e0c9ccb1c..6ae96be8d508d9b598ae3bb3c396760fea6047da 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -54,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;
@@ -134,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;
 
@@ -186,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;
@@ -199,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
         *