mc_api::get_automaton_transition_label() defined and called in run()

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index a1009eb..e9a2fe2 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -406,9 +406,10 @@ void LivenessChecker::run()
     for (int i = mcapi::get().get_dynar_length(current_pair->automaton_state->out) - 1; i >= 0; i--) {
       const xbt_automaton_transition* transition_succ =
           xbt_dynar_get_as(current_pair->automaton_state->out, i, xbt_automaton_transition_t);
-      if (evaluate_label(transition_succ->label, *prop_values))
+      auto transition_succ_label = mcapi::get().get_automaton_transition_label(current_pair->automaton_state->out, i);
+      if (evaluate_label(transition_succ_label, *prop_values))
         exploration_stack_.push_back(this->create_pair(current_pair.get(), transition_succ->dst, prop_values));
-     }
+    }
   }
 
   XBT_INFO("No property violation found.");

diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp
index 4446b42..f62534c 100644 (file)
--- a/src/mc/mc_api.cpp
+++ b/src/mc/mc_api.cpp
@@ -879,5 +879,12 @@ void mc_api::set_property_automaton(xbt_automaton_state_t const& automaton_state
   mc::property_automaton->current_state = automaton_state;
 }
 
+xbt_automaton_exp_label_t mc_api::get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const
+{
+  const xbt_automaton_transition* transition =
+      xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
+  return transition->label;
+}
+
 } // namespace mc
 } // namespace simgrid

diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp
index 705dd60..5bf4e2a 100644 (file)
--- a/src/mc/mc_api.hpp
+++ b/src/mc/mc_api.hpp
@@ -129,6 +129,8 @@ public:
   inline int automaton_state_compare(const_xbt_automaton_state_t const& s1, const_xbt_automaton_state_t const& s2) const {
     return xbt_automaton_state_compare(s1, s2);
   }
+  xbt_automaton_exp_label_t get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const;
+
   // DYNAR APIs
   inline unsigned long get_dynar_length(const_xbt_dynar_t const& dynar) const {
     return xbt_dynar_length(dynar);