* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/checker/LivenessChecker.hpp"
-#include "src/mc/Session.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_request.hpp"
#include "src/mc/mc_smx.hpp"
-#include "src/mc/mc_api.hpp"
#include <boost/range/algorithm.hpp>
#include <cstring>
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
mcapi::get().request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
- this->get_session().execute(state->transition_);
+ mcapi::get().execute(state->transition_);
}
/* Update statistics */
visited_pairs_count_++;
- mc_model_checker->executed_transitions++;
+ mcapi::get().mc_inc_executed_trans();
depth++;
}
}
}
-LivenessChecker::LivenessChecker(Session& s) : Checker(s)
+LivenessChecker::LivenessChecker() : Checker()
{
}
mcapi::get().log_state();
}
-Checker* createLivenessChecker(Session& s)
+Checker* createLivenessChecker()
{
- return new LivenessChecker(s);
+ return new LivenessChecker();
}
} // namespace mc