Make Liveness and CommDet more similar to Safety

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 7ed417d..e014bed 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -354,16 +354,6 @@ RemotePtr<kernel::activity::ActivityImpl> Api::get_comm_remote_addr(smx_simcall_
   THROW_IMPOSSIBLE;
 }
 
-void Api::handle_simcall(Transition const& transition) const
-{
-  mc_model_checker->handle_simcall(transition);
-}
-
-void Api::mc_wait_for_requests() const
-{
-  mc_model_checker->wait_for_requests();
-}
-
 void Api::mc_exit(int status) const
 {
   mc_model_checker->exit(status);

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 3885f22..199f456 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -98,8 +98,6 @@ public:
   void mc_inc_visited_states() const;
   unsigned long mc_get_visited_states() const;
   void mc_check_deadlock() const;
-  void handle_simcall(Transition const& transition) const;
-  void mc_wait_for_requests() const;
   XBT_ATTRIB_NORETURN void mc_exit(int status) const;
   void dump_record_path() const;
   bool mc_state_choose_request(simgrid::mc::State* state) const;

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index a973d78..a1a136b 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -369,9 +369,8 @@ void CommunicationDeterminismChecker::restoreState()
 
     /* TODO : handle test and testany simcalls */
     CallType call = MC_get_call_type(req);
-    api::get().handle_simcall(state->transition_);
+    state->transition_.execute();
     handle_comm_pattern(call, req, req_num, 1);
-    api::get().mc_wait_for_requests();
 
     /* Update statistics */
     api::get().mc_inc_visited_states();
@@ -440,14 +439,11 @@ void CommunicationDeterminismChecker::real_run()
         call = MC_get_call_type(req);
 
       /* Answer the request */
-      api::get().handle_simcall(cur_state->transition_);
+      cur_state->transition_.execute();
       /* After this call req is no longer useful */
 
       handle_comm_pattern(call, req, req_num, 0);
 
-      /* Wait for requests (schedules processes) */
-      api::get().mc_wait_for_requests();
-
       /* Create the new expanded state */
       ++expanded_states_count_;
       auto next_state = std::make_unique<State>(expanded_states_count_);

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index c4f33a7..8eff59c 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -353,17 +353,12 @@ void LivenessChecker::run()
       fflush(dot_output);
     }
 
+    current_pair->graph_state->transition_.execute();
     XBT_DEBUG("Execute: %s", current_pair->graph_state->transition_.to_string().c_str());
 
     if (not current_pair->exploration_started)
       visited_pairs_count_++;
 
-    /* Answer the request */
-    api::get().handle_simcall(current_pair->graph_state->transition_);
-
-    /* Wait for requests (schedules processes) */
-    api::get().mc_wait_for_requests();
-
     current_pair->requests--;
     current_pair->exploration_started = true;