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; }
};
} // namespace simgrid::mc
}
}
+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 (auto & [aid, transition] : previous_state->get_sleep_set()) {
+
+ XBT_DEBUG("Transition >>%s<< will be explored ?", transition.to_string().c_str());
+ 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(); });
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()) {
+ 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;
/** Snapshot of system state (if needed) */
std::shared_ptr<Snapshot> system_state_;
+ std::map<aid_t, Transition> sleep_set_;
+
public:
explicit State(const RemoteApp& remote_app);
-
+ explicit State(const RemoteApp& remote_app, const State* previous_state);
/* Returns a positive number if there is another transition to pick, or -1 if not */
aid_t next_transition() const;
long get_num() const { return num_; }
std::size_t count_todo() const;
void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); }
- void set_done(aid_t actor) {actors_to_run_.at(actor).set_done();}
+ void mark_done(aid_t actor) { actors_to_run_.at(actor).mark_done();}
void mark_all_todo();
bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
Transition* get_transition() const;
Snapshot* get_system_state() const { return system_state_.get(); }
void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
+ std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
+ void set_sleep_set(Transition* t) {sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); }
+
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }
};
mc_model_checker->finalize_app();
XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
state->get_num(), stack_.size());
- stack_.pop_back();
}
continue;
}
+ XBT_VERB("Sleep set actually containing:");
+ for (auto & [aid, transition] : state->get_sleep_set()) {
+
+ XBT_VERB("###<%ld,%s>", aid, transition.to_string().c_str());
+
+ }
+
/* Actually answer the request: let's execute the selected request (MCed does one step) */
state->execute_next(next);
on_transition_execute_signal(state->get_transition(), get_remote_app());
state->get_transition()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo());
/* Create the new expanded state (copy the state of MCed into our MCer data) */
- auto next_state = std::make_unique<State>(get_remote_app());
+ std::__detail::__unique_ptr_t<simgrid::mc::State> next_state;
+
+ /* If we want sleep set reduction, we pass it to old one to the new state */
+ if (sleep_set_reduction_)
+ next_state = std::make_unique<State>(get_remote_app(), state);
+ else
+ next_state = std::make_unique<State>(get_remote_app());
+
on_state_creation_signal(next_state.get(), get_remote_app());
+ XBT_VERB("New sleep set containing:");
+ for (auto & [aid, transition] : next_state->get_sleep_set()) {
+
+ XBT_VERB("###<%ld,%s>", aid, transition.to_string().c_str());
+
+ }
+
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
if (visited_state_ == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
for (auto const& [aid, _] : next_state->get_actors_list()) {
- if (next_state->is_actor_enabled(aid)) {
+ if (next_state->is_actor_enabled(aid) and not next_state->is_done(aid)) {
next_state->mark_todo(aid);
if (reduction_mode_ == ReductionMode::dpor)
break; // With DPOR, we take the first enabled transition
get_remote_app().check_deadlock();
+ if (stack_.back()->get_transition()->aid_ == 0)
+ stack_.pop_back();
+
/* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that
* have it empty in the way. For each deleted state, check if the request that has generated it (from its
* predecessor state), depends on any other previous request executed before it. If it does then add it to the
bool found_backtracking_point = false;
while (not stack_.empty() && not found_backtracking_point) {
std::unique_ptr<State> state = std::move(stack_.back());
+
stack_.pop_back();
- state->set_done(state->get_transition()->aid_);
+
+ XBT_DEBUG("Maarking Transition >>%s<< of process %ld done and addint it to the sleep set", state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
+ state->mark_done(state->get_transition()->aid_);
+ state->set_sleep_set(state->get_transition());
+
if (reduction_mode_ == ReductionMode::dpor) {
aid_t issuer_id = state->get_transition()->aid_;
for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
private:
void check_non_termination(const State* current_state);
void backtrack();
+ bool sleep_set_reduction_ = true;
/** Stack representing the position in the exploration graph */
std::list<std::unique_ptr<State>> stack_;
