X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/41966a6d30f870c0c7cc5ad5e64c0263e63970a8..3f9b311ec56db95ec539001a860ae3c838c48312:/src/mc/transition/TransitionAny.cpp diff --git a/src/mc/transition/TransitionAny.cpp b/src/mc/transition/TransitionAny.cpp index 0f10bb1080..b3c7b63cb3 100644 --- a/src/mc/transition/TransitionAny.cpp +++ b/src/mc/transition/TransitionAny.cpp @@ -7,10 +7,6 @@ #include "simgrid/config.h" #include "xbt/asserts.h" #include "xbt/string.hpp" -#if SIMGRID_HAVE_MC -#include "src/mc/api/RemoteApp.hpp" -#include "src/mc/api/State.hpp" -#endif #include @@ -25,22 +21,35 @@ TestAnyTransition::TestAnyTransition(aid_t issuer, int times_considered, std::st xbt_assert(stream >> size); for (int i = 0; i < size; i++) { Transition* t = deserialize_transition(issuer, 0, stream); - XBT_DEBUG("TestAny received a transition %s", t->to_string(true).c_str()); + XBT_INFO("TestAny received a transition %s", t->to_string(true).c_str()); transitions_.push_back(t); } } std::string TestAnyTransition::to_string(bool verbose) const { - auto res = xbt::string_printf("TestAny{ "); - for (auto const* t : transitions_) + auto res = xbt::string_printf("TestAny(%s){ ", this->result() ? "TRUE" : "FALSE"); + for (auto const* t : transitions_) { res += t->to_string(verbose); + res += "; "; + } res += " }"; return res; } bool TestAnyTransition::depends(const Transition* other) const { + // Actions executed by the same actor are always dependent + if (other->aid_ == aid_) + return true; + return transitions_[times_considered_]->depends(other); } +bool TestAnyTransition::reversible_race(const Transition* other) const +{ + xbt_assert(type_ == Type::TESTANY, "Unexpected transition type %s", to_c_str(type_)); + + return true; // TestAny is always enabled +} + WaitAnyTransition::WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream) : Transition(Type::WAITANY, issuer, times_considered) { @@ -48,6 +57,7 @@ WaitAnyTransition::WaitAnyTransition(aid_t issuer, int times_considered, std::st xbt_assert(stream >> size); for (int i = 0; i < size; i++) { Transition* t = deserialize_transition(issuer, 0, stream); + XBT_INFO("WaitAny received transition %d/%d %s", (i + 1), size, t->to_string(true).c_str()); transitions_.push_back(t); } } @@ -56,12 +66,22 @@ std::string WaitAnyTransition::to_string(bool verbose) const auto res = xbt::string_printf("WaitAny{ "); for (auto const* t : transitions_) res += t->to_string(verbose); - res += " }"; + res += " } (times considered = " + std::to_string(times_considered_) + ")"; return res; } bool WaitAnyTransition::depends(const Transition* other) const { + // Actions executed by the same actor are always dependent + if (other->aid_ == aid_) + return true; return transitions_[times_considered_]->depends(other); } +bool WaitAnyTransition::reversible_race(const Transition* other) const +{ + xbt_assert(type_ == Type::WAITANY, "Unexpected transition type %s", to_c_str(type_)); + + // TODO: We need to check if any of the transitions waited on occurred before `e1` + return true; // Let's overapproximate to not miss branches +} } // namespace simgrid::mc