X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/558e19f535bb0c65b610bc758c8133ded549ca3c..603a2971cfa9ec8a4fd4493b74c5680956828423:/src/mc/checker/LivenessChecker.cpp

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 4f3a21a431..4c5a2ca033 100644
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -1,5 +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. */
@@ -16,20 +15,19 @@
 
 #include <xbt/automaton.h>
 #include <xbt/dynar.h>
-#include <xbt/dynar.hpp>
 #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/mc_exit.h"
-#include "src/mc/mc_private.h"
-#include "src/mc/mc_private.h"
-#include "src/mc/mc_record.h"
-#include "src/mc/mc_replay.h"
-#include "src/mc/mc_request.h"
-#include "src/mc/mc_smx.h"
+#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"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification");
@@ -76,6 +74,7 @@ static bool evaluate_label(xbt_automaton_exp_label_t l, std::vector<int> const&
           return values[cursor] != 0;
       }
       xbt_die("Missing predicate");
+      break;
     }
   case xbt_automaton_exp_label::AUT_ONE:
     return true;
@@ -203,7 +202,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)
 {
@@ -252,7 +251,7 @@ void LivenessChecker::purgeVisitedPairs()
   }
 }
 
-LivenessChecker::LivenessChecker(Session& session) : Checker(session)
+LivenessChecker::LivenessChecker(Session& s) : Checker(s)
 {
 }
 
@@ -266,7 +265,6 @@ RecordTrace LivenessChecker::getRecordTrace() // override
 
 void LivenessChecker::logState() // override
 {
-  Checker::logState();
   XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
   XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
@@ -277,12 +275,12 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth)
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
   XBT_INFO("|             ACCEPTANCE CYCLE            |");
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-  XBT_INFO("Counter-example that violates formula :");
+  XBT_INFO("Counter-example that violates formula:");
+  for (auto const& s : this->getTextualTrace())
+    XBT_INFO("  %s", s.c_str());
   simgrid::mc::dumpRecordPath();
-  for (auto& s : this->getTextualTrace())
-    XBT_INFO("%s", s.c_str());
   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
@@ -301,7 +299,8 @@ std::vector<std::string> LivenessChecker::getTextualTrace() // override
 std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state,
                                                std::shared_ptr<const std::vector<int>> propositions)
 {
-  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(++expandedPairsCount_);
+  expandedPairsCount_++;
+  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(expandedPairsCount_);
   next_pair->automaton_state      = state;
   next_pair->graph_state          = std::shared_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
   next_pair->atomic_propositions  = std::move(propositions);
@@ -346,8 +345,8 @@ void LivenessChecker::backtrack()
 
 void LivenessChecker::run()
 {
-  XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
-  MC_automaton_load(_sg_mc_property_file);
+  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();
@@ -383,26 +382,28 @@ void LivenessChecker::run()
     }
 
     std::shared_ptr<VisitedPair> reached_pair;
-    if (current_pair->automaton_state->type == 1 && not current_pair->exploration_started &&
-        (reached_pair = this->insertAcceptancePair(current_pair.get())) == nullptr) {
-      this->showAcceptanceCycle(current_pair->depth);
-      throw simgrid::mc::LivenessError();
+    if (current_pair->automaton_state->type == 1 && not current_pair->exploration_started) {
+      reached_pair = this->insertAcceptancePair(current_pair.get());
+      if (reached_pair == nullptr) {
+        this->showAcceptanceCycle(current_pair->depth);
+        throw simgrid::mc::LivenessError();
+      }
     }
 
     /* Pair already visited ? stop the exploration on the current path */
-    int visited_num = -1;
-    if ((not current_pair->exploration_started) &&
-        (visited_num = this->insertVisitedPair(reached_pair, current_pair.get())) != -1) {
-      if (dot_output != nullptr){
-        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-          this->previousPair_, visited_num,
-          this->previousRequest_.c_str());
-        fflush(dot_output);
+    if (not current_pair->exploration_started) {
+      int visited_num = this->insertVisitedPair(reached_pair, current_pair.get());
+      if (visited_num != -1) {
+        if (dot_output != nullptr) {
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previousPair_, visited_num,
+                  this->previousRequest_.c_str());
+          fflush(dot_output);
+        }
+        XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
+        current_pair->requests = 0;
+        this->backtrack();
+        continue;
       }
-      XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
-      current_pair->requests = 0;
-      this->backtrack();
-      continue;
     }
 
     smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
@@ -445,8 +446,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));
@@ -458,9 +460,9 @@ void LivenessChecker::run()
   simgrid::mc::session->logState();
 }
 
-Checker* createLivenessChecker(Session& session)
+Checker* createLivenessChecker(Session& s)
 {
-  return new LivenessChecker(session);
+  return new LivenessChecker(s);
 }
 
 }