+ ++expanded_pairs_count_;
+ ++expanded_states_count_;
+ auto next_pair = std::make_shared<Pair>(expanded_pairs_count_);
+ next_pair->automaton_state = state;
+ next_pair->graph_state = std::make_shared<State>(expanded_states_count_);
+ 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 */
+ if (mc::actor_is_enabled(actor.copy.get_buffer()))
+ auto actors = mcapi::get().get_actors();
+ for (auto& actor : actors)
+ next_pair->graph_state->add_interleaving_set(actor.copy.get_buffer());
+ next_pair->requests = next_pair->graph_state->interleave_size();
+ /* 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 (not exploration_stack_.empty()) {
+ std::shared_ptr<simgrid::mc::Pair> current_pair = exploration_stack_.back();
+ exploration_stack_.pop_back();
+ if (current_pair->requests > 0) {
+ /* We found a backtracking point */
+ XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
+ exploration_stack_.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->remove_acceptance_pair(current_pair->num);
+ }
+ }
+}
+
+void LivenessChecker::run()
+{
+ XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str());
+ mcapi::get().automaton_load(_sg_mc_property_file.get().c_str());
+
+ XBT_DEBUG("Starting the liveness algorithm");
+ mcapi::get().session_initialize();
+
+ /* Initialize */
+ this->previous_pair_ = 0;
+
+ std::shared_ptr<const std::vector<int>> propos = this->get_proposition_values();
+
+ // For each initial state of the property automaton, push a
+ // (application_state, automaton_state) pair to the exploration stack:
+ unsigned int cursor = 0;
+ xbt_automaton_state_t automaton_state;
+ xbt_dynar_foreach (mc::property_automaton->states, cursor, automaton_state)
+ if (automaton_state->type == -1)
+ exploration_stack_.push_back(this->create_pair(nullptr, automaton_state, propos));
+
+ /* Actually run the double DFS search for counter-examples */
+ while (not exploration_stack_.empty()) {
+ std::shared_ptr<Pair> current_pair = exploration_stack_.back();