+ HashTable<const char *, FuncInst *, uintptr_t, 4, model_malloc, model_calloc, model_free> func_inst_map;
+
+ /* List of all atomic actions in this function */
+ func_inst_list_mt inst_list;
+
+ /* Possible entry atomic actions in this function */
+ func_inst_list_mt entry_insts;
+
+ /* Map a FuncInst to the its predicate when updating predicate trees */
+ ModelVector< ModelVector<inst_pred_map_t *> * > thrd_inst_pred_maps;
+
+ /* Number FuncInsts to detect loops when updating predicate trees */
+ ModelVector< ModelVector<inst_id_map_t *> *> thrd_inst_id_maps;
+
+ /* Detect read actions at the same locations when updating predicate trees */
+ ModelVector< ModelVector<loc_inst_map_t *> *> thrd_loc_inst_maps;
+
+ void init_local_maps(thread_id_t tid);
+ void reset_local_maps(thread_id_t tid);
+
+ void update_inst_tree(func_inst_list_t * inst_list);
+ void update_predicate_tree(ModelAction * act);
+ bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, Predicate ** unset_predicate);
+
+ void infer_predicates(FuncInst * next_inst, ModelAction * next_act, SnapVector<struct half_pred_expr *> * half_pred_expressions);
+ void generate_predicates(Predicate * curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
+ bool amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act);
+
+ /* Set of locations read by this FuncNode */
+ loc_set_t * read_locations;
+
+ /* Set of locations written to by this FuncNode */
+ loc_set_t * write_locations;