+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>(MC_state_new(++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 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))
+ next_pair->graph_state->interleave(&p.copy);
+ next_pair->requests = next_pair->graph_state->interleaveSize();
+ /* 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);
+}
+