X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=promise.h;h=e306e14a261aafe8d38b0753524cd194dfc730f0;hp=84d5aa49b3af7b8156ef4744e270f128c6a0cabf;hb=6014243b7130f34b7ffd1098da225b0b8de5c328;hpb=e79a7cd8e9c85d37a5d5c2a81ca14b1017b1b305 diff --git a/promise.h b/promise.h index 84d5aa4..e306e14 100644 --- a/promise.h +++ b/promise.h @@ -31,11 +31,13 @@ class Promise { bool eliminate_thread(thread_id_t tid); void add_thread(thread_id_t tid); bool thread_is_available(thread_id_t tid) const; + bool thread_was_available(thread_id_t tid) const; unsigned int max_available_thread_idx() const; bool has_failed() const; void set_write(const ModelAction *act) { write = act; } const ModelAction * get_write() const { return write; } int get_num_available_threads() const { return num_available_threads; } + int get_num_was_available_threads() const { return num_was_available_threads; } bool is_compatible(const ModelAction *act) const; bool is_compatible_exclusive(const ModelAction *act) const; bool same_value(const ModelAction *write) const; @@ -60,8 +62,10 @@ class Promise { /** @brief Thread ID(s) for thread(s) that potentially can satisfy this * promise */ SnapVector available_thread; + SnapVector was_available_thread; int num_available_threads; + int num_was_available_threads; const future_value fv;