-std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions)
-{
- std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(++expandedPairsCount_);
- next_pair->automaton_state = state;
- next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
- next_pair->atomic_propositions = std::move(propositions);
- if (current_pair)
- next_pair->depth = current_pair->depth + 1;
- else
- next_pair->depth = 1;
- /* Get enabled actors and insert them in the interleave set of the next graph_state */
- for (auto& actor : mc_model_checker->process().actors())
- if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
- next_pair->graph_state->interleave(actor.copy.getBuffer());
- next_pair->requests = next_pair->graph_state->interleaveSize();
- /* FIXME : get search_cycle value for each accepting state */
- if (next_pair->automaton_state->type == 1 ||
- (current_pair && current_pair->search_cycle))
- next_pair->search_cycle = true;
- else
- next_pair->search_cycle = false;
- return next_pair;
-}
-
-void LivenessChecker::backtrack()
-{
- /* Traverse the stack backwards until a pair with a non empty interleave
- set is found, deleting all the pairs that have it empty in the way. */
- while (!explorationStack_.empty()) {
- std::shared_ptr<simgrid::mc::Pair> current_pair = explorationStack_.back();
- explorationStack_.pop_back();
- if (current_pair->requests > 0) {
- /* We found a backtracking point */
- XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
- explorationStack_.push_back(std::move(current_pair));
- this->replay();
- XBT_DEBUG("Backtracking done");
- break;
- } else {
- XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth);
- if (current_pair->automaton_state->type == 1)
- this->removeAcceptancePair(current_pair->num);
- }
- }
-}
-
-void LivenessChecker::run()
-{
- XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
- MC_automaton_load(_sg_mc_property_file);
-
- XBT_DEBUG("Starting the liveness algorithm");
- simgrid::mc::session->initialize();
- this->prepare();
-
- this->main();
-}
-