Skip to content

Nft: tape-specific alphabets#612

Open
bruderjakob17 wants to merge 2 commits intoVeriFIT:develfrom
bruderjakob17:nft_tape_alphabets
Open

Nft: tape-specific alphabets#612
bruderjakob17 wants to merge 2 commits intoVeriFIT:develfrom
bruderjakob17:nft_tape_alphabets

Conversation

@bruderjakob17
Copy link
Copy Markdown

Adds an option to have tape-specific alphabet pointers in an Nft.

The idea is that, if an optional vector of tape alphabet pointers is given, those are preferred when e.g. printing the Nft to dot format. A symbol is hence translated as determined by

  • the tape-specific alphabet, if it exists (i.e. the vector of tape alphabet pointers is not nullopt, and there is a non-null pointer to some Alphabet at the current level), or otherwise
  • the "generic" alphabet of the Nft, if it exists (i.e. it is a non-null pointer to some Alphabet)

meaning the tape-specific alphabet (if existent) is preferred over the generic Nft alphabet.

Also, this PR includes some modifications to keep the specific and generic alphabets during some common constructions.

@bruderjakob17 bruderjakob17 requested a review from Adda0 as a code owner February 23, 2026 13:28
@codecov

This comment was marked as outdated.

@Adda0
Copy link
Copy Markdown
Collaborator

Adda0 commented Mar 10, 2026

We have been thinking about this a bit, and it might not be a bad idea after all. What we are thinking now is having a single alphabet, as before, but within that alphabet, there will be a vector of pointers to alphabets, one per tape. This will make the interface cleaner while allowing for per-tape alphabets.

@bruderjakob17
Copy link
Copy Markdown
Author

Regarding this, a few comments/questions:

  1. I think your proposed solution is very nice! In particular, in cases where the user wants to just use one alphabet, there could be a function like set_alphabet(Alphabet* alph) that changes the alphabet pointers at all levels to be alph.
  2. As a general question, is there a reason that raw pointers are used when handling alphabets (instead of shared_ptrs)? I feel like this increases the mental workload as programmer to keep alphabets alive as long as some Nfa/Nft might still point to it. I could be wrong, though.
  3. Most methods also accept some alphabet as argument to "override" the stored alphabet. It would be an idea to just remove these arguments, and require the user to set the Nfa/Nft alphabets before calling such functions. For example, the print_to_dot function could then just look up if an alphabet exists, and if so, use it as if it were specified as argument by the user.

Expanding on 3.:

  • Functions that strictly require some alphabet (like complement or make_complete) could as well look up the stored alphabet, and if not present, scan through delta to find all symbols.
  • There might be some functions where the user might want to use a different alphabet without changing the automaton alphabet: e.g., make_complete would make sense to ensure that at least w.r.t. some symbols, the transition function is always defined. In this specific case, maybe it would be an idea to add a parametric version make_complete(OrdVector<Symbol>), and have a non-parametric make_complete() that calls this version with the symbols of the stored alphabet (or scans through delta if the stored alphabet is nullptr).

@Adda0
Copy link
Copy Markdown
Collaborator

Adda0 commented Mar 24, 2026

  1. Exactly.
  2. There is some not-negligible performance cost of using std::shared_ptr, but as you say, the mental gymnastics the users need to do with normal pointers with alphabets is way too much. We already agreed to use std::shared_ptr when this alphabet refactoring is being done.
  3. That is the idea as well. We are on the fence about whether we can keep the parameters for when needed, but when working with the std::shared_ptr alphabet, it might be unnecessary, since changing the automaton's alphabet will be easy. I am still thinking about creating some utility functions that would create a wrapper over an automaton instance (holding a pointer to the original automaton without modifications) and make ad hoc changes to it, such as changing the alphabet, maybe more. If this is done correctly, it would allow passing this wrapper where an instance of the Nfa or Nft class is expected.

I am glad to hear that your thoughts about alphabets (as the sole extensive user of alphabets in Mata) are similar to what we came up with at the drawing board.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants