namespace simgrid {
namespace mc {
+/** A channel for exchanging messages between model-checker and model-checked
+ *
+ * This hides the way the messages are transfered. Currently, they are sent
+ * over a SOCK_DGRAM socket.
+ */
class Channel {
int socket_ = -1;
template<class M>
namespace simgrid {
namespace mc {
+/** Model-checked-side of the communication protocol
+ *
+ * Send messages to the model-checker and handles message from it.
+ */
class XBT_PUBLIC() Client {
private:
bool active_ = false;
}
-// TODO, deduplicate with SafetyChecker
RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
{
RecordTrace res;
return res;
}
-// TODO, deduplicate with SafetyChecker
std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
{
std::vector<std::string> trace;
namespace simgrid {
namespace mc {
-/** Can this requests can be executed.
+/** Can this requests can be executed?
*
* Most requests are always enabled but WAIT and WAITANY
* are not always enabled: a WAIT where the communication does not
simgrid::mc::Process* process = &mc_model_checker->process();
- /* Horrible hack to find the offset of the id in the simgrid::s4u::Host.
+ /* HACK, Horrible hack to find the offset of the id in the simgrid::s4u::Host.
Offsetof is not supported for non-POD types but this should
work in pratice for the targets currently supported by the MC