-static simgrid::config::Flag<int> _sg_mc_max_visited_states__{
- "model-check/visited", "Specify the number of visited state stored for state comparison reduction. If value=5, the "
- "last 5 visited states are stored. If value=0 (the default), all states are stored.",
- 0, [](int value) {
- _mc_cfg_cb_check("number of stored visited states");
- _sg_mc_max_visited_states = value;
- }};
-
-simgrid::config::Flag<std::string> _sg_mc_dot_output_file{
- "model-check/dot-output",
- "Name of dot output file corresponding to graph state",
- "",
- [](const std::string&) { _mc_cfg_cb_check("file name for a dot output of graph state"); }};
-
-simgrid::config::Flag<bool> _sg_mc_termination{
- "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"); }};
-
-#endif
+simgrid::mc::ReductionMode simgrid::mc::get_model_checking_reduction()
+{
+ 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") {
+ return ReductionMode::odpor;
+ } else if (cfg_mc_reduction.get() == "udpor") {
+ XBT_INFO("No reduction will be used: "
+ "UDPOR has a dedicated invocation 'model-check/unfolding-checker' "
+ "but is not yet fully supported in SimGrid");
+ return ReductionMode::none;
+ } else {
+ XBT_INFO("Unknown reduction mode: defaulting to no reduction");
+ return ReductionMode::none;
+ }
+}