Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Clang format over some mc files
authormlaurent <mathieu.laurent@ens-rennes.fr>
Thu, 9 Nov 2023 09:40:50 +0000 (10:40 +0100)
committermlaurent <mathieu.laurent@ens-rennes.fr>
Thu, 9 Nov 2023 09:40:50 +0000 (10:40 +0100)
src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/explo/DFSExplorer.cpp
src/mc/explo/odpor/Execution.cpp
src/mc/explo/odpor/ReversibleRaceCalculator.cpp
src/mc/transition/TransitionSynchro.cpp

index 6190f25..52ffde6 100644 (file)
@@ -227,10 +227,9 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
 void State::sprout_tree_from_parent_state()
 {
 
-    XBT_DEBUG("Initializing Wut with parent one:");
-    XBT_DEBUG("\n%s", parent_state_->wakeup_tree_.string_of_whole_tree().c_str());
+  XBT_DEBUG("Initializing Wut with parent one:");
+  XBT_DEBUG("\n%s", parent_state_->wakeup_tree_.string_of_whole_tree().c_str());
 
-    
   xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state "
                                        "(or what appears to be, rather for state without a parent defined)");
   const auto min_process_node = parent_state_->wakeup_tree_.get_min_single_process_node();
@@ -270,11 +269,11 @@ void State::remove_subtree_using_current_out_transition()
   wakeup_tree_.remove_min_single_process_subtree();
 }
 
-    void State::remove_subtree_at_aid(const aid_t proc) {
-       wakeup_tree_.remove_subtree_at_aid(proc);
-       
-    }
-    
+void State::remove_subtree_at_aid(const aid_t proc)
+{
+  wakeup_tree_.remove_subtree_at_aid(proc);
+}
+
 odpor::WakeupTree::InsertionResult State::insert_into_wakeup_tree(const odpor::PartialExecution& pe,
                                                                   const odpor::Execution& E)
 {
index 3988504..6603ff0 100644 (file)
@@ -147,7 +147,6 @@ public:
   bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
   std::string string_of_wut() const { return this->wakeup_tree_.string_of_whole_tree(); }
 
-  
   /**
    * @brief
    */
index 8d85325..180fe70 100644 (file)
@@ -138,7 +138,6 @@ void DFSExplorer::run()
     const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
                                                                : std::get<0>(state->next_transition_guided());
 
-
     if (next < 0 || not state->is_actor_enabled(next)) {
       if (next >= 0) { // Actor is not enabled, then
         XBT_INFO("Reduction %s wants to execute a disabled transition %s. If it's ODPOR, ReversibleRace is suboptimal.",
@@ -148,9 +147,9 @@ void DFSExplorer::run()
           XBT_INFO("Current trace:");
           for (auto elm : get_textual_trace())
             XBT_ERROR("%s", elm.c_str());
-         // Remove the disabled transition from the wakeup tree so that ODPOR doesn't try it again
-         state->remove_subtree_at_aid(next);
-         state->add_sleep_set(state->get_actors_list().at(next).get_transition());
+          // Remove the disabled transition from the wakeup tree so that ODPOR doesn't try it again
+          state->remove_subtree_at_aid(next);
+          state->add_sleep_set(state->get_actors_list().at(next).get_transition());
         }
       }
       // If there is no more transition in the current state (or if ODPOR picked an actor that is not enabled --
index 536c3f0..ba6f7ba 100644 (file)
@@ -106,8 +106,7 @@ std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execu
     // it (since this would transitively make it the event
     // which "happens-between" `target` and `e`)
     if (disqualified_events.count(e_i) == 0) {
-       XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` is a valid racing event",
-                  target, e_i);
+      XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` is a valid racing event", target, e_i);
       racing_events.insert(e_i);
       disqualified_events.insert(e_i);
     }
index d1b7b2a..a7de9b9 100644 (file)
@@ -175,7 +175,7 @@ bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Ex
 bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1,
                                                           const Transition* /*e2*/)
 {
-  
+
   const auto e1_transition = E.get_transition_for_handle(e1);
   if (e1_transition->type_ == Transition::Type::SEM_UNLOCK &&
       static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() <= 1) {
index f98a352..8486a0c 100644 (file)
@@ -109,11 +109,10 @@ bool MutexTransition::depends(const Transition* o) const
 std::string SemaphoreTransition::to_string(bool verbose) const
 {
   if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK)
-      return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), sem_, capacity_);
+    return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), sem_, capacity_);
   if (type_ == Type::SEM_WAIT)
     return xbt::string_printf("%s(semaphore: %u, capacity: %u, granted: %s)", Transition::to_c_str(type_), sem_,
-                             capacity_,
-                              granted_ ? "yes" : "no");
+                              capacity_, granted_ ? "yes" : "no");
   THROW_IMPOSSIBLE;
 }
 SemaphoreTransition::SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
@@ -148,9 +147,9 @@ bool SemaphoreTransition::depends(const Transition* o) const
       return false;
 
     // UNLCOK indep with a WAIT if the semaphore had enought capacity anyway
-    if (type_ == Type::SEM_UNLOCK && capacity_ > 1 && other->type_ == Type::SEM_WAIT )
+    if (type_ == Type::SEM_UNLOCK && capacity_ > 1 && other->type_ == Type::SEM_WAIT)
       return false;
-    
+
     // WAIT indep WAIT:
     // if both enabled (may happen in the initial value is sufficient), the ordering has no impact on the result.
     // If only one enabled, the other won't be enabled by the first one.
@@ -158,7 +157,6 @@ bool SemaphoreTransition::depends(const Transition* o) const
     if (type_ == Type::SEM_WAIT && other->type_ == Type::SEM_WAIT)
       return false;
 
-    
     return true; // Other semaphore cases are dependent
   }