Fix few typos and add random seed intializer

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index a97acd7..753b136 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -31,7 +31,7 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_)
     strategy_ = std::make_shared<MaxMatchComm>();
   else if (_sg_mc_strategy == "min_match_comm")
     strategy_ = std::make_shared<MinMatchComm>();
-  else if (_sg_mc_strategy == "uniform") {
+  else if (_sg_mc_strategy == "uniform") 
     strategy_ = std::make_shared<UniformStrategy>();
   else
     THROW_IMPOSSIBLE;
@@ -56,7 +56,7 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
     strategy_ = std::make_shared<MaxMatchComm>();
   else if (_sg_mc_strategy == "min_match_comm")
     strategy_ = std::make_shared<MinMatchComm>();
-  else if (_sg_mc_strategy == "uniform") {
+  else if (_sg_mc_strategy == "uniform") 
     strategy_ = std::make_shared<UniformStrategy>();
   else
     THROW_IMPOSSIBLE;

diff --git a/src/mc/api/strategy/MaxMatchComm.hpp b/src/mc/api/strategy/MaxMatchComm.hpp
index fd3b68a..4cb5891 100644 (file)
--- a/src/mc/api/strategy/MaxMatchComm.hpp
+++ b/src/mc/api/strategy/MaxMatchComm.hpp
@@ -36,7 +36,7 @@ public:
       mailbox_[cast_strategy->last_mailbox_]++;
 
     for (auto const& [_, val] : mailbox_)
-       value_of_state += std::abs(val);
+       value_of_state_ += std::abs(val);
   }
   MaxMatchComm()                     = default;
   ~MaxMatchComm() override           = default;

diff --git a/src/mc/api/strategy/MinMatchComm.hpp b/src/mc/api/strategy/MinMatchComm.hpp
index e62076d..f5a9a06 100644 (file)
--- a/src/mc/api/strategy/MinMatchComm.hpp
+++ b/src/mc/api/strategy/MinMatchComm.hpp
@@ -37,7 +37,7 @@ public:
          mailbox_[cast_strategy->last_mailbox_]++;
 
       for (auto const& [_, val] : mailbox_) 
-         value_of_state -= std::abs(val);
+         value_of_state_ -= std::abs(val);
       if (value_of_state_ < 0)
          value_of_state_ = 0;
   }

diff --git a/src/mc/api/strategy/UniformStrategy.hpp b/src/mc/api/strategy/UniformStrategy.hpp
index 709d167..72f1a37 100644 (file)
--- a/src/mc/api/strategy/UniformStrategy.hpp
+++ b/src/mc/api/strategy/UniformStrategy.hpp
@@ -7,7 +7,6 @@
 #define SIMGRID_MC_UNIFORMSTRATEGY_HPP
 
 #include "src/mc/transition/Transition.hpp"
-#include "src/plugins/cfg/CFGMap.hpp"
 
 namespace simgrid::mc {
 

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index 64a0e29..6ad0c6c 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -75,6 +75,10 @@ simgrid::config::Flag<std::string> _sg_mc_strategy{
      {"uniform", "No specific strategy: choices are made randomly based on a uniform sampling."}
     }};
 
+simgrid::config::Flag<int> _sg_mc_random_seed{"model-check/rand-seed",
+                                              "give a specific random seed to initialize the uniform distribution", 0,
+                                              [](int) { _mc_cfg_cb_check("Random seed"); }};
+
 #if SIMGRID_HAVE_STATEFUL_MC
 simgrid::config::Flag<int> _sg_mc_checkpoint{
     "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking "

diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp
index 64acccc..713156f 100644 (file)
--- a/src/mc/mc_config.hpp
+++ b/src/mc/mc_config.hpp
@@ -24,6 +24,7 @@ extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_send_determinism;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_unfolding_checker;
 extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_timeout;
 extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_max_depth;
+extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_random_seed;
 extern "C" XBT_PUBLIC int _sg_mc_max_visited_states;
 extern XBT_PRIVATE simgrid::config::Flag<std::string> _sg_mc_dot_output_file;
 extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_termination;