- int switch_to_master(ModelAction *act);
- ClockVector * get_cv(thread_id_t tid);
- ModelAction * get_parent_action(thread_id_t tid);
- bool next_execution();
- bool isfeasible();
- bool isfeasibleotherthanRMW();
- bool isfinalfeasible();
- void mo_check_promises(thread_id_t tid, const ModelAction *write);
- void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv);
- void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
- void finish_execution();
- bool isfeasibleprefix();
- void set_assert() {asserted=true;}
-
- /** @brief Alert the model-checker that an incorrectly-ordered
- * synchronization was made */
- void set_bad_synchronization() { bad_synchronization = true; }
+ uint64_t switch_to_master(ModelAction *act);
+ 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(const ModelAction *act, bool is_read_check);
+ void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
+ bool isfeasibleprefix() const;
+
+ bool assert_bug(const char *msg);
+ void assert_user_bug(const char *msg);