Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of https://framagit.org/simgrid/simgrid
authormlaurent <mathieu.laurent@ens-rennes.fr>
Thu, 16 Feb 2023 10:29:59 +0000 (11:29 +0100)
committermlaurent <mathieu.laurent@ens-rennes.fr>
Thu, 16 Feb 2023 10:29:59 +0000 (11:29 +0100)
1  2 
src/mc/api/ActorState.hpp
src/mc/api/State.cpp

@@@ -95,7 -95,7 +95,7 @@@ public
    unsigned int do_consider()
    {
      if (max_consider_ <= times_considered_ + 1)
 -      set_done();
 +      mark_done();
      return times_considered_++;
    }
    unsigned int get_times_considered() const { return times_considered_; }
      this->state_            = InterleavingType::todo;
      this->times_considered_ = 0;
    }
 -  void set_done() { this->state_ = InterleavingType::done; }
 +  void mark_done() { this->state_ = InterleavingType::done; }
  
    inline Transition* get_transition(unsigned times_considered)
    {
      xbt_assert(times_considered < this->pending_transitions_.size(),
-                "Actor %lu does not have a state available transition with `times_considered = %d`,\n"
+                "Actor %ld does not have a state available transition with `times_considered = %u`,\n"
                 "yet one was asked for",
                 aid_, times_considered);
      return this->pending_transitions_[times_considered].get();
    inline void set_transition(std::unique_ptr<Transition> t, unsigned times_considered)
    {
      xbt_assert(times_considered < this->pending_transitions_.size(),
-                "Actor %lu does not have a state available transition with `times_considered = %d`, "
+                "Actor %ld does not have a state available transition with `times_considered = %u`, "
                 "yet one was attempted to be set",
                 aid_, times_considered);
      this->pending_transitions_[times_considered] = std::move(t);
diff --combined src/mc/api/State.cpp
@@@ -24,56 -24,14 +24,56 @@@ State::State(const RemoteApp& remote_ap
    }
  }
  
 +State::State(const RemoteApp& remote_app, const State* previous_state) : num_(++expended_states_)
 +{
 +
 +  remote_app.get_actors_status(actors_to_run_);
 +
 +  transition_.reset(new Transition());
 +  /* Stateful model checking */
 +  if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
 +    system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_);
 +  }
 +
 +  /* For each actor in the previous sleep set, keep it if it is not dependent with current transition.
 +   * 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] : previous_state->get_sleep_set()) {
 +      
 +      if (not previous_state->get_transition()->depends(&transition)) {
 +            
 +        sleep_set_.emplace(aid, transition);
 +        if (actors_to_run_.count(aid) != 0) {
 +            XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
 +
 +            actors_to_run_.at(aid).mark_done();
 +        }
 +      }
 +      else
 +        XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<", transition.to_string().c_str(), previous_state->get_transition()->to_string().c_str());
 +  
 +  }
 +    
 +}
 +    
  std::size_t State::count_todo() const
  {
    return boost::range::count_if(this->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
  }
  
 +void State::mark_all_todo() 
 +{
 +    for (auto & [aid, actor] : actors_to_run_) {
 +
 +      if (actor.is_enabled() and not actor.is_done() and not actor.is_todo())
 +          actor.mark_todo();
 +      
 +    }
 +}
 +    
  Transition* State::get_transition() const
  {
 -  return transition_;
 +    return transition_;
  }
  
  aid_t State::next_transition() const
    XBT_DEBUG("Search for an actor to run. %zu actors to consider", actors_to_run_.size());
    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())
 -      continue;
 +      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); 
 +
 +        if (not actor.is_enabled())
 +            XBT_DEBUG("Can't run actor %ld because it is not enabled", aid);
 +
 +        if (actor.is_done())
 +            XBT_DEBUG("Can't run actor %ld because it has already been done", aid);
 +
 +        
 +        continue;
 +
 +
 +      }
  
      return aid;
    }
@@@ -113,7 -57,7 +113,7 @@@ void State::execute_next(aid_t next
    const unsigned times_considered          = actor_state.do_consider();
    const auto* expected_executed_transition = actor_state.get_transition(times_considered);
    xbt_assert(expected_executed_transition != nullptr,
-              "Expected a transition with %d times considered to be noted in actor %lu", times_considered, next);
+              "Expected a transition with %u times considered to be noted in actor %ld", times_considered, next);
  
    XBT_DEBUG("Let's run actor %ld (times_considered = %u)", next, times_considered);
  
    Transition::executed_transitions_++;
    auto* just_executed = mc_model_checker->handle_simcall(next, times_considered, true);
    xbt_assert(just_executed->type_ == expected_executed_transition->type_,
-              "The transition that was just executed by actor %lu, viz:\n"
+              "The transition that was just executed by actor %ld, viz:\n"
               "%s\n"
               "is not what was purportedly scheduled to execute, which was:\n"
               "%s\n",