From 0f0aacb167ddc9427ea1da1c8f1b66ef2d6f532e Mon Sep 17 00:00:00 2001 From: mlaurent Date: Thu, 9 Nov 2023 10:40:50 +0100 Subject: [PATCH] Clang format over some mc files --- src/mc/api/State.cpp | 15 +++++++-------- src/mc/api/State.hpp | 1 - src/mc/explo/DFSExplorer.cpp | 7 +++---- src/mc/explo/odpor/Execution.cpp | 3 +-- src/mc/explo/odpor/ReversibleRaceCalculator.cpp | 2 +- src/mc/transition/TransitionSynchro.cpp | 10 ++++------ 6 files changed, 16 insertions(+), 22 deletions(-) diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 6190f25414..52ffde6044 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -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) { diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 3988504ec2..6603ff0831 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -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 */ diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 8d85325ef7..180fe70b16 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -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 -- diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 536c3f05a6..ba6f7babc5 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -106,8 +106,7 @@ std::unordered_set 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); } diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp index d1b7b2a693..a7de9b92ec 100644 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp @@ -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(e1_transition)->get_capacity() <= 1) { diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp index f98a352af3..8486a0ca83 100644 --- a/src/mc/transition/TransitionSynchro.cpp +++ b/src/mc/transition/TransitionSynchro.cpp @@ -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 } -- 2.20.1