Avoid using should-be-private-stuff oustside of State.
RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
{
RecordTrace res;
- for (auto const& state : stack_) {
- int value = 0;
- smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
- const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
- const int pid = issuer->pid;
- res.push_back(RecordTraceElement(pid, value));
- }
+ for (auto const& state : stack_)
+ res.push_back(state->getRecordElement());
return res;
}
RecordTrace LivenessChecker::getRecordTrace() // override
{
RecordTrace res;
- for (std::shared_ptr<Pair> const& pair : explorationStack_) {
- int value;
- smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
- if (req && req->call != SIMCALL_NONE) {
- smx_process_t issuer = MC_smx_simcall_get_issuer(req);
- const int pid = issuer->pid;
- res.push_back(RecordTraceElement(pid, value));
- }
- }
+ for (std::shared_ptr<Pair> const& pair : explorationStack_)
+ res.push_back(pair->graph_state->getRecordElement());
return res;
}
RecordTrace SafetyChecker::getRecordTrace() // override
{
RecordTrace res;
- for (auto const& state : stack_) {
- int value = 0;
- smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
- const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
- const int pid = issuer->pid;
- res.push_back(RecordTraceElement(pid, value));
- }
+ for (auto const& state : stack_)
+ res.push_back(state->getRecordElement());
return res;
}
* @param process the MCed process
* @param req the simcall (copied in the local process)
*/
-smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req)
+smx_process_t MC_smx_simcall_get_issuer(s_smx_simcall_t const* req)
{
if (mc_mode == MC_MODE_CLIENT)
return req->issuer;
* @param process the MCed process
* @param req the simcall (copied in the local process)
*/
-XBT_PRIVATE smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req);
+XBT_PRIVATE smx_process_t MC_smx_simcall_get_issuer(s_smx_simcall_t const* req);
XBT_PRIVATE const char* MC_smx_process_get_name(smx_process_t p);
XBT_PRIVATE const char* MC_smx_process_get_host_name(smx_process_t p);
[](simgrid::mc::ProcessState const& state) { return state.isToInterleave(); });
}
+RecordTraceElement State::getRecordElement() const
+{
+ smx_process_t issuer = MC_smx_simcall_get_issuer(&this->executed_req);
+ return RecordTraceElement(issuer->pid, this->req_num);
+}
+
}
}
#include <simgrid_config.h>
#include "src/simix/smx_private.h"
#include "src/mc/mc_snapshot.h"
+#include "src/mc/mc_record.h"
namespace simgrid {
namespace mc {
{
this->processStates[process->pid].interleave();
}
+ RecordTraceElement getRecordElement() const;
};
XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);