Finish the removal of mc::api by moving the last bits to the side

I would prefer to directly kill the templated structure, but I fail to
write a correct comparison lambda because it's used over a
std::vector<std::unique_ptr<simgrid::mc::VisitedState>>

All my attempts lead to either "no conversion to std::unique_ptr<VisitedState>",
or an error saying that I try to copy a unique_ptr when my lambda
takes unique_ptr as a parameter.

Please someone better at C++ than I am, please kill it.

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index 7c81cc7..9c9270f 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -4,13 +4,13 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/VisitedState.hpp"
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/VisitedState.hpp"

+#include "src/mc/explo/Exploration.hpp"

 #include "src/mc/mc_private.hpp"
 
 #include <unistd.h>
 #include <sys/wait.h>
 #include <memory>
 #include <boost/range/algorithm.hpp>
 #include "src/mc/mc_private.hpp"
 
 #include <unistd.h>
 #include <sys/wait.h>
 #include <memory>
 #include <boost/range/algorithm.hpp>

-#include "src/mc/api.hpp"

 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_VisitedState, mc, "Logging specific to state equality detection mechanisms");
 
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_VisitedState, mc, "Logging specific to state equality detection mechanisms");
 


@@ -47,7 +47,8 @@ VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* g
   XBT_DEBUG("Snapshot %p of visited state %ld (exploration stack state %ld)", new_state->system_state.get(),
             new_state->num, graph_state->get_num());
 
   XBT_DEBUG("Snapshot %p of visited state %ld (exploration stack state %ld)", new_state->system_state.get(),
             new_state->num, graph_state->get_num());
 

-  auto [range_begin, range_end] = boost::range::equal_range(states_, new_state.get(), Api::get().compare_pair());
+  auto [range_begin, range_end] =
+      boost::range::equal_range(states_, new_state.get(), compare_pair_by_actor_count_and_used_heap());

 
   if (compare_snapshots)
     for (auto i = range_begin; i != range_end; ++i) {
 
   if (compare_snapshots)
     for (auto i = range_begin; i != range_end; ++i) {

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
deleted file mode 100644 (file)
index 9a47ed8..0000000
--- a/src/mc/api.hpp
+++ /dev/null
@@ -1,57 +0,0 @@
-/* Copyright (c) 2020-2022. The SimGrid Team. All rights reserved.          */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#ifndef SIMGRID_MC_API_HPP
-#define SIMGRID_MC_API_HPP
-
-#include <memory>
-#include <vector>
-
-#include "simgrid/forward.h"
-#include "src/mc/api/RemoteApp.hpp"
-#include "src/mc/api/State.hpp"
-#include "src/mc/mc_forward.hpp"
-#include "src/mc/mc_record.hpp"
-#include "xbt/automaton.hpp"
-#include "xbt/base.h"
-
-namespace simgrid::mc {
-
-/*
-** This class aimes to implement FACADE APIs for simgrid. The FACADE layer sits between the CheckerSide
-** (Unfolding_Checker, DPOR, ...) layer and the
-** AppSide layer. The goal is to drill down into the entagled details in the CheckerSide layer and break down the
-** detailes in a way that the CheckerSide eventually
-** be capable to acquire the required information through the FACADE layer rather than the direct access to the AppSide.
-*/
-
-class Api {
-private:
-  Api() = default;
-
-  struct DerefAndCompareByActorsCountAndUsedHeap {
-    template <class X, class Y> bool operator()(X const& a, Y const& b) const
-    {
-      return std::make_pair(a->actor_count_, a->heap_bytes_used) < std::make_pair(b->actor_count_, b->heap_bytes_used);
-    }
-  };
-
-public:
-  static Api& get()
-  {
-    static Api api;
-    return api;
-  }
-
-  // AUTOMATION APIs
-  inline DerefAndCompareByActorsCountAndUsedHeap compare_pair() const
-  {
-    return DerefAndCompareByActorsCountAndUsedHeap();
-  }
-};
-
-} // namespace simgrid::mc
-
-#endif

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index c2b8af5..5ca3182 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -4,7 +4,6 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/api/State.hpp"
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/api/State.hpp"

-#include "src/mc/api.hpp"

 #include "src/mc/mc_config.hpp"
 
 #include <boost/range/algorithm.hpp>
 #include "src/mc/mc_config.hpp"
 
 #include <boost/range/algorithm.hpp>

diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp
index bd99e25..327818e 100644 (file)
--- a/src/mc/explo/Exploration.hpp
+++ b/src/mc/explo/Exploration.hpp
@@ -6,7 +6,10 @@
 #ifndef SIMGRID_MC_CHECKER_HPP
 #define SIMGRID_MC_CHECKER_HPP
 
 #ifndef SIMGRID_MC_CHECKER_HPP
 #define SIMGRID_MC_CHECKER_HPP
 

-#include "src/mc/api.hpp"
+#include "simgrid/forward.h"
+#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/mc_record.hpp"
+#include <xbt/Extendable.hpp>

 
 #include <memory>
 
 
 #include <memory>
 


@@ -63,6 +66,18 @@ XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector<char*>& args);
 XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args);
 XBT_PUBLIC Exploration* create_udpor_checker(const std::vector<char*>& args);
 
 XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args);
 XBT_PUBLIC Exploration* create_udpor_checker(const std::vector<char*>& args);
 

+// FIXME: kill this template and use lambdas in boost::range_equal
+struct DerefAndCompareByActorsCountAndUsedHeap {
+  template <class X, class Y> bool operator()(X const& a, Y const& b) const
+  {
+    return std::make_pair(a->actor_count_, a->heap_bytes_used) < std::make_pair(b->actor_count_, b->heap_bytes_used);
+  }
+};
+static inline DerefAndCompareByActorsCountAndUsedHeap compare_pair_by_actor_count_and_used_heap()
+{
+  return DerefAndCompareByActorsCountAndUsedHeap();
+}
+

 } // namespace simgrid::mc
 
 #endif
 } // namespace simgrid::mc
 
 #endif

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 8730db9..ab212dc 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -62,7 +62,8 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
   auto new_pair =
       std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_);
 
   auto new_pair =
       std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_);
 

-  auto [res_begin, res_end] = boost::range::equal_range(acceptance_pairs_, new_pair.get(), Api::get().compare_pair());
+  auto [res_begin, res_end] =
+      boost::range::equal_range(acceptance_pairs_, new_pair.get(), compare_pair_by_actor_count_and_used_heap());

 
   if (pair->search_cycle)
     for (auto i = res_begin; i != res_end; ++i) {
 
   if (pair->search_cycle)
     for (auto i = res_begin; i != res_end; ++i) {


@@ -139,7 +140,7 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
         std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_);
 
   auto [range_begin, range_end] =
         std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_);
 
   auto [range_begin, range_end] =

-      boost::range::equal_range(visited_pairs_, visited_pair.get(), Api::get().compare_pair());
+      boost::range::equal_range(visited_pairs_, visited_pair.get(), compare_pair_by_actor_count_and_used_heap());

 
   for (auto i = range_begin; i != range_end; ++i) {
     const VisitedPair* pair_test = i->get();
 
   for (auto i = range_begin; i != range_end; ++i) {
     const VisitedPair* pair_test = i->get();

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 28adc9a..7f83b4f 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -637,7 +637,6 @@ set(MC_SRC
   src/mc/ModelChecker.hpp
   src/mc/VisitedState.cpp
   src/mc/VisitedState.hpp
   src/mc/ModelChecker.hpp
   src/mc/VisitedState.cpp
   src/mc/VisitedState.hpp

-  src/mc/api.hpp

   src/mc/api/ActorState.hpp
   src/mc/api/State.cpp
   src/mc/api/State.hpp
   src/mc/api/ActorState.hpp
   src/mc/api/State.cpp
   src/mc/api/State.hpp