include src/mc/api.hpp
include src/mc/api/State.cpp
include src/mc/api/State.hpp
-include src/mc/api/Transition.cpp
-include src/mc/api/Transition.hpp
-include src/mc/api/TransitionComm.cpp
-include src/mc/api/TransitionComm.hpp
include src/mc/checker/Checker.hpp
include src/mc/checker/CommunicationDeterminismChecker.cpp
include src/mc/checker/LivenessChecker.cpp
include src/mc/sosp/Snapshot.cpp
include src/mc/sosp/Snapshot.hpp
include src/mc/sosp/Snapshot_test.cpp
+include src/mc/transition/Transition.cpp
+include src/mc/transition/Transition.hpp
+include src/mc/transition/TransitionAny.cpp
+include src/mc/transition/TransitionAny.hpp
+include src/mc/transition/TransitionComm.cpp
+include src/mc/transition/TransitionComm.hpp
+include src/mc/transition/TransitionRandom.cpp
+include src/mc/transition/TransitionRandom.hpp
include src/mc/udpor_global.cpp
include src/mc/udpor_global.hpp
include src/msg/msg_comm.cpp
#define SIMGRID_MC_SIMCALL_OBSERVER_HPP
#include "simgrid/forward.h"
-#include "src/mc/api/Transition.hpp"
+#include "src/mc/transition/Transition.hpp"
#include "xbt/asserts.h"
#include <string>
#include "src/mc/ModelChecker.hpp"
#include "src/mc/Session.hpp"
-#include "src/mc/api/Transition.hpp"
-#include "src/mc/api/TransitionComm.hpp"
#include "src/mc/checker/Checker.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/remote/RemoteProcess.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
#include "xbt/automaton.hpp"
#include "xbt/system_error.hpp"
#ifndef SIMGRID_MC_STATE_HPP
#define SIMGRID_MC_STATE_HPP
-#include "src/mc/api/Transition.hpp"
#include "src/mc/mc_pattern.hpp"
#include "src/mc/sosp/Snapshot.hpp"
+#include "src/mc/transition/Transition.hpp"
namespace simgrid {
namespace mc {
#include "src/kernel/activity/MailboxImpl.hpp"
#include "src/mc/Session.hpp"
-#include "src/mc/api/TransitionComm.hpp"
#include "src/mc/checker/SafetyChecker.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
+#include "src/mc/transition/TransitionAny.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
#include <cstdint>
#include "src/mc/checker/SafetyChecker.hpp"
#include "src/mc/Session.hpp"
#include "src/mc/VisitedState.hpp"
-#include "src/mc/api/Transition.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_record.hpp"
+#include "src/mc/transition/Transition.hpp"
#include "src/xbt/mmalloc/mmprivate.h"
#include "xbt/log.h"
#include "src/mc/mc_record.hpp"
#include "src/kernel/activity/CommImpl.hpp"
#include "src/kernel/context/Context.hpp"
-#include "src/mc/api/Transition.hpp"
#include "src/mc/mc_base.hpp"
#include "src/mc/mc_replay.hpp"
+#include "src/mc/transition/Transition.hpp"
#if SIMGRID_HAVE_MC
#include "src/mc/api/State.hpp"
--- /dev/null
+/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/transition/Transition.hpp"
+#include "xbt/asserts.h"
+#include "xbt/string.hpp"
+#include <simgrid/config.h>
+
+#if SIMGRID_HAVE_MC
+#include "src/mc/ModelChecker.hpp"
+#include "src/mc/transition/TransitionAny.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
+#include "src/mc/transition/TransitionRandom.hpp"
+#endif
+
+#include <sstream>
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_transition, mc, "Logging specific to MC transitions");
+
+namespace simgrid {
+namespace mc {
+unsigned long Transition::executed_transitions_ = 0;
+unsigned long Transition::replayed_transitions_ = 0;
+
+// Do not move this to the header, to ensure that we have a vtable for Transition
+Transition::~Transition() = default;
+
+std::string Transition::to_string(bool) const
+{
+ return "";
+}
+std::string Transition::dot_label() const
+{
+ return xbt::string_printf("[(%ld)] %s", aid_, Transition::to_c_str(type_));
+}
+void Transition::replay() const
+{
+ replayed_transitions_++;
+
+#if SIMGRID_HAVE_MC
+ mc_model_checker->handle_simcall(aid_, times_considered_, false);
+ mc_model_checker->wait_for_requests();
+#endif
+}
+
+Transition* deserialize_transition(aid_t issuer, int times_considered, std::stringstream& stream)
+{
+#if SIMGRID_HAVE_MC
+ short type;
+ xbt_assert(stream >> type);
+ xbt_assert(type >= 0 && type <= static_cast<short>(Transition::Type::UNKNOWN), "Invalid transition type %d received",
+ type);
+
+ auto simcall = static_cast<Transition::Type>(type);
+
+ switch (simcall) {
+ case Transition::Type::COMM_RECV:
+ return new CommRecvTransition(issuer, times_considered, stream);
+ case Transition::Type::COMM_SEND:
+ return new CommSendTransition(issuer, times_considered, stream);
+ case Transition::Type::COMM_TEST:
+ return new CommTestTransition(issuer, times_considered, stream);
+ 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::WAITANY:
+ return new WaitAnyTransition(issuer, times_considered, stream);
+
+ case Transition::Type::RANDOM:
+ return new RandomTransition(issuer, times_considered, stream);
+
+ case Transition::Type::UNKNOWN:
+ return new Transition(Transition::Type::UNKNOWN, issuer, times_considered);
+ }
+ THROW_IMPOSSIBLE; // Some compilers don't detect that each branch of the above switch has a return
+#else
+ xbt_die("Deserializing transitions is only interesting in MC mode.");
+#endif
+}
+
+} // namespace mc
+} // namespace simgrid
-/* Copyright (c) 2015-2022. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
static unsigned long get_replayed_transitions() { return replayed_transitions_; }
};
-class RandomTransition : public Transition {
- int min_;
- int max_;
-
-public:
- std::string to_string(bool verbose) const override;
- std::string dot_label() const override;
- RandomTransition(aid_t issuer, int times_considered, std::stringstream& stream);
- bool depends(const Transition* other) const override { return false; } // Independent with any other transition
-};
+/** Make a new transition from serialized description */
+Transition* deserialize_transition(aid_t issuer, int times_considered, std::stringstream& stream);
} // namespace mc
} // namespace simgrid
--- /dev/null
+/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/transition/TransitionAny.hpp"
+#include "xbt/asserts.h"
+#include <simgrid/config.h>
+#if SIMGRID_HAVE_MC
+#include "src/mc/ModelChecker.hpp"
+#include "src/mc/Session.hpp"
+#include "src/mc/api/State.hpp"
+#endif
+
+#include <sstream>
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_any, mc_transition, "Logging specific to MC WaitAny / TestAny transitions");
+
+namespace simgrid {
+namespace mc {
+
+TestAnyTransition::TestAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
+ : Transition(Type::TESTANY, issuer, times_considered)
+{
+ int size;
+ 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());
+ 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 transitions_[times_considered_]->depends(other);
+}
+WaitAnyTransition::WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
+ : Transition(Type::WAITANY, issuer, times_considered)
+{
+ int size;
+ xbt_assert(stream >> size);
+ for (int i = 0; i < size; i++) {
+ Transition* t = deserialize_transition(issuer, 0, stream);
+ transitions_.push_back(t);
+ }
+}
+std::string WaitAnyTransition::to_string(bool verbose) const
+{
+ auto res = xbt::string_printf("%ld: WaitAny{ ", aid_);
+ for (auto const* t : transitions_)
+ res += t->to_string(verbose);
+ res += "}";
+ return res;
+}
+bool WaitAnyTransition::depends(const Transition* other) const
+{
+ return transitions_[times_considered_]->depends(other);
+}
+
+} // namespace mc
+} // namespace simgrid
--- /dev/null
+/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_TRANSITION_ANY_HPP
+#define SIMGRID_MC_TRANSITION_ANY_HPP
+
+#include "src/kernel/actor/SimcallObserver.hpp"
+#include "src/mc/transition/Transition.hpp"
+
+#include <sstream>
+#include <string>
+
+namespace simgrid {
+namespace mc {
+
+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;
+
+ Transition* get_current_transition() const { return transitions_.at(times_considered_); }
+};
+
+class WaitAnyTransition : public Transition {
+ std::vector<Transition*> transitions_;
+
+public:
+ WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream);
+ std::string to_string(bool verbose) const override;
+ bool depends(const Transition* other) const override;
+
+ Transition* get_current_transition() const { return transitions_.at(times_considered_); }
+};
+
+} // namespace mc
+} // namespace simgrid
+
+#endif
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
-#include "src/mc/api/TransitionComm.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
#include "xbt/asserts.h"
#include <simgrid/config.h>
#if SIMGRID_HAVE_MC
res += ")";
return res;
}
-TestAnyTransition::TestAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
- : Transition(Type::TESTANY, issuer, times_considered)
-{
- int size;
- 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());
- 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 transitions_[times_considered_]->depends(other);
-}
-WaitAnyTransition::WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
- : Transition(Type::WAITANY, issuer, times_considered)
-{
- int size;
- xbt_assert(stream >> size);
- for (int i = 0; i < size; i++) {
- Transition* t = deserialize_transition(issuer, 0, stream);
- transitions_.push_back(t);
- }
-}
-std::string WaitAnyTransition::to_string(bool verbose) const
-{
- auto res = xbt::string_printf("%ld: WaitAny{ ", aid_);
- for (auto const* t : transitions_)
- res += t->to_string(verbose);
- res += "}";
- return res;
-}
-bool WaitAnyTransition::depends(const Transition* other) const
-{
- return transitions_[times_considered_]->depends(other);
-}
bool CommSendTransition::depends(const Transition* other) const
{
return true;
}
-Transition* deserialize_transition(aid_t issuer, int times_considered, std::stringstream& stream)
-{
- short type;
- xbt_assert(stream >> type);
- xbt_assert(type >= 0 && type <= static_cast<short>(Transition::Type::UNKNOWN), "Invalid transition type %d received",
- type);
-
- auto simcall = static_cast<Transition::Type>(type);
-
- switch (simcall) {
- case Transition::Type::COMM_RECV:
- return new CommRecvTransition(issuer, times_considered, stream);
- case Transition::Type::COMM_SEND:
- return new CommSendTransition(issuer, times_considered, stream);
- case Transition::Type::COMM_TEST:
- return new CommTestTransition(issuer, times_considered, stream);
- 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::WAITANY:
- return new WaitAnyTransition(issuer, times_considered, stream);
-
- case Transition::Type::RANDOM:
- return new RandomTransition(issuer, times_considered, stream);
-
- case Transition::Type::UNKNOWN:
- return new Transition(Transition::Type::UNKNOWN, issuer, times_considered);
- }
- THROW_IMPOSSIBLE; // Some compilers don't detect that each branch of the above switch has a return
-}
-
} // namespace mc
} // namespace simgrid
-/* Copyright (c) 2015-2022. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
#define SIMGRID_MC_TRANSITION_COMM_HPP
#include "src/kernel/actor/SimcallObserver.hpp"
-#include "src/mc/api/Transition.hpp"
+#include "src/mc/transition/Transition.hpp"
#include <sstream>
#include <string>
int get_tag() const { return tag_; }
};
-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;
-
- Transition* get_current_transition() const { return transitions_.at(times_considered_); }
-};
-
-class WaitAnyTransition : public Transition {
- std::vector<Transition*> transitions_;
-
-public:
- WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream);
- std::string to_string(bool verbose) const override;
- bool depends(const Transition* other) const override;
-
- Transition* get_current_transition() const { return transitions_.at(times_considered_); }
-};
-
/** Make a new transition from serialized description */
Transition* deserialize_transition(aid_t issuer, int times_considered, std::stringstream& stream);
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
-#include "src/mc/api/Transition.hpp"
+#include "src/mc/transition/TransitionRandom.hpp"
#include "xbt/asserts.h"
#include "xbt/string.hpp"
-#include <simgrid/config.h>
-
-#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
-#endif
#include <sstream>
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_transition, mc, "Logging specific to MC transitions");
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_rand, mc_transition, "Logging specific to MC Random transitions");
namespace simgrid {
namespace mc {
-unsigned long Transition::executed_transitions_ = 0;
-unsigned long Transition::replayed_transitions_ = 0;
-
-// Do not move this to the header, to ensure that we have a vtable for Transition
-Transition::~Transition() = default;
-
-std::string Transition::to_string(bool) const
-{
- return "";
-}
-std::string Transition::dot_label() const
-{
- return xbt::string_printf("[(%ld)] %s", aid_, Transition::to_c_str(type_));
-}
-void Transition::replay() const
-{
- replayed_transitions_++;
-
-#if SIMGRID_HAVE_MC
- mc_model_checker->handle_simcall(aid_, times_considered_, false);
- mc_model_checker->wait_for_requests();
-#endif
-}
std::string RandomTransition::to_string(bool verbose) const
{
return xbt::string_printf("Random([%d;%d] ~> %d)", min_, max_, times_considered_);
--- /dev/null
+/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_TRANSITION_RANDOM_HPP
+#define SIMGRID_MC_TRANSITION_RANDOM_HPP
+
+#include "src/mc/transition/Transition.hpp"
+
+namespace simgrid {
+namespace mc {
+
+class RandomTransition : public Transition {
+ int min_;
+ int max_;
+
+public:
+ std::string to_string(bool verbose) const override;
+ std::string dot_label() const override;
+ RandomTransition(aid_t issuer, int times_considered, std::stringstream& stream);
+ bool depends(const Transition* other) const override { return false; } // Independent with any other transition
+};
+
+} // namespace mc
+} // namespace simgrid
+
+#endif
src/mc/mc_config.cpp
src/mc/mc_config.hpp
src/mc/mc_global.cpp
- src/mc/api/Transition.cpp
+ src/mc/transition/Transition.cpp
)
set(MC_SRC
src/mc/mc_exit.hpp
src/mc/api/State.hpp
src/mc/api/State.cpp
- src/mc/api/Transition.hpp
- src/mc/api/TransitionComm.cpp
- src/mc/api/TransitionComm.hpp
+ src/mc/transition/Transition.hpp
+ src/mc/transition/TransitionAny.cpp
+ src/mc/transition/TransitionAny.hpp
+ src/mc/transition/TransitionComm.cpp
+ src/mc/transition/TransitionComm.hpp
+ src/mc/transition/TransitionRandom.cpp
+ src/mc/transition/TransitionRandom.hpp
src/mc/udpor_global.cpp
src/mc/udpor_global.hpp
)
