[project-description] Fix extraction of the ns-3 version.

[simgrid.git] / src / mc / api.cpp

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 29b0608..840ffef 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -28,66 +28,11 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(Api, mc, "Logging specific to MC Facade APIs ");
 XBT_LOG_EXTERNAL_CATEGORY(mc_global);
 
-using Simcall = simgrid::simix::Simcall;
+namespace simgrid::mc {
 
-namespace simgrid {
-namespace mc {
-
-/** Statically "upcast" a s_smx_actor_t into an ActorInformation
- *
- *  This gets 'actorInfo' from '&actorInfo->copy'. It upcasts in the
- *  sense that we could achieve the same thing by having ActorInformation
- *  inherit from s_smx_actor_t but we don't really want to do that.
- */
-static simgrid::mc::ActorInformation* actor_info_cast(smx_actor_t actor)
-{
-  simgrid::mc::ActorInformation temp;
-  std::size_t offset = (char*)temp.copy.get_buffer() - (char*)&temp;
-
-  auto* process_info = reinterpret_cast<simgrid::mc::ActorInformation*>((char*)actor - offset);
-  return process_info;
-}
-
-xbt::string const& Api::get_actor_host_name(smx_actor_t actor) const
-{
-  if (mc_model_checker == nullptr)
-    return actor->get_host()->get_name();
-
-  const simgrid::mc::RemoteProcess* process = &mc_model_checker->get_remote_process();
-
-  // Read the simgrid::xbt::string in the MCed process:
-  simgrid::mc::ActorInformation* info = actor_info_cast(actor);
-
-  if (not info->hostname) {
-    Remote<s4u::Host> temp_host = process->read(remote(actor->get_host()));
-    auto remote_string_address  = remote(&xbt::string::to_string_data(temp_host.get_buffer()->get_impl()->get_name()));
-    simgrid::xbt::string_data remote_string = process->read(remote_string_address);
-    std::vector<char> hostname(remote_string.len + 1);
-    // no need to read the terminating null byte, and thus hostname[remote_string.len] is guaranteed to be '\0'
-    process->read_bytes(hostname.data(), remote_string.len, remote(remote_string.data));
-    info->hostname = &mc_model_checker->get_host_name(hostname.data());
-  }
-  return *info->hostname;
-}
-
-xbt::string const& Api::get_actor_name(smx_actor_t actor) const
-{
-  if (mc_model_checker == nullptr)
-    return actor->get_name();
-
-  simgrid::mc::ActorInformation* info = actor_info_cast(actor);
-  if (info->name.empty()) {
-    const simgrid::mc::RemoteProcess* process = &mc_model_checker->get_remote_process();
-
-    simgrid::xbt::string_data string_data = simgrid::xbt::string::to_string_data(actor->name_);
-    info->name = process->read_string(remote(string_data.data), string_data.len);
-  }
-  return info->name;
-}
-
-simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const
+simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::ExplorationAlgorithm algo)
 {
-  simgrid::mc::session_singleton = std::make_unique<simgrid::mc::Session>([argv] {
+  session_ = std::make_unique<simgrid::mc::Session>([argv] {
     int i = 1;
     while (argv[i] != nullptr && argv[i][0] == '-')
       i++;
@@ -99,20 +44,20 @@ simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgor
 
   simgrid::mc::Exploration* explo;
   switch (algo) {
-    case CheckerAlgorithm::CommDeterminism:
-      explo = simgrid::mc::create_communication_determinism_checker(session_singleton.get());
+    case ExplorationAlgorithm::CommDeterminism:
+      explo = simgrid::mc::create_communication_determinism_checker(session_.get());
       break;
 
-    case CheckerAlgorithm::UDPOR:
-      explo = simgrid::mc::create_udpor_checker(session_singleton.get());
+    case ExplorationAlgorithm::UDPOR:
+      explo = simgrid::mc::create_udpor_checker(session_.get());
       break;
 
-    case CheckerAlgorithm::Safety:
-      explo = simgrid::mc::create_safety_checker(session_singleton.get());
+    case ExplorationAlgorithm::Safety:
+      explo = simgrid::mc::create_dfs_exploration(session_.get());
       break;
 
-    case CheckerAlgorithm::Liveness:
-      explo = simgrid::mc::create_liveness_checker(session_singleton.get());
+    case ExplorationAlgorithm::Liveness:
+      explo = simgrid::mc::create_liveness_checker(session_.get());
       break;
 
     default:
@@ -142,12 +87,12 @@ std::size_t Api::get_remote_heap_bytes() const
 
 void Api::mc_inc_visited_states() const
 {
-  mc_model_checker->visited_states++;
+  mc_model_checker->inc_visited_states();
 }
 
 unsigned long Api::mc_get_visited_states() const
 {
-  return mc_model_checker->visited_states;
+  return mc_model_checker->get_visited_states();
 }
 
 void Api::mc_exit(int status) const
@@ -155,7 +100,7 @@ void Api::mc_exit(int status) const
   mc_model_checker->exit(status);
 }
 
-void Api::restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state) const
+void Api::restore_state(const simgrid::mc::Snapshot* system_state) const
 {
   system_state->restore(&mc_model_checker->get_remote_process());
 }
@@ -171,10 +116,9 @@ simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const
   return snapshot;
 }
 
-void Api::s_close() const
+void Api::s_close()
 {
-  session_singleton->close();
-  session_singleton.reset();
+  session_.reset();
   if (simgrid::mc::property_automaton != nullptr) {
     xbt_automaton_free(simgrid::mc::property_automaton);
     simgrid::mc::property_automaton = nullptr;
@@ -238,5 +182,4 @@ xbt_automaton_state_t Api::get_automaton_transition_dst(xbt_dynar_t const& dynar
   return transition->dst;
 }
 
-} // namespace mc
-} // namespace simgrid
+} // namespace simgrid::mc