rename a method

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 15d1ccd..2410b9d 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -360,7 +360,7 @@ void CommunicationDeterminismChecker::prepare()
   /* Get an enabled actor and insert it in the interleave set of the initial state */
   for (auto& actor : mc_model_checker->process().actors())
     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
   /* Get an enabled actor and insert it in the interleave set of the initial state */
   for (auto& actor : mc_model_checker->process().actors())
     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))

-      initial_state->interleave(actor.copy.getBuffer());
+      initial_state->addInterleavingSet(actor.copy.getBuffer());

 
   stack_.push_back(std::move(initial_state));
 }
 
   stack_.push_back(std::move(initial_state));
 }


@@ -488,7 +488,7 @@ void CommunicationDeterminismChecker::main()
         /* Get enabled actors and insert them in the interleave set of the next state */
         for (auto& actor : mc_model_checker->process().actors())
           if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
         /* Get enabled actors and insert them in the interleave set of the next state */
         for (auto& actor : mc_model_checker->process().actors())
           if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))

-            next_state->interleave(actor.copy.getBuffer());
+            next_state->addInterleavingSet(actor.copy.getBuffer());

 
         if (dot_output != nullptr)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 
         if (dot_output != nullptr)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 0dda3dd..f65fff1 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -316,7 +316,7 @@ std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton
   /* 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.getBuffer()))
   /* 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.getBuffer()))

-      next_pair->graph_state->interleave(actor.copy.getBuffer());
+      next_pair->graph_state->addInterleavingSet(actor.copy.getBuffer());

   next_pair->requests = next_pair->graph_state->interleaveSize();
   /* FIXME : get search_cycle value for each accepting state */
   if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))
   next_pair->requests = next_pair->graph_state->interleaveSize();
   /* FIXME : get search_cycle value for each accepting state */
   if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index d382815..4256b56 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -162,12 +162,14 @@ void SafetyChecker::run()
     if (visitedState_ == nullptr) {
 
       /* Get an enabled process and insert it in the interleave set of the next state */
     if (visitedState_ == nullptr) {
 
       /* Get an enabled process and insert it in the interleave set of the next state */

-      for (auto& actor : mc_model_checker->process().actors())
-        if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
-          next_state->interleave(actor.copy.getBuffer());
+      for (auto& remoteActor : mc_model_checker->process().actors()) {
+        auto actor = remoteActor.copy.getBuffer();
+        if (simgrid::mc::actor_is_enabled(actor)) {
+          next_state->addInterleavingSet(actor);

           if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
           if (reductionMode_ == simgrid::mc::ReductionMode::dpor)

-            break;
+            break; // With DPOR, we take the first enabled transition

         }
         }

+      }

 
       if (dot_output != nullptr)
         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 
       if (dot_output != nullptr)
         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",


@@ -231,7 +233,7 @@ void SafetyChecker::backtrack()
           }
 
           if (not prev_state->actorStates[issuer->pid].isDone())
           }
 
           if (not prev_state->actorStates[issuer->pid].isDone())

-            prev_state->interleave(issuer);
+            prev_state->addInterleavingSet(issuer);

           else
             XBT_DEBUG("Process %p is in done set", req->issuer);
 
           else
             XBT_DEBUG("Process %p is in done set", req->issuer);
 


@@ -321,7 +323,7 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session)
   /* Get an enabled actor and insert it in the interleave set of the initial state */
   for (auto& actor : mc_model_checker->process().actors())
     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
   /* Get an enabled actor and insert it in the interleave set of the initial state */
   for (auto& actor : mc_model_checker->process().actors())
     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {

-      initial_state->interleave(actor.copy.getBuffer());
+      initial_state->addInterleavingSet(actor.copy.getBuffer());

       if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }
       if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }

diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index d807e28..e4eb0d9 100644 (file)
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -137,9 +137,7 @@ struct XBT_PRIVATE State {
   State(unsigned long state_number);
 
   std::size_t interleaveSize() const;
   State(unsigned long state_number);
 
   std::size_t interleaveSize() const;

-  void interleave(smx_actor_t actor) {
-    this->actorStates[actor->pid].consider();
-  }
+  void addInterleavingSet(smx_actor_t actor) { this->actorStates[actor->pid].consider(); }

   Transition getTransition() const;
 };
 
   Transition getTransition() const;
 };