fix bug from moving read_from check_recency...check_recency had the assumption that...

[model-checker.git] / model.h

diff --git a/model.h b/model.h
index fa11cb8cbbf5f0e5ed3f3ffa727b6ac9aea8ce66..4a1fcf49e2b64e732d52865bc0dc921031a61bf9 100644 (file)
--- a/model.h
+++ b/model.h
@@ -116,12 +116,13 @@ private:
        ModelAction * initialize_curr_action(ModelAction *curr);
        bool process_read(ModelAction *curr, bool second_part_of_rmw);
        bool process_write(ModelAction *curr);
-       void process_mutex(ModelAction *curr);
+       bool process_mutex(ModelAction *curr);
+       bool process_thread_action(ModelAction *curr);
        bool check_action_enabled(ModelAction *curr);
 
        bool take_step();
 
-       void check_recency(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);