From b672b4e2edc2767dcf5f610ffed3cbf26750f960 Mon Sep 17 00:00:00 2001 From: koniksedy Date: Tue, 20 Feb 2024 13:17:25 +0100 Subject: [PATCH] default level set to 1; levels size synchronized with delta --- include/mata/nft/nft.hh | 14 ++++++++------ src/nft/builder.cc | 4 ++++ src/nft/inclusion.cc | 13 ------------- src/nft/nft.cc | 14 +++++++++++++- tests/nft/nft.cc | 4 ++-- 5 files changed, 27 insertions(+), 22 deletions(-) diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index e3f6eb9c9..eec4ccfe7 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -51,7 +51,7 @@ struct Nft : public mata::nfa::Nfa { public: /// @brief For state q, levels[q] gives the state a level. std::vector levels{}; - Level levels_cnt = 0; + Level levels_cnt = 1; /// Key value store for additional attributes for the NFT. Keys are attribute names as strings and the value types /// are up to the user. /// For example, we can set up attributes such as "state_dict" for state dictionary attribute mapping states to their @@ -62,22 +62,24 @@ public: public: explicit Nft(Delta delta = {}, utils::SparseSet initial_states = {}, - utils::SparseSet final_states = {}, std::vector levels = {}, const Level levels_cnt = 0, + utils::SparseSet final_states = {}, std::vector levels = {}, const Level levels_cnt = 1, Alphabet* alphabet = nullptr) - : mata::nfa::Nfa(std::move(delta), std::move(initial_states), std::move(final_states), alphabet), levels(levels), levels_cnt(levels_cnt) {} + : mata::nfa::Nfa(std::move(delta), std::move(initial_states), std::move(final_states), alphabet), + levels(levels.size() ? std::move(levels) : std::vector(delta.num_of_states(), 0)), levels_cnt(levels_cnt) {} /** * @brief Construct a new explicit NFT with num_of_states states and optionally set initial and final states. * * @param[in] num_of_states Number of states for which to preallocate Delta. */ explicit Nft(const unsigned long num_of_states, StateSet initial_states = {}, - StateSet final_states = {}, std::vector levels = {}, const Level levels_cnt = 0, Alphabet* + StateSet final_states = {}, std::vector levels = {}, const Level levels_cnt = 1, Alphabet* alphabet = nullptr) - : mata::nfa::Nfa(num_of_states, std::move(initial_states), std::move(final_states), alphabet), levels(levels), levels_cnt(levels_cnt) {} + : mata::nfa::Nfa(num_of_states, std::move(initial_states), std::move(final_states), alphabet), + levels(levels.size() ? std::move(levels) : std::vector(num_of_states, 0)), levels_cnt(levels_cnt) {} explicit Nft(const mata::nfa::Nfa& other) : mata::nfa::Nfa(other.delta, other.initial, other.final, other.alphabet), - levels(std::vector()), levels_cnt(0) {} + levels(std::vector(other.delta.num_of_states(), 0)), levels_cnt(1) {} /** * @brief Construct a new explicit NFT from other NFT. diff --git a/src/nft/builder.cc b/src/nft/builder.cc index aebaf392f..2d799f9f5 100644 --- a/src/nft/builder.cc +++ b/src/nft/builder.cc @@ -340,5 +340,9 @@ Nft builder::create_from_nfa(const mata::nfa::Nfa& nfa, Level level_cnt, const s std::ranges::for_each(nfa.initial, [&](const State nfa_state){ nft.initial.insert(state_mapping[nfa_state]); }); nft.final.reserve(nfa.final.size()); std::ranges::for_each(nfa.final, [&](const State nfa_state){ nft.final.insert(state_mapping[nfa_state]); }); + + // TODO(nft): HACK. Levels do not work if the size of delta differs from the size of the vector level. + nft.levels.resize(nft.delta.num_of_states()); + return nft; } diff --git a/src/nft/inclusion.cc b/src/nft/inclusion.cc index ec9844e14..8d7867469 100644 --- a/src/nft/inclusion.cc +++ b/src/nft/inclusion.cc @@ -37,7 +37,6 @@ bool mata::nft::algorithms::is_included_antichains( Run* cex) { // {{{ if (smaller.levels_cnt != bigger.levels_cnt) { return false; } - if (smaller.levels_cnt == 0) { return nfa::algorithms::is_included_antichains(smaller, bigger, alphabet, cex); } OrdVector symbols; if (alphabet == nullptr) { @@ -58,17 +57,6 @@ bool mata::nft::algorithms::is_included_antichains( namespace { using AlgoType = decltype(algorithms::is_included_naive)*; - bool compute_equivalence(const Nft &lhs, const Nft &rhs, const mata::Alphabet *const alphabet, const AlgoType &algo) { - //alphabet should not be needed as input parameter - if (algo(lhs, rhs, alphabet, nullptr)) { - if (algo(rhs, lhs, alphabet, nullptr)) { - return true; - } - } - - return false; - } - AlgoType set_algorithm(const std::string &function_name, const ParameterMap ¶ms) { if (!haskey(params, "algorithm")) { throw std::runtime_error(function_name + @@ -106,7 +94,6 @@ bool mata::nft::is_included( bool mata::nft::are_equivalent(const Nft& lhs, const Nft& rhs, const Alphabet *alphabet, const ParameterMap& params) { if (lhs.levels_cnt != rhs.levels_cnt) { return false; } - if (lhs.levels_cnt == 0) { return nfa::are_equivalent(lhs, rhs, alphabet, params); } OrdVector symbols; if (alphabet == nullptr) { diff --git a/src/nft/nft.cc b/src/nft/nft.cc index fb8b112a0..2a0e4977f 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -240,6 +240,13 @@ void Nft::make_one_level_aut(const utils::OrdVector &dcare_replacements) Nft Nft::get_one_level_aut(const utils::OrdVector &dcare_replacements) const { Nft result{ *this }; + + // TODO(nft): Create a class for LEVELS with overloaded getter and setter. + // HACK. Works only for automata without levels. + if (result.levels.size() != result.num_of_states()) { + return result; + } + result.make_one_level_aut(dcare_replacements); return result; } @@ -263,7 +270,12 @@ State Nft::add_state() { } State Nft::add_state(State state) { - levels.push_back(0); + const size_t levels_size = levels.size(); + if (state >= levels_size) { + levels.resize(state + 1); + const size_t begin_idx = (levels_size == 0) ? 0 : levels_size - 1; + std::fill(levels.begin() + static_cast(begin_idx), levels.end(), 0); + } return mata::nfa::Nfa::add_state(state); } diff --git a/tests/nft/nft.cc b/tests/nft/nft.cc index f2d395437..0c3ddc8a4 100644 --- a/tests/nft/nft.cc +++ b/tests/nft/nft.cc @@ -3008,7 +3008,7 @@ TEST_CASE("mata::nft::Nft::get_one_level_aut") { REPLACE_DONT_CARE(delta, inter, trg);\ SECTION("level_cnt == 1") { - Nft aut(5, {0}, {3, 4}, {0, 0, 0, 0, 0}, 1); + Nft aut(5, {0}, {3, 4}); aut.delta.add(0, 0, 1); aut.delta.add(0, 1, 2); aut.delta.add(1, 0, 1); @@ -3020,7 +3020,7 @@ TEST_CASE("mata::nft::Nft::get_one_level_aut") { aut.delta.add(4, 1, 2); aut.delta.add(4, DONT_CARE, 4); - Nft expected(5, {0}, {3, 4}, {0, 0, 0, 0, 0}, 1); + Nft expected(5, {0}, {3, 4}); expected.delta.add(0, 0, 1); expected.delta.add(0, 1, 2); expected.delta.add(1, 0, 1);