X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/fe6a4a0cfb04cbe8c0bbd93c7bf6c29ec017ddec..d872d0c0ec6694fee02a2ede409ad22fcab9258c:/src/mc/explo/DFSExplorer.hpp diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp index 0eaac540a5..8d63ca4e23 100644 --- a/src/mc/explo/DFSExplorer.hpp +++ b/src/mc/explo/DFSExplorer.hpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2022. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2023. 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. */ @@ -8,7 +8,6 @@ #include "src/mc/VisitedState.hpp" #include "src/mc/explo/Exploration.hpp" -#include "src/mc/mc_safety.hpp" #include #include @@ -18,59 +17,73 @@ namespace simgrid::mc { class XBT_PRIVATE DFSExplorer : public Exploration { - ReductionMode reductionMode_ = ReductionMode::unset; - long backtrack_count_ = 0; + XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor); - static xbt::signal on_exploration_start_signal; - static xbt::signal on_backtracking_signal; + ReductionMode reduction_mode_; + unsigned long backtrack_count_ = 0; // for statistics + unsigned long visited_states_count_ = 0; // for statistics - static xbt::signal on_state_creation_signal; + static xbt::signal on_exploration_start_signal; + static xbt::signal on_backtracking_signal; - static xbt::signal on_restore_system_state_signal; - static xbt::signal on_restore_initial_state_signal; - static xbt::signal on_transition_replay_signal; - static xbt::signal on_transition_execute_signal; + static xbt::signal on_state_creation_signal; - static xbt::signal on_log_state_signal; + static xbt::signal on_restore_system_state_signal; + static xbt::signal on_restore_initial_state_signal; + static xbt::signal on_transition_replay_signal; + static xbt::signal on_transition_execute_signal; + + static xbt::signal on_log_state_signal; public: - explicit DFSExplorer(RemoteApp& remote_app); + explicit DFSExplorer(const std::vector& args, bool with_dpor); void run() override; RecordTrace get_record_trace() override; std::vector get_textual_trace() override; void log_state() override; /** Called once when the exploration starts */ - static void on_exploration_start(std::function const& f) { on_exploration_start_signal.connect(f); } + static void on_exploration_start(std::function const& f) + { + on_exploration_start_signal.connect(f); + } /** Called each time that the exploration backtracks from a exploration end */ - static void on_backtracking(std::function const& f) { on_backtracking_signal.connect(f); } + static void on_backtracking(std::function const& f) + { + on_backtracking_signal.connect(f); + } /** Called each time that a new state is create */ - static void on_state_creation(std::function const& f) { on_state_creation_signal.connect(f); } + static void on_state_creation(std::function const& f) + { + on_state_creation_signal.connect(f); + } /** Called when rollbacking directly onto a previously checkpointed state */ - static void on_restore_system_state(std::function const& f) + static void on_restore_system_state(std::function const& f) { on_restore_system_state_signal.connect(f); } /** Called when the state to which we backtrack was not checkpointed state, forcing us to restore the initial state * before replaying some transitions */ - static void on_restore_initial_state(std::function const& f) { on_restore_initial_state_signal.connect(f); } + static void on_restore_initial_state(std::function const& f) + { + on_restore_initial_state_signal.connect(f); + } /** Called when replaying a transition that was previously executed, to reach a backtracked state */ - static void on_transition_replay(std::function const& f) + static void on_transition_replay(std::function const& f) { on_transition_replay_signal.connect(f); } /** Called when executing a new transition */ - static void on_transition_execute(std::function const& f) + static void on_transition_execute(std::function const& f) { on_transition_execute_signal.connect(f); } /** Called when displaying the statistics at the end of the exploration */ - static void on_log_state(std::function const& f) { on_log_state_signal.connect(f); } + static void on_log_state(std::function const& f) { on_log_state_signal.connect(f); } private: void check_non_termination(const State* current_state); void backtrack(); - void restore_state(); /** Stack representing the position in the exploration graph */ std::list> stack_;