namespace simgrid::mc {
/** @brief Save the current state */
-VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count)
- : actor_count_(actor_count), num_(state_number)
+VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count, RemoteApp& remote_app)
+ : heap_bytes_used_(remote_app.get_remote_process_memory()->get_remote_heap_bytes())
+ , actor_count_(actor_count)
+ , num_(state_number)
{
- this->heap_bytes_used_ = mc_model_checker->get_remote_process().get_remote_heap_bytes();
- this->system_state_ = std::make_shared<simgrid::mc::Snapshot>(state_number);
+ this->system_state_ = std::make_shared<simgrid::mc::Snapshot>(state_number, remote_app.get_page_store(),
+ *remote_app.get_remote_process_memory());
}
void VisitedStates::prune()
}
/** @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)
+std::unique_ptr<simgrid::mc::VisitedState>
+VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, RemoteApp& remote_app)
{
- auto new_state = std::make_unique<simgrid::mc::VisitedState>(state_number, graph_state->get_actor_count());
+ auto new_state =
+ std::make_unique<simgrid::mc::VisitedState>(state_number, graph_state->get_actor_count(), remote_app);
+
graph_state->set_system_state(new_state->system_state_);
XBT_DEBUG("Snapshot %p of visited state %ld (exploration stack state %ld)", new_state->system_state_.get(),
new_state->num_, graph_state->get_num());
for (auto i = range_begin; i != range_end; ++i) {
auto& visited_state = *i;
- if (*visited_state->system_state_.get() == *new_state->system_state_.get()) {
+ if (visited_state->system_state_->equals_to(*new_state->system_state_.get(),
+ *remote_app.get_remote_process_memory())) {
// The state has been visited:
std::unique_ptr<simgrid::mc::VisitedState> old_state = std::move(visited_state);