X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=c97cbf1a05f905fb79087c21b91401548b5ecf2e;hb=87d6ae25425840ccad0ef6edef6e279967e83be6;hp=76b2affb02db0a59d93c5efc8bde0973241af74d;hpb=717ddd114a51764ac33d3d86d6eeb09c7c4aee1b;p=model-checker.git diff --git a/model.h b/model.h index 76b2aff..c97cbf1 100644 --- a/model.h +++ b/model.h @@ -101,7 +101,7 @@ public: void print_summary() const; #if SUPPORT_MOD_ORDER_DUMP - void dumpGraph(char *filename); + void dumpGraph(char *filename) const; #endif void add_thread(Thread *t); @@ -148,7 +148,7 @@ private: bool next_execution(); void set_current_action(ModelAction *act); - Thread * check_current_action(ModelAction *curr); + ModelAction * check_current_action(ModelAction *curr); bool initialize_curr_action(ModelAction **curr); bool process_read(ModelAction *curr, bool second_part_of_rmw); bool process_write(ModelAction *curr); @@ -165,6 +165,7 @@ private: ModelAction * get_last_conflict(ModelAction *act); void set_backtracking(ModelAction *act); Thread * get_next_thread(ModelAction *curr); + bool set_latest_backtrack(ModelAction *act); ModelAction * get_next_backtrack(); void reset_to_initial_state(); bool resolve_promises(ModelAction *curr);