diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index 8ebb761f7..a5288ac3c 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014-2019, 2021, 2022 Laboratoire de Recherche et +// Copyright (C) 2011, 2014-2019, 2021, 2022, 2023 Laboratoire de Recherche et // Developpement de l'EPITA (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -229,12 +229,6 @@ namespace spot return b->intersecting_run(complement(ensure_graph(a))); } - static bool - is_buchi_automata(const_twa_graph_ptr const& aut) - { - return spot::acc_cond::acc_code::buchi() == aut->get_acceptance(); - } - twa_word_ptr twa::exclusive_word(const_twa_ptr other) const { @@ -256,19 +250,18 @@ namespace spot }(); // We have to find a word in A\B or in B\A. When possible, let's - // make sure the first automaton we complement is deterministic. + // make sure the first automaton we complement, i.e., b, is deterministic. auto a_twa_as_graph = std::dynamic_pointer_cast(a); - auto b_twa_as_graph = std::dynamic_pointer_cast(a); + auto b_twa_as_graph = std::dynamic_pointer_cast(b); if (a_twa_as_graph) if (is_deterministic(a_twa_as_graph)) std::swap(a, b); - bool uses_buchi = is_buchi_automata(a_twa_as_graph) - && is_buchi_automata(b_twa_as_graph); if (containment == containment_type::FORQ - && uses_buchi - && a_twa_as_graph - && b_twa_as_graph) + && a_twa_as_graph + && b_twa_as_graph + && a_twa_as_graph->acc().is_buchi() + && b_twa_as_graph->acc().is_buchi()) { if (auto word = difference_word_forq(a_twa_as_graph, b_twa_as_graph)) return word; diff --git a/spot/twaalgos/forq_contains.cc b/spot/twaalgos/forq_contains.cc index a396784d6..adf7c597a 100644 --- a/spot/twaalgos/forq_contains.cc +++ b/spot/twaalgos/forq_contains.cc @@ -19,25 +19,19 @@ #include "config.h" #include -#include "forq_contains.hh" +#include -#include #include -#include -#include #include #include -#include #include #include -#include #include #include #include #include #include #include -#include #include #include #include @@ -522,96 +516,6 @@ namespace spot::forq }; } - enum class forq_status - { - FORQ_OKAY, // The forq works as expected - FORQ_INVALID_AC_COND, // The automata passed do not - // use buchi acceptance conditions - FORQ_INCOMPATIBLE_DICTS, // The two automata are using - // different bdd_dict objects - FORQ_INCOMPATIBLE_AP, // The two automata are using - // different atomic propositions - FORQ_INVALID_INPUT_BA, // The two automata passed are - // nullptrs and are invalid - FORQ_INVALID_RESULT_PTR // The pointer forq_result, that - // was passed into function - // contains_forq, cannot be nullptr - }; - - struct forq_result - { - // Whether language of graph A is included in B - bool included; - // If the language of graph A is not included in B, - // a counter example is provided - spot::twa_word_ptr counter_example; - }; - - // Returns a human-readable string given a forq_status, - // which can be aquired through a call to contains_forq - static const char* forq_status_message(forq_status status) - { - switch (status) - { - case forq_status::FORQ_OKAY: - return "Forq was able to properly run on the two buchi automata."; - case forq_status::FORQ_INVALID_AC_COND: - return "Forq only operates on automata with buchi " - "acceptance conditions."; - case forq_status::FORQ_INCOMPATIBLE_DICTS: - return "The two input graphs must utilize the same twa_dict."; - case forq_status::FORQ_INCOMPATIBLE_AP: - return "The two input graphs must utilize the same set of atomic" - "propositions defined in their shared twa_dict."; - case forq_status::FORQ_INVALID_INPUT_BA: - return "One of the two buchi automata passed in was a nullptr."; - case forq_status::FORQ_INVALID_RESULT_PTR: - return "The result pointer passed in was a nullptr."; - default: - return "Unknown Forq Status Code."; - } - } - - static forq_status valid_automata(const_graph const& A, - const_graph const& B, - forq_result* result) - { - if (!result) - { - return forq_status::FORQ_INVALID_RESULT_PTR; - } - if (!A || !B) - { - return forq_status::FORQ_INVALID_INPUT_BA; - } - - const auto buchi_acceptance = spot::acc_cond::acc_code::buchi(); - auto accept_A = A->get_acceptance(); - auto accept_B = B->get_acceptance(); - - if (accept_A != buchi_acceptance || accept_B != buchi_acceptance) - { - return forq_status::FORQ_INVALID_AC_COND; - } - if (A->get_dict() != B->get_dict()) - { - return forq_status::FORQ_INCOMPATIBLE_DICTS; - } - if (A->ap() != B->ap()) - { - return forq_status::FORQ_INCOMPATIBLE_AP; - } - return forq_status::FORQ_OKAY; - } - - static forq_status create_result(forq_result* result, - spot::twa_word_ptr counter_example = nullptr) - { - result->included = static_cast(counter_example); - result->counter_example = std::move(counter_example); - return forq_status::FORQ_OKAY; - } - struct forq_setup { forq::forq_context context; @@ -707,32 +611,11 @@ namespace spot::forq word_of_v, setup); if (counter_example) - { - return final_state_result::failure(std::move(counter_example)); - } + return final_state_result::failure(std::move(counter_example)); } } return final_state_result::success(); } - - static forq_status forq_impl(const_graph const& A, - const_graph const& B, forq_result* result) - { - if (auto rc = valid_automata(A, B, result); rc != forq_status::FORQ_OKAY) - { - return rc; - } - forq_setup setup = create_forq_setup(A, B); - - for (auto src : util::get_final_states(A)) - { - auto final_state_result = run_from_final_state(src, setup); - if (!final_state_result.should_continue()){ - return create_result(result, final_state_result.get_counter_example()); - } - } - return create_result(result); - } } namespace spot @@ -740,13 +623,27 @@ namespace spot twa_word_ptr difference_word_forq(forq::const_graph lhs, forq::const_graph rhs) { - forq::forq_result result; - auto rc = forq::forq_impl(lhs, rhs, &result); - if (rc != forq::forq_status::FORQ_OKAY) + if (!lhs || !rhs) + throw std::runtime_error("One of the two automata passed was a nullptr."); + if (!lhs->acc().is_buchi() || !rhs->acc().is_buchi()) + throw std::runtime_error("Forq only operates on automata with Büchi " + "acceptance conditions."); + if (lhs->get_dict() != rhs->get_dict()) + throw std::runtime_error + ("The two input graphs must utilize the same twa_dict."); + if (lhs->ap() != rhs->ap()) + throw std::runtime_error("The two input graphs must use the same set " + "of APs"); + + forq::forq_setup setup = forq::create_forq_setup(lhs, rhs); + + for (auto src: forq::util::get_final_states(lhs)) { - throw std::runtime_error(forq::forq_status_message(rc)); + auto final_state_result = forq::run_from_final_state(src, setup); + if (!final_state_result.should_continue()) + return final_state_result.get_counter_example(); } - return result.counter_example; + return nullptr; } bool contains_forq(forq::const_graph lhs, forq::const_graph rhs)