}
*/
-Exploration* create_communication_determinism_checker(const std::vector<char*>& args, bool with_dpor)
+Exploration* create_communication_determinism_checker(const std::vector<char*>& args, ReductionMode mode)
{
CommDetExtension::EXTENSION_ID = simgrid::mc::Exploration::extension_create<CommDetExtension>();
StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create<StateCommDet>();
XBT_DEBUG("********* Start communication determinism verification *********");
- auto base = new DFSExplorer(args, with_dpor, true);
+ auto base = new DFSExplorer(args, mode, true);
auto extension = new CommDetExtension(*base);
DFSExplorer::on_exploration_start([extension](RemoteApp const&) {
this->restore_stack(backtracking_point);
}
-DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info)
+DFSExplorer::DFSExplorer(const std::vector<char*>& args, ReductionMode mode, bool need_memory_info)
: Exploration(args, need_memory_info || _sg_mc_termination
#if SIMGRID_HAVE_STATEFUL_MC
|| _sg_mc_checkpoint > 0
#endif
- )
+ )
+ , reduction_mode_(mode)
{
- if (with_dpor)
- reduction_mode_ = ReductionMode::dpor;
- else
- reduction_mode_ = ReductionMode::none;
-
if (_sg_mc_termination) {
- if (with_dpor) {
+ if (mode != ReductionMode::none) {
XBT_INFO("Check non progressive cycles (turning DPOR off)");
reduction_mode_ = ReductionMode::none;
} else {
opened_states_.emplace_back(stack_.back());
}
-Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor)
+Exploration* create_dfs_exploration(const std::vector<char*>& args, ReductionMode mode)
{
- return new DFSExplorer(args, with_dpor);
+ return new DFSExplorer(args, mode);
}
} // namespace simgrid::mc
#include "src/mc/api/State.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/explo/odpor/Execution.hpp"
+#include "src/mc/mc_config.hpp"
#if SIMGRID_HAVE_STATEFUL_MC
#include "src/mc/VisitedState.hpp"
using stack_t = std::deque<std::shared_ptr<State>>;
class XBT_PRIVATE DFSExplorer : public Exploration {
- XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor, sdpor);
-
+private:
ReductionMode reduction_mode_;
unsigned long backtrack_count_ = 0; // for statistics
unsigned long visited_states_count_ = 0; // for statistics
static xbt::signal<void(RemoteApp&)> on_log_state_signal;
public:
- explicit DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info = false);
+ explicit DFSExplorer(const std::vector<char*>& args, ReductionMode mode, bool need_memory_info = false);
void run() override;
RecordTrace get_record_trace() override;
void log_state() override;
#include "simgrid/forward.h"
#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_record.hpp"
#include <xbt/Extendable.hpp>
static Exploration* get_instance() { return instance_; }
// No copy:
- Exploration(Exploration const&) = delete;
+ Exploration(Exploration const&) = delete;
Exploration& operator=(Exploration const&) = delete;
/** Main function of this algorithm */
// External constructors so that the types (and the types of their content) remain hidden
XBT_PUBLIC Exploration* create_liveness_checker(const std::vector<char*>& args);
-XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor);
-XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args, bool with_dpor);
+XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector<char*>& args, ReductionMode mode);
+XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args, ReductionMode mode);
XBT_PUBLIC Exploration* create_udpor_checker(const std::vector<char*>& args);
} // namespace simgrid::mc
#if SIMGRID_HAVE_STATEFUL_MC
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- explo = std::unique_ptr<Exploration>(create_communication_determinism_checker(argv_copy, cfg_use_DPOR()));
+ explo = std::unique_ptr<Exploration>(
+ create_communication_determinism_checker(argv_copy, get_model_checking_reduction()));
else if (_sg_mc_unfolding_checker)
explo = std::unique_ptr<Exploration>(create_udpor_checker(argv_copy));
else if (not _sg_mc_property_file.get().empty())
explo = std::unique_ptr<Exploration>(create_liveness_checker(argv_copy));
else
#endif
- explo = std::unique_ptr<Exploration>(create_dfs_exploration(argv_copy, cfg_use_DPOR()));
+ explo = std::unique_ptr<Exploration>(create_dfs_exploration(argv_copy, get_model_checking_reduction()));
ExitStatus status;
try {
static simgrid::config::Flag<std::string> cfg_mc_reduction{
"model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", "dpor",
[](std::string_view value) {
- if (value != "none" && value != "dpor")
- xbt_die("configuration option 'model-check/reduction' can only take 'none' or 'dpor' as a value");
+ if (value != "none" && value != "dpor" && value != "sdpor" && value != "odpor")
+ xbt_die("configuration option 'model-check/reduction' must be one of the following: "
+ " 'none', 'dpor', 'sdpor', or 'odpor'");
}};
simgrid::config::Flag<bool> _sg_mc_sleep_set{
"model-check/termination", "Whether to enable non progressive cycle detection", false,
[](bool) { _mc_cfg_cb_check("value to enable/disable the detection of non progressive cycles"); }};
-bool simgrid::mc::cfg_use_DPOR()
+simgrid::mc::ReductionMode simgrid::mc::get_model_checking_reduction()
{
- if (cfg_mc_reduction.get() == "dpor" && _sg_mc_max_visited_states__ > 0) {
+ if ((cfg_mc_reduction.get() == "dpor" || cfg_mc_reduction.get() == "sdpor" || cfg_mc_reduction.get() == "odpor") &&
+ _sg_mc_max_visited_states__ > 0) {
XBT_INFO("Disabling DPOR since state-equality reduction is activated with 'model-check/visited'");
- return false;
+ return simgrid::mc::ReductionMode::none;
+ }
+
+ if (cfg_mc_reduction.get() == "none") {
+ return ReductionMode::none;
+ } else if (cfg_mc_reduction.get() == "dpor") {
+ return ReductionMode::dpor;
+ } else if (cfg_mc_reduction.get() == "sdpor") {
+ return ReductionMode::sdpor;
+ } else if (cfg_mc_reduction.get() == "odpor") {
+ XBT_INFO("No reduction will be used: ODPOR is not yet supported in SimGrid");
+ return simgrid::mc::ReductionMode::none;
+ } else if (cfg_mc_reduction.get() == "udpor") {
+ XBT_INFO("No reduction will be used: "
+ "UDPOR is has a dedicated invocation 'model-check/unfolding-checker' "
+ "but is not yet supported in SimGrid");
+ return ReductionMode::none;
+ } else {
+ XBT_INFO("Unknown reduction mode: defaulting to no reduction");
+ return ReductionMode::none;
}
- return cfg_mc_reduction.get() == "dpor";
}
/********************************** Configuration of MC **************************************/
namespace simgrid::mc {
-bool cfg_use_DPOR(); // "model-check/reduction" == "DPOR"
+XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor, sdpor, odpor);
XBT_DECLARE_ENUM_CLASS(ModelCheckingMode, NONE, APP_SIDE, CHECKER_SIDE, REPLAY);
+ReductionMode get_model_checking_reduction(); // "model-check/reduction" == "DPOR"
XBT_PUBLIC ModelCheckingMode get_model_checking_mode();
XBT_PUBLIC void set_model_checking_mode(ModelCheckingMode mode);
-};
+}; // namespace simgrid::mc
extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_buffering;
extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_checkpoint;