}
}
+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(); });
}
+ 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_.get();
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;
}
/** 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 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;
void set_transition(Transition* t) { transition_.reset(t); }
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_; }
};
if (next < 0) { // If there is no more transition in the current state, backtrack.
XBT_DEBUG("There remains %lu actors, but none to interleave (depth %zu).", state->get_actor_count(),
stack_.size() + 1);
-
+
if (state->get_actor_count() == 0) {
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());
+
}
+
this->backtrack();
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
backtrack_count_++;
XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str());
on_backtracking_signal(get_remote_app());
- stack_.pop_back();
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();
+
+ 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) {
if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(),
prev_state->get_transition()->to_string().c_str(), issuer_id);
- break;
+ continue;
} else if (prev_state->get_transition()->depends(state->get_transition())) {
XBT_VERB("Dependent Transitions:");
XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
- if (not prev_state->is_done(issuer_id))
- prev_state->mark_todo(issuer_id);
- else
- XBT_DEBUG("Actor %ld is in done set", issuer_id);
+ if (prev_state->is_actor_enabled(issuer_id)){
+ if (not prev_state->is_done(issuer_id))
+ prev_state->mark_todo(issuer_id);
+ else
+ XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
+ } else {
+ XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing, to stay sound, we are marking every enabled transition todo", issuer_id);
+ prev_state->mark_all_todo();
+ }
break;
} else {
XBT_VERB("INDEPENDENT Transitions:");
XBT_DEBUG("Delete state %ld at depth %zu", state->get_num(), stack_.size() + 1);
} else {
- XBT_DEBUG("Back-tracking to state %ld at depth %zu", state->get_num(), stack_.size() + 1);
+ XBT_DEBUG("Back-tracking to state %ld at depth %zu: %ld transitions left to be explored", state->get_num(), stack_.size() + 1, state->count_todo());
stack_.push_back(std::move(state)); // Put it back on the stack
found_backtracking_point = true;
}
