return std::make_shared<const std::vector<int>>(std::move(values));
}
-int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
-{
- simgrid::mc::Snapshot* s1 = state1->graph_state->system_state.get();
- simgrid::mc::Snapshot* s2 = state2->graph_state->system_state.get();
- return simgrid::mc::snapshot_compare(s1, s2);
-}
-
std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair)
{
std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(
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)
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 ||
+ *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
+ not snapshot_equal(pair_test->graph_state->system_state.get(), new_pair->graph_state->system_state.get()))
continue;
XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
exploration_stack_.pop_back();
if (pair->exploration_started) {
- int req_num = state->transition.argument;
- smx_simcall_t saved_req = &state->executed_req;
+ int req_num = state->transition_.argument_;
+ smx_simcall_t saved_req = &state->executed_req_;
smx_simcall_t req = nullptr;
state.get());
}
- this->get_session().execute(state->transition);
+ this->get_session().execute(state->transition_);
}
/* Update statistics */
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
- || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions)
- || this->compare(pair_test, visited_pair.get()) != 0)
- continue;
+ if (xbt_automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 ||
+ *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
+ not snapshot_equal(pair_test->graph_state->system_state.get(), visited_pair->graph_state->system_state.get()))
+ continue;
if (pair_test->other_num == -1)
visited_pair->other_num = pair_test->num;
else
{
RecordTrace res;
for (std::shared_ptr<Pair> const& pair : exploration_stack_)
- res.push_back(pair->graph_state->getTransition());
+ res.push_back(pair->graph_state->get_transition());
return res;
}
{
std::vector<std::string> trace;
for (std::shared_ptr<Pair> const& pair : exploration_stack_) {
- int req_num = pair->graph_state->transition.argument;
- smx_simcall_t req = &pair->graph_state->executed_req;
- if (req && req->call != SIMCALL_NONE)
+ int req_num = pair->graph_state->transition_.argument_;
+ smx_simcall_t req = &pair->graph_state->executed_req_;
+ if (req && req->call_ != SIMCALL_NONE)
trace.push_back(simgrid::mc::request_to_string(
req, req_num, simgrid::mc::RequestType::executed));
}
/* Get enabled actors and insert them in the interleave set of the next graph_state */
for (auto& actor : mc_model_checker->process().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer()))
- next_pair->graph_state->addInterleavingSet(actor.copy.get_buffer());
- next_pair->requests = next_pair->graph_state->interleaveSize();
+ next_pair->graph_state->add_interleaving_set(actor.copy.get_buffer());
+ next_pair->requests = next_pair->graph_state->interleave_size();
/* FIXME : get search_cycle value for each accepting state */
if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))
next_pair->search_cycle = true;
XBT_DEBUG(
"********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)",
- current_pair->depth, current_pair->search_cycle, current_pair->graph_state->interleaveSize(), current_pair->num,
- current_pair->requests);
+ current_pair->depth, current_pair->search_cycle, current_pair->graph_state->interleave_size(),
+ current_pair->num, current_pair->requests);
if (current_pair->requests == 0) {
this->backtrack();
}
smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
- int req_num = current_pair->graph_state->transition.argument;
+ int req_num = current_pair->graph_state->transition_.argument_;
if (dot_output != nullptr) {
if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) {
visited_pairs_count_++;
/* Answer the request */
- mc_model_checker->handle_simcall(current_pair->graph_state->transition);
+ mc_model_checker->handle_simcall(current_pair->graph_state->transition_);
/* Wait for requests (schedules processes) */
mc_model_checker->wait_for_requests();