ClockVector * get_cv(thread_id_t tid) const;
ModelAction * get_parent_action(thread_id_t tid) const;
void check_promises_thread_disabled();
void mo_check_promises(thread_id_t tid, const ModelAction *write);
ClockVector * get_cv(thread_id_t tid) const;
ModelAction * get_parent_action(thread_id_t tid) const;
void check_promises_thread_disabled();
void mo_check_promises(thread_id_t tid, const ModelAction *write);
- bool sleep_can_read_from(ModelAction * curr, const ModelAction *write);
- bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
- bool mo_may_allow(const ModelAction * writer, const ModelAction *reader);
+ bool sleep_can_read_from(ModelAction *curr, const ModelAction *write);
+ bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader);
+ bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
bool has_asserted() const;
void set_assert();
void set_bad_synchronization();
bool promises_expired() const;
void execute_sleep_set();
bool has_asserted() const;
void set_assert();
void set_bad_synchronization();
bool promises_expired() const;
void execute_sleep_set();
bool read_from(ModelAction *act, const ModelAction *rf);
bool check_action_enabled(ModelAction *curr);
bool read_from(ModelAction *act, const ModelAction *rf);
bool check_action_enabled(ModelAction *curr);
void check_recency(ModelAction *curr, const ModelAction *rf);
ModelAction * get_last_conflict(ModelAction *act);
void set_backtracking(ModelAction *act);
Thread * get_next_thread(ModelAction *curr);
void check_recency(ModelAction *curr, const ModelAction *rf);
ModelAction * get_last_conflict(ModelAction *act);
void set_backtracking(ModelAction *act);
Thread * get_next_thread(ModelAction *curr);
ModelAction * get_next_backtrack();
void reset_to_initial_state();
bool resolve_promises(ModelAction *curr);
void compute_promises(ModelAction *curr);
void compute_relseq_breakwrites(ModelAction *curr);
ModelAction * get_next_backtrack();
void reset_to_initial_state();
bool resolve_promises(ModelAction *curr);
void compute_promises(ModelAction *curr);
void compute_relseq_breakwrites(ModelAction *curr);
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid) const;
ModelAction * get_last_fence_release(thread_id_t tid) const;
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid) const;
ModelAction * get_last_fence_release(thread_id_t tid) const;