+LivenessChecker::LivenessChecker(const std::vector<char*>& args) : Exploration(args) {}
+LivenessChecker::~LivenessChecker()
+{
+ if (property_automaton_ != nullptr)
+ xbt_automaton_free(property_automaton_);
+}
+
+xbt_automaton_t LivenessChecker::property_automaton_ = nullptr;
+
+void LivenessChecker::automaton_load(const char* file)
+{
+ if (property_automaton_ == nullptr)
+ property_automaton_ = xbt_automaton_new();
+
+ xbt_automaton_load(property_automaton_, file);
+}
+
+std::vector<int> LivenessChecker::automaton_propositional_symbol_evaluate() const
+{
+ unsigned int cursor = 0;
+ std::vector<int> values;
+ xbt_automaton_propositional_symbol_t ps = nullptr;
+ xbt_dynar_foreach (property_automaton_->propositional_symbols, cursor, ps)
+ values.push_back(xbt_automaton_propositional_symbol_evaluate(ps));
+ return values;
+}
+
+std::vector<xbt_automaton_state_t> LivenessChecker::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 (property_automaton_->states, cursor, automaton_state)
+ if (automaton_state->type == -1)
+ automaton_stack.push_back(automaton_state);
+ return automaton_stack;
+}
+
+int LivenessChecker::compare_automaton_exp_label(const xbt_automaton_exp_label* l) const
+{
+ unsigned int cursor = 0;
+ xbt_automaton_propositional_symbol_t p = nullptr;
+ xbt_dynar_foreach (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 LivenessChecker::set_property_automaton(xbt_automaton_state_t const& automaton_state) const
+{
+ property_automaton_->current_state = automaton_state;
+}
+
+xbt_automaton_exp_label_t LivenessChecker::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 LivenessChecker::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;
+}
+void LivenessChecker::automaton_register_symbol(RemoteProcess& remote_process, const char* name, RemotePtr<int> address)
+{
+ if (property_automaton_ == nullptr)
+ property_automaton_ = xbt_automaton_new();
+
+ xbt::add_proposition(property_automaton_, name,
+ [&remote_process, address]() { return remote_process.read(address); });
+}