+std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state)
+{
+ std::shared_ptr<Pair> next_pair = std::make_shared<Pair>();
+ next_pair->automaton_state = state;
+ next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
+ next_pair->atomic_propositions = this->getPropositionValues();
+ if (current_pair)
+ next_pair->depth = current_pair->depth + 1;
+ else
+ next_pair->depth = 1;
+ /* Get enabled processes and insert them in the interleave set of the next graph_state */
+ for (auto& p : mc_model_checker->process().simix_processes())
+ if (simgrid::mc::process_is_enabled(&p.copy))
+ MC_state_interleave_process(next_pair->graph_state.get(), &p.copy);
+ next_pair->requests = MC_state_interleave_size(next_pair->graph_state.get());
+ /* FIXME : get search_cycle value for each acceptant 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 std::move(next_pair);
+}
+