- return SimcallObserver::dot_label(times_considered) + "Sem ACQUIRE";
-}
-
-bool SemAcquireSimcall::is_enabled() const
-{
- 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;
-}
-
-int ActivityTestanySimcall::get_max_consider() const
-{
- // 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;
-}
-
-void ActivityTestanySimcall::prepare(int times_considered)
-{
- next_value_ = times_considered;
-}
-
-/*
-std::string ActivityTestanySimcall::to_string(int times_considered) const
-{
- 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;
-}*/
-
-std::string ActivityTestanySimcall::dot_label(int times_considered) const
-{
- std::string res = SimcallObserver::dot_label(times_considered) + "TestAny ";
- if (times_considered == -1) {
- res += "FALSE";
- } else {
- res += xbt::string_printf("TRUE [%d of %zu]", times_considered + 1, activities_.size());
- }
- return res;
-}
-
-bool ActivityTestSimcall::depends(SimcallObserver* other)
-{
- if (get_issuer() == other->get_issuer())
- return false;
-
- if (dynamic_cast<ActivityTestSimcall*>(other))
- return true;
-
- const auto* comm1 = dynamic_cast<activity::CommImpl*>(activity_);
- if (comm1 == nullptr)
- return false;
-
- if (dynamic_cast<ActivityWaitSimcall*>(other) != nullptr &&
- (comm1->src_actor_.get() == nullptr || comm1->dst_actor_.get() == nullptr))
- return false;
-
- if (comm1->src_buff_ == nullptr || comm1->dst_buff_ == nullptr)
- return false;
-
- if (const auto* test = dynamic_cast<ActivityTestSimcall*>(other)) {
- const auto* comm2 = dynamic_cast<activity::CommImpl*>(test->get_activity());
- if (comm2 == nullptr)
- return false;
- else if (comm2->src_buff_ == nullptr || comm2->dst_buff_ == nullptr)
- return false;
- }
-
- if (auto* wait = dynamic_cast<ActivityWaitSimcall*>(other)) {
- auto* comm2 = dynamic_cast<activity::CommImpl*>(wait->get_activity());
- if (comm2 == nullptr)
- return false;
- if (comm1->src_buff_ == comm2->src_buff_ && comm1->dst_buff_ == comm2->dst_buff_)
- return false;
- if (comm1->src_buff_ != nullptr && comm1->dst_buff_ != nullptr && comm2->src_buff_ != nullptr &&
- comm2->dst_buff_ != nullptr && comm1->dst_buff_ != comm2->src_buff_ && comm1->dst_buff_ != comm2->dst_buff_ &&
- comm2->dst_buff_ != comm1->src_buff_)
- return false;
- }
-
- return true;
-}
-void ActivityWaitSimcall::serialize(Simcall& type, char* buffer)
-{
- std::stringstream stream;
- if (auto* comm = dynamic_cast<activity::CommImpl*>(activity_)) {
- type = Simcall::COMM_WAIT;
- stream << timeout_ << ' ' << 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() != nullptr ? comm->get_mailbox()->get_id() : 666);
- stream << ' ' << (void*)comm->src_buff_ << ' ' << (void*)comm->dst_buff_ << ' ' << comm->src_buff_size_;
- strcpy(buffer, stream.str().c_str());
- } else {
- type = Simcall::UNKNOWN;
- strcpy(buffer, stream.str().c_str());
- }