* is important in cases
*/
class ActorState {
-
/**
* @brief The transitions that the actor is allowed to execute from this
* state, viz. those that are enabled for this actor
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)
{
long State::expended_states_ = 0;
- State::State(const RemoteApp& remote_app) : default_transition(std::make_unique<Transition>()), num_(++expended_states_)
+ State::State(const RemoteApp& remote_app) : num_(++expended_states_)
{
remote_app.get_actors_status(actors_to_run_);
- transition_ = default_transition.get();
-
/* 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_);
}
}
+State::State(const RemoteApp& remote_app, const State* previous_state)
+ : default_transition(std::make_unique<Transition>()), num_(++expended_states_)
+{
+
+ remote_app.get_actors_status(actors_to_run_);
+
+ transition_ = default_transition.get();
+
+ /* 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
{
- if (transition_ == nullptr) {
- return default_transition.get();
- }
- 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;
}
class XBT_PRIVATE State : public xbt::Extendable<State> {
static long expended_states_; /* Count total amount of states, for stats */
+ /**
+ * @brief An empty transition that leads to this state by default
+ */
+ const std::unique_ptr<Transition> default_transition_ = std::make_unique<Transition>();
+
/**
* @brief The outgoing transition: what was the last transition that
* we took to leave this state?
* or a reference to the internal default transition `Transition()` if no transition has been
* set
*/
- Transition* transition_ = nullptr;
-
- /**
- * @brief An empty transition that leads to this state by default
- */
- const std::unique_ptr<Transition> default_transition;
+ Transition* transition_ = default_transition_.get();
/** Sequential state ID (used for debugging) */
long num_ = 0;
/** Snapshot of system state (if needed) */
std::shared_ptr<Snapshot> system_state_;
+ /* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep
+ * set. With this information, it is check whether it should be removed from it or not when exploring a new
+ * transition */
+ 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_ = 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 add_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_; }
};
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_replay.hpp"
+ #include "src/simgrid/sg_config.hpp"
#include <simgrid/modelchecker.h>
- #include <simgrid/sg_config.hpp>
#if SIMGRID_HAVE_MC
#include <string_view>
xbt_die("configuration option 'model-check/reduction' can only take 'none' or 'dpor' as a value");
}};
+simgrid::config::Flag<bool> _sg_mc_sleep_set{
+ "model-check/sleep-set", "Whether to enable the use of sleep-set in the reduction algorithm", false,
+ [](bool) { _mc_cfg_cb_check("value to enable/disable the use of sleep-set in the reduction algorithm"); }};
+
simgrid::config::Flag<int> _sg_mc_checkpoint{
"model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking "
"(default: 0 => stateless verification). If value=1, one checkpoint is saved for each "
