Delete redundant blank lines at the start of a code blocks (CodeFactor).

[simgrid.git] / src / mc / explo / UdporChecker.cpp

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 899073d..98bab5e 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -16,7 +16,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification
 
 namespace simgrid::mc::udpor {
 
-UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
+UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true)
 {
   // Initialize the map
 }
@@ -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
@@ -199,7 +197,7 @@ void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
                               "one transition of the state of an visited event is enabled, yet no\n"
                               "state was actually enabled. Please report this as a bug.\n"
                               "*********************************\n\n");
-  state.execute_next(next_actor);
+  state.execute_next(next_actor, get_remote_app());
 }
 
 void UdporChecker::restore_program_state_to(const State& stateC)
@@ -215,7 +213,7 @@ std::unique_ptr<State> UdporChecker::record_current_state()
   auto next_state = this->get_current_state();
 
   // In UDPOR, we care about all enabled transitions in a given state
-  next_state->mark_all_enabled_todo();
+  next_state->consider_all();
 
   return next_state;
 }