XBT_VERB("Creating a guide for the state");
if (_sg_mc_strategy == "none")
strategy_ = std::make_shared<BasicStrategy>();
- if (_sg_mc_strategy == "nb_wait")
+ else if (_sg_mc_strategy == "nb_wait")
strategy_ = std::make_shared<WaitStrategy>();
+ else
+ THROW_IMPOSSIBLE;
recipe_ = std::list<Transition*>();
remote_app.get_actors_status(strategy_->actors_to_run_);
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
/* 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(),
State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
: num_(++expended_states_), parent_state_(parent_state)
{
-
if (_sg_mc_strategy == "none")
strategy_ = std::make_shared<BasicStrategy>();
- if (_sg_mc_strategy == "nb_wait")
+ else if (_sg_mc_strategy == "nb_wait")
strategy_ = std::make_shared<WaitStrategy>();
+ else
+ THROW_IMPOSSIBLE;
*strategy_ = *(parent_state->strategy_);
recipe_ = std::list(parent_state_->get_recipe());
remote_app.get_actors_status(strategy_->actors_to_run_);
- /* Stateful model checking */
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC /* 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(),
*remote_app.get_remote_process_memory());
std::size_t State::count_todo_multiples() const
{
size_t count = 0;
- for (auto& [_, actor] : strategy_->actors_to_run_)
+ for (auto const& [_, actor] : strategy_->actors_to_run_)
if (actor.is_todo())
count += actor.get_times_not_considered();
return -1;
}
-std::pair<aid_t, double> State::next_transition_guided() const
+std::pair<aid_t, int> State::next_transition_guided() const
{
return strategy_->next_transition();
}