X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/01565540f1e39584fb5714d4f4c361ff518917f1..27a9aa0b573913afcce5c1a39aababe43b96953b:/src/mc/checker/LivenessChecker.cpp

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 37bf22227e..b14a94de6d 100644
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -10,12 +10,15 @@
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_request.hpp"
 #include "src/mc/mc_smx.hpp"
+#include "src/mc/mc_api.hpp"
 
 #include <boost/range/algorithm.hpp>
 #include <cstring>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification");
 
+using mcapi = simgrid::mc::mc_api;
+
 /********* Static functions *********/
 
 namespace simgrid {
@@ -72,19 +75,14 @@ Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs)
 
 std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values() const
 {
-  std::vector<int> values;
-  unsigned int cursor = 0;
-  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));
+  auto values = mcapi::get().automaton_propositional_symbol_evaluate();  
   return std::make_shared<const std::vector<int>>(std::move(values));
 }
 
 std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair)
 {
-  std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(
-    pair->num, pair->automaton_state, pair->atomic_propositions,
-    pair->graph_state);
+  auto new_pair =
+      std::make_shared<VisitedPair>(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 
   auto res = boost::range::equal_range(acceptance_pairs_, new_pair.get(), DerefAndCompareByActorsCountAndUsedHeap());
 
@@ -145,16 +143,14 @@ void LivenessChecker::replay()
 
       smx_simcall_t req = nullptr;
 
-      if (saved_req != nullptr) {
-        /* because we got a copy of the executed request, we have to fetch the
-             real one, pointed by the request field of the issuer process */
-        const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
-        req                      = &issuer->simcall_;
+      /* because we got a copy of the executed request, we have to fetch the
+         real one, pointed by the request field of the issuer process */
+      const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
+      req                      = &issuer->simcall_;
 
-        /* Debug information */
-        XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
-                  request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
-      }
+      /* Debug information */
+      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
+                mcapi::get().request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
 
       this->get_session().execute(state->transition_);
     }
@@ -232,7 +228,7 @@ void LivenessChecker::log_state() // override
 {
   XBT_INFO("Expanded pairs = %lu", expanded_pairs_count_);
   XBT_INFO("Visited pairs = %lu", visited_pairs_count_);
-  XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
+  XBT_INFO("Executed transitions = %lu", mcapi::get().mc_get_executed_trans());
 }
 
 void LivenessChecker::show_acceptance_cycle(std::size_t depth)
@@ -243,8 +239,8 @@ void LivenessChecker::show_acceptance_cycle(std::size_t depth)
   XBT_INFO("Counter-example that violates formula:");
   for (auto const& s : this->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
-  mc::dumpRecordPath();
-  mc::session->log_state();
+  mcapi::get().dump_record_path();
+  mcapi::get().log_state();
   XBT_INFO("Counter-example depth: %zu", depth);
 }
 
@@ -254,8 +250,8 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
   for (std::shared_ptr<Pair> const& pair : exploration_stack_) {
     int req_num       = pair->graph_state->transition_.argument_;
     smx_simcall_t req = &pair->graph_state->executed_req_;
-    if (req && req->call_ != SIMCALL_NONE)
-      trace.push_back(request_to_string(req, req_num, RequestType::executed));
+    if (req->call_ != simix::Simcall::NONE)
+      trace.push_back(mcapi::get().request_to_string(req, req_num, RequestType::executed));
   }
   return trace;
 }
@@ -263,18 +259,20 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
 std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt_automaton_state_t state,
                                                    std::shared_ptr<const std::vector<int>> propositions)
 {
-  expanded_pairs_count_++;
-  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(expanded_pairs_count_);
+  ++expanded_pairs_count_;
+  ++expanded_states_count_;
+  auto next_pair                  = std::make_shared<Pair>(expanded_pairs_count_);
   next_pair->automaton_state      = state;
-  next_pair->graph_state          = std::make_shared<State>(++expanded_states_count_);
+  next_pair->graph_state          = std::make_shared<State>(expanded_states_count_);
   next_pair->atomic_propositions  = std::move(propositions);
   if (current_pair)
     next_pair->depth = current_pair->depth + 1;
   else
     next_pair->depth = 1;
   /* Get enabled actors and insert them in the interleave set of the next graph_state */
-  for (auto& actor : mc_model_checker->get_remote_simulation().actors())
     if (mc::actor_is_enabled(actor.copy.get_buffer()))
+  auto actors = mcapi::get().get_actors();
+  for (auto& actor : actors)
       next_pair->graph_state->add_interleaving_set(actor.copy.get_buffer());
   next_pair->requests = next_pair->graph_state->interleave_size();
   /* FIXME : get search_cycle value for each accepting state */
@@ -310,10 +308,10 @@ void LivenessChecker::backtrack()
 void LivenessChecker::run()
 {
   XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str());
-  MC_automaton_load(_sg_mc_property_file.get().c_str());
+  mcapi::get().automaton_load(_sg_mc_property_file.get().c_str());
 
   XBT_DEBUG("Starting the liveness algorithm");
-  mc::session->initialize();
+  mcapi::get().session_initialize();
 
   /* Initialize */
   this->previous_pair_ = 0;
@@ -370,7 +368,7 @@ void LivenessChecker::run()
       }
     }
 
-    smx_simcall_t req = MC_state_choose_request(current_pair->graph_state.get());
+    smx_simcall_t req = mcapi::get().mc_state_choose_request(current_pair->graph_state.get());
     int req_num       = current_pair->graph_state->transition_.argument_;
 
     if (dot_output != nullptr) {
@@ -386,7 +384,7 @@ void LivenessChecker::run()
       fflush(dot_output);
     }
 
-    XBT_DEBUG("Execute: %s", request_to_string(req, req_num, RequestType::simix).c_str());
+    XBT_DEBUG("Execute: %s", mcapi::get().request_to_string(req, req_num, RequestType::simix).c_str());
 
     /* Update stats */
     mc_model_checker->executed_transitions++;