State::State(RemoteApp& remote_app, const State* parent_state)
: num_(++expended_states_), parent_state_(parent_state), guide(std::make_unique<BasicGuide>())
{
-
remote_app.get_actors_status(guide->actors_to_run_);
/* Stateful model checking */
* 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] : parent_state_->get_sleep_set()) {
-
if (not parent_state_->get_transition()->depends(&transition)) {
-
sleep_set_.try_emplace(aid, transition);
if (guide->actors_to_run_.count(aid) != 0) {
XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
for (auto const& [aid, actor] : guide->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() || actor.is_done()) {
-
if (not actor.is_todo())
XBT_DEBUG("Can't run actor %ld because it is not todo", aid);
public:
std::pair<aid_t, double> next_transition() const override
{
-
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() || actor.is_done()) {
// exploration would lead to a so-called
// "sleep-set blocked" trace.
if (enC.is_subset_of(D)) {
-
if (not C.get_events().empty()) {
// Report information...
}
constexpr unsigned K = 10;
if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
-
// Before searching the "right half", we need to make
// sure the program actually reflects the fact
// that we are searching again from `stateC` (the recursive