[mc] Remove useless comment

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

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 239bf3ca1e9293811719b2a4df9dbe036673bd04..a99d5e50ff4cfb4d57a936adee8c9fcae1b146c0 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -64,44 +64,31 @@ VisitedPair::~VisitedPair()
 {
 }
 
-static int MC_automaton_evaluate_label(
-  xbt_automaton_exp_label_t l,
-  std::vector<int> const& atomic_propositions_values)
+static bool evaluate_label(
+  xbt_automaton_exp_label_t l, std::vector<int> const& values)
 {
-
   switch (l->type) {
-  case xbt_automaton_exp_label::AUT_OR:{
-      int left_res = MC_automaton_evaluate_label(
-        l->u.or_and.left_exp, atomic_propositions_values);
-      int right_res = MC_automaton_evaluate_label(
-        l->u.or_and.right_exp, atomic_propositions_values);
-      return (left_res || right_res);
-    }
-  case xbt_automaton_exp_label::AUT_AND:{
-      int left_res = MC_automaton_evaluate_label(
-        l->u.or_and.left_exp, atomic_propositions_values);
-      int right_res = MC_automaton_evaluate_label(
-        l->u.or_and.right_exp, atomic_propositions_values);
-      return (left_res && right_res);
-    }
-  case xbt_automaton_exp_label::AUT_NOT:{
-      int res = MC_automaton_evaluate_label(
-        l->u.exp_not, atomic_propositions_values);
-      return (!res);
-    }
+  case xbt_automaton_exp_label::AUT_OR:
+    return evaluate_label(l->u.or_and.left_exp, values)
+      || evaluate_label(l->u.or_and.right_exp, values);
+  case xbt_automaton_exp_label::AUT_AND:
+    return evaluate_label(l->u.or_and.left_exp, values)
+      && evaluate_label(l->u.or_and.right_exp, values);
+  case xbt_automaton_exp_label::AUT_NOT:
+    return !evaluate_label(l->u.exp_not, values);
   case xbt_automaton_exp_label::AUT_PREDICAT:{
       unsigned int cursor = 0;
       xbt_automaton_propositional_symbol_t p = nullptr;
       xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
         if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
-          return atomic_propositions_values[cursor];
+          return values[cursor] != 0;
       }
-      return -1;
+      xbt_die("Missing predicate");
     }
   case xbt_automaton_exp_label::AUT_ONE:
-    return 2;
+    return true;
   default:
-    return -1;
+    xbt_die("Unexpected vaue for automaton");
   }
 }
 
@@ -300,22 +287,19 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair
   }
 
   visitedPairs_.insert(range.first, std::move(visited_pair));
+  this->purgeVisitedPairs();
+  return -1;
+}
 
-  if (visitedPairs_.size() > (std::size_t) _sg_mc_visited) {
-    int min2 = mc_stats->expanded_pairs;
-
-    std::list<std::shared_ptr<VisitedPair>>::iterator index2;
-    for (auto i = visitedPairs_.begin(); i != visitedPairs_.end(); ++i) {
-      if ((*i)->num < min2) {
-        index2 = i;
-        min2 = (*i)->num;
-      }
-    }
-
-    visitedPairs_.erase(index2);
+void LivenessChecker::purgeVisitedPairs()
+{
+  if (_sg_mc_visited != 0 && visitedPairs_.size() > (std::size_t) _sg_mc_visited) {
+    // Remove the oldest entry with a linear search:
+    visitedPairs_.erase(std::min_element(
+      visitedPairs_.begin(), visitedPairs_.end(),
+      [](std::shared_ptr<VisitedPair> const a, std::shared_ptr<VisitedPair> const& b) {
+        return a->num < b->num; } ));
   }
-
-  return -1;
 }
 
 LivenessChecker::LivenessChecker(Session& session) : Checker(session)
@@ -335,8 +319,6 @@ RecordTrace LivenessChecker::getRecordTrace() // override
     if (req && req->call != SIMCALL_NONE) {
       smx_process_t issuer = MC_smx_simcall_get_issuer(req);
       const int pid = issuer->pid;
-
-      // Serialization the (pid, value) pair:
       res.push_back(RecordTraceElement(pid, value));
     }
   }
@@ -456,8 +438,7 @@ int LivenessChecker::main(void)
          int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
          while (cursor >= 0) {
            xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
-           int res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
-           if (res == 1 || res == 2) { /* 1 = True transition (always enabled), 2 = enabled transition according to atomic prop values */
+           if (evaluate_label(transition_succ->label, prop_values)) {
               std::shared_ptr<Pair> next_pair = std::make_shared<Pair>();
               next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
               next_pair->automaton_state = transition_succ->dst;