Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
smx processes are now called actors, avoiding confusions in MC
[simgrid.git] / src / mc / SafetyChecker.cpp
index 78e3f61..47e2e70 100644 (file)
@@ -59,8 +59,7 @@ bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
 {
   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
     if (snapshot_compare(i->get(), current_state) == 0){
-      XBT_INFO("Non-progressive cycle : state %d -> state %d",
-        (*i)->num, current_state->num);
+      XBT_INFO("Non-progressive cycle: state %d -> state %d", (*i)->num, current_state->num);
       return true;
     }
   return false;
@@ -140,7 +139,7 @@ int SafetyChecker::run()
 
     /* Create the new expanded state */
     std::unique_ptr<simgrid::mc::State> next_state =
-      std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
+        std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 
     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
         MC_show_non_termination();
@@ -151,8 +150,8 @@ int SafetyChecker::run()
         || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
 
       /* Get an enabled process and insert it in the interleave set of the next state */
-      for (auto& p : mc_model_checker->process().simix_processes())
-        if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) {
+      for (auto& p : mc_model_checker->process().actors())
+        if (simgrid::mc::actor_is_enabled(p.copy.getBuffer())) {
           next_state->interleave(p.copy.getBuffer());
           if (reductionMode_ != simgrid::mc::ReductionMode::none)
             break;
@@ -319,15 +318,15 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session)
   XBT_DEBUG("Starting the safety algorithm");
 
   std::unique_ptr<simgrid::mc::State> initial_state =
-    std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
+      std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");
 
-  /* Get an enabled process and insert it in the interleave set of the initial state */
-  for (auto& p : mc_model_checker->process().simix_processes())
-    if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) {
-      initial_state->interleave(p.copy.getBuffer());
+  /* Get an enabled actor and insert it in the interleave set of the initial state */
+  for (auto& actor : mc_model_checker->process().actors())
+    if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
+      initial_state->interleave(actor.copy.getBuffer());
       if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }