auto res = std::equal_range(acceptancePairs_.begin(), acceptancePairs_.end(),
new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
- if (pair->search_cycle)
- for (auto i = res.first; i != res.second; ++i) {
- std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
- if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
- if (pair_test->atomic_propositions == new_pair->atomic_propositions) {
- if (this->compare(pair_test.get(), new_pair.get()) == 0) {
- XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
- livenessStack_.pop_back();
- if (dot_output != nullptr)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
- return nullptr;
- }
- }
- }
- }
+ if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) {
+ std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
+ if (xbt_automaton_state_compare(
+ pair_test->automaton_state, new_pair->automaton_state) != 0
+ || pair_test->atomic_propositions != new_pair->atomic_propositions
+ || this->compare(pair_test.get(), new_pair.get()) != 0)
+ continue;
+ XBT_INFO("Pair %d already reached (equal to pair %d) !",
+ new_pair->num, pair_test->num);
+ livenessStack_.pop_back();
+ if (dot_output != nullptr)
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
+ initial_global_state->prev_pair, pair_test->num,
+ initial_global_state->prev_req);
+ return nullptr;
+ }
acceptancePairs_.insert(res.first, new_pair);
return new_pair;
void LivenessChecker::prepare(void)
{
- simgrid::mc::Pair* initial_pair = nullptr;
mc_model_checker->wait_for_requests();
initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
xbt_dynar_foreach(simgrid::mc::property_automaton->states, cursor, automaton_state) {
if (automaton_state->type == -1) { /* Initial automaton state */
- initial_pair = new Pair();
+ std::shared_ptr<Pair> initial_pair = std::make_shared<Pair>();
initial_pair->automaton_state = automaton_state;
initial_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
initial_pair->atomic_propositions = this->getPropositionValues();
initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state.get());
initial_pair->search_cycle = false;
- livenessStack_.push_back(initial_pair);
+ livenessStack_.push_back(std::move(initial_pair));
}
}
}
void LivenessChecker::replay()
{
- smx_simcall_t req = nullptr, saved_req = NULL;
- int value, depth = 1;
- char *req_str;
-
XBT_DEBUG("**** Begin Replay ****");
/* Intermediate backtracking */
if(_sg_mc_checkpoint > 0) {
- simgrid::mc::Pair* pair = livenessStack_.back();
+ simgrid::mc::Pair* pair = livenessStack_.back().get();
if(pair->graph_state->system_state){
simgrid::mc::restore_snapshot(pair->graph_state->system_state);
return;
simgrid::mc::restore_snapshot(initial_global_state->snapshot);
/* Traverse the stack from the initial state and re-execute the transitions */
- for (simgrid::mc::Pair* pair : livenessStack_) {
+ int depth = 1;
+ for (std::shared_ptr<Pair> const& pair : livenessStack_) {
if (pair == livenessStack_.back())
break;
if (pair->exploration_started) {
- saved_req = MC_state_get_executed_request(state.get(), &value);
+ int value;
+ smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
+
+ smx_simcall_t req = nullptr;
if (saved_req != nullptr) {
/* because we got a copy of the executed request, we have to fetch the
/* Debug information */
if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
+ char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state.get());
xbt_free(req_str);
}
for (auto i = range.first; i != range.second; ++i) {
VisitedPair* pair_test = i->get();
- if (xbt_automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) == 0) {
- if (pair_test->atomic_propositions == visited_pair->atomic_propositions) {
- if (this->compare(pair_test, visited_pair.get()) == 0) {
- if (pair_test->other_num == -1)
- visited_pair->other_num = pair_test->num;
- else
- visited_pair->other_num = pair_test->other_num;
- if (dot_output == nullptr)
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
- visited_pair->num, pair_test->num);
- else
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
- visited_pair->num, pair_test->num, visited_pair->other_num);
- (*i) = std::move(visited_pair);
- return (*i)->other_num;
- }
- }
- }
+ if (xbt_automaton_state_compare(
+ pair_test->automaton_state, visited_pair->automaton_state) != 0
+ || pair_test->atomic_propositions != visited_pair->atomic_propositions
+ || this->compare(pair_test, visited_pair.get()) != 0)
+ continue;
+ if (pair_test->other_num == -1)
+ visited_pair->other_num = pair_test->num;
+ else
+ visited_pair->other_num = pair_test->other_num;
+ if (dot_output == nullptr)
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
+ visited_pair->num, pair_test->num);
+ else
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
+ visited_pair->num, pair_test->num, visited_pair->other_num);
+ (*i) = std::move(visited_pair);
+ return (*i)->other_num;
}
visitedPairs_.insert(range.first, std::move(visited_pair));
RecordTrace LivenessChecker::getRecordTrace() // override
{
RecordTrace res;
- for (simgrid::mc::Pair* pair : livenessStack_) {
+ for (std::shared_ptr<Pair> const& pair : livenessStack_) {
int value;
smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
if (req && req->call != SIMCALL_NONE) {
std::vector<std::string> LivenessChecker::getTextualTrace() // override
{
std::vector<std::string> trace;
- for (simgrid::mc::Pair* pair : livenessStack_) {
+ for (std::shared_ptr<Pair> const& pair : livenessStack_) {
int value;
smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
if (req && req->call != SIMCALL_NONE) {
int LivenessChecker::main(void)
{
- simgrid::mc::Pair* current_pair = nullptr;
- int value, res, visited_num = -1;
- smx_simcall_t req = nullptr;
- xbt_automaton_transition_t transition_succ = nullptr;
- int cursor = 0;
- std::shared_ptr<VisitedPair> reached_pair = nullptr;
+ int visited_num = -1;
while (!livenessStack_.empty()){
/* Get current pair */
- current_pair = livenessStack_.back();
+ std::shared_ptr<Pair> current_pair = livenessStack_.back();
/* Update current state in buchi automaton */
simgrid::mc::property_automaton->current_state = current_pair->automaton_state;
if (current_pair->requests > 0) {
- if (current_pair->automaton_state->type == 1 && !current_pair->exploration_started) {
- /* If new acceptance pair, return new pair */
- if ((reached_pair = this->insertAcceptancePair(current_pair)) == nullptr) {
- this->showAcceptanceCycle(current_pair->depth);
- return SIMGRID_MC_EXIT_LIVENESS;
- }
+ std::shared_ptr<VisitedPair> reached_pair;
+ if (current_pair->automaton_state->type == 1 && !current_pair->exploration_started
+ && (reached_pair = this->insertAcceptancePair(current_pair.get())) == nullptr) {
+ this->showAcceptanceCycle(current_pair->depth);
+ return SIMGRID_MC_EXIT_LIVENESS;
}
/* Pair already visited ? stop the exploration on the current path */
if ((!current_pair->exploration_started)
&& (visited_num = this->insertVisitedPair(
- reached_pair, current_pair)) != -1) {
+ reached_pair, current_pair.get())) != -1) {
if (dot_output != nullptr){
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, visited_num, initial_global_state->prev_req);
}else{
- req = MC_state_get_request(current_pair->graph_state.get(), &value);
+ int value;
+ smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get(), &value);
if (dot_output != nullptr) {
if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
std::vector<int> prop_values = this->getPropositionValues();
/* Evaluate enabled/true transitions in automaton according to atomic propositions values and create new pairs */
- cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
+ int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
while (cursor >= 0) {
- transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
- res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
+ xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
+ int res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
if (res == 1 || res == 2) { /* 1 = True transition (always enabled), 2 = enabled transition according to atomic prop values */
- Pair* next_pair = new Pair();
+ std::shared_ptr<Pair> next_pair = std::make_shared<Pair>();
next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
next_pair->automaton_state = transition_succ->dst;
next_pair->atomic_propositions = this->getPropositionValues();
next_pair->search_cycle = true;
/* Add new pair to the exploration stack */
- livenessStack_.push_back(next_pair);
+ livenessStack_.push_back(std::move(next_pair));
}
cursor--;
/* 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 (!livenessStack_.empty()) {
- current_pair = livenessStack_.back();
+ std::shared_ptr<simgrid::mc::Pair> current_pair = livenessStack_.back();
livenessStack_.pop_back();
if (current_pair->requests > 0) {
/* We found a backtracking point */
XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
- livenessStack_.push_back(current_pair);
+ livenessStack_.push_back(std::move(current_pair));
this->replay();
XBT_DEBUG("Backtracking done");
break;
}else{
- /* Delete pair */
XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth);
if (current_pair->automaton_state->type == 1)
this->removeAcceptancePair(current_pair->num);
- delete current_pair;
}
}
