remote_app.get_actors_status(strategy_->actors_to_run_);
+ for (auto const& [aid, _] : strategy_->actors_to_run_)
+ strategy_->penalties_[aid] = parent_state_->strategy_->penalties_[aid];
+
/* 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_, remote_app.get_page_store(),
{
XBT_DEBUG("Search for an actor to run. %zu actors to consider", strategy_->actors_to_run_.size());
for (auto const& [aid, actor] : strategy_->actors_to_run_) {
- XBT_DEBUG("Current penalty for actor %ld:%f", aid, strategy_->penalties_[aid]);
/* 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())
std::pair<aid_t, double> State::next_transition_guided() const
{
+
+ for (auto const& [aid, penalty] : strategy_->penalties_)
+ XBT_DEBUG("Current penalty for actor %ld:%f", aid, strategy_->penalties_[aid]);
+
for (auto const& [aid, actor] : strategy_->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);
void execute_next(aid_t aid, RemoteApp& app) override
{
auto actor = actors_to_run_.at(aid);
- if (actor.get_transition(actor.get_times_considered())->type_ != Transition::Type::TESTANY)
- penalties_[aid] += 1.0;
+ if (actor.get_transition(actor.get_times_considered())->type_ == Transition::Type::TESTANY)
+ penalties_[aid] = penalties_[aid] + 1.0;
return;
}