- xbt_fifo_item_t item;
- mc_state_t stack_state;
- for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
- stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
- if(snapshot_compare(stack_state, current_state) == 0){
- XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
- return 1;
+static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
+{
+ simgrid::mc::Snapshot* s1 = state1->system_state.get();
+ simgrid::mc::Snapshot* s2 = state2->system_state.get();
+ int num1 = state1->num;
+ int num2 = state2->num;
+ return snapshot_compare(num1, s1, num2, s2);
+}
+
+bool SafetyChecker::is_exploration_stack_state(simgrid::mc::State* current_state)
+{
+ for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
+ if(snapshot_compare(*i, current_state) == 0){
+ XBT_INFO("Non-progressive cycle : state %d -> state %d",
+ (*i)->num, current_state->num);
+ return true;
+ }
+ return false;
+}
+
+RecordTrace SafetyChecker::getRecordTrace() // override
+{
+ RecordTrace res;
+ for (simgrid::mc::State* state : stack_) {
+ int value = 0;
+ smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ const int pid = issuer->pid;
+ res.push_back(RecordTraceElement(pid, value));
+ }
+ return res;
+}
+
+std::vector<std::string> SafetyChecker::getTextualTrace() // override
+{
+ std::vector<std::string> trace;
+ for (simgrid::mc::State* state : stack_) {
+ int value;
+ smx_simcall_t req = MC_state_get_executed_request(state, &value);
+ if (req) {
+ char* req_str = simgrid::mc::request_to_string(
+ req, value, simgrid::mc::RequestType::executed);
+ trace.push_back(req_str);
+ xbt_free(req_str);