Rename mc::Checker to mc::Exploration as it defines an exploration algo

diff --git a/MANIFEST.in b/MANIFEST.in
index f5cec52..ea185af 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2343,16 +2343,16 @@ include src/mc/api.cpp
 include src/mc/api.hpp
 include src/mc/api/State.cpp
 include src/mc/api/State.hpp
-include src/mc/checker/Checker.hpp
-include src/mc/checker/CommunicationDeterminismChecker.cpp
-include src/mc/checker/LivenessChecker.cpp
-include src/mc/checker/LivenessChecker.hpp
-include src/mc/checker/SafetyChecker.cpp
-include src/mc/checker/SafetyChecker.hpp
-include src/mc/checker/UdporChecker.cpp
-include src/mc/checker/UdporChecker.hpp
-include src/mc/checker/simgrid_mc.cpp
 include src/mc/compare.cpp
+include src/mc/explo/CommunicationDeterminismChecker.cpp
+include src/mc/explo/Exploration.hpp
+include src/mc/explo/LivenessChecker.cpp
+include src/mc/explo/LivenessChecker.hpp
+include src/mc/explo/SafetyChecker.cpp
+include src/mc/explo/SafetyChecker.hpp
+include src/mc/explo/UdporChecker.cpp
+include src/mc/explo/UdporChecker.hpp
+include src/mc/explo/simgrid_mc.cpp
 include src/mc/inspect/DwarfExpression.cpp
 include src/mc/inspect/DwarfExpression.hpp
 include src/mc/inspect/Frame.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index e389394..2b0d821 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -5,7 +5,7 @@
 
 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/Session.hpp"
-#include "src/mc/checker/Checker.hpp"
+#include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
@@ -136,9 +136,9 @@ static void MC_report_crash(int status)
   if (not xbt_log_no_loc)
     XBT_INFO("%s core dump was generated by the system.", WCOREDUMP(status) ? "A" : "No");
   XBT_INFO("Counter-example execution trace:");
-  for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
+  for (auto const& s : mc_model_checker->get_exploration()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
-  XBT_INFO("Path = %s", mc_model_checker->getChecker()->get_record_trace().to_string().c_str());
+  XBT_INFO("Path = %s", mc_model_checker->get_exploration()->get_record_trace().to_string().c_str());
   session_singleton->log_state();
   if (xbt_log_no_loc) {
     XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
@@ -227,9 +227,9 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       XBT_INFO("*** PROPERTY NOT VALID ***");
       XBT_INFO("**************************");
       XBT_INFO("Counter-example execution trace:");
-      for (auto const& s : getChecker()->get_textual_trace())
+      for (auto const& s : get_exploration()->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
-      XBT_INFO("Path = %s", getChecker()->get_record_trace().to_string().c_str());
+      XBT_INFO("Path = %s", get_exploration()->get_record_trace().to_string().c_str());
       session_singleton->log_state();
 
       this->exit(SIMGRID_MC_EXIT_SAFETY);

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index fd305fb..8bf67d3 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -27,7 +27,7 @@ class ModelChecker {
   // This is the parent snapshot of the current state:
   PageStore page_store_{500};
   std::unique_ptr<RemoteProcess> remote_process_;
-  Checker* checker_ = nullptr;
+  Exploration* exploration_ = nullptr;
 
   // Expect MessageType::SIMCALL_TO_STRING or MessageType::SIMCALL_DOT_LABEL
   std::string simcall_to_string(MessageType type, aid_t aid, int times_considered);
@@ -59,8 +59,8 @@ public:
 
   void finalize_app(bool terminate_asap = false);
 
-  Checker* getChecker() const { return checker_; }
-  void setChecker(Checker* checker) { checker_ = checker; }
+  Exploration* get_exploration() const { return exploration_; }
+  void set_exploration(Exploration* exploration) { exploration_ = exploration; }
 
 private:
   void setup_ignore();

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 0fbe964..dffeed7 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -4,9 +4,9 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/Session.hpp"
-#include "src/mc/checker/Checker.hpp"
-#include "src/mc/mc_config.hpp"
 #include "src/internal_config.h" // HAVE_SMPI
+#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/mc_config.hpp"
 #if HAVE_SMPI
 #include "smpi/smpi.h"
 #include "src/smpi/include/private.hpp"
@@ -116,7 +116,7 @@ void Session::restore_initial_state() const
 
 void Session::log_state() const
 {
-  model_checker_->getChecker()->log_state();
+  model_checker_->get_exploration()->log_state();
 
   if (not _sg_mc_dot_output_file.get().empty()) {
     fprintf(dot_output, "}\n");
@@ -169,9 +169,9 @@ void Session::check_deadlock() const
     XBT_CINFO(mc_global, "*** DEADLOCK DETECTED ***");
     XBT_CINFO(mc_global, "**************************");
     XBT_CINFO(mc_global, "Counter-example execution trace:");
-    for (auto const& frame : model_checker_->getChecker()->get_textual_trace())
+    for (auto const& frame : model_checker_->get_exploration()->get_textual_trace())
       XBT_CINFO(mc_global, "  %s", frame.c_str());
-    XBT_CINFO(mc_global, "Path = %s", model_checker_->getChecker()->get_record_trace().to_string().c_str());
+    XBT_CINFO(mc_global, "Path = %s", model_checker_->get_exploration()->get_record_trace().to_string().c_str());
     log_state();
     throw DeadlockError();
   }

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 6590c22..8ac88e5 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -9,7 +9,7 @@
 #include "src/kernel/activity/MutexImpl.hpp"
 #include "src/kernel/actor/SimcallObserver.hpp"
 #include "src/mc/Session.hpp"
-#include "src/mc/checker/Checker.hpp"
+#include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_base.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_pattern.hpp"
@@ -85,7 +85,7 @@ xbt::string const& Api::get_actor_name(smx_actor_t actor) const
   return info->name;
 }
 
-simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const
+simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const
 {
   auto session = new simgrid::mc::Session([argv] {
     int i = 1;
@@ -97,22 +97,22 @@ simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm
     xbt_die("The model-checked process failed to exec(%s): %s", argv[i], strerror(errno));
   });
 
-  simgrid::mc::Checker* checker;
+  simgrid::mc::Exploration* explo;
   switch (algo) {
     case CheckerAlgorithm::CommDeterminism:
-      checker = simgrid::mc::create_communication_determinism_checker(session);
+      explo = simgrid::mc::create_communication_determinism_checker(session);
       break;
 
     case CheckerAlgorithm::UDPOR:
-      checker = simgrid::mc::create_udpor_checker(session);
+      explo = simgrid::mc::create_udpor_checker(session);
       break;
 
     case CheckerAlgorithm::Safety:
-      checker = simgrid::mc::create_safety_checker(session);
+      explo = simgrid::mc::create_safety_checker(session);
       break;
 
     case CheckerAlgorithm::Liveness:
-      checker = simgrid::mc::create_liveness_checker(session);
+      explo = simgrid::mc::create_liveness_checker(session);
       break;
 
     default:
@@ -121,8 +121,8 @@ simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm
 
   // FIXME: session and checker are never deleted
   simgrid::mc::session_singleton = session;
-  mc_model_checker->setChecker(checker);
-  return checker;
+  mc_model_checker->set_exploration(explo);
+  return explo;
 }
 
 std::vector<simgrid::mc::ActorInformation>& Api::get_actors() const

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 1134b94..3889583 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -63,7 +63,7 @@ public:
     return api;
   }
 
-  simgrid::mc::Checker* initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const;
+  simgrid::mc::Exploration* initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const;
 
   // ACTOR APIs
   std::vector<simgrid::mc::ActorInformation>& get_actors() const;

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp
similarity index 95%
rename from src/mc/checker/CommunicationDeterminismChecker.cpp
rename to src/mc/explo/CommunicationDeterminismChecker.cpp
index 4a13814..e2b5d55 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/explo/CommunicationDeterminismChecker.cpp
@@ -5,7 +5,7 @@
 
 #include "src/kernel/activity/MailboxImpl.hpp"
 #include "src/mc/Session.hpp"
-#include "src/mc/checker/SafetyChecker.hpp"
+#include "src/mc/explo/SafetyChecker.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_forward.hpp"
@@ -32,15 +32,15 @@ enum class PatternCommunicationType {
 
 class PatternCommunication {
 public:
-  int num = 0;
+  int num                       = 0;
   uintptr_t comm_addr           = 0;
   PatternCommunicationType type = PatternCommunicationType::send;
   unsigned long src_proc        = 0;
   unsigned long dst_proc        = 0;
   unsigned mbox                 = 0;
   unsigned size                 = 0;
-  int tag   = 0;
-  int index = 0;
+  int tag                       = 0;
+  int index                     = 0;
 
   PatternCommunication dup() const
   {
@@ -49,10 +49,10 @@ public:
     res.comm_addr = this->comm_addr;
     res.type      = this->type;
     res.src_proc  = this->src_proc;
-    res.dst_proc = this->dst_proc;
-    res.mbox     = this->mbox;
+    res.dst_proc  = this->dst_proc;
+    res.mbox      = this->mbox;
     res.tag       = this->tag;
-    res.index = this->index;
+    res.index     = this->index;
     return res;
   }
 };
@@ -65,7 +65,7 @@ struct PatternCommunicationList {
 /********** Checker extension **********/
 
 struct CommDetExtension {
-  static simgrid::xbt::Extension<simgrid::mc::Checker, CommDetExtension> EXTENSION_ID;
+  static simgrid::xbt::Extension<simgrid::mc::Exploration, CommDetExtension> EXTENSION_ID;
 
   std::vector<simgrid::mc::PatternCommunicationList> initial_communications_pattern;
   std::vector<std::vector<simgrid::mc::PatternCommunication*>> incomplete_communications_pattern;
@@ -89,7 +89,7 @@ struct CommDetExtension {
   void complete_comm_pattern(const CommWaitTransition* transition);
   void handle_comm_pattern(const Transition* transition);
 };
-simgrid::xbt::Extension<simgrid::mc::Checker, CommDetExtension> CommDetExtension::EXTENSION_ID;
+simgrid::xbt::Extension<simgrid::mc::Exploration, CommDetExtension> CommDetExtension::EXTENSION_ID;
 /********** State Extension ***********/
 
 class StateCommDet {
@@ -246,7 +246,7 @@ void CommDetExtension::get_comm_pattern(const Transition* transition)
   } else if (transition->type_ == Transition::Type::COMM_RECV) {
     auto* recv = static_cast<const CommRecvTransition*>(transition);
 
-    pattern->type = PatternCommunicationType::receive;
+    pattern->type      = PatternCommunicationType::receive;
     pattern->comm_addr = recv->get_comm();
     pattern->tag       = recv->get_tag();
   }
@@ -285,7 +285,6 @@ void CommDetExtension::complete_comm_pattern(const CommWaitTransition* transitio
   }
 }
 
-
 void CommDetExtension::handle_comm_pattern(const Transition* transition)
 {
   if (not _sg_mc_comms_determinism && not _sg_mc_send_determinism)
@@ -323,9 +322,9 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition)
       }
  */
 
-Checker* create_communication_determinism_checker(Session* session)
+Exploration* create_communication_determinism_checker(Session* session)
 {
-  CommDetExtension::EXTENSION_ID = simgrid::mc::Checker::extension_create<CommDetExtension>();
+  CommDetExtension::EXTENSION_ID = simgrid::mc::Exploration::extension_create<CommDetExtension>();
   StateCommDet::EXTENSION_ID     = simgrid::mc::State::extension_create<StateCommDet>();
 
   XBT_DEBUG("********* Start communication determinism verification *********");

diff --git a/src/mc/checker/Checker.hpp b/src/mc/explo/Exploration.hpp
similarity index 75%
rename from src/mc/checker/Checker.hpp
rename to src/mc/explo/Exploration.hpp
index 542ba96..f0f7a3a 100644 (file)
--- a/src/mc/checker/Checker.hpp
+++ b/src/mc/explo/Exploration.hpp
@@ -12,7 +12,7 @@
 namespace simgrid {
 namespace mc {
 
-/** A model-checking algorithm
+/** A model-checking exploration algorithm
  *
  *  This is an abstract base class used to group the data, state, configuration
  *  of a model-checking algorithm.
@@ -25,17 +25,17 @@ namespace mc {
  * `Session` interface (but currently the `Session` interface does not
  *  have all the necessary features). */
 // abstract
-class Checker : public xbt::Extendable<Checker> {
+class Exploration : public xbt::Extendable<Exploration> {
   Session* session_;
 
 public:
-  explicit Checker(Session* session) : session_(session) {}
+  explicit Exploration(Session* session) : session_(session) {}
 
   // No copy:
-  Checker(Checker const&) = delete;
-  Checker& operator=(Checker const&) = delete;
+  Exploration(Exploration const&) = delete;
+  Exploration& operator=(Exploration const&) = delete;
 
-  virtual ~Checker() = default;
+  virtual ~Exploration() = default;
 
   /** Main function of this algorithm */
   virtual void run() = 0;
@@ -59,10 +59,10 @@ public:
 };
 
 // External constructors so that the types (and the types of their content) remain hidden
-XBT_PUBLIC Checker* create_liveness_checker(Session* session);
-XBT_PUBLIC Checker* create_safety_checker(Session* session);
-XBT_PUBLIC Checker* create_communication_determinism_checker(Session* session);
-XBT_PUBLIC Checker* create_udpor_checker(Session* session);
+XBT_PUBLIC Exploration* create_liveness_checker(Session* session);
+XBT_PUBLIC Exploration* create_safety_checker(Session* session);
+XBT_PUBLIC Exploration* create_communication_determinism_checker(Session* session);
+XBT_PUBLIC Exploration* create_udpor_checker(Session* session);
 
 } // namespace mc
 } // namespace simgrid

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
similarity index 84%
rename from src/mc/checker/LivenessChecker.cpp
rename to src/mc/explo/LivenessChecker.cpp
index 1a512aa..a0073d2 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -3,7 +3,7 @@
 /* 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. */
 
-#include "src/mc/checker/LivenessChecker.hpp"
+#include "src/mc/explo/LivenessChecker.hpp"
 #include "src/mc/Session.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
@@ -29,34 +29,31 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
   this->graph_state = std::move(graph_state);
   if (this->graph_state->system_state_ == nullptr)
     this->graph_state->system_state_ = std::make_shared<Snapshot>(pair_num);
-  this->heap_bytes_used = api::get().get_remote_heap_bytes();
+  this->heap_bytes_used     = api::get().get_remote_heap_bytes();
   this->actors_count        = api::get().get_actors().size();
-  this->other_num = -1;
+  this->other_num           = -1;
   this->atomic_propositions = std::move(atomic_propositions);
 }
 
 static bool evaluate_label(const xbt_automaton_exp_label* l, std::vector<int> const& values)
 {
   switch (l->type) {
-  case xbt_automaton_exp_label::AUT_OR:
-    return evaluate_label(l->u.or_and.left_exp, values)
-      || evaluate_label(l->u.or_and.right_exp, values);
-  case xbt_automaton_exp_label::AUT_AND:
-    return evaluate_label(l->u.or_and.left_exp, values)
-      && evaluate_label(l->u.or_and.right_exp, values);
-  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;
-  case xbt_automaton_exp_label::AUT_ONE:
-    return true;
-  default:
-    xbt_die("Unexpected value for automaton");
+    case xbt_automaton_exp_label::AUT_OR:
+      return evaluate_label(l->u.or_and.left_exp, values) || evaluate_label(l->u.or_and.right_exp, values);
+    case xbt_automaton_exp_label::AUT_AND:
+      return evaluate_label(l->u.or_and.left_exp, values) && evaluate_label(l->u.or_and.right_exp, values);
+    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;
+    case xbt_automaton_exp_label::AUT_ONE:
+      return true;
+    default:
+      xbt_die("Unexpected value for automaton");
   }
 }
 
-Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs)
-{}
+Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) {}
 
 std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values() const
 {
@@ -71,19 +68,21 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
 
   auto res = boost::range::equal_range(acceptance_pairs_, new_pair.get(), api::get().compare_pair());
 
-  if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) {
-    std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
-    if (api::get().automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 ||
-        *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
-        not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(), new_pair->graph_state->system_state_.get()))
-      continue;
-    XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
-    exploration_stack_.pop_back();
-    if (dot_output != nullptr)
-      fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num,
-              this->previous_request_.c_str());
-    return nullptr;
-  }
+  if (pair->search_cycle)
+    for (auto i = res.first; i != res.second; ++i) {
+      std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
+      if (api::get().automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 ||
+          *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
+          not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(),
+                                        new_pair->graph_state->system_state_.get()))
+        continue;
+      XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
+      exploration_stack_.pop_back();
+      if (dot_output != nullptr)
+        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num,
+                this->previous_request_.c_str());
+      return nullptr;
+    }
 
   acceptance_pairs_.insert(res.first, new_pair);
   return new_pair;
@@ -103,7 +102,7 @@ void LivenessChecker::replay()
   XBT_DEBUG("**** Begin Replay ****");
 
   /* Intermediate backtracking */
-  if(_sg_mc_checkpoint > 0) {
+  if (_sg_mc_checkpoint > 0) {
     const Pair* pair = exploration_stack_.back().get();
     if (pair->graph_state->system_state_) {
       api::get().restore_state(pair->graph_state->system_state_);
@@ -151,7 +150,8 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
     const VisitedPair* pair_test = i->get();
     if (api::get().automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 ||
         *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
-        not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(), visited_pair->graph_state->system_state_.get()))
+        not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(),
+                                      visited_pair->graph_state->system_state_.get()))
       continue;
     if (pair_test->other_num == -1)
       visited_pair->other_num = pair_test->num;
@@ -160,8 +160,8 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
     if (dot_output == nullptr)
       XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", visited_pair->num, pair_test->num);
     else
-      XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
-        visited_pair->num, pair_test->num, visited_pair->other_num);
+      XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", visited_pair->num,
+                pair_test->num, visited_pair->other_num);
     (*i) = std::move(visited_pair);
     return (*i)->other_num;
   }
@@ -181,7 +181,7 @@ void LivenessChecker::purge_visited_pairs()
   }
 }
 
-LivenessChecker::LivenessChecker(Session* session) : Checker(session) {}
+LivenessChecker::LivenessChecker(Session* session) : Exploration(session) {}
 
 RecordTrace LivenessChecker::get_record_trace() // override
 {
@@ -224,10 +224,10 @@ std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt
                                                    std::shared_ptr<const std::vector<int>> propositions)
 {
   ++expanded_pairs_count_;
-  auto next_pair                  = std::make_shared<Pair>(expanded_pairs_count_);
-  next_pair->automaton_state      = state;
-  next_pair->graph_state          = std::make_shared<State>();
-  next_pair->atomic_propositions  = std::move(propositions);
+  auto next_pair                 = std::make_shared<Pair>(expanded_pairs_count_);
+  next_pair->automaton_state     = state;
+  next_pair->graph_state         = std::make_shared<State>();
+  next_pair->atomic_propositions = std::move(propositions);
   if (current_pair)
     next_pair->depth = current_pair->depth + 1;
   else
@@ -372,7 +372,7 @@ void LivenessChecker::run()
   log_state();
 }
 
-Checker* create_liveness_checker(Session* session)
+Exploration* create_liveness_checker(Session* session)
 {
   return new LivenessChecker(session);
 }

diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp
similarity index 84%
rename from src/mc/checker/LivenessChecker.hpp
rename to src/mc/explo/LivenessChecker.hpp
index d2d34df..ea7c0e6 100644 (file)
--- a/src/mc/checker/LivenessChecker.hpp
+++ b/src/mc/explo/LivenessChecker.hpp
@@ -8,7 +8,7 @@
 #define SIMGRID_MC_LIVENESS_CHECKER_HPP
 
 #include "src/mc/api/State.hpp"
-#include "src/mc/checker/Checker.hpp"
+#include "src/mc/explo/Exploration.hpp"
 #include "xbt/automaton.hpp"
 
 #include <list>
@@ -20,13 +20,13 @@ namespace mc {
 
 class XBT_PRIVATE Pair {
 public:
-  int num = 0;
-  bool search_cycle = false;
+  int num                               = 0;
+  bool search_cycle                     = false;
   std::shared_ptr<State> graph_state    = nullptr; /* System state included */
   xbt_automaton_state_t automaton_state = nullptr;
   std::shared_ptr<const std::vector<int>> atomic_propositions;
-  int requests = 0;
-  int depth = 0;
+  int requests             = 0;
+  int depth                = 0;
   bool exploration_started = false;
 
   explicit Pair(unsigned long expanded_pairs);
@@ -38,7 +38,7 @@ public:
 class XBT_PRIVATE VisitedPair {
 public:
   int num;
-  int other_num = 0; /* Dot output for */
+  int other_num                      = 0;       /* Dot output for */
   std::shared_ptr<State> graph_state = nullptr; /* System state included */
   xbt_automaton_state_t automaton_state;
   std::shared_ptr<const std::vector<int>> atomic_propositions;
@@ -49,7 +49,7 @@ public:
               std::shared_ptr<const std::vector<int>> atomic_propositions, std::shared_ptr<State> graph_state);
 };
 
-class XBT_PRIVATE LivenessChecker : public Checker {
+class XBT_PRIVATE LivenessChecker : public Exploration {
 public:
   explicit LivenessChecker(Session* session);
   void run() override;
@@ -73,9 +73,9 @@ private:
   std::list<std::shared_ptr<Pair>> exploration_stack_;
   std::list<std::shared_ptr<VisitedPair>> acceptance_pairs_;
   std::list<std::shared_ptr<VisitedPair>> visited_pairs_;
-  unsigned long visited_pairs_count_   = 0;
-  unsigned long expanded_pairs_count_  = 0;
-  int previous_pair_                   = 0;
+  unsigned long visited_pairs_count_  = 0;
+  unsigned long expanded_pairs_count_ = 0;
+  int previous_pair_                  = 0;
   std::string previous_request_;
 };
 

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/explo/SafetyChecker.cpp
similarity index 98%
rename from src/mc/checker/SafetyChecker.cpp
rename to src/mc/explo/SafetyChecker.cpp
index 284acd4..07e176d 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/explo/SafetyChecker.cpp
@@ -3,7 +3,7 @@
 /* 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. */
 
-#include "src/mc/checker/SafetyChecker.hpp"
+#include "src/mc/explo/SafetyChecker.hpp"
 #include "src/mc/Session.hpp"
 #include "src/mc/VisitedState.hpp"
 #include "src/mc/mc_config.hpp"
@@ -268,7 +268,7 @@ void SafetyChecker::restore_state()
   }
 }
 
-SafetyChecker::SafetyChecker(Session* session) : Checker(session)
+SafetyChecker::SafetyChecker(Session* session) : Exploration(session)
 {
   reductionMode_ = reduction_mode;
   if (_sg_mc_termination)
@@ -309,7 +309,7 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session)
   stack_.push_back(std::move(initial_state));
 }
 
-Checker* create_safety_checker(Session* session)
+Exploration* create_safety_checker(Session* session)
 {
   return new SafetyChecker(session);
 }

diff --git a/src/mc/checker/SafetyChecker.hpp b/src/mc/explo/SafetyChecker.hpp
similarity index 97%
rename from src/mc/checker/SafetyChecker.hpp
rename to src/mc/explo/SafetyChecker.hpp
index 3851d39..3cd00c7 100644 (file)
--- a/src/mc/checker/SafetyChecker.hpp
+++ b/src/mc/explo/SafetyChecker.hpp
@@ -8,7 +8,7 @@
 #define SIMGRID_MC_SAFETY_CHECKER_HPP
 
 #include "src/mc/VisitedState.hpp"
-#include "src/mc/checker/Checker.hpp"
+#include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_safety.hpp"
 
 #include <list>
@@ -19,7 +19,7 @@
 namespace simgrid {
 namespace mc {
 
-class XBT_PRIVATE SafetyChecker : public Checker {
+class XBT_PRIVATE SafetyChecker : public Exploration {
   ReductionMode reductionMode_ = ReductionMode::unset;
   long backtrack_count_        = 0;
 

diff --git a/src/mc/checker/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
similarity index 79%
rename from src/mc/checker/UdporChecker.cpp
rename to src/mc/explo/UdporChecker.cpp
index 904e066..fd932b6 100644 (file)
--- a/src/mc/checker/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -3,7 +3,7 @@
 /* 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. */
 
-#include "src/mc/checker/UdporChecker.hpp"
+#include "src/mc/explo/UdporChecker.hpp"
 #include <xbt/log.h>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety verification ");
@@ -11,7 +11,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety ver
 namespace simgrid {
 namespace mc {
 
-UdporChecker::UdporChecker(Session* session) : Checker(session) {}
+UdporChecker::UdporChecker(Session* session) : Exploration(session) {}
 
 void UdporChecker::run() {}
 
@@ -29,7 +29,7 @@ std::vector<std::string> UdporChecker::get_textual_trace()
 
 void UdporChecker::log_state() {}
 
-Checker* create_udpor_checker(Session* session)
+Exploration* create_udpor_checker(Session* session)
 {
   return new UdporChecker(session);
 }

diff --git a/src/mc/checker/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp
similarity index 87%
rename from src/mc/checker/UdporChecker.hpp
rename to src/mc/explo/UdporChecker.hpp
index 514c7f4..069c515 100644 (file)
--- a/src/mc/checker/UdporChecker.hpp
+++ b/src/mc/explo/UdporChecker.hpp
@@ -7,13 +7,13 @@
 #ifndef SIMGRID_MC_UDPOR_CHECKER_HPP
 #define SIMGRID_MC_UDPOR_CHECKER_HPP
 
-#include "src/mc/checker/Checker.hpp"
+#include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_record.hpp"
 
 namespace simgrid {
 namespace mc {
 
-class XBT_PRIVATE UdporChecker : public Checker {
+class XBT_PRIVATE UdporChecker : public Exploration {
 public:
   explicit UdporChecker(Session* session);
   void run() override;

diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp
similarity index 90%
rename from src/mc/checker/simgrid_mc.cpp
rename to src/mc/explo/simgrid_mc.cpp
index 5ad9992..8da0002 100644 (file)
--- a/src/mc/checker/simgrid_mc.cpp
+++ b/src/mc/explo/simgrid_mc.cpp
@@ -1,14 +1,13 @@
-/* Copyright (c) 2015-2022. The SimGrid Team.
- * All rights reserved.                                                     */
+/* Copyright (c) 2015-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. */
 
 #include "simgrid/sg_config.hpp"
-#include "src/mc/checker/Checker.hpp"
+#include "src/internal_config.h"
+#include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
-#include "src/internal_config.h"
 
 #if HAVE_SMPI
 #include "smpi/smpi.h"
@@ -20,8 +19,7 @@
 
 using api = simgrid::mc::Api;
 
-static inline
-char** argvdup(int argc, char** argv)
+static inline char** argvdup(int argc, char** argv)
 {
   auto* argv_copy = new char*[argc + 1];
   std::memcpy(argv_copy, argv, sizeof(char*) * argc);

diff --git a/src/mc/mc_forward.hpp b/src/mc/mc_forward.hpp
index dc0e571..5972ec1 100644 (file)
--- a/src/mc/mc_forward.hpp
+++ b/src/mc/mc_forward.hpp
@@ -29,8 +29,7 @@ class Frame;
 class ActorInformation;
 
 class Session;
-class Checker;
-
+class Exploration;
 }
 }
 

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 51c4074..5a75da0 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -8,7 +8,7 @@
 
 #if SIMGRID_HAVE_MC
 #include "src/mc/Session.hpp"
-#include "src/mc/checker/Checker.hpp"
+#include "src/mc/explo/Exploration.hpp"
 #include "src/mc/inspect/mc_unw.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_private.hpp"

diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp
index ff31303..dbc8e7c 100644 (file)
--- a/src/mc/mc_record.cpp
+++ b/src/mc/mc_record.cpp
@@ -12,7 +12,7 @@
 
 #if SIMGRID_HAVE_MC
 #include "src/mc/api/State.hpp"
-#include "src/mc/checker/Checker.hpp"
+#include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_private.hpp"
 #endif
 

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 68a60f0..9750bf5 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -558,14 +558,14 @@ set(MC_SRC_BASE
   )
 
 set(MC_SRC
-  src/mc/checker/Checker.hpp
-  src/mc/checker/CommunicationDeterminismChecker.cpp
-  src/mc/checker/SafetyChecker.cpp
-  src/mc/checker/SafetyChecker.hpp
-  src/mc/checker/LivenessChecker.cpp
-  src/mc/checker/LivenessChecker.hpp
-  src/mc/checker/UdporChecker.cpp
-  src/mc/checker/UdporChecker.hpp
+  src/mc/explo/Exploration.hpp
+  src/mc/explo/CommunicationDeterminismChecker.cpp
+  src/mc/explo/SafetyChecker.cpp
+  src/mc/explo/SafetyChecker.hpp
+  src/mc/explo/LivenessChecker.cpp
+  src/mc/explo/LivenessChecker.hpp
+  src/mc/explo/UdporChecker.cpp
+  src/mc/explo/UdporChecker.hpp
 
   src/mc/inspect/DwarfExpression.hpp
   src/mc/inspect/DwarfExpression.cpp
@@ -640,7 +640,7 @@ set(MC_SRC
   src/mc/udpor_global.hpp
   )
 
-set(MC_SIMGRID_MC_SRC  src/mc/checker/simgrid_mc.cpp)
+set(MC_SIMGRID_MC_SRC  src/mc/explo/simgrid_mc.cpp)
 
 set(headers_to_install
   include/simgrid/actor.h