*/
class ModelChecker {
CheckerSide checker_side_;
- // This is the parent snapshot of the current state:
- PageStore page_store_{500};
std::unique_ptr<RemoteProcess> remote_process_;
Exploration* exploration_ = nullptr;
- unsigned long visited_states_ = 0;
-
public:
ModelChecker(ModelChecker const&) = delete;
ModelChecker& operator=(ModelChecker const&) = delete;
RemoteProcess& get_remote_process() { return *remote_process_; }
Channel& channel() { return checker_side_.get_channel(); }
- PageStore& page_store() { return page_store_; }
void start();
void shutdown();
Exploration* get_exploration() const { return exploration_; }
void set_exploration(Exploration* exploration) { exploration_ = exploration; }
- unsigned long get_visited_states() const { return visited_states_; }
- void inc_visited_states() { visited_states_++; }
-
private:
void setup_ignore();
bool handle_message(const char* buffer, ssize_t size);