X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=clockvector.h;h=739a336e1adc6c81178686c10da60d411cd903b8;hb=b13a6b0ff467444f01b5dfa3277f3f9515ede0f5;hp=d233cdd136c46f7e00c547f9ac1d4be95d62cdee;hpb=f3ef22bef8d339c7d45b7d7232cdcf183a0b7776;p=model-checker.git diff --git a/clockvector.h b/clockvector.h index d233cdd..739a336 100644 --- a/clockvector.h +++ b/clockvector.h @@ -8,6 +8,7 @@ #include "threads.h" #include "mymemory.h" +typedef unsigned int modelclock_t; /* Forward declaration */ class ModelAction; @@ -15,14 +16,19 @@ class ClockVector { public: ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL); ~ClockVector(); - void merge(ClockVector *cv); - bool synchronized_since(ModelAction *act); + void merge(const ClockVector *cv); + bool synchronized_since(const ModelAction *act) const; + bool has_synchronized_with(const ClockVector *cv) const; - void print(); + void print() const; + modelclock_t getClock(thread_id_t thread); - MEMALLOC + SNAPSHOTALLOC private: - int *clock; + /** @brief Holds the actual clock data, as an array. */ + modelclock_t *clock; + + /** @brief The number of threads recorded in clock (i.e., its length). */ int num_threads; };