From ec691feeffd9ce18d50fa1f4fea48498db86d989 Mon Sep 17 00:00:00 2001 From: tmokenc Date: Wed, 8 Apr 2026 15:08:26 +0200 Subject: [PATCH 1/5] feat: support for alphabet per tape/level This is a very naive implementation, not sure if it is actually correct or I missed something. (cherry picked from commit 705db38a415c5ccee4113744a1a222764f9d64f2) --- include/mata/nft/nft.hh | 122 +++++++++++++++++++++++++++++++++++++--- src/nft/nft.cc | 5 +- src/nft/operations.cc | 8 +-- 3 files changed, 123 insertions(+), 12 deletions(-) diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index b5d2cfaf9..5992ff499 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -126,6 +126,16 @@ public: */ Levels levels{}; + /** + * @brief Optional per-level alphabets. + * + * When empty, the NFT falls back to the shared @ref alphabet inherited from @ref nfa::Nfa. + * When non-empty, the vector is indexed by NFT level. If all entries are the same pointer, + * the inherited shared @ref alphabet is kept in sync with that pointer; otherwise it is set + * to @c nullptr because no single shared alphabet describes the whole NFT. + */ + std::vector level_alphabets{}; + /// 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 @@ -135,12 +145,45 @@ public: // dictionary in the attributes. public: + static std::vector repeated_level_alphabets(const size_t num_of_levels, Alphabet* alphabet) { + return std::vector(num_of_levels, alphabet); + } + + static Alphabet* shared_alphabet_or_null(const std::vector& level_alphabets) { + if (level_alphabets.empty()) { + return nullptr; + } + + const Alphabet* first = level_alphabets.front(); + for (const Alphabet* alphabet : level_alphabets) { + if (alphabet != first) { + return nullptr; + } + } + + return const_cast(first); + } + explicit Nft( Delta delta = {}, utils::SparseSet initial_states = {}, utils::SparseSet final_states = {}, Levels levels = {}, Alphabet* alphabet = nullptr) : Nfa{ std::move(delta), std::move(initial_states), std::move(final_states), alphabet }, - levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states(), DEFAULT_LEVEL } : std::move(levels) } {} + levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states(), DEFAULT_LEVEL } : std::move(levels) }, + level_alphabets{ repeated_level_alphabets(this->levels.num_of_levels, alphabet) } {} + + explicit Nft( + Delta delta, utils::SparseSet initial_states, utils::SparseSet final_states, Levels levels, + std::vector level_alphabets) + : Nfa{ + std::move(delta), std::move(initial_states), std::move(final_states), + shared_alphabet_or_null(level_alphabets) }, + levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states(), DEFAULT_LEVEL } : std::move(levels) }, + level_alphabets{ std::move(level_alphabets) } { + if (!this->level_alphabets.empty()) { + assert(this->level_alphabets.size() == this->levels.num_of_levels); + } + } /** * @brief Construct a new explicit NFT with num_of_states states and optionally set initial and final states. @@ -155,7 +198,19 @@ public: utils::SparseSet final_states = {}, Levels levels = {}, Alphabet* alphabet = nullptr) : Nfa{ num_of_states, std::move(initial_states), std::move(final_states), alphabet }, - levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states, DEFAULT_LEVEL } : std::move(levels) } {} + levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states, DEFAULT_LEVEL } : std::move(levels) }, + level_alphabets{ repeated_level_alphabets(this->levels.num_of_levels, alphabet) } {} + + explicit Nft( + const size_t num_of_states, utils::SparseSet initial_states, utils::SparseSet final_states, + Levels levels, std::vector level_alphabets) + : Nfa{ num_of_states, std::move(initial_states), std::move(final_states), shared_alphabet_or_null(level_alphabets) }, + levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states, DEFAULT_LEVEL } : std::move(levels) }, + level_alphabets{ std::move(level_alphabets) } { + if (!this->level_alphabets.empty()) { + assert(this->level_alphabets.size() == this->levels.num_of_levels); + } + } static Nft with_levels( Levels levels, const size_t num_of_states = 0, utils::SparseSet initial_states = {}, @@ -163,31 +218,63 @@ public: return Nft{ num_of_states, std::move(initial_states), std::move(final_states), std::move(levels), alphabet }; } + static Nft with_levels( + Levels levels, const size_t num_of_states, utils::SparseSet initial_states, + utils::SparseSet final_states, std::vector level_alphabets) { + return Nft{ + num_of_states, std::move(initial_states), std::move(final_states), std::move(levels), + std::move(level_alphabets) }; + } + static Nft with_levels( Levels levels, Delta delta, utils::SparseSet initial_states = {}, utils::SparseSet final_states = {}, Alphabet* alphabet = nullptr) { return Nft{ std::move(delta), std::move(initial_states), std::move(final_states), std::move(levels), alphabet }; } + static Nft with_levels( + Levels levels, Delta delta, utils::SparseSet initial_states, + utils::SparseSet final_states, std::vector level_alphabets) { + return Nft{ + std::move(delta), std::move(initial_states), std::move(final_states), std::move(levels), + std::move(level_alphabets) }; + } + static Nft with_levels( const size_t num_of_levels, const size_t num_of_states = 0, utils::SparseSet initial_states = {}, utils::SparseSet final_states = {}, Alphabet* alphabet = nullptr) { return Nft{ num_of_states, std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, alphabet }; } + static Nft with_levels( + const size_t num_of_levels, const size_t num_of_states, utils::SparseSet initial_states, + utils::SparseSet final_states, std::vector level_alphabets) { + return Nft{ + num_of_states, std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, + std::move(level_alphabets) }; + } + static Nft with_levels( const size_t num_of_levels, Delta delta, utils::SparseSet initial_states = {}, utils::SparseSet final_states = {}, Alphabet* alphabet = nullptr) { return Nft{ std::move(delta), std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, alphabet }; } + static Nft with_levels( + const size_t num_of_levels, Delta delta, utils::SparseSet initial_states, + utils::SparseSet final_states, std::vector level_alphabets) { + return Nft{ + std::move(delta), std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, + std::move(level_alphabets) }; + } + /** * @brief Construct a new explicit NFT from other NFT. */ Nft(const Nft& other) = default; Nft(Nft&& other) noexcept - : levels{ std::move(other.levels) } { + : levels{ std::move(other.levels) }, level_alphabets{ std::move(other.level_alphabets) } { delta = std::move(other.delta); initial = std::move(other.initial); final = std::move(other.final); @@ -211,7 +298,8 @@ public: * @param default_level Default level for the states. (default: 0) */ explicit Nft(const mata::nfa::Nfa& other, const size_t num_of_levels = 1, const Level default_level = DEFAULT_LEVEL) - : mata::nfa::Nfa(other), levels{ num_of_levels, num_of_states(), default_level } {} + : mata::nfa::Nfa(other), levels{ num_of_levels, num_of_states(), default_level }, + level_alphabets{ repeated_level_alphabets(num_of_levels, alphabet) } {} /** * @brief Construct a new NFT with @p num_of_levels levels from NFA. @@ -225,7 +313,8 @@ public: * @param default_level Default level for the states. (default: 0) */ explicit Nft(Nfa&& other, const size_t num_of_levels = 1, const Level default_level = DEFAULT_LEVEL) - : Nfa(std::move(other)), levels{ num_of_levels, num_of_states(), default_level } {} + : Nfa(std::move(other)), levels{ num_of_levels, num_of_states(), default_level }, + level_alphabets{ repeated_level_alphabets(num_of_levels, alphabet) } {} /** * @brief Construct a new NFT with @p num_of_levels levels from NFA. @@ -237,7 +326,9 @@ public: * @param other NFA to be converted to NFT. * @param levels Levels for the states of the NFA @c other. */ - explicit Nft(const Nfa& other, Levels levels): Nfa(other), levels{ std::move(levels) } {} + explicit Nft(const Nfa& other, Levels levels) + : Nfa(other), levels{ std::move(levels) }, + level_alphabets{ repeated_level_alphabets(this->levels.num_of_levels, alphabet) } {} /** * @brief Construct a new NFT with @p num_of_levels levels from NFA. @@ -249,7 +340,24 @@ public: * @param other NFA to be converted to NFT. * @param levels Levels for the states of the NFA @c other. */ - explicit Nft(Nfa&& other, Levels levels): Nfa{ std::move(other) }, levels{ std::move(levels) } {} + explicit Nft(Nfa&& other, Levels levels) + : Nfa{ std::move(other) }, levels{ std::move(levels) }, + level_alphabets{ repeated_level_alphabets(this->levels.num_of_levels, alphabet) } {} + + const Alphabet* alphabet_of_level(const size_t level) const { + if (!level_alphabets.empty() && level < level_alphabets.size() && level_alphabets[level] != nullptr) { + return level_alphabets[level]; + } + return alphabet; + } + + void set_level_alphabets(std::vector new_level_alphabets) { + if (!new_level_alphabets.empty()) { + assert(new_level_alphabets.size() == levels.num_of_levels); + } + alphabet = shared_alphabet_or_null(new_level_alphabets); + level_alphabets = std::move(new_level_alphabets); + } Nft& operator=(const Nfa& other) noexcept; Nft& operator=(Nfa&& other) noexcept; diff --git a/src/nft/nft.cc b/src/nft/nft.cc index c43dfc7cb..23bb9fad7 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -528,9 +528,10 @@ void Nft::unwind_jumps( Nft& Nft::operator=(Nft&& other) noexcept { if (this != &other) { - Nfa::operator=(other); + Nfa::operator=(std::move(other)); levels = std::move(other.levels); levels.num_of_levels = other.levels.num_of_levels; + level_alphabets = std::move(other.level_alphabets); } return *this; } @@ -541,6 +542,7 @@ Nft& Nft::operator=(const Nfa& other) noexcept { Nfa::operator=(other); levels = Levels(num_of_states(), DEFAULT_LEVEL); levels.num_of_levels = 1; + level_alphabets = Nft::repeated_level_alphabets(levels.num_of_levels, alphabet); } return *this; } @@ -550,6 +552,7 @@ Nft& Nft::operator=(Nfa&& other) noexcept { Nfa::operator=(std::move(other)); levels = Levels(num_of_states(), DEFAULT_LEVEL); levels.num_of_levels = 1; + level_alphabets = Nft::repeated_level_alphabets(levels.num_of_levels, alphabet); } return *this; } diff --git a/src/nft/operations.cc b/src/nft/operations.cc index 686d2e88f..1a897b7ed 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -338,7 +338,7 @@ Nft mata::nft::project_out(const Nft& nft, const utils::OrdVector& levels } // Construct the automaton with projected levels. - Nft result{ Nft::with_levels(nft.levels, Delta{}, nft.initial, nft.final, nft.alphabet) }; + Nft result{ Nft::with_levels(nft.levels, Delta{}, nft.initial, nft.final, nft.level_alphabets) }; for (State src_state{ 0 }; src_state < num_of_states_in_delta; src_state++) { // For every state. for (const State cls_state : closure[src_state]) { // For every state in its epsilon closure. if (nft.final[cls_state] && can_be_final(src_state)) result.final.insert(src_state); @@ -448,7 +448,7 @@ Nft mata::nft::insert_levels(const Nft& nft, const BoolVector& new_levels_mask, Nft result( Nft::with_levels( Levels{ new_levels_mask.size(), new_state_levels }, - nft.num_of_states(), nft.initial, nft.final, nft.alphabet + nft.num_of_states(), nft.initial, nft.final, nft.level_alphabets ) ); @@ -718,7 +718,7 @@ Nft nft::invert_levels(const Nft& aut, const JumpMode jump_mode) { // Create new automaton Nft aut_inv = Nft::with_levels( { aut.levels.num_of_levels, num_of_zero_states, DEFAULT_LEVEL }, - num_of_zero_states, std::move(new_initial), std::move(new_final), aut.alphabet + num_of_zero_states, std::move(new_initial), std::move(new_final), aut.level_alphabets ); // Creates new states with inverted levels for each inner state in the path. @@ -1032,7 +1032,7 @@ Nft mata::nft::reduce(const Nft& aut, StateRenaming* state_renaming, const Param Nft nft::determinize(const Nft& nft, std::unordered_map* subset_map) { Nft result{ Nft::with_levels(nft.levels.num_of_levels) }; - result.alphabet = nft.alphabet; + result.set_level_alphabets(nft.level_alphabets); if (nft.initial.empty()) { return result; } // Assuming all sets targets are non-empty. From 75f6351e75a1f705adf8102fd80a0d489f692675 Mon Sep 17 00:00:00 2001 From: tmokenc Date: Thu, 16 Apr 2026 01:39:09 +0200 Subject: [PATCH 2/5] refactors: move function bodies to .cc file --- include/mata/nft/nft.hh | 59 ++++++++++++++++++++--------------------- src/nft/nft.cc | 34 ++++++++++++++++++++++++ 2 files changed, 63 insertions(+), 30 deletions(-) diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index 5992ff499..5b643cbcc 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -145,24 +145,19 @@ public: // dictionary in the attributes. public: - static std::vector repeated_level_alphabets(const size_t num_of_levels, Alphabet* alphabet) { - return std::vector(num_of_levels, alphabet); - } - - static Alphabet* shared_alphabet_or_null(const std::vector& level_alphabets) { - if (level_alphabets.empty()) { - return nullptr; - } - - const Alphabet* first = level_alphabets.front(); - for (const Alphabet* alphabet : level_alphabets) { - if (alphabet != first) { - return nullptr; - } - } + /** + * Create a repeated vector of @p num_of_levels entries of the same @p alphabet pointer for the level alphabets. + * + * @param num_of_levels The number of levels for which to create the vector. + */ + static std::vector repeated_level_alphabets(const size_t num_of_levels, Alphabet* alphabet); - return const_cast(first); - } + /** + * Check if all entries in @p level_alphabets are the same pointer and return that pointer if so, or return nullptr + * + * @param level_alphabets The vector of level alphabets to check for being all the same pointer. + */ + static Alphabet* shared_alphabet_or_null(const std::vector& level_alphabets); explicit Nft( Delta delta = {}, utils::SparseSet initial_states = {}, @@ -344,20 +339,24 @@ public: : Nfa{ std::move(other) }, levels{ std::move(levels) }, level_alphabets{ repeated_level_alphabets(this->levels.num_of_levels, alphabet) } {} - const Alphabet* alphabet_of_level(const size_t level) const { - if (!level_alphabets.empty() && level < level_alphabets.size() && level_alphabets[level] != nullptr) { - return level_alphabets[level]; - } - return alphabet; - } + /** + * @brief Get the alphabet of the NFT for a given level. + * If the level has a specific alphabet in @c level_alphabets, return that alphabet; + * otherwise, return the shared @ref alphabet. + * + * @param level The level for which to get the alphabet. + */ + const Alphabet* alphabet_of_level(const size_t level) const; - void set_level_alphabets(std::vector new_level_alphabets) { - if (!new_level_alphabets.empty()) { - assert(new_level_alphabets.size() == levels.num_of_levels); - } - alphabet = shared_alphabet_or_null(new_level_alphabets); - level_alphabets = std::move(new_level_alphabets); - } + /** + * @brief Set the level alphabets for the NFT. + * + * When the vector of level alphabets is non-empty, it must have a size equal to the number of levels in the NFT. + * If the vector is empty, the NFT falls back to using the shared @ref alphabet for all levels. + * + * @param new_level_alphabets The new vector of level alphabets to set for the NFT. + */ + void set_level_alphabets(std::vector new_level_alphabets); Nft& operator=(const Nfa& other) noexcept; Nft& operator=(Nfa&& other) noexcept; diff --git a/src/nft/nft.cc b/src/nft/nft.cc index 23bb9fad7..2d01ed6d6 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -816,3 +816,37 @@ bool Nft::make_complete( return transition_added; } + +std::vector Nft::repeated_level_alphabets(const size_t num_of_levels, mata::Alphabet* alphabet) { + return std::vector(num_of_levels, alphabet); +} + +mata::Alphabet* Nft::shared_alphabet_or_null(const std::vector& level_alphabets) { + if (level_alphabets.empty()) { + return nullptr; + } + + const mata::Alphabet* first = level_alphabets.front(); + for (const mata::Alphabet* alphabet : level_alphabets) { + if (alphabet != first) { + return nullptr; + } + } + + return const_cast(first); +} + +const mata::Alphabet* Nft::alphabet_of_level(const size_t level) const { + if (!level_alphabets.empty() && level < level_alphabets.size() && level_alphabets[level] != nullptr) { + return level_alphabets[level]; + } + return alphabet; +} + +void Nft::set_level_alphabets(std::vector new_level_alphabets) { + if (!new_level_alphabets.empty()) { + assert(new_level_alphabets.size() == levels.num_of_levels); + } + alphabet = shared_alphabet_or_null(new_level_alphabets); + level_alphabets = std::move(new_level_alphabets); +} From 9e1d342f42340c4c8edd8dba8a58f34098d73a39 Mon Sep 17 00:00:00 2001 From: tmokenc Date: Fri, 17 Apr 2026 11:11:53 +0200 Subject: [PATCH 3/5] refactors: level-awar alphabet handling into LevelAlphabet instead of a field in Nft --- include/mata/alphabet.hh | 270 +++++++++++++++++++++++++++++++++++++-- include/mata/nft/nft.hh | 126 +----------------- src/alphabet.cc | 44 +++++++ src/nft/builder.cc | 4 +- src/nft/nft.cc | 69 +++------- src/nft/operations.cc | 11 +- tests/nft/nft.cc | 88 +++++++++++++ 7 files changed, 420 insertions(+), 192 deletions(-) diff --git a/include/mata/alphabet.hh b/include/mata/alphabet.hh index 22e81fd69..573fe19f2 100644 --- a/include/mata/alphabet.hh +++ b/include/mata/alphabet.hh @@ -7,6 +7,7 @@ #include #include #include +#include #include "utils/ord-vector.hh" #include "utils/utils.hh" @@ -22,9 +23,26 @@ using WordName = std::vector; */ class Alphabet { public: - /// translates a string into a symbol + /** + * @brief Translate a string into a symbol. + * + * @param[in] symb Symbol name to translate. + * @return Translated symbol value. + */ virtual Symbol translate_symb(const std::string &symb) = 0; + /** + * @brief Translate a string into a symbol on a specific level. + * + * @param[in] symb Symbol name to translate. + * @param[in] level Level on which the translation should happen. + * @return Translated symbol value. + */ + virtual Symbol translate_symb(const std::string &symb, size_t level) { + (void)level; + return translate_symb(symb); + } + /** * Translate sequence of symbol names to sequence of their respective values. */ @@ -42,6 +60,18 @@ public: */ virtual std::string reverse_translate_symbol(Symbol symbol) const = 0; + /** + * @brief Translate internal @p symbol representation back to its original string name on a specific level. + * + * @param[in] symbol Symbol to translate. + * @param[in] level Level on which the reverse translation should happen. + * @return @p symbol original name. + */ + virtual std::string reverse_translate_symbol(Symbol symbol, size_t level) const { + (void)level; + return reverse_translate_symbol(symbol); + } + /// also translates strings to symbols Symbol operator[](const std::string &symb) { return this->translate_symb(symb); } @@ -52,11 +82,42 @@ public: */ virtual utils::OrdVector get_alphabet_symbols() const { throw std::runtime_error("Unimplemented"); } - /// complement of a set of symbols wrt the alphabet - virtual utils::OrdVector get_complement(const utils::OrdVector& symbols) const { // {{{ - (void) symbols; + /** + * @brief Get a set of all symbols in the alphabet on a specific level. + * + * @param[in] level Level on which the symbols should be retrieved. + * @return Set of symbols known to the alphabet on the given level. + */ + virtual utils::OrdVector get_alphabet_symbols(size_t level) const { + (void)level; + using AlphabetSymbolsFn = utils::OrdVector (Alphabet::*)() const; + return (this->*static_cast(&Alphabet::get_alphabet_symbols))(); + } + + /** + * @brief Get complement of a set of symbols with respect to the alphabet. + * + * @param[in] symbols Symbols whose complement should be computed. + * @return Complement of @p symbols. + */ + virtual utils::OrdVector get_complement(const utils::OrdVector& symbols) const { + (void)symbols; throw std::runtime_error("Unimplemented"); - } // }}} + } + + /** + * @brief Get complement of a set of symbols with respect to the alphabet on a specific level. + * + * @param[in] symbols Symbols whose complement should be computed. + * @param[in] level Level on which the complement should be computed. + * @return Complement of @p symbols. + */ + virtual utils::OrdVector get_complement( + const utils::OrdVector& symbols, size_t level) const { + (void)level; + using ComplementFn = utils::OrdVector (Alphabet::*)(const utils::OrdVector&) const; + return (this->*static_cast(&Alphabet::get_complement))(symbols); + } virtual ~Alphabet() = default; @@ -83,12 +144,38 @@ public: bool operator==(const Alphabet &) const = delete; /** - * Checks whether the alphabet has any symbols. + * @brief Check whether the alphabet has any symbols. + * + * @return True if the alphabet is empty, false otherwise. */ virtual bool empty() const = 0; + /** + * @brief Check whether the alphabet has any symbols on a specific level. + * + * @param[in] level Level on which emptiness should be checked. + * @return True if the alphabet is empty, false otherwise. + */ + virtual bool empty(size_t level) const { + (void)level; + return empty(); + } + + /** + * @brief Clear symbols from the alphabet. + */ virtual void clear() { throw std::runtime_error("Unimplemented"); } + /** + * @brief Clear symbols from the alphabet on a specific level. + * + * @param[in] level Level on which the alphabet should be cleared. + */ + virtual void clear(size_t level) { + (void)level; + clear(); + } + protected: virtual const void* address() const { return this; } }; // class Alphabet. @@ -103,8 +190,14 @@ protected: */ class IntAlphabet : public Alphabet { public: - IntAlphabet() : alphabet_instance_(IntAlphabetSingleton::get()) {} + using Alphabet::clear; + using Alphabet::empty; + using Alphabet::get_alphabet_symbols; + using Alphabet::get_complement; + using Alphabet::reverse_translate_symbol; + using Alphabet::translate_symb; + IntAlphabet() : alphabet_instance_(IntAlphabetSingleton::get()) {} Symbol translate_symb(const std::string &symb) override; std::string reverse_translate_symbol(const Symbol symbol) const override { return std::to_string(symbol); } @@ -114,7 +207,7 @@ public: } utils::OrdVector get_complement(const utils::OrdVector& symbols) const override { - (void) symbols; + (void)symbols; throw std::runtime_error("Nonsensical use of get_complement() on IntAlphabet."); } @@ -177,15 +270,20 @@ private: */ class EnumAlphabet : public Alphabet { public: + using Alphabet::clear; + using Alphabet::empty; + using Alphabet::get_alphabet_symbols; + using Alphabet::get_complement; + using Alphabet::reverse_translate_symbol; + using Alphabet::translate_symb; + explicit EnumAlphabet() = default; EnumAlphabet(const EnumAlphabet& alphabet) = default; explicit EnumAlphabet(const EnumAlphabet* const alphabet): EnumAlphabet(*alphabet) {} EnumAlphabet(EnumAlphabet&& rhs) = default; utils::OrdVector get_alphabet_symbols() const override { return symbols_; } - utils::OrdVector get_complement(const utils::OrdVector& symbols) const override { - return symbols_.difference(symbols); - } + utils::OrdVector get_complement(const utils::OrdVector& symbols) const override { return symbols_.difference(symbols); } std::string reverse_translate_symbol(Symbol symbol) const override; @@ -245,8 +343,6 @@ public: */ size_t get_number_of_symbols() const { return symbols_.size(); } - bool empty() const override { return symbols_.empty(); } - private: mata::utils::OrdVector symbols_{}; ///< Map of string transition symbols to symbol values. Symbol next_symbol_value_{ 0 }; ///< Next value to be used for a newly added symbol. @@ -282,6 +378,8 @@ public: symbols_.erase(first, last); } + bool empty() const override { return symbols_.empty(); } + void clear() override { symbols_.clear(); next_symbol_value_ = 0; } }; // class EnumAlphabet. @@ -291,6 +389,13 @@ public: */ class OnTheFlyAlphabet : public Alphabet { public: + using Alphabet::clear; + using Alphabet::empty; + using Alphabet::get_alphabet_symbols; + using Alphabet::get_complement; + using Alphabet::reverse_translate_symbol; + using Alphabet::translate_symb; + using StringToSymbolMap = std::unordered_map; /// Result of the insertion of a new symbol. @@ -445,6 +550,145 @@ public: void clear() override { symbol_map_.clear(); next_symbol_value_ = 0; } }; // class OnTheFlyAlphabet. +class LevelAlphabet : public Alphabet { +public: + explicit LevelAlphabet(std::vector alphabets = {}) : alphabets_{ std::move(alphabets) } {} + + /** + * @brief Translate a symbol name using the alphabet selected without a specific level. + * + * @param[in] symb Symbol name to translate. + * @return Translated symbol value. + * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. + */ + Symbol translate_symb(const std::string& symb) override { + (void)symb; + throw std::runtime_error("LevelAlphabet operation requires an explicit level."); + } + + /** + * @brief Translate a symbol name using the alphabet for the given level. + * + * @param[in] symb Symbol name to translate. + * @param[in] level Level selecting the underlying alphabet. + * @return Translated symbol value. + */ + Symbol translate_symb(const std::string& symb, size_t level) override; + + /** + * @brief Translate a symbol value back to its name using the alphabet selected without a specific level. + * + * @param[in] symbol Symbol value to translate. + * @return Original symbol name. + * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. + */ + std::string reverse_translate_symbol(Symbol symbol) const override { + (void)symbol; + throw std::runtime_error("LevelAlphabet operation requires an explicit level."); + } + + /** + * @brief Translate a symbol value back to its name using the alphabet for the given level. + * + * @param[in] symbol Symbol value to translate. + * @param[in] level Level selecting the underlying alphabet. + * @return Original symbol name. + */ + std::string reverse_translate_symbol(Symbol symbol, size_t level) const override; + + /** + * @brief Get the union of symbols from all underlying alphabets. + * + * @return Set of symbols known to the level alphabet. + * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. + */ + utils::OrdVector get_alphabet_symbols() const override { + throw std::runtime_error("LevelAlphabet operation requires an explicit level."); + } + + /** + * @brief Get the symbols known to the alphabet on the given level. + * + * @param[in] level Level selecting the underlying alphabet. + * @return Set of symbols known to the selected alphabet. + */ + utils::OrdVector get_alphabet_symbols(size_t level) const override; + + /** + * @brief Get the complement of @p symbols with respect to the alphabet selected for the given level. + * + * @param[in] symbols Symbols whose complement should be computed. + * @return Complement of @p symbols with respect to the alphabet selected for the given @p level. + * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. + */ + utils::OrdVector get_complement(const utils::OrdVector& symbols) const override { + (void)symbols; + throw std::runtime_error("LevelAlphabet operation requires an explicit level."); + } + + /** + * @brief Get the complement of @p symbols with respect to the alphabet for the given level. + * + * @param[in] symbols Symbols whose complement should be computed. + * @param[in] level Level selecting the underlying alphabet. + * @return Complement of @p symbols with respect to the selected alphabet. + */ + utils::OrdVector get_complement( + const utils::OrdVector& symbols, size_t level) const override; + + /** + * @brief Check whether the alphabet selected without a specific level is empty. + * + * @return True if the selected alphabet is empty, false otherwise. + * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. + */ + bool empty() const override { throw std::runtime_error("LevelAlphabet operation requires an explicit level."); } + + /** + * @brief Check whether the alphabet for the given level is empty. + * + * @param[in] level Level selecting the underlying alphabet. + * @return True if the selected alphabet is empty, false otherwise. + */ + bool empty(size_t level) const override; + + /** + * @brief Clear the alphabet selected without a specific level. + * + * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. + */ + void clear() override { throw std::runtime_error("LevelAlphabet operation requires an explicit level."); } + + /** + * @brief Clear the alphabet for the given level. + * + * @param[in] level Level selecting the underlying alphabet. + */ + void clear(size_t level) override; + + /** + * @brief Get the alphabet assigned to a specific level. + * + * @param[in] level Level whose alphabet should be returned. + * @return Alphabet assigned to @p level, or @c nullptr if the level is out of range. + */ + const Alphabet* alphabet_of_level(size_t level) const; + + const std::vector& alphabets() const { return alphabets_; } + +private: + /** + * @brief Resolve the alphabet to use for the given level. + * + * @param[in] level Level selecting the underlying alphabet. + * @return Resolved alphabet reference. + * @throws std::runtime_error If the level is invalid. + */ + const Alphabet& resolve_alphabet(size_t level) const; + + std::vector alphabets_{}; +}; + /** * @brief Encode a word using UTF-8 encoding. * diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index 5b643cbcc..f597ff0a8 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -126,16 +126,6 @@ public: */ Levels levels{}; - /** - * @brief Optional per-level alphabets. - * - * When empty, the NFT falls back to the shared @ref alphabet inherited from @ref nfa::Nfa. - * When non-empty, the vector is indexed by NFT level. If all entries are the same pointer, - * the inherited shared @ref alphabet is kept in sync with that pointer; otherwise it is set - * to @c nullptr because no single shared alphabet describes the whole NFT. - */ - std::vector level_alphabets{}; - /// 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 @@ -144,41 +134,12 @@ public: // TODO: When there is a need for state dictionary, consider creating default library implementation of state // dictionary in the attributes. -public: - /** - * Create a repeated vector of @p num_of_levels entries of the same @p alphabet pointer for the level alphabets. - * - * @param num_of_levels The number of levels for which to create the vector. - */ - static std::vector repeated_level_alphabets(const size_t num_of_levels, Alphabet* alphabet); - - /** - * Check if all entries in @p level_alphabets are the same pointer and return that pointer if so, or return nullptr - * - * @param level_alphabets The vector of level alphabets to check for being all the same pointer. - */ - static Alphabet* shared_alphabet_or_null(const std::vector& level_alphabets); - explicit Nft( Delta delta = {}, utils::SparseSet initial_states = {}, utils::SparseSet final_states = {}, Levels levels = {}, Alphabet* alphabet = nullptr) : Nfa{ std::move(delta), std::move(initial_states), std::move(final_states), alphabet }, - levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states(), DEFAULT_LEVEL } : std::move(levels) }, - level_alphabets{ repeated_level_alphabets(this->levels.num_of_levels, alphabet) } {} - - explicit Nft( - Delta delta, utils::SparseSet initial_states, utils::SparseSet final_states, Levels levels, - std::vector level_alphabets) - : Nfa{ - std::move(delta), std::move(initial_states), std::move(final_states), - shared_alphabet_or_null(level_alphabets) }, - levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states(), DEFAULT_LEVEL } : std::move(levels) }, - level_alphabets{ std::move(level_alphabets) } { - if (!this->level_alphabets.empty()) { - assert(this->level_alphabets.size() == this->levels.num_of_levels); - } - } + levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states(), DEFAULT_LEVEL } : std::move(levels) } {} /** * @brief Construct a new explicit NFT with num_of_states states and optionally set initial and final states. @@ -193,19 +154,7 @@ public: utils::SparseSet final_states = {}, Levels levels = {}, Alphabet* alphabet = nullptr) : Nfa{ num_of_states, std::move(initial_states), std::move(final_states), alphabet }, - levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states, DEFAULT_LEVEL } : std::move(levels) }, - level_alphabets{ repeated_level_alphabets(this->levels.num_of_levels, alphabet) } {} - - explicit Nft( - const size_t num_of_states, utils::SparseSet initial_states, utils::SparseSet final_states, - Levels levels, std::vector level_alphabets) - : Nfa{ num_of_states, std::move(initial_states), std::move(final_states), shared_alphabet_or_null(level_alphabets) }, - levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states, DEFAULT_LEVEL } : std::move(levels) }, - level_alphabets{ std::move(level_alphabets) } { - if (!this->level_alphabets.empty()) { - assert(this->level_alphabets.size() == this->levels.num_of_levels); - } - } + levels{ levels.empty() ? Levels{ levels.num_of_levels, num_of_states, DEFAULT_LEVEL } : std::move(levels) } {} static Nft with_levels( Levels levels, const size_t num_of_states = 0, utils::SparseSet initial_states = {}, @@ -213,69 +162,31 @@ public: return Nft{ num_of_states, std::move(initial_states), std::move(final_states), std::move(levels), alphabet }; } - static Nft with_levels( - Levels levels, const size_t num_of_states, utils::SparseSet initial_states, - utils::SparseSet final_states, std::vector level_alphabets) { - return Nft{ - num_of_states, std::move(initial_states), std::move(final_states), std::move(levels), - std::move(level_alphabets) }; - } - static Nft with_levels( Levels levels, Delta delta, utils::SparseSet initial_states = {}, utils::SparseSet final_states = {}, Alphabet* alphabet = nullptr) { return Nft{ std::move(delta), std::move(initial_states), std::move(final_states), std::move(levels), alphabet }; } - static Nft with_levels( - Levels levels, Delta delta, utils::SparseSet initial_states, - utils::SparseSet final_states, std::vector level_alphabets) { - return Nft{ - std::move(delta), std::move(initial_states), std::move(final_states), std::move(levels), - std::move(level_alphabets) }; - } - static Nft with_levels( const size_t num_of_levels, const size_t num_of_states = 0, utils::SparseSet initial_states = {}, utils::SparseSet final_states = {}, Alphabet* alphabet = nullptr) { return Nft{ num_of_states, std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, alphabet }; } - static Nft with_levels( - const size_t num_of_levels, const size_t num_of_states, utils::SparseSet initial_states, - utils::SparseSet final_states, std::vector level_alphabets) { - return Nft{ - num_of_states, std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, - std::move(level_alphabets) }; - } - static Nft with_levels( const size_t num_of_levels, Delta delta, utils::SparseSet initial_states = {}, utils::SparseSet final_states = {}, Alphabet* alphabet = nullptr) { return Nft{ std::move(delta), std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, alphabet }; } - static Nft with_levels( - const size_t num_of_levels, Delta delta, utils::SparseSet initial_states, - utils::SparseSet final_states, std::vector level_alphabets) { - return Nft{ - std::move(delta), std::move(initial_states), std::move(final_states), Levels{ num_of_levels }, - std::move(level_alphabets) }; - } - /** * @brief Construct a new explicit NFT from other NFT. */ Nft(const Nft& other) = default; Nft(Nft&& other) noexcept - : levels{ std::move(other.levels) }, level_alphabets{ std::move(other.level_alphabets) } { - delta = std::move(other.delta); - initial = std::move(other.initial); - final = std::move(other.final); - attributes = std::move(other.attributes); - alphabet = other.alphabet; - other.alphabet = nullptr; + : Nfa{ std::move(other) }, levels{ std::move(other.levels) } { } Nft& operator=(const Nft& other) = default; @@ -293,8 +204,7 @@ public: * @param default_level Default level for the states. (default: 0) */ explicit Nft(const mata::nfa::Nfa& other, const size_t num_of_levels = 1, const Level default_level = DEFAULT_LEVEL) - : mata::nfa::Nfa(other), levels{ num_of_levels, num_of_states(), default_level }, - level_alphabets{ repeated_level_alphabets(num_of_levels, alphabet) } {} + : mata::nfa::Nfa(other), levels{ num_of_levels, num_of_states(), default_level } {} /** * @brief Construct a new NFT with @p num_of_levels levels from NFA. @@ -308,8 +218,7 @@ public: * @param default_level Default level for the states. (default: 0) */ explicit Nft(Nfa&& other, const size_t num_of_levels = 1, const Level default_level = DEFAULT_LEVEL) - : Nfa(std::move(other)), levels{ num_of_levels, num_of_states(), default_level }, - level_alphabets{ repeated_level_alphabets(num_of_levels, alphabet) } {} + : Nfa(std::move(other)), levels{ num_of_levels, num_of_states(), default_level } {} /** * @brief Construct a new NFT with @p num_of_levels levels from NFA. @@ -322,8 +231,7 @@ public: * @param levels Levels for the states of the NFA @c other. */ explicit Nft(const Nfa& other, Levels levels) - : Nfa(other), levels{ std::move(levels) }, - level_alphabets{ repeated_level_alphabets(this->levels.num_of_levels, alphabet) } {} + : Nfa(other), levels{ std::move(levels) } {} /** * @brief Construct a new NFT with @p num_of_levels levels from NFA. @@ -336,27 +244,7 @@ public: * @param levels Levels for the states of the NFA @c other. */ explicit Nft(Nfa&& other, Levels levels) - : Nfa{ std::move(other) }, levels{ std::move(levels) }, - level_alphabets{ repeated_level_alphabets(this->levels.num_of_levels, alphabet) } {} - - /** - * @brief Get the alphabet of the NFT for a given level. - * If the level has a specific alphabet in @c level_alphabets, return that alphabet; - * otherwise, return the shared @ref alphabet. - * - * @param level The level for which to get the alphabet. - */ - const Alphabet* alphabet_of_level(const size_t level) const; - - /** - * @brief Set the level alphabets for the NFT. - * - * When the vector of level alphabets is non-empty, it must have a size equal to the number of levels in the NFT. - * If the vector is empty, the NFT falls back to using the shared @ref alphabet for all levels. - * - * @param new_level_alphabets The new vector of level alphabets to set for the NFT. - */ - void set_level_alphabets(std::vector new_level_alphabets); + : Nfa{ std::move(other) }, levels{ std::move(levels) } {} Nft& operator=(const Nfa& other) noexcept; Nft& operator=(Nfa&& other) noexcept; diff --git a/src/alphabet.cc b/src/alphabet.cc index a3c6692e2..9bf0a47cb 100644 --- a/src/alphabet.cc +++ b/src/alphabet.cc @@ -4,6 +4,7 @@ #include using mata::Symbol; +using mata::LevelAlphabet; using mata::OnTheFlyAlphabet; mata::utils::OrdVector OnTheFlyAlphabet::get_alphabet_symbols() const { @@ -202,6 +203,49 @@ size_t mata::OnTheFlyAlphabet::erase(const std::string& symbol_name) { return 0; } +const mata::Alphabet& LevelAlphabet::resolve_alphabet(const size_t level) const { + if (alphabets_.empty()) { + throw std::runtime_error("LevelAlphabet has no underlying alphabets."); + } + + if (level >= alphabets_.size()) { + throw std::runtime_error("Requested level " + std::to_string(level) + " is out of range."); + } + if (alphabets_[level] == nullptr) { + throw std::runtime_error("Requested level " + std::to_string(level) + " has no alphabet."); + } + return *alphabets_[level]; +} + +Symbol LevelAlphabet::translate_symb(const std::string& symb, const size_t level) { + return const_cast(resolve_alphabet(level)).translate_symb(symb); +} + +std::string LevelAlphabet::reverse_translate_symbol(const Symbol symbol, const size_t level) const { + return resolve_alphabet(level).reverse_translate_symbol(symbol); +} + +mata::utils::OrdVector LevelAlphabet::get_alphabet_symbols(const size_t level) const { + return resolve_alphabet(level).get_alphabet_symbols(); +} + +mata::utils::OrdVector LevelAlphabet::get_complement( + const mata::utils::OrdVector& symbols, const size_t level) const { + return resolve_alphabet(level).get_complement(symbols); +} + +bool LevelAlphabet::empty(const size_t level) const { + return resolve_alphabet(level).empty(); +} + +void LevelAlphabet::clear(const size_t level) { + const_cast(resolve_alphabet(level)).clear(); +} + +const mata::Alphabet* LevelAlphabet::alphabet_of_level(const size_t level) const { + return level < alphabets_.size() ? alphabets_[level] : nullptr; +} + mata::Word mata::encode_word_utf8(const mata::Word& word) { mata::Word utf8_encoded_word; for (const Symbol symbol: word) { diff --git a/src/nft/builder.cc b/src/nft/builder.cc index 10085e9b3..7c667a308 100644 --- a/src/nft/builder.cc +++ b/src/nft/builder.cc @@ -126,7 +126,7 @@ Nft builder::construct(const mata::parser::ParsedSection& parsec, mata::Alphabet } const State source = get_state_name(body_line[0]); - const Symbol symbol = alphabet->translate_symb(body_line[1]); + const Symbol symbol = alphabet->translate_symb(body_line[1], aut.levels[source]); const State target = get_state_name(body_line[2]); aut.delta.add(source, symbol, target); } @@ -178,7 +178,7 @@ Nft builder::construct(const mata::IntermediateAut& inter_aut, mata::Alphabet* a } const State source = get_state_name(formula_node.name); - const Symbol symbol = alphabet->translate_symb(formula_graph.children[0].node.name); + const Symbol symbol = alphabet->translate_symb(formula_graph.children[0].node.name, aut.levels[source]); const State target = get_state_name(formula_graph.children[1].node.name); aut.delta.add(source, symbol, target); diff --git a/src/nft/nft.cc b/src/nft/nft.cc index 2d01ed6d6..0a0b485fc 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -200,26 +200,27 @@ void Nft::print_to_dot( } }; - auto translate_symbol = [&](const Symbol symbol) -> std::string { + auto translate_symbol = [&](const Symbol symbol, const size_t level) -> std::string { switch (symbol) { case EPSILON: return ""; default: break; } if (decode_ascii_chars) { return to_ascii(symbol); } else if (alphabet != nullptr) { - return alphabet->reverse_translate_symbol(symbol); - } else if (this->alphabet != nullptr) { return this->alphabet->reverse_translate_symbol(symbol); } else { + return alphabet->reverse_translate_symbol(symbol, level); + } else if (this->alphabet != nullptr) { return this->alphabet->reverse_translate_symbol(symbol, level); } else { return std::to_string(symbol); } }; - auto vec_of_symbols_to_string = [&](const OrdVector& symbols) { + auto vec_of_symbols_to_string = [&](const OrdVector& symbols, const size_t level) { std::string result; - for (const Symbol& symbol : symbols) { result += translate_symbol(symbol) + ","; } + for (const Symbol& symbol : symbols) { result += translate_symbol(symbol, level) + ","; } result.pop_back(); // Remove last comma return result; }; - auto vec_of_symbols_to_string_with_intervals = [&](const OrdVector& symbols) { + auto vec_of_symbols_to_string_with_intervals = [&]( + const OrdVector& symbols, const size_t level) { std::string result; const auto intervals{ @@ -241,10 +242,12 @@ void Nft::print_to_dot( for (const auto& [symbol_from, symbol_to] : intervals) { if (const size_t interval_size{ symbol_to - symbol_from + 1 }; interval_size == 1) { - result += translate_symbol(symbol_from) + ","; + result += translate_symbol(symbol_from, level) + ","; } else if (interval_size == 2) { - result += translate_symbol(symbol_from) + "," + translate_symbol(symbol_to) + ","; - } else { result += "[" + translate_symbol(symbol_from) + "-" + translate_symbol(symbol_to) + "],"; } + result += translate_symbol(symbol_from, level) + "," + translate_symbol(symbol_to, level) + ","; + } else { + result += "[" + translate_symbol(symbol_from, level) + "-" + translate_symbol(symbol_to, level) + "],"; + } } result.pop_back(); // Remove last comma @@ -279,9 +282,10 @@ void Nft::print_to_dot( continue; } + const size_t source_level = source < levels.size() ? levels[source] : 0; std::string label = use_intervals - ? vec_of_symbols_to_string_with_intervals(symbols) - : vec_of_symbols_to_string(symbols); + ? vec_of_symbols_to_string_with_intervals(symbols, source_level) + : vec_of_symbols_to_string(symbols, source_level); std::string on_hover_label = replace_all(replace_all(label, "<", "<"), ">", ">"); bool is_shortened = false; if (max_label_length > 0 && label.length() > static_cast(max_label_length)) { @@ -363,11 +367,11 @@ void Nft::print_to_mata(std::ostream& output) const { output << "%LevelsNum " << levels.num_of_levels << std::endl; for (const Transition& trans : delta.transitions()) { - output << "q" << trans.source << " " + output << "q" << trans.source << " " << ((alphabet != nullptr) - ? alphabet->reverse_translate_symbol(trans.symbol) + ? alphabet->reverse_translate_symbol(trans.symbol, levels[trans.source]) : ((this->alphabet != nullptr) - ? this->alphabet->reverse_translate_symbol(trans.symbol) + ? this->alphabet->reverse_translate_symbol(trans.symbol, levels[trans.source]) : std::to_string(trans.symbol))) << " q" << trans.target << std::endl; } @@ -531,7 +535,6 @@ Nft& Nft::operator=(Nft&& other) noexcept { Nfa::operator=(std::move(other)); levels = std::move(other.levels); levels.num_of_levels = other.levels.num_of_levels; - level_alphabets = std::move(other.level_alphabets); } return *this; } @@ -542,7 +545,6 @@ Nft& Nft::operator=(const Nfa& other) noexcept { Nfa::operator=(other); levels = Levels(num_of_states(), DEFAULT_LEVEL); levels.num_of_levels = 1; - level_alphabets = Nft::repeated_level_alphabets(levels.num_of_levels, alphabet); } return *this; } @@ -552,7 +554,6 @@ Nft& Nft::operator=(Nfa&& other) noexcept { Nfa::operator=(std::move(other)); levels = Levels(num_of_states(), DEFAULT_LEVEL); levels.num_of_levels = 1; - level_alphabets = Nft::repeated_level_alphabets(levels.num_of_levels, alphabet); } return *this; } @@ -816,37 +817,3 @@ bool Nft::make_complete( return transition_added; } - -std::vector Nft::repeated_level_alphabets(const size_t num_of_levels, mata::Alphabet* alphabet) { - return std::vector(num_of_levels, alphabet); -} - -mata::Alphabet* Nft::shared_alphabet_or_null(const std::vector& level_alphabets) { - if (level_alphabets.empty()) { - return nullptr; - } - - const mata::Alphabet* first = level_alphabets.front(); - for (const mata::Alphabet* alphabet : level_alphabets) { - if (alphabet != first) { - return nullptr; - } - } - - return const_cast(first); -} - -const mata::Alphabet* Nft::alphabet_of_level(const size_t level) const { - if (!level_alphabets.empty() && level < level_alphabets.size() && level_alphabets[level] != nullptr) { - return level_alphabets[level]; - } - return alphabet; -} - -void Nft::set_level_alphabets(std::vector new_level_alphabets) { - if (!new_level_alphabets.empty()) { - assert(new_level_alphabets.size() == levels.num_of_levels); - } - alphabet = shared_alphabet_or_null(new_level_alphabets); - level_alphabets = std::move(new_level_alphabets); -} diff --git a/src/nft/operations.cc b/src/nft/operations.cc index 1a897b7ed..d9f246c57 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -338,7 +338,7 @@ Nft mata::nft::project_out(const Nft& nft, const utils::OrdVector& levels } // Construct the automaton with projected levels. - Nft result{ Nft::with_levels(nft.levels, Delta{}, nft.initial, nft.final, nft.level_alphabets) }; + Nft result{ Nft::with_levels(nft.levels, Delta{}, nft.initial, nft.final, nft.alphabet) }; for (State src_state{ 0 }; src_state < num_of_states_in_delta; src_state++) { // For every state. for (const State cls_state : closure[src_state]) { // For every state in its epsilon closure. if (nft.final[cls_state] && can_be_final(src_state)) result.final.insert(src_state); @@ -446,10 +446,7 @@ Nft mata::nft::insert_levels(const Nft& nft, const BoolVector& new_levels_mask, // Construct an empty automaton with updated levels. Nft result( - Nft::with_levels( - Levels{ new_levels_mask.size(), new_state_levels }, - nft.num_of_states(), nft.initial, nft.final, nft.level_alphabets - ) + Nft::with_levels(Levels{ new_levels_mask.size(), new_state_levels }, nft.num_of_states(), nft.initial, nft.final, nft.alphabet) ); // Function to create a transition between source and target states. @@ -718,7 +715,7 @@ Nft nft::invert_levels(const Nft& aut, const JumpMode jump_mode) { // Create new automaton Nft aut_inv = Nft::with_levels( { aut.levels.num_of_levels, num_of_zero_states, DEFAULT_LEVEL }, - num_of_zero_states, std::move(new_initial), std::move(new_final), aut.level_alphabets + num_of_zero_states, std::move(new_initial), std::move(new_final), aut.alphabet ); // Creates new states with inverted levels for each inner state in the path. @@ -1032,7 +1029,7 @@ Nft mata::nft::reduce(const Nft& aut, StateRenaming* state_renaming, const Param Nft nft::determinize(const Nft& nft, std::unordered_map* subset_map) { Nft result{ Nft::with_levels(nft.levels.num_of_levels) }; - result.set_level_alphabets(nft.level_alphabets); + result.alphabet = nft.alphabet; if (nft.initial.empty()) { return result; } // Assuming all sets targets are non-empty. diff --git a/tests/nft/nft.cc b/tests/nft/nft.cc index 027b3cacf..e846545b6 100644 --- a/tests/nft/nft.cc +++ b/tests/nft/nft.cc @@ -47,6 +47,94 @@ TEST_CASE("mata::nft::Nft()") { CHECK(nft.levels == std::vector{ 0, 3, 1 }); } +TEST_CASE("mata::nft::Nft level alphabets are initialized and updated correctly") { + IntAlphabet shared_alphabet{}; + IntAlphabet input_alphabet{}; + IntAlphabet output_alphabet{}; + LevelAlphabet repeated_level_alphabet{ std::vector{ &shared_alphabet, &shared_alphabet } }; + LevelAlphabet split_level_alphabet{ std::vector{ &input_alphabet, &output_alphabet } }; + + SECTION("shared alphabet stays a plain alphabet pointer") { + Nft nft{ 3, { 0 }, { 2 }, Levels{ 2, { 0, 1, 0 } }, &shared_alphabet }; + + REQUIRE(nft.alphabet == &shared_alphabet); + CHECK(nft.alphabet->translate_symb("7", 0) == 7); + CHECK(nft.alphabet->translate_symb("7", 1) == 7); + } + + SECTION("per-level alphabets are represented by a LevelAlphabet") { + Nft nft{ 3, { 0 }, { 2 }, Levels{ 2, { 0, 1, 0 } }, &split_level_alphabet }; + + auto* level_alphabet = dynamic_cast(nft.alphabet); + REQUIRE(level_alphabet != nullptr); + CHECK(level_alphabet->alphabet_of_level(0) == &input_alphabet); + CHECK(level_alphabet->alphabet_of_level(1) == &output_alphabet); + } + + SECTION("level-aware translation requires the correct level") { + Nft nft{ 3, { 0 }, { 2 }, Levels{ 2, { 0, 1, 0 } }, &split_level_alphabet }; + + CHECK_NOTHROW(nft.alphabet->translate_symb("1", 0)); + CHECK_NOTHROW(nft.alphabet->translate_symb("1", 1)); + CHECK_THROWS(nft.alphabet->translate_symb("1")); + CHECK_THROWS(nft.alphabet->reverse_translate_symbol(1)); + CHECK(nft.alphabet->reverse_translate_symbol(1, 0) == "1"); + CHECK(nft.alphabet->reverse_translate_symbol(1, 1) == "1"); + CHECK_THROWS(repeated_level_alphabet.translate_symb("2")); + } + + SECTION("level-aware complement uses the selected level") { + EnumAlphabet input_symbols{ 1, 2, 3 }; + EnumAlphabet output_symbols{ 2, 4 }; + LevelAlphabet complement_alphabet{ std::vector{ &input_symbols, &output_symbols } }; + + CHECK(complement_alphabet.get_alphabet_symbols(0) == OrdVector{ 1, 2, 3 }); + CHECK(complement_alphabet.get_alphabet_symbols(1) == OrdVector{ 2, 4 }); + CHECK_THROWS(complement_alphabet.get_alphabet_symbols()); + CHECK(complement_alphabet.get_complement({ 2 }, 0) == OrdVector{ 1, 3 }); + CHECK(complement_alphabet.get_complement({ 2 }, 1) == OrdVector{ 4 }); + CHECK_THROWS(complement_alphabet.get_complement({ 2 })); + } + + SECTION("level-aware empty and clear use the selected level") { + OnTheFlyAlphabet input_symbols{}; + OnTheFlyAlphabet output_symbols{}; + input_symbols.add_new_symbol("a"); + output_symbols.add_new_symbol("b"); + LevelAlphabet mutable_level_alphabet{ std::vector{ &input_symbols, &output_symbols } }; + + CHECK_FALSE(mutable_level_alphabet.empty(0)); + CHECK_FALSE(mutable_level_alphabet.empty(1)); + CHECK_THROWS(mutable_level_alphabet.empty()); + + mutable_level_alphabet.clear(0); + CHECK(input_symbols.empty()); + CHECK_FALSE(output_symbols.empty()); + CHECK(mutable_level_alphabet.empty(0)); + CHECK_FALSE(mutable_level_alphabet.empty(1)); + CHECK_THROWS(mutable_level_alphabet.clear()); + } +} + +TEST_CASE("mata::nft::determinize preserves level alphabets") { + IntAlphabet input_alphabet{}; + IntAlphabet output_alphabet{}; + + LevelAlphabet level_alphabet{ std::vector{ &input_alphabet, &output_alphabet } }; + + Nft nft{ 3, { 0 }, { 2 }, Levels{ 2, { 0, 1, 0 } }, &level_alphabet }; + nft.delta.add(0, 1, 1); + nft.delta.add(1, 2, 2); + + Nft determinized = determinize(nft); + + REQUIRE(determinized.alphabet == &level_alphabet); + auto* determinized_level_alphabet = dynamic_cast(determinized.alphabet); + REQUIRE(determinized_level_alphabet != nullptr); + CHECK(determinized_level_alphabet->alphabet_of_level(0) == &input_alphabet); + CHECK(determinized_level_alphabet->alphabet_of_level(1) == &output_alphabet); +} + TEST_CASE("mata::nft::size()") { Nft nft{}; CHECK(nft.num_of_states() == 0); From 8e52ae548ca0ed2ea447ab61a9a84f1ad900b40a Mon Sep 17 00:00:00 2001 From: tmokenc Date: Thu, 23 Apr 2026 18:25:22 +0200 Subject: [PATCH 4/5] refactor: simplify the Alphabet --- include/mata/alphabet.hh | 292 +++++++++++++------------------------- include/mata/nft/types.hh | 2 +- src/alphabet.cc | 54 ++++--- 3 files changed, 135 insertions(+), 213 deletions(-) diff --git a/include/mata/alphabet.hh b/include/mata/alphabet.hh index 573fe19f2..48692c85f 100644 --- a/include/mata/alphabet.hh +++ b/include/mata/alphabet.hh @@ -5,6 +5,7 @@ #define MATA_ALPHABET_HH #include +#include #include #include #include @@ -15,6 +16,7 @@ namespace mata { using Symbol = unsigned; +using Level = unsigned; using Word = std::vector; using WordName = std::vector; @@ -24,24 +26,13 @@ using WordName = std::vector; class Alphabet { public: /** - * @brief Translate a string into a symbol. + * @brief Translate a string into a symbol, optionally on a specific level. * * @param[in] symb Symbol name to translate. + * @param[in] level Optional level on which the translation should happen. * @return Translated symbol value. */ - virtual Symbol translate_symb(const std::string &symb) = 0; - - /** - * @brief Translate a string into a symbol on a specific level. - * - * @param[in] symb Symbol name to translate. - * @param[in] level Level on which the translation should happen. - * @return Translated symbol value. - */ - virtual Symbol translate_symb(const std::string &symb, size_t level) { - (void)level; - return translate_symb(symb); - } + virtual Symbol translate_symb(const std::string& symb, std::optional level = std::nullopt) = 0; /** * Translate sequence of symbol names to sequence of their respective values. @@ -52,71 +43,44 @@ public: } /** - * @brief Translate internal @p symbol representation back to its original string name. + * @brief Translate internal @p symbol representation back to its original string name, + * optionally on a specific level. * * Throws an exception when the @p symbol is missing in the alphabet. * @param[in] symbol Symbol to translate. + * @param[in] level Optional level on which the reverse translation should happen. * @return @p symbol original name. */ - virtual std::string reverse_translate_symbol(Symbol symbol) const = 0; - - /** - * @brief Translate internal @p symbol representation back to its original string name on a specific level. - * - * @param[in] symbol Symbol to translate. - * @param[in] level Level on which the reverse translation should happen. - * @return @p symbol original name. - */ - virtual std::string reverse_translate_symbol(Symbol symbol, size_t level) const { - (void)level; - return reverse_translate_symbol(symbol); - } + virtual std::string reverse_translate_symbol( + Symbol symbol, std::optional level = std::nullopt) const = 0; /// also translates strings to symbols Symbol operator[](const std::string &symb) { return this->translate_symb(symb); } /** - * @brief Get a set of all symbols in the alphabet. + * @brief Get a set of all symbols in the alphabet, optionally on a specific level. * * The result does not have to equal the list of symbols in the automaton using this alphabet. + * @param[in] level Optional level on which the symbols should be retrieved. */ - virtual utils::OrdVector get_alphabet_symbols() const { throw std::runtime_error("Unimplemented"); } - - /** - * @brief Get a set of all symbols in the alphabet on a specific level. - * - * @param[in] level Level on which the symbols should be retrieved. - * @return Set of symbols known to the alphabet on the given level. - */ - virtual utils::OrdVector get_alphabet_symbols(size_t level) const { + virtual utils::OrdVector get_alphabet_symbols(std::optional level = std::nullopt) const { (void)level; - using AlphabetSymbolsFn = utils::OrdVector (Alphabet::*)() const; - return (this->*static_cast(&Alphabet::get_alphabet_symbols))(); - } - - /** - * @brief Get complement of a set of symbols with respect to the alphabet. - * - * @param[in] symbols Symbols whose complement should be computed. - * @return Complement of @p symbols. - */ - virtual utils::OrdVector get_complement(const utils::OrdVector& symbols) const { - (void)symbols; throw std::runtime_error("Unimplemented"); } /** - * @brief Get complement of a set of symbols with respect to the alphabet on a specific level. + * @brief Get complement of a set of symbols with respect to the alphabet, + * optionally on a specific level. * * @param[in] symbols Symbols whose complement should be computed. - * @param[in] level Level on which the complement should be computed. + * @param[in] level Optional level on which the complement should be computed. * @return Complement of @p symbols. */ virtual utils::OrdVector get_complement( - const utils::OrdVector& symbols, size_t level) const { + const utils::OrdVector& symbols, std::optional level = std::nullopt) const { + (void)symbols; (void)level; - using ComplementFn = utils::OrdVector (Alphabet::*)(const utils::OrdVector&) const; - return (this->*static_cast(&Alphabet::get_complement))(symbols); + throw std::runtime_error("Unimplemented"); } virtual ~Alphabet() = default; @@ -144,36 +108,21 @@ public: bool operator==(const Alphabet &) const = delete; /** - * @brief Check whether the alphabet has any symbols. + * @brief Check whether the alphabet has any symbols, optionally on a specific level. * + * @param[in] level Optional level on which emptiness should be checked. * @return True if the alphabet is empty, false otherwise. */ - virtual bool empty() const = 0; - - /** - * @brief Check whether the alphabet has any symbols on a specific level. - * - * @param[in] level Level on which emptiness should be checked. - * @return True if the alphabet is empty, false otherwise. - */ - virtual bool empty(size_t level) const { - (void)level; - return empty(); - } - - /** - * @brief Clear symbols from the alphabet. - */ - virtual void clear() { throw std::runtime_error("Unimplemented"); } + virtual bool empty(std::optional level = std::nullopt) const = 0; /** - * @brief Clear symbols from the alphabet on a specific level. + * @brief Clear symbols from the alphabet, optionally on a specific level. * - * @param[in] level Level on which the alphabet should be cleared. + * @param[in] level Optional level on which the alphabet should be cleared. */ - virtual void clear(size_t level) { + virtual void clear(std::optional level = std::nullopt) { (void)level; - clear(); + throw std::runtime_error("Unimplemented"); } protected: @@ -190,24 +139,24 @@ protected: */ class IntAlphabet : public Alphabet { public: - using Alphabet::clear; - using Alphabet::empty; - using Alphabet::get_alphabet_symbols; - using Alphabet::get_complement; - using Alphabet::reverse_translate_symbol; - using Alphabet::translate_symb; - IntAlphabet() : alphabet_instance_(IntAlphabetSingleton::get()) {} - Symbol translate_symb(const std::string &symb) override; + Symbol translate_symb(const std::string& symb, std::optional level = std::nullopt) override; - std::string reverse_translate_symbol(const Symbol symbol) const override { return std::to_string(symbol); } + std::string reverse_translate_symbol( + const Symbol symbol, std::optional level = std::nullopt) const override { + (void)level; + return std::to_string(symbol); + } - utils::OrdVector get_alphabet_symbols() const override { + utils::OrdVector get_alphabet_symbols(std::optional level = std::nullopt) const override { + (void)level; throw std::runtime_error("Nonsensical use of get_alphabet_symbols() on IntAlphabet."); } - utils::OrdVector get_complement(const utils::OrdVector& symbols) const override { + utils::OrdVector get_complement( + const utils::OrdVector& symbols, std::optional level = std::nullopt) const override { (void)symbols; + (void)level; throw std::runtime_error("Nonsensical use of get_complement() on IntAlphabet."); } @@ -215,9 +164,12 @@ public: IntAlphabet& operator=(const IntAlphabet& int_alphabet) = delete; - bool empty() const override { return false; } + bool empty(std::optional level = std::nullopt) const override { (void)level; return false; } - void clear() override { throw std::runtime_error("Nonsensical use of clear() on IntAlphabet."); } + void clear(std::optional level = std::nullopt) override { + (void)level; + throw std::runtime_error("Nonsensical use of clear() on IntAlphabet."); + } protected: const void* address() const override { return &alphabet_instance_; } @@ -270,22 +222,23 @@ private: */ class EnumAlphabet : public Alphabet { public: - using Alphabet::clear; - using Alphabet::empty; - using Alphabet::get_alphabet_symbols; - using Alphabet::get_complement; - using Alphabet::reverse_translate_symbol; - using Alphabet::translate_symb; - explicit EnumAlphabet() = default; EnumAlphabet(const EnumAlphabet& alphabet) = default; explicit EnumAlphabet(const EnumAlphabet* const alphabet): EnumAlphabet(*alphabet) {} EnumAlphabet(EnumAlphabet&& rhs) = default; - utils::OrdVector get_alphabet_symbols() const override { return symbols_; } - utils::OrdVector get_complement(const utils::OrdVector& symbols) const override { return symbols_.difference(symbols); } + utils::OrdVector get_alphabet_symbols(std::optional level = std::nullopt) const override { + (void)level; + return symbols_; + } + utils::OrdVector get_complement( + const utils::OrdVector& symbols, std::optional level = std::nullopt) const override { + (void)level; + return symbols_.difference(symbols); + } - std::string reverse_translate_symbol(Symbol symbol) const override; + std::string reverse_translate_symbol( + Symbol symbol, std::optional level = std::nullopt) const override; EnumAlphabet& operator=(const EnumAlphabet& rhs) = default; EnumAlphabet& operator=(EnumAlphabet&& rhs) = default; @@ -311,7 +264,7 @@ public: } EnumAlphabet(const std::initializer_list l) : EnumAlphabet(l.begin(), l.end()) {} - Symbol translate_symb(const std::string& str) override; + Symbol translate_symb(const std::string& str, std::optional level = std::nullopt) override; Word translate_word(const WordName& word_name) const override; /** @@ -378,9 +331,16 @@ public: symbols_.erase(first, last); } - bool empty() const override { return symbols_.empty(); } + bool empty(std::optional level = std::nullopt) const override { + (void)level; + return symbols_.empty(); + } - void clear() override { symbols_.clear(); next_symbol_value_ = 0; } + void clear(std::optional level = std::nullopt) override { + (void)level; + symbols_.clear(); + next_symbol_value_ = 0; + } }; // class EnumAlphabet. /** @@ -389,13 +349,6 @@ public: */ class OnTheFlyAlphabet : public Alphabet { public: - using Alphabet::clear; - using Alphabet::empty; - using Alphabet::get_alphabet_symbols; - using Alphabet::get_complement; - using Alphabet::reverse_translate_symbol; - using Alphabet::translate_symb; - using StringToSymbolMap = std::unordered_map; /// Result of the insertion of a new symbol. @@ -426,10 +379,12 @@ public: } } - utils::OrdVector get_alphabet_symbols() const override; - utils::OrdVector get_complement(const utils::OrdVector& symbols) const override; + utils::OrdVector get_alphabet_symbols(std::optional level = std::nullopt) const override; + utils::OrdVector get_complement( + const utils::OrdVector& symbols, std::optional level = std::nullopt) const override; - std::string reverse_translate_symbol(Symbol symbol) const override; + std::string reverse_translate_symbol( + Symbol symbol, std::optional level = std::nullopt) const override; public: OnTheFlyAlphabet& operator=(const OnTheFlyAlphabet& rhs) = default; @@ -451,7 +406,7 @@ public: */ void add_symbols_from(const StringToSymbolMap& new_symbol_map); - Symbol translate_symb(const std::string& str) override; + Symbol translate_symb(const std::string& str, std::optional level = std::nullopt) override; Word translate_word(const WordName& word_name) const override; @@ -505,7 +460,10 @@ public: */ const StringToSymbolMap& get_symbol_map() const { return symbol_map_; } - bool empty() const override { return symbol_map_.empty(); } + bool empty(std::optional level = std::nullopt) const override { + (void)level; + return symbol_map_.empty(); + } private: StringToSymbolMap symbol_map_{}; ///< Map of string transition symbols to symbol values. @@ -547,124 +505,74 @@ public: symbol_map_.erase(first, last); } - void clear() override { symbol_map_.clear(); next_symbol_value_ = 0; } + void clear(std::optional level = std::nullopt) override { + (void)level; + symbol_map_.clear(); + next_symbol_value_ = 0; + } }; // class OnTheFlyAlphabet. class LevelAlphabet : public Alphabet { public: explicit LevelAlphabet(std::vector alphabets = {}) : alphabets_{ std::move(alphabets) } {} - /** - * @brief Translate a symbol name using the alphabet selected without a specific level. - * - * @param[in] symb Symbol name to translate. - * @return Translated symbol value. - * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. - */ - Symbol translate_symb(const std::string& symb) override { - (void)symb; - throw std::runtime_error("LevelAlphabet operation requires an explicit level."); - } - /** * @brief Translate a symbol name using the alphabet for the given level. * * @param[in] symb Symbol name to translate. - * @param[in] level Level selecting the underlying alphabet. + * @param[in] level Level selecting the underlying alphabet (required). * @return Translated symbol value. + * @throws std::runtime_error If @p level is @c std::nullopt or out of range. */ - Symbol translate_symb(const std::string& symb, size_t level) override; - - /** - * @brief Translate a symbol value back to its name using the alphabet selected without a specific level. - * - * @param[in] symbol Symbol value to translate. - * @return Original symbol name. - * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. - */ - std::string reverse_translate_symbol(Symbol symbol) const override { - (void)symbol; - throw std::runtime_error("LevelAlphabet operation requires an explicit level."); - } + Symbol translate_symb(const std::string& symb, std::optional level = std::nullopt) override; /** * @brief Translate a symbol value back to its name using the alphabet for the given level. * * @param[in] symbol Symbol value to translate. - * @param[in] level Level selecting the underlying alphabet. + * @param[in] level Level selecting the underlying alphabet (required). * @return Original symbol name. + * @throws std::runtime_error If @p level is @c std::nullopt or out of range. */ - std::string reverse_translate_symbol(Symbol symbol, size_t level) const override; - - /** - * @brief Get the union of symbols from all underlying alphabets. - * - * @return Set of symbols known to the level alphabet. - * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. - */ - utils::OrdVector get_alphabet_symbols() const override { - throw std::runtime_error("LevelAlphabet operation requires an explicit level."); - } + std::string reverse_translate_symbol( + Symbol symbol, std::optional level = std::nullopt) const override; /** * @brief Get the symbols known to the alphabet on the given level. * - * @param[in] level Level selecting the underlying alphabet. + * @param[in] level Level selecting the underlying alphabet (required). * @return Set of symbols known to the selected alphabet. + * @throws std::runtime_error If @p level is @c std::nullopt or out of range. */ - utils::OrdVector get_alphabet_symbols(size_t level) const override; - - /** - * @brief Get the complement of @p symbols with respect to the alphabet selected for the given level. - * - * @param[in] symbols Symbols whose complement should be computed. - * @return Complement of @p symbols with respect to the alphabet selected for the given @p level. - * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. - */ - utils::OrdVector get_complement(const utils::OrdVector& symbols) const override { - (void)symbols; - throw std::runtime_error("LevelAlphabet operation requires an explicit level."); - } + utils::OrdVector get_alphabet_symbols(std::optional level = std::nullopt) const override; /** * @brief Get the complement of @p symbols with respect to the alphabet for the given level. * * @param[in] symbols Symbols whose complement should be computed. - * @param[in] level Level selecting the underlying alphabet. + * @param[in] level Level selecting the underlying alphabet (required). * @return Complement of @p symbols with respect to the selected alphabet. + * @throws std::runtime_error If @p level is @c std::nullopt or out of range. */ utils::OrdVector get_complement( - const utils::OrdVector& symbols, size_t level) const override; - - /** - * @brief Check whether the alphabet selected without a specific level is empty. - * - * @return True if the selected alphabet is empty, false otherwise. - * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. - */ - bool empty() const override { throw std::runtime_error("LevelAlphabet operation requires an explicit level."); } + const utils::OrdVector& symbols, std::optional level = std::nullopt) const override; /** * @brief Check whether the alphabet for the given level is empty. * - * @param[in] level Level selecting the underlying alphabet. + * @param[in] level Level selecting the underlying alphabet (required). * @return True if the selected alphabet is empty, false otherwise. + * @throws std::runtime_error If @p level is @c std::nullopt or out of range. */ - bool empty(size_t level) const override; - - /** - * @brief Clear the alphabet selected without a specific level. - * - * @throws std::runtime_error Always, because LevelAlphabet requires an explicit level. - */ - void clear() override { throw std::runtime_error("LevelAlphabet operation requires an explicit level."); } + bool empty(std::optional level = std::nullopt) const override; /** * @brief Clear the alphabet for the given level. * - * @param[in] level Level selecting the underlying alphabet. + * @param[in] level Level selecting the underlying alphabet (required). + * @throws std::runtime_error If @p level is @c std::nullopt or out of range. */ - void clear(size_t level) override; + void clear(std::optional level = std::nullopt) override; /** * @brief Get the alphabet assigned to a specific level. @@ -672,7 +580,7 @@ public: * @param[in] level Level whose alphabet should be returned. * @return Alphabet assigned to @p level, or @c nullptr if the level is out of range. */ - const Alphabet* alphabet_of_level(size_t level) const; + const Alphabet* alphabet_of_level(Level level) const; const std::vector& alphabets() const { return alphabets_; } @@ -682,9 +590,9 @@ private: * * @param[in] level Level selecting the underlying alphabet. * @return Resolved alphabet reference. - * @throws std::runtime_error If the level is invalid. + * @throws std::runtime_error If the level is @c std::nullopt or out of range. */ - const Alphabet& resolve_alphabet(size_t level) const; + const Alphabet& resolve_alphabet(std::optional level) const; std::vector alphabets_{}; }; diff --git a/include/mata/nft/types.hh b/include/mata/nft/types.hh index 12e1c359f..b486fc3b7 100644 --- a/include/mata/nft/types.hh +++ b/include/mata/nft/types.hh @@ -17,7 +17,7 @@ namespace mata::nft { extern const std::string TYPE_NFT; -using Level = unsigned; +using Level = mata::Level; using State = nfa::State; using StateSet = nfa::StateSet; diff --git a/src/alphabet.cc b/src/alphabet.cc index 9bf0a47cb..cb1af9f3e 100644 --- a/src/alphabet.cc +++ b/src/alphabet.cc @@ -7,7 +7,8 @@ using mata::Symbol; using mata::LevelAlphabet; using mata::OnTheFlyAlphabet; -mata::utils::OrdVector OnTheFlyAlphabet::get_alphabet_symbols() const { +mata::utils::OrdVector OnTheFlyAlphabet::get_alphabet_symbols(std::optional level) const { + (void)level; utils::OrdVector result; for (const auto& symbol : symbol_map_ | std::views::values) { result.insert(symbol); @@ -15,7 +16,9 @@ mata::utils::OrdVector OnTheFlyAlphabet::get_alphabet_symbols() const { return result; } // OnTheFlyAlphabet::get_alphabet_symbols. -mata::utils::OrdVector OnTheFlyAlphabet::get_complement(const mata::utils::OrdVector& symbols) const { +mata::utils::OrdVector OnTheFlyAlphabet::get_complement( + const mata::utils::OrdVector& symbols, std::optional level) const { + (void)level; mata::utils::OrdVector symbols_alphabet{}; symbols_alphabet.reserve(symbol_map_.size()); for (const auto& symbol : symbol_map_ | std::views::values) { @@ -31,7 +34,9 @@ void OnTheFlyAlphabet::add_symbols_from(const StringToSymbolMap& new_symbol_map) } } -std::string mata::OnTheFlyAlphabet::reverse_translate_symbol(const Symbol symbol) const { +std::string mata::OnTheFlyAlphabet::reverse_translate_symbol( + const Symbol symbol, std::optional level) const { + (void)level; for (const auto& [symbol_name, symbol_val]: symbol_map_) { if (symbol_val == symbol) { return symbol_name; @@ -46,7 +51,8 @@ void mata::OnTheFlyAlphabet::add_symbols_from(const std::vector& sy } } -Symbol mata::OnTheFlyAlphabet::translate_symb(const std::string& str) { +Symbol mata::OnTheFlyAlphabet::translate_symb(const std::string& str, std::optional level) { + (void)level; const auto [it, inserted] = symbol_map_.insert({str, next_symbol_value_}); if (inserted) { return next_symbol_value_++; @@ -106,7 +112,8 @@ std::ostream &std::operator<<(std::ostream &os, const mata::Alphabet& alphabet) return os << std::to_string(alphabet); } -Symbol mata::IntAlphabet::translate_symb(const std::string& symb) { +Symbol mata::IntAlphabet::translate_symb(const std::string& symb, std::optional level) { + (void)level; Symbol symbol; std::istringstream stream{ symb }; stream >> symbol; @@ -116,14 +123,17 @@ Symbol mata::IntAlphabet::translate_symb(const std::string& symb) { return symbol; } -std::string mata::EnumAlphabet::reverse_translate_symbol(const Symbol symbol) const { +std::string mata::EnumAlphabet::reverse_translate_symbol( + const Symbol symbol, std::optional level) const { + (void)level; if (symbols_.find(symbol) == symbols_.end()) { throw std::runtime_error("Symbol '" + std::to_string(symbol) + "' is out of range of enumeration."); } return std::to_string(symbol); } -Symbol mata::EnumAlphabet::translate_symb(const std::string& str) { +Symbol mata::EnumAlphabet::translate_symb(const std::string& str, std::optional level) { + (void)level; Symbol symbol; std::istringstream stream{ str }; stream >> symbol; @@ -203,46 +213,50 @@ size_t mata::OnTheFlyAlphabet::erase(const std::string& symbol_name) { return 0; } -const mata::Alphabet& LevelAlphabet::resolve_alphabet(const size_t level) const { +const mata::Alphabet& LevelAlphabet::resolve_alphabet(const std::optional level) const { + if (!level.has_value()) { + throw std::runtime_error("LevelAlphabet operation requires an explicit level."); + } if (alphabets_.empty()) { throw std::runtime_error("LevelAlphabet has no underlying alphabets."); } - if (level >= alphabets_.size()) { - throw std::runtime_error("Requested level " + std::to_string(level) + " is out of range."); + if (*level >= alphabets_.size()) { + throw std::runtime_error("Requested level " + std::to_string(*level) + " is out of range."); } - if (alphabets_[level] == nullptr) { - throw std::runtime_error("Requested level " + std::to_string(level) + " has no alphabet."); + if (alphabets_[*level] == nullptr) { + throw std::runtime_error("Requested level " + std::to_string(*level) + " has no alphabet."); } - return *alphabets_[level]; + return *alphabets_[*level]; } -Symbol LevelAlphabet::translate_symb(const std::string& symb, const size_t level) { +Symbol LevelAlphabet::translate_symb(const std::string& symb, const std::optional level) { return const_cast(resolve_alphabet(level)).translate_symb(symb); } -std::string LevelAlphabet::reverse_translate_symbol(const Symbol symbol, const size_t level) const { +std::string LevelAlphabet::reverse_translate_symbol( + const Symbol symbol, const std::optional level) const { return resolve_alphabet(level).reverse_translate_symbol(symbol); } -mata::utils::OrdVector LevelAlphabet::get_alphabet_symbols(const size_t level) const { +mata::utils::OrdVector LevelAlphabet::get_alphabet_symbols(const std::optional level) const { return resolve_alphabet(level).get_alphabet_symbols(); } mata::utils::OrdVector LevelAlphabet::get_complement( - const mata::utils::OrdVector& symbols, const size_t level) const { + const mata::utils::OrdVector& symbols, const std::optional level) const { return resolve_alphabet(level).get_complement(symbols); } -bool LevelAlphabet::empty(const size_t level) const { +bool LevelAlphabet::empty(const std::optional level) const { return resolve_alphabet(level).empty(); } -void LevelAlphabet::clear(const size_t level) { +void LevelAlphabet::clear(const std::optional level) { const_cast(resolve_alphabet(level)).clear(); } -const mata::Alphabet* LevelAlphabet::alphabet_of_level(const size_t level) const { +const mata::Alphabet* LevelAlphabet::alphabet_of_level(const mata::Level level) const { return level < alphabets_.size() ? alphabets_[level] : nullptr; } From 0ad8823e7b67c9f26c28962bac0d70bb4be3d8d8 Mon Sep 17 00:00:00 2001 From: tmokenc Date: Thu, 23 Apr 2026 18:32:02 +0200 Subject: [PATCH 5/5] refactor: rename the resolve_alphabet into get_alphabet_for_level --- include/mata/alphabet.hh | 20 ++++++++++++++++---- src/alphabet.cc | 28 ++++++++++++---------------- 2 files changed, 28 insertions(+), 20 deletions(-) diff --git a/include/mata/alphabet.hh b/include/mata/alphabet.hh index 48692c85f..8370b0263 100644 --- a/include/mata/alphabet.hh +++ b/include/mata/alphabet.hh @@ -586,13 +586,25 @@ public: private: /** - * @brief Resolve the alphabet to use for the given level. + * @brief Get the alphabet to use for the given level. * * @param[in] level Level selecting the underlying alphabet. - * @return Resolved alphabet reference. - * @throws std::runtime_error If the level is @c std::nullopt or out of range. + * @return Alphabet reference for @p level. + * @throws std::runtime_error If the level is out of range. */ - const Alphabet& resolve_alphabet(std::optional level) const; + const Alphabet& get_alphabet_for_level(Level level) const; + + /** + * @brief Unwrap an optional level, throwing if it is @c std::nullopt. + * + * @param[in] level Optional level supplied through the @c Alphabet interface. + * @return Unwrapped level value. + * @throws std::runtime_error If @p level is @c std::nullopt. + */ + static Level require_level(std::optional level) { + if (!level) { throw std::runtime_error("LevelAlphabet operation requires an explicit level."); } + return *level; + } std::vector alphabets_{}; }; diff --git a/src/alphabet.cc b/src/alphabet.cc index cb1af9f3e..090eba1e1 100644 --- a/src/alphabet.cc +++ b/src/alphabet.cc @@ -213,47 +213,43 @@ size_t mata::OnTheFlyAlphabet::erase(const std::string& symbol_name) { return 0; } -const mata::Alphabet& LevelAlphabet::resolve_alphabet(const std::optional level) const { - if (!level.has_value()) { - throw std::runtime_error("LevelAlphabet operation requires an explicit level."); - } +const mata::Alphabet& LevelAlphabet::get_alphabet_for_level(const mata::Level level) const { if (alphabets_.empty()) { throw std::runtime_error("LevelAlphabet has no underlying alphabets."); } - - if (*level >= alphabets_.size()) { - throw std::runtime_error("Requested level " + std::to_string(*level) + " is out of range."); + if (level >= alphabets_.size()) { + throw std::runtime_error("Requested level " + std::to_string(level) + " is out of range."); } - if (alphabets_[*level] == nullptr) { - throw std::runtime_error("Requested level " + std::to_string(*level) + " has no alphabet."); + if (alphabets_[level] == nullptr) { + throw std::runtime_error("Requested level " + std::to_string(level) + " has no alphabet."); } - return *alphabets_[*level]; + return *alphabets_[level]; } Symbol LevelAlphabet::translate_symb(const std::string& symb, const std::optional level) { - return const_cast(resolve_alphabet(level)).translate_symb(symb); + return const_cast(get_alphabet_for_level(require_level(level))).translate_symb(symb); } std::string LevelAlphabet::reverse_translate_symbol( const Symbol symbol, const std::optional level) const { - return resolve_alphabet(level).reverse_translate_symbol(symbol); + return get_alphabet_for_level(require_level(level)).reverse_translate_symbol(symbol); } mata::utils::OrdVector LevelAlphabet::get_alphabet_symbols(const std::optional level) const { - return resolve_alphabet(level).get_alphabet_symbols(); + return get_alphabet_for_level(require_level(level)).get_alphabet_symbols(); } mata::utils::OrdVector LevelAlphabet::get_complement( const mata::utils::OrdVector& symbols, const std::optional level) const { - return resolve_alphabet(level).get_complement(symbols); + return get_alphabet_for_level(require_level(level)).get_complement(symbols); } bool LevelAlphabet::empty(const std::optional level) const { - return resolve_alphabet(level).empty(); + return get_alphabet_for_level(require_level(level)).empty(); } void LevelAlphabet::clear(const std::optional level) { - const_cast(resolve_alphabet(level)).clear(); + const_cast(get_alphabet_for_level(require_level(level))).clear(); } const mata::Alphabet* LevelAlphabet::alphabet_of_level(const mata::Level level) const {