nodestack: pass writer ModelAction to add_future_value()

[model-checker.git] / nodestack.h

diff --git a/nodestack.h b/nodestack.h
index 2dddf729b077c532f51e03e3be0fe8f60e1fccc5..d2e6491b2edec5891943351e9891b358f2b05594 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -43,7 +43,6 @@ struct fairness_info {
        bool priority;
 };
 
-
 /**
  * @brief A single node in a NodeStack
  *
@@ -77,9 +76,8 @@ public:
         * occurred previously in the stack. */
        Node * get_parent() const { return parent; }
 
-       bool add_future_value(uint64_t value, modelclock_t expiration);
-       uint64_t get_future_value() const;
-       modelclock_t get_future_value_expiration() const;
+       bool add_future_value(const ModelAction *writer, modelclock_t expiration);
+       struct future_value get_future_value() const;
        bool increment_future_value();
        bool future_value_empty() const;