Move the automaton from mc::api to Liveness. An ugly trick is needed :(

See the comment in Liveness.hpp for the full details on that trick.

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 47f9dd0..9e24ee2 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -5,6 +5,7 @@
 
 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/LivenessChecker.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
@@ -211,14 +212,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
       XBT_DEBUG("Received symbol: %s", message.name.data());
 
-      if (property_automaton == nullptr)
-        property_automaton = xbt_automaton_new();
-
-      const RemoteProcess* process    = &this->get_remote_process();
-      RemotePtr<int> address          = remote((int*)message.data);
-      xbt::add_proposition(property_automaton, message.name.data(),
-                           [process, address]() { return process->read(address); });
-
+      LivenessChecker::automaton_register_symbol(get_remote_process(), message.name.data(), remote((int*)message.data));
       break;
     }
 

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 9e3f27f..a49f6e2 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -107,69 +107,4 @@ simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const
   return snapshot;
 }
 
-void Api::s_close()
-{
-  if (simgrid::mc::property_automaton != nullptr) {
-    xbt_automaton_free(simgrid::mc::property_automaton);
-    simgrid::mc::property_automaton = nullptr;
-  }
-}
-
-void Api::automaton_load(const char* file) const
-{
-  if (simgrid::mc::property_automaton == nullptr)
-    simgrid::mc::property_automaton = xbt_automaton_new();
-
-  xbt_automaton_load(simgrid::mc::property_automaton, file);
-}
-
-std::vector<int> Api::automaton_propositional_symbol_evaluate() const
-{
-  unsigned int cursor = 0;
-  std::vector<int> values;
-  xbt_automaton_propositional_symbol_t ps = nullptr;
-  xbt_dynar_foreach (mc::property_automaton->propositional_symbols, cursor, ps)
-    values.push_back(xbt_automaton_propositional_symbol_evaluate(ps));
-  return values;
-}
-
-std::vector<xbt_automaton_state_t> Api::get_automaton_state() const
-{
-  std::vector<xbt_automaton_state_t> automaton_stack;
-  unsigned int cursor = 0;
-  xbt_automaton_state_t automaton_state;
-  xbt_dynar_foreach (mc::property_automaton->states, cursor, automaton_state)
-    if (automaton_state->type == -1)
-      automaton_stack.push_back(automaton_state);
-  return automaton_stack;
-}
-
-int Api::compare_automaton_exp_label(const xbt_automaton_exp_label* l) const
-{
-  unsigned int cursor                    = 0;
-  xbt_automaton_propositional_symbol_t p = nullptr;
-  xbt_dynar_foreach (simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
-    if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
-      return cursor;
-  }
-  return -1;
-}
-
-void Api::set_property_automaton(xbt_automaton_state_t const& automaton_state) const
-{
-  mc::property_automaton->current_state = automaton_state;
-}
-
-xbt_automaton_exp_label_t Api::get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const
-{
-  const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
-  return transition->label;
-}
-
-xbt_automaton_state_t Api::get_automaton_transition_dst(xbt_dynar_t const& dynar, int index) const
-{
-  const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
-  return transition->dst;
-}
-
 } // namespace simgrid::mc

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index fda31aa..b07437a 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -70,21 +70,11 @@ public:
   bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) const;
   simgrid::mc::Snapshot* take_snapshot(long num_state) const;
 
-  // SESSION APIs
-  void s_close();
-
   // AUTOMATION APIs
-  void automaton_load(const char* file) const;
-  std::vector<int> automaton_propositional_symbol_evaluate() const;
-  std::vector<xbt_automaton_state_t> get_automaton_state() const;
-  int compare_automaton_exp_label(const xbt_automaton_exp_label* l) const;
-  void set_property_automaton(xbt_automaton_state_t const& automaton_state) const;
   inline DerefAndCompareByActorsCountAndUsedHeap compare_pair() const
   {
     return DerefAndCompareByActorsCountAndUsedHeap();
   }
-  xbt_automaton_exp_label_t get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const;
-  xbt_automaton_state_t get_automaton_transition_dst(xbt_dynar_t const& dynar, int index) const;
 };
 
 } // namespace simgrid::mc

diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp
index 4201cfd..b341657 100644 (file)
--- a/src/mc/api/RemoteApp.hpp
+++ b/src/mc/api/RemoteApp.hpp
@@ -54,6 +54,9 @@ public:
 
   /* Get the list of actors that are ready to run at that step. Usually shorter than maxpid */
   void get_actors_status(std::map<aid_t, ActorState>& whereto);
+
+  /* Get the remote process */
+  RemoteProcess& get_remote_process() { return model_checker_->get_remote_process(); }
 };
 } // namespace simgrid::mc
 

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 11bbb87..297fd0a 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -31,7 +31,7 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t prop_state,
   this->atomic_propositions = std::move(atomic_propositions);
 }
 
-static bool evaluate_label(const xbt_automaton_exp_label* l, std::vector<int> const& values)
+bool LivenessChecker::evaluate_label(const xbt_automaton_exp_label* l, std::vector<int> const& values)
 {
   switch (l->type) {
     case xbt_automaton_exp_label::AUT_OR:
@@ -41,7 +41,7 @@ static bool evaluate_label(const xbt_automaton_exp_label* l, std::vector<int> co
     case xbt_automaton_exp_label::AUT_NOT:
       return not evaluate_label(l->u.exp_not, values);
     case xbt_automaton_exp_label::AUT_PREDICAT:
-      return values.at(Api::get().compare_automaton_exp_label(l)) != 0;
+      return values.at(compare_automaton_exp_label(l)) != 0;
     case xbt_automaton_exp_label::AUT_ONE:
       return true;
     default:
@@ -53,7 +53,7 @@ Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) {}
 
 std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values() const
 {
-  auto values = Api::get().automaton_propositional_symbol_evaluate();
+  auto values = automaton_propositional_symbol_evaluate();
   return std::make_shared<const std::vector<int>>(std::move(values));
 }
 
@@ -179,6 +179,78 @@ void LivenessChecker::purge_visited_pairs()
 }
 
 LivenessChecker::LivenessChecker(RemoteApp& remote_app) : Exploration(remote_app) {}
+LivenessChecker::~LivenessChecker()
+{
+  if (property_automaton_ != nullptr)
+    xbt_automaton_free(property_automaton_);
+}
+
+xbt_automaton_t LivenessChecker::property_automaton_ = nullptr;
+
+void LivenessChecker::automaton_load(const char* file)
+{
+  if (property_automaton_ == nullptr)
+    property_automaton_ = xbt_automaton_new();
+
+  xbt_automaton_load(property_automaton_, file);
+}
+
+std::vector<int> LivenessChecker::automaton_propositional_symbol_evaluate() const
+{
+  unsigned int cursor = 0;
+  std::vector<int> values;
+  xbt_automaton_propositional_symbol_t ps = nullptr;
+  xbt_dynar_foreach (property_automaton_->propositional_symbols, cursor, ps)
+    values.push_back(xbt_automaton_propositional_symbol_evaluate(ps));
+  return values;
+}
+
+std::vector<xbt_automaton_state_t> LivenessChecker::get_automaton_state() const
+{
+  std::vector<xbt_automaton_state_t> automaton_stack;
+  unsigned int cursor = 0;
+  xbt_automaton_state_t automaton_state;
+  xbt_dynar_foreach (property_automaton_->states, cursor, automaton_state)
+    if (automaton_state->type == -1)
+      automaton_stack.push_back(automaton_state);
+  return automaton_stack;
+}
+
+int LivenessChecker::compare_automaton_exp_label(const xbt_automaton_exp_label* l) const
+{
+  unsigned int cursor                    = 0;
+  xbt_automaton_propositional_symbol_t p = nullptr;
+  xbt_dynar_foreach (property_automaton_->propositional_symbols, cursor, p) {
+    if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
+      return cursor;
+  }
+  return -1;
+}
+
+void LivenessChecker::set_property_automaton(xbt_automaton_state_t const& automaton_state) const
+{
+  property_automaton_->current_state = automaton_state;
+}
+
+xbt_automaton_exp_label_t LivenessChecker::get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const
+{
+  const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
+  return transition->label;
+}
+
+xbt_automaton_state_t LivenessChecker::get_automaton_transition_dst(xbt_dynar_t const& dynar, int index) const
+{
+  const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
+  return transition->dst;
+}
+void LivenessChecker::automaton_register_symbol(RemoteProcess& remote_process, const char* name, RemotePtr<int> address)
+{
+  if (property_automaton_ == nullptr)
+    property_automaton_ = xbt_automaton_new();
+
+  xbt::add_proposition(property_automaton_, name,
+                       [&remote_process, address]() { return remote_process.read(address); });
+}
 
 RecordTrace LivenessChecker::get_record_trace() // override
 {
@@ -269,7 +341,7 @@ void LivenessChecker::backtrack()
 void LivenessChecker::run()
 {
   XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str());
-  Api::get().automaton_load(_sg_mc_property_file.get().c_str());
+  automaton_load(_sg_mc_property_file.get().c_str());
 
   XBT_DEBUG("Starting the liveness algorithm");
 
@@ -280,7 +352,7 @@ void LivenessChecker::run()
 
   // For each initial state of the property automaton, push a
   // (application_state, automaton_state) pair to the exploration stack:
-  auto automaton_stack = Api::get().get_automaton_state();
+  auto automaton_stack = get_automaton_state();
   for (auto* automaton_state : automaton_stack) {
     if (automaton_state->type == -1)
       exploration_stack_.push_back(this->create_pair(nullptr, automaton_state, propos));
@@ -291,7 +363,7 @@ void LivenessChecker::run()
     std::shared_ptr<Pair> current_pair = exploration_stack_.back();
 
     /* Update current state in buchi automaton */
-    Api::get().set_property_automaton(current_pair->prop_state_);
+    set_property_automaton(current_pair->prop_state_);
 
     XBT_DEBUG(
         "********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)",
@@ -356,8 +428,8 @@ void LivenessChecker::run()
     // For each enabled transition in the property automaton, push a
     // (application_state, automaton_state) pair to the exploration stack:
     for (int i = xbt_dynar_length(current_pair->prop_state_->out) - 1; i >= 0; i--) {
-      const auto* transition_succ_label = Api::get().get_automaton_transition_label(current_pair->prop_state_->out, i);
-      auto* transition_succ_dst         = Api::get().get_automaton_transition_dst(current_pair->prop_state_->out, i);
+      const auto* transition_succ_label = get_automaton_transition_label(current_pair->prop_state_->out, i);
+      auto* transition_succ_dst         = get_automaton_transition_dst(current_pair->prop_state_->out, i);
       if (evaluate_label(transition_succ_label, *prop_values))
         exploration_stack_.push_back(this->create_pair(current_pair.get(), transition_succ_dst, prop_values));
     }

diff --git a/src/mc/explo/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp
index 45d3c18..819871f 100644 (file)
--- a/src/mc/explo/LivenessChecker.hpp
+++ b/src/mc/explo/LivenessChecker.hpp
@@ -51,6 +51,8 @@ public:
 class XBT_PRIVATE LivenessChecker : public Exploration {
 public:
   explicit LivenessChecker(RemoteApp& remote_app);
+  virtual ~LivenessChecker();
+
   void run() override;
   RecordTrace get_record_trace() override;
   std::vector<std::string> get_textual_trace() override;
@@ -76,6 +78,29 @@ private:
   unsigned long expanded_pairs_count_ = 0;
   int previous_pair_                  = 0;
   std::string previous_request_;
+
+  /* The property automaton must be a static because it's sometimes used before the explorer is even created.
+   *
+   * This can happen if some symbols are created during the application's initialization process, before the first
+   * decision point for the model-checker. Since the first snapshot is taken at the first decision point and since the
+   * explorer is created after the first snapshot, this may result in some symbols being registered even before the
+   * model-checker notices that this is a LivenessChecker to create.
+   *
+   * This situation is unfortunate, but I guess that it's the best I can achieve given the state of our initialization
+   * code.
+   */
+  static xbt_automaton_t property_automaton_;
+  bool evaluate_label(const xbt_automaton_exp_label* l, std::vector<int> const& values);
+
+public:
+  void automaton_load(const char* file);
+  std::vector<int> automaton_propositional_symbol_evaluate() const;
+  std::vector<xbt_automaton_state_t> get_automaton_state() const;
+  int compare_automaton_exp_label(const xbt_automaton_exp_label* l) const;
+  void set_property_automaton(xbt_automaton_state_t const& automaton_state) const;
+  xbt_automaton_exp_label_t get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const;
+  xbt_automaton_state_t get_automaton_transition_dst(xbt_dynar_t const& dynar, int index) const;
+  static void automaton_register_symbol(RemoteProcess& remote_process, const char* name, RemotePtr<int> addr);
 };
 
 } // namespace simgrid::mc

diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp
index df44857..bcbe09c 100644 (file)
--- a/src/mc/explo/simgrid_mc.cpp
+++ b/src/mc/explo/simgrid_mc.cpp
@@ -71,6 +71,7 @@ int main(int argc, char** argv)
   int res      = SIMGRID_MC_EXIT_SUCCESS;
   std::unique_ptr<simgrid::mc::Exploration> checker{
       simgrid::mc::Api::get().initialize(argv_copy.data(), environment, algo)};
+
   try {
     checker->run();
   } catch (const simgrid::mc::DeadlockError&) {
@@ -80,6 +81,5 @@ int main(int argc, char** argv)
   } catch (const simgrid::mc::LivenessError&) {
     res = SIMGRID_MC_EXIT_LIVENESS;
   }
-  simgrid::mc::Api::get().s_close();
   return res;
 }

diff --git a/src/mc/mc_private.hpp b/src/mc/mc_private.hpp
index fc37957..969d5fe 100644 (file)
--- a/src/mc/mc_private.hpp
+++ b/src/mc/mc_private.hpp
@@ -27,8 +27,6 @@ XBT_PRIVATE void find_object_address(std::vector<simgrid::xbt::VmMap> const& map
 XBT_PRIVATE
 bool snapshot_equal(const Snapshot* s1, const Snapshot* s2);
 
-// Move is somewhere else (in the LivenessChecker class, in the Session class?):
-extern XBT_PRIVATE xbt_automaton_t property_automaton;
 } // namespace simgrid::mc
 
 #endif