mc: move some files related to ELF, DWARF or unwind reading into their own directory

[simgrid.git] / src / mc / checker / LivenessChecker.cpp

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index cf35963..cd49a87 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2011-2017. 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. */
@@ -15,7 +15,6 @@
 
 #include <xbt/automaton.h>
 #include <xbt/dynar.h>
-#include <xbt/dynar.hpp>
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 
@@ -32,7 +31,6 @@
 #include "src/mc/remote/Client.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification");
-extern std::string _sg_mc_property_file;
 
 /********* Static functions *********/
 
@@ -102,9 +100,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)
@@ -204,7 +200,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)
 {
@@ -253,7 +249,7 @@ void LivenessChecker::purgeVisitedPairs()
   }
 }
 
-LivenessChecker::LivenessChecker(Session& session) : Checker(session)
+LivenessChecker::LivenessChecker(Session& s) : Checker(s)
 {
 }
 
@@ -277,12 +273,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());
+    XBT_INFO("  %s", s.c_str());
+  simgrid::mc::dumpRecordPath();
   simgrid::mc::session->logState();
-  XBT_INFO("Counter-example depth : %zu", depth);
+  XBT_INFO("Counter-example depth: %zu", depth);
 }
 
 std::vector<std::string> LivenessChecker::getTextualTrace() // override
@@ -347,8 +343,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();
@@ -448,8 +444,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));
@@ -461,9 +458,9 @@ void LivenessChecker::run()
   simgrid::mc::session->logState();
 }
 
-Checker* createLivenessChecker(Session& session)
+Checker* createLivenessChecker(Session& s)
 {
-  return new LivenessChecker(session);
+  return new LivenessChecker(s);
 }
 
 }