Update copyright lines.

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

diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp
index 1953d6d..bcb4f66 100644 (file)
--- a/src/mc/mc_api.cpp
+++ b/src/mc/mc_api.cpp
@@ -5,13 +5,13 @@
 #include "src/mc/Session.hpp"
 #include "src/mc/mc_comm_pattern.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/mc_record.hpp"
 #include "src/mc/mc_smx.hpp"
 #include "src/mc/remote/RemoteSimulation.hpp"
 #include "src/mc/mc_pattern.hpp"
 #include "src/mc/checker/SimcallInspector.hpp"
 #include <xbt/asserts.h>
 #include <xbt/log.h>
+// #include <xbt/dynar.h>
 
 #if HAVE_SMPI
 #include "src/smpi/include/smpi_request.hpp"
@@ -202,7 +202,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta
   return req;
 }
 
-void mc_api::initialize(char** argv)
+void mc_api::initialize(char** argv) const
 {
   simgrid::mc::session = new simgrid::mc::Session([argv] {
     int i = 1;
@@ -416,6 +416,13 @@ Checker* mc_api::mc_get_checker() const
   return mc_model_checker->getChecker();
 }
 
+void mc_api::set_checker(Checker* const checker) const
+{
+  xbt_assert(mc_model_checker);
+  xbt_assert(mc_model_checker->getChecker() == nullptr);
+  mc_model_checker->setChecker(checker);
+}
+
 RemoteSimulation& mc_api::mc_get_remote_simulation() const
 {
   return mc_model_checker->get_remote_simulation();
@@ -862,7 +869,7 @@ std::vector<xbt_automaton_state_t> mc_api::get_automaton_state() const
   return automaton_stack;
 }
 
-int mc_api::compare_automaton_exp_lable(const xbt_automaton_exp_label* l, std::vector<int> const& values) const
+int mc_api::compare_automaton_exp_label(const xbt_automaton_exp_label* l) const
 {
   unsigned int cursor = 0;
   xbt_automaton_propositional_symbol_t p = nullptr;
@@ -878,5 +885,19 @@ 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;
+}
+
+xbt_automaton_state_t mc_api::get_automaton_transition_dst(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->dst;
+}
+
 } // namespace mc
 } // namespace simgrid