Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
MC: rename some methods to make their intent clear
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Wed, 11 Sep 2019 23:31:35 +0000 (01:31 +0200)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 13 Sep 2019 09:22:05 +0000 (11:22 +0200)
src/mc/checker/CommunicationDeterminismChecker.cpp
src/mc/checker/LivenessChecker.cpp
src/mc/checker/SafetyChecker.cpp
src/mc/mc_state.cpp
src/mc/mc_state.hpp

index a4b48c9..1302502 100644 (file)
@@ -425,7 +425,7 @@ void CommunicationDeterminismChecker::real_run()
     mc_model_checker->visited_states++;
 
     if (stack_.size() <= (std::size_t)_sg_mc_max_depth)
-      req = MC_state_get_request(cur_state);
+      req = MC_state_choose_request(cur_state);
     else
       req = nullptr;
 
index 4f6000f..bbced3a 100644 (file)
@@ -379,7 +379,7 @@ void LivenessChecker::run()
       }
     }
 
-    smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
+    smx_simcall_t req = MC_state_choose_request(current_pair->graph_state.get());
     int req_num       = current_pair->graph_state->transition_.argument_;
 
     if (dot_output != nullptr) {
index ecc8ca3..c08ecaa 100644 (file)
@@ -113,7 +113,7 @@ void SafetyChecker::run()
 
     // Search an enabled transition in the current state; backtrack if the interleave set is empty
     // get_request also sets state.transition to be the one corresponding to the returned req
-    smx_simcall_t req = MC_state_get_request(state);
+    smx_simcall_t req = MC_state_choose_request(state);
     // req is now the transition of the process that was selected to be executed
 
     if (req == nullptr) {
index 0106b84..535dae9 100644 (file)
@@ -60,7 +60,7 @@ Transition State::get_transition() const
  * Things can get muddled with the WAITANY and TESTANY simcalls, that are rewritten on the fly to a bunch of WAIT
  * (resp TEST) transitions using the transition.argument field to remember what was the last returned sub-transition.
  */
-static inline smx_simcall_t MC_state_get_request_for_process(simgrid::mc::State* state, smx_actor_t actor)
+static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::State* state, smx_actor_t actor)
 {
   /* reset the outgoing transition */
   simgrid::mc::ActorState* procstate   = &state->actor_states_[actor->get_pid()];
@@ -202,14 +202,14 @@ static inline smx_simcall_t MC_state_get_request_for_process(simgrid::mc::State*
   return req;
 }
 
-smx_simcall_t MC_state_get_request(simgrid::mc::State* state)
+smx_simcall_t MC_state_choose_request(simgrid::mc::State* state)
 {
   for (auto& actor : mc_model_checker->process().actors()) {
     /* Only consider the actors that were marked as interleaving by the checker algorithm */
     if (not state->actor_states_[actor.copy.get_buffer()->get_pid()].is_todo())
       continue;
 
-    smx_simcall_t res = MC_state_get_request_for_process(state, actor.copy.get_buffer());
+    smx_simcall_t res = MC_state_choose_request_for_process(state, actor.copy.get_buffer());
     if (res)
       return res;
   }
index 96b5910..4123468 100644 (file)
@@ -130,6 +130,6 @@ public:
 }
 }
 
-XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state);
+XBT_PRIVATE smx_simcall_t MC_state_choose_request(simgrid::mc::State* state);
 
 #endif