return true;
}
-int ActivityTestanySimcall::get_max_consider() const
+ActivityTestanySimcall::ActivityTestanySimcall(ActorImpl* actor, const std::vector<activity::ActivityImpl*>& activities)
+ : ResultingSimcall(actor, -1), activities_(activities)
{
- // Only Comms are of interest to MC for now. When all types of activities can be consider, this function can simply
- // return the size of activities_.
- int count = 0;
- for (const auto& act : activities_)
- if (dynamic_cast<activity::CommImpl*>(act) != nullptr)
- count++;
- return count;
+ // list all the activities that are ready
+ for (unsigned i = 0; i < activities_.size(); i++)
+ if (activities_[i]->test(get_issuer()))
+ indexes_.push_back(i);
}
-void ActivityTestanySimcall::prepare(int times_considered)
+int ActivityTestanySimcall::get_max_consider() const
{
- next_value_ = times_considered;
+ return indexes_.size() + 1;
}
-/*
-std::string ActivityTestanySimcall::to_string(int times_considered) const
+void ActivityTestanySimcall::prepare(int times_considered)
{
- std::string res = SimcallObserver::to_string(times_considered);
- if (times_considered == -1) {
- res += "TestAny FALSE(-)";
- } else {
- res += "TestAny(" + xbt::string_printf("(%d of %zu)", times_considered + 1, activities_.size());
- }
-
- return res;
-}*/
-void ActivityWaitSimcall::serialize(std::stringstream& stream) const
+ if (times_considered < static_cast<int>(indexes_.size()))
+ next_value_ = indexes_.at(times_considered);
+ else
+ next_value_ = -1;
+}
+static void serialize_activity(const activity::ActivityImpl* act, std::stringstream& stream)
{
- if (auto* comm = dynamic_cast<activity::CommImpl*>(activity_)) {
- stream << (short)mc::Transition::Type::COMM_WAIT << ' ';
- stream << (timeout_ > 0) << ' ' << comm;
+ if (auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
+ stream << (short)mc::Transition::Type::COMM_TEST << ' ';
stream << ' ' << (comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1);
stream << ' ' << (comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1);
stream << ' ' << comm->get_mailbox_id();
stream << (short)mc::Transition::Type::UNKNOWN;
}
}
-void ActivityTestSimcall::serialize(std::stringstream& stream) const
+void ActivityTestanySimcall::serialize(std::stringstream& stream) const
+{
+ stream << (short)mc::Transition::Type::TESTANY << ' ' << activities_.size() << ' ';
+ for (auto const& act : activities_)
+ serialize_activity(act, stream);
+}
+void ActivityWaitSimcall::serialize(std::stringstream& stream) const
{
if (auto* comm = dynamic_cast<activity::CommImpl*>(activity_)) {
- stream << (short)mc::Transition::Type::COMM_TEST << ' ';
+ stream << (short)mc::Transition::Type::COMM_WAIT << ' ';
+ stream << (timeout_ > 0) << ' ' << comm;
stream << ' ' << (comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1);
stream << ' ' << (comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1);
stream << ' ' << comm->get_mailbox_id();
stream << (short)mc::Transition::Type::UNKNOWN;
}
}
+void ActivityTestSimcall::serialize(std::stringstream& stream) const
+{
+ serialize_activity(activity_, stream);
+}
bool ActivityWaitSimcall::is_enabled() const
{
class ActivityTestanySimcall : public ResultingSimcall<ssize_t> {
const std::vector<activity::ActivityImpl*>& activities_;
+ std::vector<int> indexes_; // indexes in activities_ pointing to ready activities (=whose test() is positive)
int next_value_ = 0;
public:
- ActivityTestanySimcall(ActorImpl* actor, const std::vector<activity::ActivityImpl*>& activities)
- : ResultingSimcall(actor, -1), activities_(activities)
- {
- }
+ ActivityTestanySimcall(ActorImpl* actor, const std::vector<activity::ActivityImpl*>& activities);
bool is_visible() const override { return true; }
+ bool is_enabled() const override { return true; /* can return -1 if no activity is ready */ }
+ void serialize(std::stringstream& stream) const override;
int get_max_consider() const override;
void prepare(int times_considered) override;
const std::vector<activity::ActivityImpl*>& get_activities() const { return activities_; }
if (this->remote_process_->running())
checker_side_.dispatch(); // The app may send messages while processing the transition
- if (new_transition)
- return recv_transition(aid, times_considered, answer.buffer);
- else
+ if (new_transition) {
+ std::stringstream stream(answer.buffer);
+ return recv_transition(aid, times_considered, stream);
+ } else
return nullptr;
}
bool ModelChecker::simcall_is_visible(aid_t aid)
friend State; // FIXME remove this once we have a proper class to handle the statistics
public:
- XBT_DECLARE_ENUM_CLASS(Type, UNKNOWN, RANDOM, COMM_RECV, COMM_SEND, COMM_TEST, COMM_WAIT);
+ XBT_DECLARE_ENUM_CLASS(Type, UNKNOWN, RANDOM, COMM_RECV, COMM_SEND, COMM_TEST, COMM_WAIT, TESTANY);
Type type_ = Type::UNKNOWN;
aid_t aid_ = 0;
res += ")";
return res;
}
+TestAnyTransition::TestAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
+{
+ int size;
+ stream >> size;
+ for (int i = 0; i < size; i++) {
+
+ Transition* t = recv_transition(issuer, 0, stream);
+ transitions_.push_back(t);
+ }
+}
+std::string TestAnyTransition::to_string(bool verbose) const
+{
+ auto res = xbt::string_printf("%ld: TestAny{ ", aid_);
+ for (auto const* t : transitions_)
+ res += t->to_string(verbose);
+ res += "}";
+ return res;
+}
+bool TestAnyTransition::depends(const Transition* other) const
+{
+ return true;
+}
bool CommSendTransition::depends(const Transition* other) const
{
return true;
}
-Transition* recv_transition(aid_t issuer, int times_considered, char* buffer)
+Transition* recv_transition(aid_t issuer, int times_considered, std::stringstream& stream)
{
- std::stringstream stream(buffer);
short type;
stream >> type;
Transition::Type simcall = static_cast<Transition::Type>(type);
case Transition::Type::COMM_WAIT:
return new CommWaitTransition(issuer, times_considered, stream);
+ case Transition::Type::TESTANY:
+ return new TestAnyTransition(issuer, times_considered, stream);
+
case Transition::Type::RANDOM:
return new RandomTransition(issuer, times_considered, stream);
bool depends(const Transition* other) const override;
};
+class TestAnyTransition : public Transition {
+ std::vector<Transition*> transitions_;
+
+public:
+ TestAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream);
+ std::string to_string(bool verbose) const override;
+ bool depends(const Transition* other) const override;
+};
+
/** Make a new transition from serialized description */
-Transition* recv_transition(aid_t issuer, int times_considered, char* buffer);
+Transition* recv_transition(aid_t issuer, int times_considered, std::stringstream& stream);
} // namespace mc
} // namespace simgrid
continue;
}
- /* Actually answer the request: let execute the selected request (MCed does one step) */
+ /* Actually answer the request: let's execute the selected request (MCed does one step) */
state->execute_next(next);
// If there are processes to interleave and the maximum depth has not been
req_str = api::get().request_get_dot_output(state->get_transition());
/* Create the new expanded state (copy the state of MCed into our MCer data) */
- auto next_state = std::make_unique<State>();
+ auto next_state = std::make_unique<State>();
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
engine->reset_actor_dynar();
for (auto const& kv : engine->get_actor_list()) {
auto actor = kv.second;
- if (actor->simcall_.observer_ != nullptr)
- actor->simcall_.mc_max_consider_ = actor->simcall_.observer_->get_max_consider();
+ if (auto* observer = actor->simcall_.observer_)
+ actor->simcall_.mc_max_consider_ = observer->get_max_consider();
engine->add_actor_to_dynar(actor);
}
#endif
