Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Delete redundant blank lines at the start of a code blocks (CodeFactor).
authorArnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Fri, 24 Mar 2023 13:54:41 +0000 (14:54 +0100)
committerArnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Fri, 24 Mar 2023 15:29:50 +0000 (16:29 +0100)
src/mc/api/State.cpp
src/mc/api/guide/BasicGuide.hpp
src/mc/explo/UdporChecker.cpp
src/mc/transition/TransitionComm.cpp

index 967c625..ce8daed 100644 (file)
@@ -29,7 +29,6 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_), guide(std::make_
 State::State(RemoteApp& remote_app, const State* parent_state)
     : num_(++expended_states_), parent_state_(parent_state), guide(std::make_unique<BasicGuide>())
 {
-
   remote_app.get_actors_status(guide->actors_to_run_);
 
   /* Stateful model checking */
@@ -43,9 +42,7 @@ State::State(RemoteApp& remote_app, const State* parent_state)
      * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
      * it is not explored*/
     for (auto& [aid, transition] : parent_state_->get_sleep_set()) {
-
       if (not parent_state_->get_transition()->depends(&transition)) {
-
         sleep_set_.try_emplace(aid, transition);
         if (guide->actors_to_run_.count(aid) != 0) {
           XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
@@ -75,7 +72,6 @@ aid_t State::next_transition() const
   for (auto const& [aid, actor] : guide->actors_to_run_) {
     /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
     if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) {
-
       if (not actor.is_todo())
         XBT_DEBUG("Can't run actor %ld because it is not todo", aid);
 
index daa5733..c550675 100644 (file)
@@ -14,7 +14,6 @@ class BasicGuide : public GuidedState {
 public:
   std::pair<aid_t, double> next_transition() const override
   {
-
     for (auto const& [aid, actor] : actors_to_run_) {
       /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
       if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) {
index 550e5b7..98bab5e 100644 (file)
@@ -53,7 +53,6 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::
   // exploration would lead to a so-called
   // "sleep-set blocked" trace.
   if (enC.is_subset_of(D)) {
-
     if (not C.get_events().empty()) {
       // Report information...
     }
@@ -99,7 +98,6 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::
 
   constexpr unsigned K = 10;
   if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
-
     // Before searching the "right half", we need to make
     // sure the program actually reflects the fact
     // that we are searching again from `stateC` (the recursive
index 376c301..de0ec2b 100644 (file)
@@ -78,7 +78,6 @@ std::string CommTestTransition::to_string(bool verbose) const
 }
 bool CommTestTransition::depends(const Transition* other) const
 {
-
   if (other->type_ < type_)
     return other->depends(this);