X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=action.h;h=d178976a2c8e0206128750b5eaddac1485a4b432;hb=af25bde59ce05189adee92825ecc03fbb83e675b;hp=2bf01dce092b71d1a0fa37bc82a29802036e9d1c;hpb=1ced3dc2f0a7640ec7f724c477ea87affc697ea9;p=model-checker.git diff --git a/action.h b/action.h index 2bf01dc..d178976 100644 --- a/action.h +++ b/action.h @@ -7,11 +7,13 @@ #include #include +#include -#include "threads.h" #include "mymemory.h" -#include "clockvector.h" #include "memoryorder.h" +#include "modeltypes.h" + +class ClockVector; using std::memory_order; using std::memory_order_relaxed; @@ -64,7 +66,7 @@ class ModelAction { public: ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE); ~ModelAction(); - void print(bool print_cv = true) const; + void print() const; thread_id_t get_tid() const { return tid; } action_type get_type() const { return type; } @@ -78,6 +80,7 @@ public: void set_node(Node *n) { node = n; } void copy_from_new(ModelAction *newaction); + void set_seq_number(modelclock_t num); void set_try_lock(bool obtainedlock); bool is_mutex_op() const; bool is_lock() const; @@ -102,7 +105,7 @@ public: void create_cv(const ModelAction *parent = NULL); ClockVector * get_cv() const { return cv; } - void read_from(const ModelAction *act); + bool read_from(const ModelAction *act); bool synchronize_with(const ModelAction *act); bool has_synchronized_with(const ModelAction *act) const;