std::list<VisitedPair*> LivenessChecker::acceptance_pairs;
std::list<Pair*> LivenessChecker::liveness_stack;
-xbt_dynar_t LivenessChecker::visited_pairs;
+std::list<VisitedPair*> LivenessChecker::visited_pairs;
VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, std::shared_ptr<simgrid::mc::State> graph_state)
{
{
simgrid::mc::Pair* initial_pair = nullptr;
mc_model_checker->wait_for_requests();
+
acceptance_pairs.clear();
- if(_sg_mc_visited > 0)
- LivenessChecker::visited_pairs = xbt_dynar_new(sizeof(simgrid::mc::VisitedPair*), nullptr);
+ visited_pairs.clear();
initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
initial_global_state->prev_pair = 0;
else
new_visited_pair = visited_pair;
- auto visited_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(LivenessChecker::visited_pairs);
-
auto range = std::equal_range(visited_pairs.begin(), visited_pairs.end(),
new_visited_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
for (auto i = range.first; i != range.second; ++i) {
simgrid::mc::VisitedPair* pair_test = *i;
- std::size_t cursor = i - visited_pairs.begin();
if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
if (xbt_automaton_propositional_symbols_compare_value(
pair_test->atomic_propositions.get(),
XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
else
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);
- xbt_dynar_remove_at(LivenessChecker::visited_pairs, cursor, &pair_test);
- xbt_dynar_insert_at(LivenessChecker::visited_pairs, cursor, &new_visited_pair);
+ *i = new_visited_pair;
pair_test->visited_removed = 1;
if (!pair_test->acceptance_pair
|| pair_test->acceptance_removed == 1)
}
}
- xbt_dynar_insert_at(LivenessChecker::visited_pairs, range.first - visited_pairs.begin(), &new_visited_pair);
+ visited_pairs.insert(range.first, new_visited_pair);
- if ((ssize_t) visited_pairs.size() > _sg_mc_visited) {
+ if (visited_pairs.size() > (std::size_t) _sg_mc_visited) {
int min2 = mc_stats->expanded_pairs;
- unsigned int index2 = 0;
- for (std::size_t i = 0; i != (std::size_t) visited_pairs.size(); ++i) {
- simgrid::mc::VisitedPair* pair_test = visited_pairs[i];
- if (pair_test->num < min2) {
+
+ std::list<VisitedPair*>::iterator index2;
+ for (auto i = visited_pairs.begin(); i != visited_pairs.end(); ++i) {
+ if ((*i)->num < min2) {
index2 = i;
- min2 = pair_test->num;
+ min2 = (*i)->num;
}
}
- simgrid::mc::VisitedPair* pair_test = nullptr;
- xbt_dynar_remove_at(LivenessChecker::visited_pairs, index2, &pair_test);
+
+ simgrid::mc::VisitedPair* pair_test = *index2;
+ visited_pairs.erase(index2);
pair_test->visited_removed = 1;
if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
delete pair_test;