diff --git a/include/mata/alphabet.hh b/include/mata/alphabet.hh index 22e81fd69..8370b0263 100644 --- a/include/mata/alphabet.hh +++ b/include/mata/alphabet.hh @@ -5,8 +5,10 @@ #define MATA_ALPHABET_HH #include +#include #include #include +#include #include "utils/ord-vector.hh" #include "utils/utils.hh" @@ -14,6 +16,7 @@ namespace mata { using Symbol = unsigned; +using Level = unsigned; using Word = std::vector; using WordName = std::vector; @@ -22,8 +25,14 @@ using WordName = std::vector; */ class Alphabet { public: - /// translates a string into a symbol - virtual Symbol translate_symb(const std::string &symb) = 0; + /** + * @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, std::optional level = std::nullopt) = 0; /** * Translate sequence of symbol names to sequence of their respective values. @@ -34,29 +43,45 @@ 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; + 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"); } + virtual utils::OrdVector get_alphabet_symbols(std::optional level = std::nullopt) const { + (void)level; + 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 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 Optional level on which the complement should be computed. + * @return Complement of @p symbols. + */ + virtual utils::OrdVector get_complement( + const utils::OrdVector& symbols, std::optional level = std::nullopt) const { + (void)symbols; + (void)level; throw std::runtime_error("Unimplemented"); - } // }}} + } virtual ~Alphabet() = default; @@ -83,11 +108,22 @@ public: bool operator==(const Alphabet &) const = delete; /** - * Checks 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; + virtual bool empty(std::optional level = std::nullopt) const = 0; - virtual void clear() { throw std::runtime_error("Unimplemented"); } + /** + * @brief Clear symbols from the alphabet, optionally on a specific level. + * + * @param[in] level Optional level on which the alphabet should be cleared. + */ + virtual void clear(std::optional level = std::nullopt) { + (void)level; + throw std::runtime_error("Unimplemented"); + } protected: virtual const void* address() const { return this; } @@ -104,17 +140,23 @@ protected: class IntAlphabet : public Alphabet { public: IntAlphabet() : alphabet_instance_(IntAlphabetSingleton::get()) {} + Symbol translate_symb(const std::string& symb, std::optional level = std::nullopt) override; - Symbol translate_symb(const std::string &symb) 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 { - (void) symbols; + 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."); } @@ -122,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_; } @@ -182,12 +227,18 @@ public: 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 { + 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; @@ -213,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; /** @@ -245,8 +296,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,7 +331,16 @@ public: symbols_.erase(first, last); } - void clear() override { symbols_.clear(); next_symbol_value_ = 0; } + bool empty(std::optional level = std::nullopt) const override { + (void)level; + return symbols_.empty(); + } + + void clear(std::optional level = std::nullopt) override { + (void)level; + symbols_.clear(); + next_symbol_value_ = 0; + } }; // class EnumAlphabet. /** @@ -321,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; @@ -346,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; @@ -400,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. @@ -442,9 +505,110 @@ 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 for the given level. + * + * @param[in] symb Symbol name to translate. + * @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, 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 (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, 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 (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(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 (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, 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 (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(std::optional level = std::nullopt) const override; + + /** + * @brief Clear the alphabet for the given level. + * + * @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(std::optional level = std::nullopt) 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(Level level) const; + + const std::vector& alphabets() const { return alphabets_; } + +private: + /** + * @brief Get the alphabet to use for the given level. + * + * @param[in] level Level selecting the underlying alphabet. + * @return Alphabet reference for @p level. + * @throws std::runtime_error If the level is out of range. + */ + 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_{}; +}; + /** * @brief Encode a word using UTF-8 encoding. * diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index b5d2cfaf9..f597ff0a8 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -134,7 +134,6 @@ public: // TODO: When there is a need for state dictionary, consider creating default library implementation of state // dictionary in the attributes. -public: explicit Nft( Delta delta = {}, utils::SparseSet initial_states = {}, utils::SparseSet final_states = {}, Levels levels = {}, @@ -187,13 +186,7 @@ public: Nft(const Nft& other) = default; Nft(Nft&& other) noexcept - : levels{ std::move(other.levels) } { - 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; @@ -237,7 +230,8 @@ 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) } {} /** * @brief Construct a new NFT with @p num_of_levels levels from NFA. @@ -249,7 +243,8 @@ 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) } {} Nft& operator=(const Nfa& other) noexcept; Nft& operator=(Nfa&& other) noexcept; 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 a3c6692e2..090eba1e1 100644 --- a/src/alphabet.cc +++ b/src/alphabet.cc @@ -4,9 +4,11 @@ #include 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); @@ -14,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) { @@ -30,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; @@ -45,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_++; @@ -105,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; @@ -115,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; @@ -202,6 +213,49 @@ size_t mata::OnTheFlyAlphabet::erase(const std::string& symbol_name) { return 0; } +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 (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 std::optional level) { + 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 get_alphabet_for_level(require_level(level)).reverse_translate_symbol(symbol); +} + +mata::utils::OrdVector LevelAlphabet::get_alphabet_symbols(const std::optional level) const { + 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 get_alphabet_for_level(require_level(level)).get_complement(symbols); +} + +bool LevelAlphabet::empty(const std::optional level) const { + return get_alphabet_for_level(require_level(level)).empty(); +} + +void LevelAlphabet::clear(const std::optional level) { + const_cast(get_alphabet_for_level(require_level(level))).clear(); +} + +const mata::Alphabet* LevelAlphabet::alphabet_of_level(const mata::Level 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 c43dfc7cb..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; } @@ -528,7 +532,7 @@ 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; } diff --git a/src/nft/operations.cc b/src/nft/operations.cc index 686d2e88f..d9f246c57 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -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.alphabet - ) + 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. 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);