X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/49e85177c669d793e84242983a1b1f430e47184e..ed9b07e5c0c7eb6d4d38b0fe5aaea80d6996a8a7:/include/simgrid/modelchecker.h diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 34d9124df0..0d41344468 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -6,6 +6,8 @@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ +#include + #include /* HAVE_MC ? */ #include #include "xbt/automaton.h" @@ -15,6 +17,8 @@ SG_BEGIN_DECL() +XBT_PUBLIC(int) MC_random(int min, int max); + #ifdef HAVE_MC extern int _sg_do_model_check; /* please don't use directly: we inline MC_is_active, but that's what you should use */ @@ -24,7 +28,6 @@ extern int _sg_mc_visited; #define MC_visited_reduction() _sg_mc_visited XBT_PUBLIC(void) MC_assert(int); -XBT_PUBLIC(int) MC_random(int min, int max); XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct); XBT_PUBLIC(void *) MC_snapshot(void); XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2); @@ -37,7 +40,6 @@ XBT_PUBLIC(void) MC_ignore(void *addr, size_t size); #define MC_visited_reduction() 0 #define MC_assert(a) xbt_assert(a) -#define MC_random(a, b) 0 #define MC_automaton_new_propositional_symbol(a, b) ((void)0) #define MC_snapshot() ((void*)0) #define MC_compare_snapshots(a, b) 0 @@ -46,6 +48,17 @@ XBT_PUBLIC(void) MC_ignore(void *addr, size_t size); #endif +/** Replay path (if any) in string representation + * + * This is a path as generated by `MC_record_stack_to_string()`. + */ +XBT_PUBLIC_DATA(char*) MC_record_path; + +/** Whether the replay mode is enabled */ +static inline bool MC_record_replay_is_active(void) { + return MC_record_path; +} + SG_END_DECL() #endif /* SIMGRID_MODELCHECKER_H */