From: mlaurent <mathieu.laurent@ens-rennes.fr>
Date: Mon, 5 Jun 2023 11:56:03 +0000 (+0200)
Subject: Fix few typos and add random seed intializer
X-Git-Tag: v3.34~41^2~16
X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/f50afc03bed61a42cd816ce73fa48aedd1331fcc

Fix few typos and add random seed intializer
---

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index a97acd7cd2..753b1360fc 100644
--- 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 fd3b68a08e..4cb58913ca 100644
--- 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 e62076d7bd..f5a9a06cd5 100644
--- 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 709d1673ba..72f1a37799 100644
--- 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 64a0e29a79..6ad0c6c70a 100644
--- 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 64acccc142..713156f23b 100644
--- 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;