}
}
-Pair::Pair() : num(++mc_stats->expanded_pairs)
+Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs)
{}
Pair::~Pair() {}
}
/* Update statistics */
- mc_stats->visited_pairs++;
+ visitedPairsCount_++;
mc_stats->executed_transitions++;
depth++;
void LivenessChecker::logState() // override
{
Checker::logState();
- XBT_INFO("Expanded pairs = %lu", mc_stats->expanded_pairs);
- XBT_INFO("Visited pairs = %lu", mc_stats->visited_pairs);
+ XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
+ XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
}
/* Update mc_stats */
mc_stats->executed_transitions++;
if (!current_pair->exploration_started)
- mc_stats->visited_pairs++;
+ visitedPairsCount_++;
/* Answer the request */
mc_model_checker->handle_simcall(current_pair->graph_state->transition);
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>();
+ 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());
next_pair->atomic_propositions = std::move(propositions);
int depth = 0;
bool exploration_started = false;
- Pair();
+ Pair(unsigned long expanded_pairs);
~Pair();
Pair(Pair const&) = delete;
std::list<std::shared_ptr<Pair>> explorationStack_;
std::list<std::shared_ptr<VisitedPair>> acceptancePairs_;
std::list<std::shared_ptr<VisitedPair>> visitedPairs_;
+private:
+ unsigned long visitedPairsCount_ = 0;
+ unsigned long expandedPairsCount_ = 0;
};
}
typedef struct mc_stats {
unsigned long state_size;
unsigned long visited_states;
- unsigned long visited_pairs;
unsigned long expanded_states;
- unsigned long expanded_pairs;
unsigned long executed_transitions;
} s_mc_stats_t, *mc_stats_t;