namespace simgrid {
namespace mc {
+static void MC_show_non_termination(void)
+{
+ XBT_INFO("******************************************");
+ XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
+ XBT_INFO("******************************************");
+ XBT_INFO("Counter-example execution trace:");
+ MC_dump_stack_safety(mc_stack);
+ MC_print_statistics(mc_stats);
+}
+
static int is_exploration_stack_state(mc_state_t current_state){
xbt_fifo_item_t item;
MC_print_statistics(mc_stats);
}
-void MC_show_non_termination(void){
- XBT_INFO("******************************************");
- XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
- XBT_INFO("******************************************");
- XBT_INFO("Counter-example execution trace:");
- MC_dump_stack_safety(mc_stack);
- MC_print_statistics(mc_stats);
-}
-
void MC_print_statistics(mc_stats_t stats)
{
if(_sg_mc_comms_determinism) {
XBT_PRIVATE void MC_show_deadlock(void);
XBT_PRIVATE void MC_show_stack_safety(xbt_fifo_t stack);
XBT_PRIVATE void MC_dump_stack_safety(xbt_fifo_t stack);
-XBT_PRIVATE void MC_show_non_termination(void);
/** Stack (of `mc_state_t`) representing the current position of the
* the MC in the exploration graph