Skip to content

feat: add support for per-level alphabet in NFT #618

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tmokenc wants to merge 5 commits into
base: devel
Choose a base branch
from
Open

feat: add support for per-level alphabet in NFT #618

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
ec691fe
feat: support for alphabet per tape/level
tmokenc Apr 8, 2026
75f6351
refactors: move function bodies to .cc file
tmokenc Apr 15, 2026
9e1d342
refactors: level-awar alphabet handling into LevelAlphabet instead of…
tmokenc Apr 17, 2026
8e52ae5
refactor: simplify the Alphabet
tmokenc Apr 23, 2026
0ad8823
refactor: rename the resolve_alphabet into get_alphabet_for_level
tmokenc Apr 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
232 changes: 198 additions & 34 deletions include/mata/alphabet.hh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,15 +5,18 @@
#define MATA_ALPHABET_HH

#include <limits>
#include <optional>
#include <string>
#include <utility>
#include <vector>

#include "utils/ord-vector.hh"
#include "utils/utils.hh"

namespace mata {

using Symbol = unsigned;
using Level = unsigned;
Copy link
Copy Markdown
Collaborator

@Adda0 Adda0 Apr 24, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Use using Level = mata::Level here instead.

using Word = std::vector<Symbol>;
using WordName = std::vector<std::string>;

Expand All @@ -22,8 +25,14 @@ using WordName = std::vector<std::string>;
*/
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> level = std::nullopt) = 0;

/**
* Translate sequence of symbol names to sequence of their respective values.
Expand All @@ -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> 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<Symbol> get_alphabet_symbols() const { throw std::runtime_error("Unimplemented"); }
virtual utils::OrdVector<Symbol> get_alphabet_symbols(std::optional<Level> level = std::nullopt) const {
(void)level;
throw std::runtime_error("Unimplemented");
}

/// complement of a set of symbols wrt the alphabet
virtual utils::OrdVector<Symbol> get_complement(const utils::OrdVector<Symbol>& 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<Symbol> get_complement(
const utils::OrdVector<Symbol>& symbols, std::optional<Level> level = std::nullopt) const {
(void)symbols;
(void)level;
throw std::runtime_error("Unimplemented");
} // }}}
}

virtual ~Alphabet() = default;

Expand All @@ -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> 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> level = std::nullopt) {
(void)level;
throw std::runtime_error("Unimplemented");
}

protected:
virtual const void* address() const { return this; }
Expand All @@ -104,27 +140,36 @@ protected:
class IntAlphabet : public Alphabet {
public:
IntAlphabet() : alphabet_instance_(IntAlphabetSingleton::get()) {}
Symbol translate_symb(const std::string& symb, std::optional<Level> 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> level = std::nullopt) const override {
(void)level;
return std::to_string(symbol);
}

utils::OrdVector<Symbol> get_alphabet_symbols() const override {
utils::OrdVector<Symbol> get_alphabet_symbols(std::optional<Level> level = std::nullopt) const override {
(void)level;
throw std::runtime_error("Nonsensical use of get_alphabet_symbols() on IntAlphabet.");
}

utils::OrdVector<Symbol> get_complement(const utils::OrdVector<Symbol>& symbols) const override {
(void) symbols;
utils::OrdVector<Symbol> get_complement(
const utils::OrdVector<Symbol>& symbols, std::optional<Level> level = std::nullopt) const override {
(void)symbols;
(void)level;
throw std::runtime_error("Nonsensical use of get_complement() on IntAlphabet.");
}

IntAlphabet(const IntAlphabet&) = default;

IntAlphabet& operator=(const IntAlphabet& int_alphabet) = delete;

bool empty() const override { return false; }
bool empty(std::optional<Level> 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> 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_; }
Expand Down Expand Up @@ -182,12 +227,18 @@ public:
explicit EnumAlphabet(const EnumAlphabet* const alphabet): EnumAlphabet(*alphabet) {}
EnumAlphabet(EnumAlphabet&& rhs) = default;

utils::OrdVector<Symbol> get_alphabet_symbols() const override { return symbols_; }
utils::OrdVector<Symbol> get_complement(const utils::OrdVector<Symbol>& symbols) const override {
utils::OrdVector<Symbol> get_alphabet_symbols(std::optional<Level> level = std::nullopt) const override {
(void)level;
return symbols_;
}
utils::OrdVector<Symbol> get_complement(
const utils::OrdVector<Symbol>& symbols, std::optional<Level> 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> level = std::nullopt) const override;

EnumAlphabet& operator=(const EnumAlphabet& rhs) = default;
EnumAlphabet& operator=(EnumAlphabet&& rhs) = default;
Expand All @@ -213,7 +264,7 @@ public:
}
EnumAlphabet(const std::initializer_list<std::string> l) : EnumAlphabet(l.begin(), l.end()) {}

Symbol translate_symb(const std::string& str) override;
Symbol translate_symb(const std::string& str, std::optional<Level> level = std::nullopt) override;
Word translate_word(const WordName& word_name) const override;

/**
Expand Down Expand Up @@ -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<Symbol> symbols_{}; ///< Map of string transition symbols to symbol values.
Symbol next_symbol_value_{ 0 }; ///< Next value to be used for a newly added symbol.
Expand Down Expand Up @@ -282,7 +331,16 @@ public:
symbols_.erase(first, last);
}

void clear() override { symbols_.clear(); next_symbol_value_ = 0; }
bool empty(std::optional<Level> level = std::nullopt) const override {
(void)level;
return symbols_.empty();
}

void clear(std::optional<Level> level = std::nullopt) override {
(void)level;
symbols_.clear();
next_symbol_value_ = 0;
}
}; // class EnumAlphabet.

/**
Expand Down Expand Up @@ -321,10 +379,12 @@ public:
}
}

utils::OrdVector<Symbol> get_alphabet_symbols() const override;
utils::OrdVector<Symbol> get_complement(const utils::OrdVector<Symbol>& symbols) const override;
utils::OrdVector<Symbol> get_alphabet_symbols(std::optional<Level> level = std::nullopt) const override;
utils::OrdVector<Symbol> get_complement(
const utils::OrdVector<Symbol>& symbols, std::optional<Level> level = std::nullopt) const override;

std::string reverse_translate_symbol(Symbol symbol) const override;
std::string reverse_translate_symbol(
Symbol symbol, std::optional<Level> level = std::nullopt) const override;

public:
OnTheFlyAlphabet& operator=(const OnTheFlyAlphabet& rhs) = default;
Expand All @@ -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> level = std::nullopt) override;

Word translate_word(const WordName& word_name) const override;

Expand Down Expand Up @@ -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> level = std::nullopt) const override {
(void)level;
return symbol_map_.empty();
}

private:
StringToSymbolMap symbol_map_{}; ///< Map of string transition symbols to symbol values.
Expand Down Expand Up @@ -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> level = std::nullopt) override {
(void)level;
symbol_map_.clear();
next_symbol_value_ = 0;
}
}; // class OnTheFlyAlphabet.

class LevelAlphabet : public Alphabet {
public:
explicit LevelAlphabet(std::vector<Alphabet*> 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> 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> 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<Symbol> get_alphabet_symbols(std::optional<Level> 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<Symbol> get_complement(
const utils::OrdVector<Symbol>& symbols, std::optional<Level> 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> 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> 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<Alphabet*>& 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> level) {
if (!level) { throw std::runtime_error("LevelAlphabet operation requires an explicit level."); }
return *level;
}

std::vector<Alphabet*> alphabets_{};
Copy link
Copy Markdown
Collaborator

@Adda0 Adda0 Apr 24, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thinking about the usage, there should be an easy way to set level alphabets and access them. Maybe this is supposed to be public? But then again, you would have to explicitly cast to LevelAlphabet to access this data member. Not sure what the best approach is.

};

/**
* @brief Encode a word using UTF-8 encoding.
*
Expand Down
Loading
Loading