X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/74abafcd3702b62d42041354260d1f5e3508fa38..fa99c09da4eba77232ea090dd79e6dfa98e783dc:/src/mc/checker/LivenessChecker.cpp

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index c1afd7a597..2f7a6a9379 100644
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -1,34 +1,18 @@
-/* Copyright (c) 2011-2018. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2011-2019. 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 <cstring>
-
-#include <memory>
-#include <list>
-
-#include <boost/range/algorithm.hpp>
-
-#include <unistd.h>
-#include <sys/wait.h>
-
-#include <xbt/automaton.h>
-#include <xbt/dynar.h>
-#include <xbt/log.h>
-#include <xbt/sysdep.h>
-
-#include "src/mc/Session.hpp"
-#include "src/mc/Transition.hpp"
 #include "src/mc/checker/LivenessChecker.hpp"
+#include "src/mc/Session.hpp"
+#include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/mc_private.hpp"
-#include "src/mc/mc_record.hpp"
-#include "src/mc/mc_replay.hpp"
 #include "src/mc/mc_request.hpp"
 #include "src/mc/mc_smx.hpp"
-#include "src/mc/remote/Client.hpp"
+
+#include <boost/range/algorithm.hpp>
+#include <cstring>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification");
 
@@ -100,9 +84,7 @@ int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::Visi
 {
   simgrid::mc::Snapshot* s1 = state1->graph_state->system_state.get();
   simgrid::mc::Snapshot* s2 = state2->graph_state->system_state.get();
-  int num1 = state1->num;
-  int num2 = state2->num;
-  return simgrid::mc::snapshot_compare(num1, s1, num2, s2);
+  return simgrid::mc::snapshot_compare(s1, s2);
 }
 
 std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair)
@@ -150,13 +132,13 @@ void LivenessChecker::replay()
   if(_sg_mc_checkpoint > 0) {
     simgrid::mc::Pair* pair = explorationStack_.back().get();
     if(pair->graph_state->system_state){
-      simgrid::mc::restore_snapshot(pair->graph_state->system_state);
+      pair->graph_state->system_state->restore(&mc_model_checker->process());
       return;
     }
   }
 
   /* Restore the initial state */
-  simgrid::mc::session->restoreInitialState();
+  simgrid::mc::session->restore_initial_state();
 
   /* Traverse the stack from the initial state and re-execute the transitions */
   int depth = 1;
@@ -202,7 +184,7 @@ void LivenessChecker::replay()
 }
 
 /**
- * \brief Checks whether a given pair has already been visited by the algorithm.
+ * @brief Checks whether a given pair has already been visited by the algorithm.
  */
 int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair)
 {
@@ -251,7 +233,7 @@ void LivenessChecker::purgeVisitedPairs()
   }
 }
 
-LivenessChecker::LivenessChecker(Session& session) : Checker(session)
+LivenessChecker::LivenessChecker(Session& s) : Checker(s)
 {
 }
 
@@ -275,12 +257,12 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth)
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
   XBT_INFO("|             ACCEPTANCE CYCLE            |");
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-  XBT_INFO("Counter-example that violates formula :");
-  simgrid::mc::dumpRecordPath();
+  XBT_INFO("Counter-example that violates formula:");
   for (auto const& s : this->getTextualTrace())
-    XBT_INFO("%s", s.c_str());
-  simgrid::mc::session->logState();
-  XBT_INFO("Counter-example depth : %zu", depth);
+    XBT_INFO("  %s", s.c_str());
+  simgrid::mc::dumpRecordPath();
+  simgrid::mc::session->log_state();
+  XBT_INFO("Counter-example depth: %zu", depth);
 }
 
 std::vector<std::string> LivenessChecker::getTextualTrace() // override
@@ -345,8 +327,8 @@ void LivenessChecker::backtrack()
 
 void LivenessChecker::run()
 {
-  XBT_INFO("Check the liveness property %s", _sg_mc_property_file.c_str());
-  MC_automaton_load(_sg_mc_property_file.c_str());
+  XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str());
+  MC_automaton_load(_sg_mc_property_file.get().c_str());
 
   XBT_DEBUG("Starting the liveness algorithm");
   simgrid::mc::session->initialize();
@@ -446,8 +428,9 @@ void LivenessChecker::run()
 
     // For each enabled transition in the property automaton, push a
     // (application_state, automaton_state) pair to the exploration stack:
-    for (int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1; cursor >= 0; cursor--) {
-      xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
+    for (int i = xbt_dynar_length(current_pair->automaton_state->out) - 1; i >= 0; i--) {
+      xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(
+          current_pair->automaton_state->out, i, xbt_automaton_transition_t);
       if (evaluate_label(transition_succ->label, *prop_values))
           explorationStack_.push_back(this->newPair(
             current_pair.get(), transition_succ->dst, prop_values));
@@ -456,12 +439,12 @@ void LivenessChecker::run()
   }
 
   XBT_INFO("No property violation found.");
-  simgrid::mc::session->logState();
+  simgrid::mc::session->log_state();
 }
 
-Checker* createLivenessChecker(Session& session)
+Checker* createLivenessChecker(Session& s)
 {
-  return new LivenessChecker(session);
+  return new LivenessChecker(s);
 }
 
 }