Obey coding standard for the field names in mc:State.

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index 24e3c5c..cb4d2d9 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -51,7 +51,7 @@ VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* g
 {
   std::unique_ptr<simgrid::mc::VisitedState> new_state =
     std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState(state_number));
 {
   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_);
 
   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state.get(),
             new_state->num, graph_state->num_);
 

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index b735472..41d5962 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -356,8 +356,8 @@ void CommunicationDeterminismChecker::restoreState()
 {
   /* Intermediate backtracking */
   State* last_state = stack_.back().get();
 {
   /* 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;
   }
     MC_restore_communications_pattern(last_state);
     return;
   }

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 0e3d3ef..a1485bf 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -29,8 +29,8 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
   RemoteClient* process = &(mc_model_checker->process());
 
   this->graph_state = std::move(graph_state);
   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();
   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();


@@ -92,7 +92,7 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
     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) ||
     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();
       continue;
     XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
     exploration_stack_.pop_back();


@@ -122,8 +122,8 @@ void LivenessChecker::replay()
   /* Intermediate backtracking */
   if(_sg_mc_checkpoint > 0) {
     Pair* pair = exploration_stack_.back().get();
   /* 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;
     }
   }
       return;
     }
   }


@@ -186,7 +186,7 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
     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) ||
     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;
       continue;
     if (pair_test->other_num == -1)
       visited_pair->other_num = pair_test->num;

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index d926af5..33d26b8 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -34,7 +34,7 @@ namespace mc {
 void SafetyChecker::check_non_termination(State* current_state)
 {
   for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
 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 ***");
       XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num_, current_state->num_);
       XBT_INFO("******************************************");
       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");


@@ -190,14 +190,14 @@ void SafetyChecker::backtrack()
     std::unique_ptr<State> state = std::move(stack_.back());
     stack_.pop_back();
     if (reductionMode_ == ReductionMode::dpor) {
     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 (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_;
           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
             XBT_DEBUG("Dependent Transitions:");
             int value              = prev_state->transition_.argument_;


@@ -215,15 +215,15 @@ void SafetyChecker::backtrack()
           else
             XBT_DEBUG("Process %p is in done set", req->issuer_);
           break;
           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_),
           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 {
           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_,
           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_);

         }
       }
     }
         }
       }
     }


@@ -245,8 +245,8 @@ void SafetyChecker::restore_state()
 {
   /* Intermediate backtracking */
   State* last_state = stack_.back().get();
 {
   /* 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;
   }
 
     return;
   }
 

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index b811c1d..9669200 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -18,14 +18,14 @@ namespace mc {
 
 State::State(unsigned long state_number) : num_(state_number)
 {
 
 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) {
   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);
     if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
       MC_state_copy_incomplete_communications_pattern(this);
       MC_state_copy_index_communications_pattern(this);


@@ -149,47 +149,47 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta
   state->transition_.pid_ = actor->get_pid();
   state->executed_req_    = *req;
   // Fetch the data of the request and translate it:
   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: {
 
   /* 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_));
       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:
       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_));
 
       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:
       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)));
                                              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:
       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)));
                                              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:
       break;
 
     default:

diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp
index 4123468..9e70190 100644 (file)
--- a/src/mc/mc_state.hpp
+++ b/src/mc/mc_state.hpp
@@ -109,13 +109,13 @@ public:
    * SIMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST
    * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
    */
    * 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 */
 
   /* 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) */
 
   /** 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_;
 
   // For CommunicationDeterminismChecker
   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;