mc_api::set_property_automaton(), it is called in run()

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

diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp
index f83804824f1a1dace6b010472387ba725e54ed23..42f2a6e063961331f18446866be8db044223e199 100644 (file)
--- a/src/mc/mc_api.cpp
+++ b/src/mc/mc_api.cpp
@@ -474,6 +474,11 @@ void mc_api::restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state)
   system_state->restore(&mc_model_checker->get_remote_simulation());
 }
 
+void mc_api::log_state() const
+{
+  session->log_state();
+}
+
 bool mc_api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const
 {
   return simgrid::mc::snapshot_equal(s1, s2);
@@ -517,9 +522,31 @@ std::vector<int> mc_api::automaton_propositional_symbol_evaluate() const
   return values;
 }
 
-void mc_api::log_state() const
+std::vector<xbt_automaton_state_t> mc_api::get_automaton_state() const
 {
-  session->log_state();
+  std::vector<xbt_automaton_state_t> automaton_stack;
+  unsigned int cursor = 0;
+  xbt_automaton_state_t automaton_state;
+  xbt_dynar_foreach (mc::property_automaton->states, cursor, automaton_state)
+    if (automaton_state->type == -1)
+      automaton_stack.push_back(automaton_state);
+  return automaton_stack;
+}
+
+int mc_api::compare_automaton_exp_lable(const xbt_automaton_exp_label* l, std::vector<int> const& values) const
+{
+  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 cursor;
+  }
+  return -1;
+}
+
+void mc_api::set_property_automaton(xbt_automaton_state_t const& automaton_state) const
+{
+  mc::property_automaton->current_state = automaton_state;
 }
 
 } // namespace mc