We can get rid of s_mc_global_t in SafetyChecker.
int CommunicationDeterminismChecker::run()
{
XBT_INFO("Check communication determinism");
- mc_model_checker->wait_for_requests();
+ simgrid::mc::session->initialize();
this->prepare();
initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
- initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
initial_global_state->initial_communications_pattern_done = 0;
initial_global_state->recv_deterministic = 1;
initial_global_state->send_deterministic = 1;
void LivenessChecker::prepare(void)
{
- initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
initial_global_state->prev_pair = 0;
std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
}
/* Restore the initial state */
- simgrid::mc::restore_snapshot(initial_global_state->snapshot);
+ simgrid::mc::session->restoreInitialState();
/* Traverse the stack from the initial state and re-execute the transitions */
int depth = 1;
{
XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
MC_automaton_load(_sg_mc_property_file);
- mc_model_checker->wait_for_requests();
XBT_DEBUG("Starting the liveness algorithm");
-
- /* Create the initial state */
simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
-
+ simgrid::mc::session->initialize();
this->prepare();
+
int res = this->main();
simgrid::mc::initial_global_state = nullptr;
XBT_INFO("No property violation found.");
simgrid::mc::session->logState();
- initial_global_state = nullptr;
return SIMGRID_MC_EXIT_SUCCESS;
}
XBT_INFO("Check non progressive cycles");
else
XBT_INFO("Check a safety property");
- mc_model_checker->wait_for_requests();
+ simgrid::mc::session->initialize();
XBT_DEBUG("Starting the safety algorithm");
}
stack_.push_back(std::move(initial_state));
-
- /* Save the initial state */
- initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
- initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
}
SafetyChecker::SafetyChecker(Session& session) : Checker(session)
this->close();
}
+void Session::initialize()
+{
+ xbt_assert(initialSnapshot_ == nullptr);
+ mc_model_checker->wait_for_requests();
+ initialSnapshot_ = simgrid::mc::take_snapshot(0);
+}
+
void Session::execute(Transition const& transition)
{
modelChecker_->handle_simcall(transition);
modelChecker_->wait_for_requests();
}
+void Session::restoreInitialState()
+{
+ simgrid::mc::restore_snapshot(this->initialSnapshot_);
+}
+
void Session::logState()
{
mc_model_checker->getChecker()->logState();
void Session::close()
{
+ initialSnapshot_ = nullptr;
if (modelChecker_) {
modelChecker_->shutdown();
modelChecker_ = nullptr;
class Session {
private:
std::unique_ptr<ModelChecker> modelChecker_;
+ std::shared_ptr<simgrid::mc::Snapshot> initialSnapshot_;
private:
Session(pid_t pid, int socket);
void close();
public:
+ void initialize();
void execute(Transition const& transition);
void logState();
+ void restoreInitialState();
+
public: // static constructors
/** Create a new session by forking
/* Restore the initial state */
- simgrid::mc::restore_snapshot(simgrid::mc::initial_global_state->snapshot);
+ simgrid::mc::session->restoreInitialState();
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
// int n = xbt_dynar_length(incomplete_communications_pattern);
} s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
typedef struct s_mc_global_t {
- std::shared_ptr<simgrid::mc::Snapshot> snapshot;
int prev_pair = 0;
std::string prev_req;
int initial_communications_pattern_done = 0;