{
std::unique_ptr<simgrid::mc::VisitedState> new_state =
std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState(state_number));
- graph_state->system_state = new_state->system_state;
+ graph_state->system_state_ = new_state->system_state;
XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state.get(),
new_state->num, graph_state->num_);
{
/* Intermediate backtracking */
State* last_state = stack_.back().get();
- if (last_state->system_state) {
- last_state->system_state->restore(&mc_model_checker->process());
+ if (last_state->system_state_) {
+ last_state->system_state_->restore(&mc_model_checker->process());
MC_restore_communications_pattern(last_state);
return;
}
RemoteClient* process = &(mc_model_checker->process());
this->graph_state = std::move(graph_state);
- if(this->graph_state->system_state == nullptr)
- this->graph_state->system_state = std::make_shared<Snapshot>(pair_num);
+ if (this->graph_state->system_state_ == nullptr)
+ this->graph_state->system_state_ = std::make_shared<Snapshot>(pair_num);
this->heap_bytes_used = mmalloc_get_bytes_used_remote(process->get_heap()->heaplimit, process->get_malloc_info());
this->actors_count = mc_model_checker->process().actors().size();
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) ||
- not snapshot_equal(pair_test->graph_state->system_state.get(), new_pair->graph_state->system_state.get()))
+ 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();
/* Intermediate backtracking */
if(_sg_mc_checkpoint > 0) {
Pair* pair = exploration_stack_.back().get();
- if(pair->graph_state->system_state){
- pair->graph_state->system_state->restore(&mc_model_checker->process());
+ if (pair->graph_state->system_state_) {
+ pair->graph_state->system_state_->restore(&mc_model_checker->process());
return;
}
}
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) ||
- not snapshot_equal(pair_test->graph_state->system_state.get(), visited_pair->graph_state->system_state.get()))
+ 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;
void SafetyChecker::check_non_termination(State* current_state)
{
for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
- if (snapshot_equal((*state)->system_state.get(), current_state->system_state.get())) {
+ if (snapshot_equal((*state)->system_state_.get(), current_state->system_state_.get())) {
XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num_, current_state->num_);
XBT_INFO("******************************************");
XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
std::unique_ptr<State> state = std::move(stack_.back());
stack_.pop_back();
if (reductionMode_ == ReductionMode::dpor) {
- smx_simcall_t req = &state->internal_req;
+ smx_simcall_t req = &state->internal_req_;
if (req->call_ == SIMCALL_MUTEX_LOCK || req->call_ == SIMCALL_MUTEX_TRYLOCK)
xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none");
const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
State* prev_state = i->get();
- if (request_depend(req, &prev_state->internal_req)) {
+ if (request_depend(req, &prev_state->internal_req_)) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
XBT_DEBUG("Dependent Transitions:");
int value = prev_state->transition_.argument_;
else
XBT_DEBUG("Process %p is in done set", req->issuer_);
break;
- } else if (req->issuer_ == prev_state->internal_req.issuer_) {
+ } else if (req->issuer_ == prev_state->internal_req_.issuer_) {
XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(req->call_),
- SIMIX_simcall_name(prev_state->internal_req.call_));
+ SIMIX_simcall_name(prev_state->internal_req_.call_));
break;
} else {
- const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
+ const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req_);
XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent",
SIMIX_simcall_name(req->call_), issuer->get_pid(), state->num_,
- SIMIX_simcall_name(prev_state->internal_req.call_), previous_issuer->get_pid(), prev_state->num_);
+ SIMIX_simcall_name(prev_state->internal_req_.call_), previous_issuer->get_pid(), prev_state->num_);
}
}
}
{
/* Intermediate backtracking */
State* last_state = stack_.back().get();
- if (last_state->system_state) {
- last_state->system_state->restore(&mc_model_checker->process());
+ if (last_state->system_state_) {
+ last_state->system_state_->restore(&mc_model_checker->process());
return;
}
State::State(unsigned long state_number) : num_(state_number)
{
- this->internal_comm.clear();
- this->internal_req = s_smx_simcall();
+ this->internal_comm_.clear();
+ this->internal_req_ = s_smx_simcall();
this->executed_req_ = s_smx_simcall();
actor_states_.resize(MC_smx_get_maxpid());
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (state_number % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
- system_state = std::make_shared<simgrid::mc::Snapshot>(num_);
+ system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
MC_state_copy_incomplete_communications_pattern(this);
MC_state_copy_index_communications_pattern(this);
state->transition_.pid_ = actor->get_pid();
state->executed_req_ = *req;
// Fetch the data of the request and translate it:
- state->internal_req = *req;
+ state->internal_req_ = *req;
/* The waitany and testany request are transformed into a wait or test request over the corresponding communication
* action so it can be treated later by the dependence function. */
switch (req->call_) {
case SIMCALL_COMM_WAITANY: {
- state->internal_req.call_ = SIMCALL_COMM_WAIT;
+ state->internal_req_.call_ = SIMCALL_COMM_WAIT;
simgrid::kernel::activity::CommImpl* remote_comm;
remote_comm = mc_model_checker->process().read(
remote(simcall_comm_waitany__get__comms(req) + state->transition_.argument_));
- mc_model_checker->process().read(state->internal_comm, remote(remote_comm));
- simcall_comm_wait__set__comm(&state->internal_req, state->internal_comm.get_buffer());
- simcall_comm_wait__set__timeout(&state->internal_req, 0);
+ mc_model_checker->process().read(state->internal_comm_, remote(remote_comm));
+ simcall_comm_wait__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
+ simcall_comm_wait__set__timeout(&state->internal_req_, 0);
break;
}
case SIMCALL_COMM_TESTANY:
- state->internal_req.call_ = SIMCALL_COMM_TEST;
+ state->internal_req_.call_ = SIMCALL_COMM_TEST;
if (state->transition_.argument_ > 0) {
simgrid::kernel::activity::CommImpl* remote_comm = mc_model_checker->process().read(
remote(simcall_comm_testany__get__comms(req) + state->transition_.argument_));
- mc_model_checker->process().read(state->internal_comm, remote(remote_comm));
+ mc_model_checker->process().read(state->internal_comm_, remote(remote_comm));
}
- simcall_comm_test__set__comm(&state->internal_req, state->internal_comm.get_buffer());
- simcall_comm_test__set__result(&state->internal_req, state->transition_.argument_);
+ simcall_comm_test__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
+ simcall_comm_test__set__result(&state->internal_req_, state->transition_.argument_);
break;
case SIMCALL_COMM_WAIT:
- mc_model_checker->process().read_bytes(&state->internal_comm, sizeof(state->internal_comm),
+ mc_model_checker->process().read_bytes(&state->internal_comm_, sizeof(state->internal_comm_),
remote(simcall_comm_wait__getraw__comm(req)));
- simcall_comm_wait__set__comm(&state->executed_req_, state->internal_comm.get_buffer());
- simcall_comm_wait__set__comm(&state->internal_req, state->internal_comm.get_buffer());
+ simcall_comm_wait__set__comm(&state->executed_req_, state->internal_comm_.get_buffer());
+ simcall_comm_wait__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
break;
case SIMCALL_COMM_TEST:
- mc_model_checker->process().read_bytes(&state->internal_comm, sizeof(state->internal_comm),
+ mc_model_checker->process().read_bytes(&state->internal_comm_, sizeof(state->internal_comm_),
remote(simcall_comm_test__getraw__comm(req)));
- simcall_comm_test__set__comm(&state->executed_req_, state->internal_comm.get_buffer());
- simcall_comm_test__set__comm(&state->internal_req, state->internal_comm.get_buffer());
+ simcall_comm_test__set__comm(&state->executed_req_, state->internal_comm_.get_buffer());
+ simcall_comm_test__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
break;
default:
* SIMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST
* and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
*/
- s_smx_simcall internal_req;
+ s_smx_simcall internal_req_;
/* Can be used as a copy of the remote synchro object */
- simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> internal_comm;
+ simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> internal_comm_;
/** Snapshot of system state (if needed) */
- std::shared_ptr<simgrid::mc::Snapshot> system_state;
+ std::shared_ptr<simgrid::mc::Snapshot> system_state_;
// For CommunicationDeterminismChecker
std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;