Ensure that the verified application still works if get_max_consider() is not called...

This can happen after a backtrack: the Checker already knows how many
times this can be considered, but the App was reset in between so it
forgot.

So, make get_max_consider() const, and do the initialization in the
observer constructor, where it belongs. Too bad for the tiny little
tiny loss of performance compared to the lazy initialization.

diff --git a/src/kernel/actor/CommObserver.cpp b/src/kernel/actor/CommObserver.cpp
index f44571e..e15d6aa 100644 (file)
--- a/src/kernel/actor/CommObserver.cpp
+++ b/src/kernel/actor/CommObserver.cpp
@@ -18,16 +18,16 @@ namespace simgrid::kernel::actor {
 
 ActivityTestanySimcall::ActivityTestanySimcall(ActorImpl* actor, const std::vector<activity::ActivityImpl*>& activities)
     : ResultingSimcall(actor, -1), activities_(activities)
-{
-}
-
-int ActivityTestanySimcall::get_max_consider()
 {
   indexes_.clear();
   // list all the activities that are ready
   for (unsigned i = 0; i < activities_.size(); i++)
     if (activities_[i]->test(get_issuer()))
       indexes_.push_back(i);
+}
+
+int ActivityTestanySimcall::get_max_consider() const
+{
   return indexes_.size() + 1;
 }
 
@@ -94,6 +94,11 @@ ActivityWaitanySimcall::ActivityWaitanySimcall(ActorImpl* actor, const std::vect
                                                double timeout)
     : ResultingSimcall(actor, -1), activities_(activities), timeout_(timeout)
 {
+  // list all the activities that are ready
+  indexes_.clear();
+  for (unsigned i = 0; i < activities_.size(); i++)
+    if (activities_[i]->test(get_issuer()))
+      indexes_.push_back(i);
 }
 
 bool ActivityWaitSimcall::is_enabled()
@@ -119,14 +124,8 @@ bool ActivityWaitanySimcall::is_enabled()
   return not indexes_.empty();
 }
 
-int ActivityWaitanySimcall::get_max_consider()
+int ActivityWaitanySimcall::get_max_consider() const
 {
-  // list all the activities that are ready
-  indexes_.clear();
-  for (unsigned i = 0; i < activities_.size(); i++)
-    if (activities_[i]->test(get_issuer()))
-      indexes_.push_back(i);
-
   int res = indexes_.size();
   //  if (_sg_mc_timeout && timeout_)
   //    res++;

diff --git a/src/kernel/actor/CommObserver.hpp b/src/kernel/actor/CommObserver.hpp
index 9cba17d..41607aa 100644 (file)
--- a/src/kernel/actor/CommObserver.hpp
+++ b/src/kernel/actor/CommObserver.hpp
@@ -38,7 +38,7 @@ public:
   bool is_visible() const override { return true; }
   bool is_enabled() override { return true; /* can return -1 if no activity is ready */ }
   void serialize(std::stringstream& stream) const override;
-  int get_max_consider() override;
+  int get_max_consider() const override;
   void prepare(int times_considered) override;
   const std::vector<activity::ActivityImpl*>& get_activities() const { return activities_; }
   int get_value() const { return next_value_; }
@@ -73,7 +73,7 @@ public:
   void serialize(std::stringstream& stream) const override;
   bool is_visible() const override { return true; }
   void prepare(int times_considered) override;
-  int get_max_consider() override;
+  int get_max_consider() const override;
   const std::vector<activity::ActivityImpl*>& get_activities() const { return activities_; }
   double get_timeout() const { return timeout_; }
   int get_value() const { return next_value_; }

diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp
index e4ffca2..87991cc 100644 (file)
--- a/src/kernel/actor/SimcallObserver.cpp
+++ b/src/kernel/actor/SimcallObserver.cpp
@@ -32,7 +32,7 @@ void RandomSimcall::prepare(int times_considered)
   XBT_DEBUG("MC_RANDOM(%d, %d) will return %d after %d times", min_, max_, next_value_, times_considered);
 }
 
-int RandomSimcall::get_max_consider()
+int RandomSimcall::get_max_consider() const
 {
   return max_ - min_ + 1;
 }

diff --git a/src/kernel/actor/SimcallObserver.hpp b/src/kernel/actor/SimcallObserver.hpp
index 6eabf88..a4095e4 100644 (file)
--- a/src/kernel/actor/SimcallObserver.hpp
+++ b/src/kernel/actor/SimcallObserver.hpp
@@ -37,7 +37,7 @@ public:
    * If it's more than one (as with mc_random or waitany), we need to consider this transition several times to start
    * differing branches
    */
-  virtual int get_max_consider() { return 1; }
+  virtual int get_max_consider() const { return 1; }
 
   /** Prepares the simcall to be used.
    *
@@ -83,7 +83,7 @@ public:
     xbt_assert(min < max);
   }
   void serialize(std::stringstream& stream) const override;
-  int get_max_consider() override;
+  int get_max_consider() const override;
   void prepare(int times_considered) override;
   int get_value() const { return next_value_; }
 };

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 93eef1a..a35833c 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -40,9 +40,7 @@ namespace simgrid::mc {
 void execute_actors()
 {
   auto* engine = kernel::EngineImpl::get_instance();
-#if SIMGRID_HAVE_MC
-  xbt_assert(mc_model_checker == nullptr, "This must be called from the client");
-#endif
+
   while (engine->has_actors_to_run()) {
     engine->run_all_actors();
     for (auto const& actor : engine->get_actors_that_ran()) {