small comments improvements around a complex code

[simgrid.git] / src / mc / checker / LivenessChecker.cpp

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index e04712b..4f6000f 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -30,7 +30,7 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
 
   this->graph_state = std::move(graph_state);
   if(this->graph_state->system_state == nullptr)
-    this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
+    this->graph_state->system_state = std::make_shared<simgrid::mc::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();
@@ -80,13 +80,6 @@ std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values(
   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>(
@@ -98,10 +91,9 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
 
   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();
@@ -150,8 +142,8 @@ void LivenessChecker::replay()
 
     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;
 
@@ -169,7 +161,7 @@ void LivenessChecker::replay()
           state.get());
       }
 
-      this->get_session().execute(state->transition);
+      this->get_session().execute(state->transition_);
     }
 
     /* Update statistics */
@@ -200,11 +192,10 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
 
   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
@@ -241,7 +232,7 @@ RecordTrace LivenessChecker::get_record_trace() // override
 {
   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;
 }
 
@@ -269,9 +260,9 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
 {
   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));
   }
@@ -293,8 +284,8 @@ std::shared_ptr<Pair> LivenessChecker::create_pair(Pair* current_pair, xbt_autom
   /* 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;
@@ -355,8 +346,8 @@ void LivenessChecker::run()
 
     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();
@@ -389,7 +380,7 @@ void LivenessChecker::run()
     }
 
     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) {
@@ -414,7 +405,7 @@ void LivenessChecker::run()
       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();