};
#define MC_SET_RAW_MEM mmalloc_set_current_heap(raw_heap)
-#define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap)
+#define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap)
+
+int raw_mem_set;
/******************************* MEMORY MAPPINGS ***************************/
/* These functions and data structures implements a binary interface for */
/********************************** DPOR for safety **************************************/
+typedef enum {
+ e_mc_reduce_unset,
+ e_mc_reduce_none,
+ e_mc_reduce_dpor
+} e_mc_reduce_t;
+extern e_mc_reduce_t mc_reduce_kind;
void MC_dpor_init(void);
void MC_dpor(void);
/********************************** Double-DFS for liveness property**************************************/
extern mc_snapshot_t initial_snapshot_liveness;
-extern xbt_automaton_t automaton;
+extern xbt_automaton_t _mc_property_automaton;
typedef struct s_mc_pair{
mc_snapshot_t system_state;
void MC_pair_stateless_delete(mc_pair_stateless_t pair);
/********************************** Configuration of MC **************************************/
-
-extern int _surf_do_mc_checkpoint;
extern xbt_fifo_t mc_stack_safety;
+extern int _surf_mc_checkpoint;
+extern char* _surf_mc_property_file;
+
#endif