-/* Copyright (c) 2016. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2016-2017. 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/mc_private.h"
#include "src/mc/mc_record.h"
#include "src/mc/mc_request.h"
-#include "src/mc/mc_safety.h"
#include "src/mc/mc_smx.h"
-#include "src/mc/mc_state.h"
-#include "src/mc/remote/Client.hpp"
#include "src/xbt/mmalloc/mmprivate.h"
* We do so iteratively instead of recursively, dealing with the call stack manually.
* This allows to explore the call stack at wish. */
- while (!stack_.empty()) {
+ while (not stack_.empty()) {
/* Get current state */
simgrid::mc::State* state = stack_.back().get();
this->checkNonTermination(next_state.get());
/* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
- if (_sg_mc_max_visited_states == true)
+ if (_sg_mc_max_visited_states > 0)
visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
/* If this is a new state (or if we don't care about state-equality reduction) */
if (visitedState_ == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
- for (auto& actor : mc_model_checker->process().actors())
- if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
- next_state->interleave(actor.copy.getBuffer());
+ for (auto& remoteActor : mc_model_checker->process().actors()) {
+ auto actor = remoteActor.copy.getBuffer();
+ if (simgrid::mc::actor_is_enabled(actor)) {
+ next_state->addInterleavingSet(actor);
if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
- break;
+ break; // With DPOR, we take the first enabled transition
}
+ }
if (dot_output != nullptr)
std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
executed before it. If it does then add it to the interleave set of the
state that executed that previous request. */
- while (!stack_.empty()) {
+ while (not stack_.empty()) {
std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
stack_.pop_back();
if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
state->num);
}
- if (!prev_state->actorStates[issuer->pid].isDone())
- prev_state->interleave(issuer);
+ if (not prev_state->actorStates[issuer->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 independant",
+ 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,
if (_sg_mc_termination)
XBT_INFO("Check non progressive cycles");
else
- XBT_INFO("Check a safety property");
+ XBT_INFO("Check a safety property. Reduction is: %s.",
+ (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
+ (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
simgrid::mc::session->initialize();
XBT_DEBUG("Starting the safety algorithm");
/* Get an enabled actor and insert it in the interleave set of the initial state */
for (auto& actor : mc_model_checker->process().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
- initial_state->interleave(actor.copy.getBuffer());
+ initial_state->addInterleavingSet(actor.copy.getBuffer());
if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}
stack_.push_back(std::move(initial_state));
}
-SafetyChecker::~SafetyChecker()
-{
-}
-
Checker* createSafetyChecker(Session& session)
{
return new SafetyChecker(session);
}
-
+
}
}