// For each initial state of the property automaton, push a
// (application_state, automaton_state) pair to the exploration stack:
- unsigned int cursor = 0;
- xbt_automaton_state_t automaton_state;
- xbt_dynar_foreach (mc::property_automaton->states, cursor, automaton_state)
+ auto automaton_stack = mcapi::get().get_automaton_state();
+ std::for_each(automaton_stack.begin(), automaton_stack.end(), [&](xbt_automaton_state_t const& automaton_state) {
if (automaton_state->type == -1)
exploration_stack_.push_back(this->create_pair(nullptr, automaton_state, propos));
+ });
/* Actually run the double DFS search for counter-examples */
while (not exploration_stack_.empty()) {
return values;
}
+std::vector<xbt_automaton_state_t> mc_api::get_automaton_state() const
+{
+ 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;
+}
+
} // namespace mc
} // namespace simgrid
#include "src/mc/mc_forward.hpp"
#include "src/mc/mc_request.hpp"
#include "src/mc/mc_state.hpp"
+#include "xbt/automaton.hpp"
#include "xbt/base.h"
namespace simgrid {
void automaton_load(const char *file) const;
#endif
std::vector<int> automaton_propositional_symbol_evaluate() const;
+ std::vector<xbt_automaton_state_t> get_automaton_state() const;
};
} // namespace mc