-/* Copyright (c) 2016-2017. The SimGrid Team. All rights reserved. */
+/* Copyright (c) 2016-2019. 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.hpp"
#include "src/mc/VisitedState.hpp"
#include "src/mc/checker/SafetyChecker.hpp"
-#include "src/mc/mc_exit.h"
-#include "src/mc/mc_private.h"
-#include "src/mc/mc_record.h"
-#include "src/mc/mc_request.h"
-#include "src/mc/mc_smx.h"
+#include "src/mc/mc_exit.hpp"
+#include "src/mc/mc_private.hpp"
+#include "src/mc/mc_record.hpp"
+#include "src/mc/mc_request.hpp"
+#include "src/mc/mc_smx.hpp"
#include "src/xbt/mmalloc/mmprivate.h"
void SafetyChecker::logState() // override
{
- Checker::logState();
XBT_INFO("Expanded states = %lu", expandedStatesCount_);
XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
state->num);
}
- if (not prev_state->actorStates[issuer->pid].isDone())
+ if (not prev_state->actorStates[issuer->get_pid()].isDone())
prev_state->addInterleavingSet(issuer);
else
XBT_DEBUG("Process %p is in done set", req->issuer);
} else {
const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
- XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independent",
- req->call, issuer->pid, state->num,
- prev_state->internal_req.call,
- previous_issuer->pid,
+ XBT_DEBUG("Simcall %d, process %ld (state %d) and simcall %d, process %ld (state %d) are independent",
+ req->call, issuer->get_pid(), state->num, prev_state->internal_req.call, previous_issuer->get_pid(),
prev_state->num);
-
}
}
}