X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=action.h;h=61c7c4cb9f7b5c7ffc15d270792ad856cdfe80e8;hb=110c70c7f5a9b438ba04824e91a277e73e8334ef;hp=7c9146fdda694adfd97c7f932f75822e53a4303c;hpb=89bcfc74c2999b15984759e5b0eab4a9c46feaf3;p=model-checker.git diff --git a/action.h b/action.h index 7c9146f..61c7c4c 100644 --- a/action.h +++ b/action.h @@ -5,7 +5,6 @@ #ifndef __ACTION_H__ #define __ACTION_H__ -#include #include #include @@ -17,6 +16,10 @@ class ClockVector; class Thread; class Promise; +namespace std { + class mutex; +} + using std::memory_order; using std::memory_order_relaxed; using std::memory_order_acquire; @@ -82,8 +85,10 @@ public: uint64_t get_value() const { return value; } uint64_t get_reads_from_value() const; uint64_t get_write_value() const; + uint64_t get_return_value() const; const ModelAction * get_reads_from() const { return reads_from; } Promise * get_reads_from_promise() const { return reads_from_promise; } + std::mutex * get_mutex() const; Node * get_node() const; void set_node(Node *n) { node = n; } @@ -115,6 +120,7 @@ public: bool is_uninitialized() const; bool is_read() const; bool is_write() const; + bool is_yield() const; bool could_be_write() const; bool is_rmwr() const; bool is_rmwc() const;