- static bool warned = false;
- if (not warned) {
- XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk");
- warned = true;
- }
- return true;
-}
-
-ActivityTestanySimcall::ActivityTestanySimcall(ActorImpl* actor, const std::vector<activity::ActivityImpl*>& activities)
- : ResultingSimcall(actor, -1), activities_(activities)
-{
-}
-
-int ActivityTestanySimcall::get_max_consider()
-{
- indexes_.clear();
- // 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);
- return indexes_.size() + 1;
-}
-
-void ActivityTestanySimcall::prepare(int times_considered)
-{
- if (times_considered < static_cast<int>(indexes_.size()))
- next_value_ = indexes_.at(times_considered);
- else
- next_value_ = -1;
-}
-static void serialize_activity_test(const activity::ActivityImpl* act, std::stringstream& stream)
-{
- if (auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
- stream << " " << (short)mc::Transition::Type::COMM_TEST;
- stream << ' ' << (uintptr_t)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 << ' ' << (uintptr_t)comm->src_buff_ << ' ' << (uintptr_t)comm->dst_buff_ << ' ' << comm->src_buff_size_;
- } else {
- stream << (short)mc::Transition::Type::UNKNOWN;
- }
-}
-void ActivityTestanySimcall::serialize(std::stringstream& stream) const
-{
- stream << (short)mc::Transition::Type::TESTANY << ' ' << activities_.size() << ' ';
- for (auto const& act : activities_) {
- serialize_activity_test(act, stream);
- stream << ' ';
- }
-}
-void ActivityTestSimcall::serialize(std::stringstream& stream) const
-{
- serialize_activity_test(activity_, stream);