this->system_state = simgrid::mc::take_snapshot(state_number);
this->num = state_number;
- this->other_num = -1;
+ this->original_num = -1;
}
VisitedState::~VisitedState()
}
}
-/**
- * \brief Checks whether a given state has already been visited by the algorithm.
+/** \brief Checks whether a given state has already been visited by the algorithm.
*/
std::unique_ptr<simgrid::mc::VisitedState> VisitedStates::addVisitedState(
unsigned long state_number, simgrid::mc::State* graph_state, bool compare_snpashots)
std::unique_ptr<simgrid::mc::VisitedState> old_state =
std::move(visited_state);
- if (old_state->other_num == -1)
- new_state->other_num = old_state->num;
- else
- new_state->other_num = old_state->other_num;
+ if (old_state->original_num == -1) // I'm the copy of an original process
+ new_state->original_num = old_state->num;
+ else // I'm the copy of a copy
+ new_state->original_num = old_state->original_num;
if (dot_output == nullptr)
XBT_DEBUG("State %d already visited ! (equal to state %d)",
- new_state->num, old_state->num);
+ new_state->num, old_state->num);
else
- XBT_DEBUG(
- "State %d already visited ! (equal to state %d (state %d in dot_output))",
- new_state->num, old_state->num, new_state->other_num);
+ XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))",
+ new_state->num, old_state->num, new_state->original_num);
/* Replace the old state with the new one (with a bigger num)
(when the max number of visited states is reached, the oldest
struct XBT_PRIVATE VisitedState {
std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr;
std::size_t heap_bytes_used = 0;
- int actors_count = 0;
- int num = 0;
- int other_num = 0; // dot_output for
+ int actors_count = 0;
+ int num = 0; // unique id of that state in the storage of all stored IDs
+ int original_num = 0; // num field of the VisitedState to which I was declared equal to (used for dot_output)
VisitedState(unsigned long state_number);
~VisitedState();
state->num, next_state->num, req_str.c_str());
} else if (dot_output != nullptr)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
- state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
+ visited_state->original_num == -1 ? visited_state->num : visited_state->original_num, req_str.c_str());
stack_.push_back(std::move(next_state));
if (stack_.size() > (std::size_t) _sg_mc_max_depth)
XBT_WARN("/!\\ Max depth reached ! /!\\ ");
else if (visited_state != nullptr)
- XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
+ XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
+ visited_state->original_num == -1 ? visited_state->num : visited_state->original_num);
else
XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
stack_.size());
{
/* This function runs the DFS algorithm the state space.
* We do so iteratively instead of recursively, dealing with the call stack manually.
- * This allows to explore the call stack when we want to. */
+ * This allows to explore the call stack at wish. */
while (!stack_.empty()) {
// Backtrack if we are revisiting a state we saw previously
if (visitedState_ != nullptr) {
XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
- visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
+ visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num);
visitedState_ = nullptr;
this->backtrack();
}
// Search an enabled transition in the current state; backtrack if the interleave set is empty
+ // get_request also sets state.transition to be the one corresponding to the returned req
smx_simcall_t req = MC_state_get_request(state);
+ // req is now the transition of the process that was selected to be executed
+
if (req == nullptr) {
XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size() + 1);
mc_model_checker->executed_transitions++;
- /* Answer the request */
+ /* Actually answer the request: let the remote process do execute that request */
this->getSession().execute(state->transition);
/* Create the new expanded state */
state->num, next_state->num, req_str.c_str());
} else if (dot_output != nullptr)
- std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
- state->num,
- visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
+ std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
+ visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num,
+ req_str.c_str());
stack_.push_back(std::move(next_state));
}
if (state->interleaveSize()
&& stack_.size() < (std::size_t) _sg_mc_max_depth) {
/* We found a back-tracking point, let's loop */
- XBT_DEBUG("Back-tracking to state %d at depth %zi",
- state->num, stack_.size() + 1);
+ XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1);
stack_.push_back(std::move(state));
this->restoreState();
XBT_DEBUG("Back-tracking to state %d at depth %zi done",
xbt_dynar_t comms;
simgrid::kernel::activity::Comm *act =
static_cast<simgrid::kernel::activity::Comm*>(simcall_comm_wait__get__comm(req));
-#if HAVE_MC
+#if HAVE_MC
s_xbt_dynar_t comms_buffer;
size_t buffer_size = 0;
if (mc_model_checker != nullptr) {
}
}
+/* Search an enabled transition for the given process.
+ *
+ * This can be seen as an iterator returning the next transition of the process.
+ *
+ * We only consider the processes that are both
+ * - marked "to be interleaved" in their ProcessState (controled by the checker algo).
+ * - which simcall can currently be executed (like a comm where the other partner is already known)
+ * Once we returned the last enabled transition of a process, it is marked done.
+ *
+ * Things can get muddled with the WAITANY and TESTANY simcalls, that are rewritten
+ * on the fly to a bunch of WAIT (resp TEST) transitions using the transition.argument
+ * field to remember what was the last returned sub-transition.
+ */
static inline smx_simcall_t MC_state_get_request_for_process(
simgrid::mc::State* state, smx_actor_t process)
{
+ /* reset the outgoing transition */
simgrid::mc::ProcessState* procstate = &state->processStates[process->pid];
- state->transition.pid = -1;
- state->transition.argument = -1;
+ state->transition.pid = -1;
+ state->transition.argument = -1;
+ state->executed_req.call = SIMCALL_NONE;
if (!procstate->isToInterleave())
return nullptr;
smx_simcall_t MC_state_get_request(simgrid::mc::State* state)
{
- for (auto& p : mc_model_checker->process().actors()) {
- smx_simcall_t res = MC_state_get_request_for_process(state, p.copy.getBuffer());
+ for (auto& actor : mc_model_checker->process().actors()) {
+ smx_simcall_t res = MC_state_get_request_for_process(state, actor.copy.getBuffer());
if (res)
return res;
}
Transition transition;
- /** The simcall which was executed */
+ /** The simcall which was executed, going out of that state */
s_smx_simcall_t executed_req;
- /* Internal translation of the simcall
+ /* Internal translation of the executed_req simcall
*
* SIMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST
- * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
+ * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT.
*/
s_smx_simcall_t internal_req;
State(unsigned long state_number);
std::size_t interleaveSize() const;
- void interleave(smx_actor_t process)
- {
+ void interleave(smx_actor_t process) {
this->processStates[process->pid].interleave();
}
Transition getTransition() const;
