- void check_recency(ModelAction *curr, bool already_added);
- ModelAction * get_last_conflict(ModelAction *act);
+ bool next_execution();
+ ModelAction * check_current_action(ModelAction *curr);
+ bool initialize_curr_action(ModelAction **curr);
+ bool process_read(ModelAction *curr);
+ bool process_write(ModelAction *curr);
+ bool process_fence(ModelAction *curr);
+ bool process_mutex(ModelAction *curr);
+ bool process_thread_action(ModelAction *curr);
+ void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue);
+ bool read_from(ModelAction *act, const ModelAction *rf);
+ bool check_action_enabled(ModelAction *curr);
+
+ Thread * take_step(ModelAction *curr);
+
+ template <typename T>
+ bool check_recency(ModelAction *curr, const T *rf) const;
+
+ template <typename T, typename U>
+ bool should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const;
+
+ ModelAction * get_last_fence_conflict(ModelAction *act) const;
+ ModelAction * get_last_conflict(ModelAction *act) const;