Prepare to debug the depends

[simgrid.git] / src / mc / mc_state.cpp

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index f92aaa142fac114ec7c38b549d43659a05936393..9871c79be658f8ff8095be9c81153fd92f152661 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -18,12 +18,15 @@ using api = simgrid::mc::Api;
 namespace simgrid {
 namespace mc {
 
-State::State(unsigned long state_number) : num_(state_number)
+long State::expended_states_ = 0;
+
+State::State() : num_(++expended_states_)
 {
   const unsigned long maxpid = api::get().get_maxpid();
   actor_states_.resize(maxpid);
+  transition_.reset(new Transition());
   /* Stateful model checking */
-  if ((_sg_mc_checkpoint > 0 && (state_number % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
+  if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
     auto snapshot_ptr = api::get().take_snapshot(num_);
     system_state_ = std::shared_ptr<simgrid::mc::Snapshot>(snapshot_ptr);
     if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
@@ -40,7 +43,7 @@ std::size_t State::count_todo() const
 
 Transition* State::get_transition() const
 {
-  return const_cast<Transition*>(&this->transition_);
+  return transition_.get();
 }
 
 int State::next_transition() const
@@ -59,7 +62,7 @@ int State::next_transition() const
   }
   return -1;
 }
-RemotePtr<simgrid::kernel::actor::SimcallObserver> State::execute_next(int next)
+Transition* State::execute_next(int next)
 {
   std::vector<ActorInformation>& actors = mc_model_checker->get_remote_process().actors();
 
@@ -78,12 +81,17 @@ RemotePtr<simgrid::kernel::actor::SimcallObserver> State::execute_next(int next)
     actor_state->set_done();
   }
 
-  transition_.init(aid, times_considered);
+  transition_->init(aid, times_considered);
   executed_req_ = actor->simcall_;
 
-  XBT_DEBUG("Let's run actor %ld, going for transition %s", aid, transition_.to_string().c_str());
+  XBT_DEBUG("Let's run actor %ld, going for transition %s", aid, transition_->to_cstring());
+
+  Transition::executed_transitions_++;
+
+  Transition* res = mc_model_checker->handle_simcall(*transition_, true);
+  mc_model_checker->wait_for_requests();
 
-  return transition_.replay();
+  return res;
 }
 
 void State::copy_incomplete_comm_pattern()