src/mc/LivenessChecker.cpp

   1 /* Copyright (c) 2011-2015. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include <cstring>
   8
   9 #include <algorithm>
  10 #include <memory>
  11 #include <list>
  12
  13 #include <unistd.h>
  14 #include <sys/wait.h>
  15
  16 #include <xbt/automaton.h>
  17 #include <xbt/dynar.h>
  18 #include <xbt/dynar.hpp>
  19 #include <xbt/log.h>
  20 #include <xbt/sysdep.h>
  21
  22 #include "src/mc/mc_request.h"
  23 #include "src/mc/LivenessChecker.hpp"
  24 #include "src/mc/mc_private.h"
  25 #include "src/mc/mc_record.h"
  26 #include "src/mc/mc_smx.h"
  27 #include "src/mc/Client.hpp"
  28 #include "src/mc/mc_private.h"
  29 #include "src/mc/mc_replay.h"
  30 #include "src/mc/mc_safety.h"
  31 #include "src/mc/mc_exit.h"
  32
  33 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  34                                 "Logging specific to algorithms for liveness properties verification");
  35
  36 /********* Global variables *********/
  37
  38 /********* Static functions *********/
  39
  40 namespace simgrid {
  41 namespace mc {
  42
  43 std::list<VisitedPair*> LivenessChecker::acceptance_pairs;
  44 std::list<Pair*> LivenessChecker::liveness_stack;
  45
  46 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, simgrid::mc::State* graph_state)
  47 {
  48   simgrid::mc::Process* process = &(mc_model_checker->process());
  49
  50   this->graph_state = graph_state;
  51   if(this->graph_state->system_state == nullptr)
  52     this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
  53   this->heap_bytes_used = mmalloc_get_bytes_used_remote(
  54     process->get_heap()->heaplimit,
  55     process->get_malloc_info());
  56
  57   this->nb_processes =
  58     mc_model_checker->process().simix_processes().size();
  59
  60   this->automaton_state = automaton_state;
  61   this->num = pair_num;
  62   this->other_num = -1;
  63   this->acceptance_removed = 0;
  64   this->visited_removed = 0;
  65   this->acceptance_pair = 0;
  66   this->atomic_propositions = simgrid::xbt::unique_ptr<s_xbt_dynar_t>(
  67     xbt_dynar_new(sizeof(int), nullptr));
  68
  69   unsigned int cursor = 0;
  70   int value;
  71   xbt_dynar_foreach(atomic_propositions, cursor, value)
  72       xbt_dynar_push_as(this->atomic_propositions.get(), int, value);
  73 }
  74
  75 static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair)
  76 {
  77   for (auto i = LivenessChecker::liveness_stack.rbegin(); i != LivenessChecker::liveness_stack.rend(); ++i) {
  78     if ((*i)->num == pair->num) {
  79       (*i)->visited_pair_removed = 1;
  80       return true;
  81     }
  82   }
  83   return false;
  84 }
  85
  86 VisitedPair::~VisitedPair()
  87 {
  88   if( !is_exploration_stack_pair(this))
  89     MC_state_delete(this->graph_state, 1);
  90 }
  91
  92 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
  93                                        xbt_dynar_t atomic_propositions_values)
  94 {
  95
  96   switch (l->type) {
  97   case 0:{
  98       int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
  99       int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
 100       return (left_res || right_res);
 101     }
 102   case 1:{
 103       int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
 104       int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
 105       return (left_res && right_res);
 106     }
 107   case 2:{
 108       int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
 109       return (!res);
 110     }
 111   case 3:{
 112       unsigned int cursor = 0;
 113       xbt_automaton_propositional_symbol_t p = nullptr;
 114       xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
 115         if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
 116           return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, int);
 117       }
 118       return -1;
 119     }
 120   case 4:
 121     return 2;
 122   default:
 123     return -1;
 124   }
 125 }
 126
 127 static xbt_dynar_t visited_pairs;
 128
 129 Pair::Pair() : num(++mc_stats->expanded_pairs),
 130   visited_pair_removed(_sg_mc_visited > 0 ? 0 : 1)
 131 {}
 132
 133 Pair::~Pair() {
 134   if (this->visited_pair_removed)
 135     MC_state_delete(this->graph_state, 1);
 136 }
 137
 138 simgrid::xbt::unique_ptr<s_xbt_dynar_t> LivenessChecker::getPropositionValues()
 139 {
 140   unsigned int cursor = 0;
 141   xbt_automaton_propositional_symbol_t ps = nullptr;
 142   simgrid::xbt::unique_ptr<s_xbt_dynar_t> values = simgrid::xbt::unique_ptr<s_xbt_dynar_t>(xbt_dynar_new(sizeof(int), nullptr));
 143   xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, ps) {
 144     int res = xbt_automaton_propositional_symbol_evaluate(ps);
 145     xbt_dynar_push_as(values.get(), int, res);
 146   }
 147   return values;
 148 }
 149
 150 int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
 151 {
 152   simgrid::mc::Snapshot* s1 = state1->graph_state->system_state.get();
 153   simgrid::mc::Snapshot* s2 = state2->graph_state->system_state.get();
 154   int num1 = state1->num;
 155   int num2 = state2->num;
 156   return simgrid::mc::snapshot_compare(num1, s1, num2, s2);
 157 }
 158
 159 simgrid::mc::VisitedPair* LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair)
 160 {
 161   auto new_pair =
 162     std::unique_ptr<simgrid::mc::VisitedPair>(new VisitedPair(
 163       pair->num, pair->automaton_state, pair->atomic_propositions.get(),
 164       pair->graph_state));
 165   new_pair->acceptance_pair = 1;
 166
 167   auto res = std::equal_range(acceptance_pairs.begin(), acceptance_pairs.end(),
 168     new_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 169
 170   if (pair->search_cycle == 1)
 171     for (auto i = res.first; i != res.second; ++i) {
 172       simgrid::mc::VisitedPair* pair_test = *i;
 173       if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
 174         if (xbt_automaton_propositional_symbols_compare_value(
 175             pair_test->atomic_propositions.get(),
 176             new_pair->atomic_propositions.get()) == 0) {
 177           if (this->compare(pair_test, new_pair.get()) == 0) {
 178             XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
 179             liveness_stack.pop_back();
 180             if (dot_output != nullptr)
 181               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
 182             return nullptr;
 183           }
 184         }
 185       }
 186     }
 187
 188   auto new_raw_pair = new_pair.release();
 189   acceptance_pairs.insert(res.first, new_raw_pair);
 190   return new_raw_pair;
 191 }
 192
 193 void LivenessChecker::removeAcceptancePair(int pair_num)
 194 {
 195   for (auto i = acceptance_pairs.begin(); i != acceptance_pairs.end(); ++i)
 196     if ((*i)->num == pair_num) {
 197       acceptance_pairs.erase(i);
 198       (*i)->acceptance_removed = 1;
 199       if (_sg_mc_visited == 0 || (*i)->visited_removed == 1)
 200         delete *i;
 201       break;
 202     }
 203 }
 204
 205 void LivenessChecker::prepare(void)
 206 {
 207   simgrid::mc::Pair* initial_pair = nullptr;
 208   mc_model_checker->wait_for_requests();
 209   acceptance_pairs.clear();
 210   if(_sg_mc_visited > 0)
 211     simgrid::mc::visited_pairs = xbt_dynar_new(sizeof(simgrid::mc::VisitedPair*), nullptr);
 212
 213   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 214   initial_global_state->prev_pair = 0;
 215
 216   unsigned int cursor = 0;
 217   xbt_automaton_state_t automaton_state;
 218
 219   xbt_dynar_foreach(simgrid::mc::property_automaton->states, cursor, automaton_state) {
 220     if (automaton_state->type == -1) {  /* Initial automaton state */
 221
 222       initial_pair = new Pair();
 223       initial_pair->automaton_state = automaton_state;
 224       initial_pair->graph_state = MC_state_new();
 225       initial_pair->atomic_propositions = this->getPropositionValues();
 226       initial_pair->depth = 1;
 227
 228       /* Get enabled processes and insert them in the interleave set of the graph_state */
 229       for (auto& p : mc_model_checker->process().simix_processes())
 230         if (simgrid::mc::process_is_enabled(&p.copy))
 231           MC_state_interleave_process(initial_pair->graph_state, &p.copy);
 232
 233       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
 234       initial_pair->search_cycle = 0;
 235
 236       liveness_stack.push_back(initial_pair);
 237     }
 238   }
 239 }
 240
 241
 242 void LivenessChecker::replay()
 243 {
 244   simgrid::mc::State* state = nullptr;
 245   smx_simcall_t req = nullptr, saved_req = NULL;
 246   int value, depth = 1;
 247   char *req_str;
 248
 249   XBT_DEBUG("**** Begin Replay ****");
 250
 251   /* Intermediate backtracking */
 252   if(_sg_mc_checkpoint > 0) {
 253     simgrid::mc::Pair* pair = liveness_stack.back();
 254     if(pair->graph_state->system_state){
 255       simgrid::mc::restore_snapshot(pair->graph_state->system_state);
 256       return;
 257     }
 258   }
 259
 260   /* Restore the initial state */
 261   simgrid::mc::restore_snapshot(initial_global_state->snapshot);
 262
 263   /* Traverse the stack from the initial state and re-execute the transitions */
 264   for (simgrid::mc::Pair* pair : liveness_stack) {
 265     if (pair == liveness_stack.back())
 266       break;
 267
 268       state = (simgrid::mc::State*) pair->graph_state;
 269
 270       if (pair->exploration_started) {
 271
 272         saved_req = MC_state_get_executed_request(state, &value);
 273
 274         if (saved_req != nullptr) {
 275           /* because we got a copy of the executed request, we have to fetch the
 276              real one, pointed by the request field of the issuer process */
 277           const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
 278           req = &issuer->simcall;
 279
 280           /* Debug information */
 281           if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
 282             req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
 283             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
 284             xbt_free(req_str);
 285           }
 286
 287         }
 288
 289         simgrid::mc::handle_simcall(req, value);
 290         mc_model_checker->wait_for_requests();
 291       }
 292
 293       /* Update statistics */
 294       mc_stats->visited_pairs++;
 295       mc_stats->executed_transitions++;
 296
 297       depth++;
 298
 299   }
 300
 301   XBT_DEBUG("**** End Replay ****");
 302 }
 303
 304 /**
 305  * \brief Checks whether a given pair has already been visited by the algorithm.
 306  */
 307 int LivenessChecker::insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair)
 308 {
 309   if (_sg_mc_visited == 0)
 310     return -1;
 311
 312   simgrid::mc::VisitedPair* new_visited_pair = nullptr;
 313   if (visited_pair == nullptr)
 314     new_visited_pair = new simgrid::mc::VisitedPair(
 315       pair->num, pair->automaton_state, pair->atomic_propositions.get(),
 316       pair->graph_state);
 317   else
 318     new_visited_pair = visited_pair;
 319
 320   auto visited_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(simgrid::mc::visited_pairs);
 321
 322   auto range = std::equal_range(visited_pairs.begin(), visited_pairs.end(),
 323     new_visited_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 324
 325   for (auto i = range.first; i != range.second; ++i) {
 326     simgrid::mc::VisitedPair* pair_test = *i;
 327     std::size_t cursor = i - visited_pairs.begin();
 328     if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
 329       if (xbt_automaton_propositional_symbols_compare_value(
 330           pair_test->atomic_propositions.get(),
 331           new_visited_pair->atomic_propositions.get()) == 0) {
 332         if (this->compare(pair_test, new_visited_pair) == 0) {
 333           if (pair_test->other_num == -1)
 334             new_visited_pair->other_num = pair_test->num;
 335           else
 336             new_visited_pair->other_num = pair_test->other_num;
 337           if (dot_output == nullptr)
 338             XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
 339           else
 340             XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
 341           xbt_dynar_remove_at(simgrid::mc::visited_pairs, cursor, &pair_test);
 342           xbt_dynar_insert_at(simgrid::mc::visited_pairs, cursor, &new_visited_pair);
 343           pair_test->visited_removed = 1;
 344           if (!pair_test->acceptance_pair
 345               || pair_test->acceptance_removed == 1)
 346             delete pair_test;
 347           return new_visited_pair->other_num;
 348         }
 349       }
 350     }
 351   }
 352
 353   xbt_dynar_insert_at(simgrid::mc::visited_pairs, range.first - visited_pairs.begin(), &new_visited_pair);
 354
 355   if ((ssize_t) visited_pairs.size() > _sg_mc_visited) {
 356     int min2 = mc_stats->expanded_pairs;
 357     unsigned int index2 = 0;
 358     for (std::size_t i = 0; i != (std::size_t) visited_pairs.size(); ++i) {
 359       simgrid::mc::VisitedPair* pair_test = visited_pairs[i];
 360       if (pair_test->num < min2) {
 361         index2 = i;
 362         min2 = pair_test->num;
 363       }
 364     }
 365     simgrid::mc::VisitedPair* pair_test = nullptr;
 366     xbt_dynar_remove_at(simgrid::mc::visited_pairs, index2, &pair_test);
 367     pair_test->visited_removed = 1;
 368     if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
 369       delete pair_test;
 370   }
 371
 372   return -1;
 373 }
 374
 375 LivenessChecker::LivenessChecker(Session& session) : Checker(session)
 376 {
 377 }
 378
 379 LivenessChecker::~LivenessChecker()
 380 {
 381 }
 382
 383 RecordTrace LivenessChecker::getRecordTrace() // override
 384 {
 385   RecordTrace res;
 386   for (simgrid::mc::Pair* pair : liveness_stack) {
 387     int value;
 388     smx_simcall_t req = MC_state_get_executed_request(pair->graph_state, &value);
 389     if (req && req->call != SIMCALL_NONE) {
 390       smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 391       const int pid = issuer->pid;
 392
 393       // Serialization the (pid, value) pair:
 394       res.push_back(RecordTraceElement(pid, value));
 395     }
 396   }
 397   return res;
 398 }
 399
 400 void LivenessChecker::showAcceptanceCycle(std::size_t depth)
 401 {
 402   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 403   XBT_INFO("|             ACCEPTANCE CYCLE            |");
 404   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 405   XBT_INFO("Counter-example that violates formula :");
 406   simgrid::mc::dumpRecordPath();
 407   for (auto& s : this->getTextualTrace())
 408     XBT_INFO("%s", s.c_str());
 409   MC_print_statistics(mc_stats);
 410   XBT_INFO("Counter-example depth : %zd", depth);
 411 }
 412
 413 std::vector<std::string> LivenessChecker::getTextualTrace() // override
 414 {
 415   std::vector<std::string> trace;
 416   for (simgrid::mc::Pair* pair : liveness_stack) {
 417     int value;
 418     smx_simcall_t req = MC_state_get_executed_request(pair->graph_state, &value);
 419     if (req && req->call != SIMCALL_NONE) {
 420       char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::executed);
 421       trace.push_back(std::string(req_str));
 422       xbt_free(req_str);
 423     }
 424   }
 425   return trace;
 426 }
 427
 428 int LivenessChecker::main(void)
 429 {
 430   simgrid::mc::Pair* current_pair = nullptr;
 431   int value, res, visited_num = -1;
 432   smx_simcall_t req = nullptr;
 433   xbt_automaton_transition_t transition_succ = nullptr;
 434   int cursor = 0;
 435   simgrid::mc::Pair* next_pair = nullptr;
 436   simgrid::xbt::unique_ptr<s_xbt_dynar_t> prop_values;
 437   simgrid::mc::VisitedPair* reached_pair = nullptr;
 438
 439   while (!liveness_stack.empty()){
 440
 441     /* Get current pair */
 442     current_pair = liveness_stack.back();
 443
 444     /* Update current state in buchi automaton */
 445     simgrid::mc::property_automaton->current_state = current_pair->automaton_state;
 446
 447     XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size = %d, pair_num = %d, requests = %d)",
 448        current_pair->depth, current_pair->search_cycle,
 449        MC_state_interleave_size(current_pair->graph_state), current_pair->num,
 450        current_pair->requests);
 451
 452     if (current_pair->requests > 0) {
 453
 454       if (current_pair->automaton_state->type == 1 && current_pair->exploration_started == 0) {
 455         /* If new acceptance pair, return new pair */
 456         if ((reached_pair = this->insertAcceptancePair(current_pair)) == nullptr) {
 457           this->showAcceptanceCycle(current_pair->depth);
 458           return SIMGRID_MC_EXIT_LIVENESS;
 459         }
 460       }
 461
 462       /* Pair already visited ? stop the exploration on the current path */
 463       if ((current_pair->exploration_started == 0)
 464         && (visited_num = this->insertVisitedPair(
 465           reached_pair, current_pair)) != -1) {
 466
 467         if (dot_output != nullptr){
 468           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, visited_num, initial_global_state->prev_req);
 469           fflush(dot_output);
 470         }
 471
 472         XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
 473         current_pair->requests = 0;
 474         goto backtracking;
 475
 476       }else{
 477
 478         req = MC_state_get_request(current_pair->graph_state, &value);
 479
 480          if (dot_output != nullptr) {
 481            if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
 482              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, current_pair->num, initial_global_state->prev_req);
 483              xbt_free(initial_global_state->prev_req);
 484            }
 485            initial_global_state->prev_pair = current_pair->num;
 486            initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, value);
 487            if (current_pair->search_cycle)
 488              fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
 489            fflush(dot_output);
 490          }
 491
 492          char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
 493          XBT_DEBUG("Execute: %s", req_str);
 494          xbt_free(req_str);
 495
 496          /* Set request as executed */
 497          MC_state_set_executed_request(current_pair->graph_state, req, value);
 498
 499          /* Update mc_stats */
 500          mc_stats->executed_transitions++;
 501          if(current_pair->exploration_started == 0)
 502            mc_stats->visited_pairs++;
 503
 504          /* Answer the request */
 505          simgrid::mc::handle_simcall(req, value);
 506
 507          /* Wait for requests (schedules processes) */
 508          mc_model_checker->wait_for_requests();
 509
 510          current_pair->requests--;
 511          current_pair->exploration_started = 1;
 512
 513          /* Get values of atomic propositions (variables used in the property formula) */
 514          prop_values = this->getPropositionValues();
 515
 516          /* Evaluate enabled/true transitions in automaton according to atomic propositions values and create new pairs */
 517          cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
 518          while (cursor >= 0) {
 519            transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
 520            res = MC_automaton_evaluate_label(transition_succ->label, prop_values.get());
 521            if (res == 1 || res == 2) { /* 1 = True transition (always enabled), 2 = enabled transition according to atomic prop values */
 522               next_pair = new Pair();
 523               next_pair->graph_state = MC_state_new();
 524               next_pair->automaton_state = transition_succ->dst;
 525               next_pair->atomic_propositions = this->getPropositionValues();
 526               next_pair->depth = current_pair->depth + 1;
 527               /* Get enabled processes and insert them in the interleave set of the next graph_state */
 528               for (auto& p : mc_model_checker->process().simix_processes())
 529                 if (simgrid::mc::process_is_enabled(&p.copy))
 530                   MC_state_interleave_process(next_pair->graph_state, &p.copy);
 531
 532               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
 533
 534               /* FIXME : get search_cycle value for each acceptant state */
 535               if (next_pair->automaton_state->type == 1 || current_pair->search_cycle)
 536                 next_pair->search_cycle = 1;
 537
 538               /* Add new pair to the exploration stack */
 539               liveness_stack.push_back(next_pair);
 540
 541            }
 542            cursor--;
 543          }
 544
 545       } /* End of visited_pair test */
 546
 547     } else {
 548
 549     backtracking:
 550       if(visited_num == -1)
 551         XBT_DEBUG("No more request to execute. Looking for backtracking point.");
 552
 553       prop_values.reset();
 554
 555       /* Traverse the stack backwards until a pair with a non empty interleave
 556          set is found, deleting all the pairs that have it empty in the way. */
 557       while (!liveness_stack.empty()) {
 558         current_pair = liveness_stack.back();
 559         liveness_stack.pop_back();
 560         if (current_pair->requests > 0) {
 561           /* We found a backtracking point */
 562           XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
 563           liveness_stack.push_back(current_pair);
 564           this->replay();
 565           XBT_DEBUG("Backtracking done");
 566           break;
 567         }else{
 568           /* Delete pair */
 569           XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth);
 570           if (current_pair->automaton_state->type == 1)
 571             this->removeAcceptancePair(current_pair->num);
 572           delete current_pair;
 573         }
 574       }
 575
 576     } /* End of if (current_pair->requests > 0) else ... */
 577
 578   }
 579
 580   XBT_INFO("No property violation found.");
 581   MC_print_statistics(mc_stats);
 582   return SIMGRID_MC_EXIT_SUCCESS;
 583 }
 584
 585 int LivenessChecker::run()
 586 {
 587   XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
 588   MC_automaton_load(_sg_mc_property_file);
 589   mc_model_checker->wait_for_requests();
 590
 591   XBT_DEBUG("Starting the liveness algorithm");
 592   _sg_mc_liveness = 1;
 593
 594   /* Create exploration stack */
 595   liveness_stack.clear();
 596
 597   /* Create the initial state */
 598   simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 599
 600   this->prepare();
 601   int res = this->main();
 602   simgrid::mc::initial_global_state = nullptr;
 603   return res;
 604 }
 605
 606 }
 607 }