Adda0 · Oct 4, 2026
@@ -9,7 +9,7 @@ from libmata.utils cimport COrdVector
 
 
 cdef extern from "mata/alphabet.hh" namespace "mata":
-    ctypedef uintptr_t Symbol
+    ctypedef unsigned int Symbol
     ctypedef uintptr_t Level
 
     cdef cppclass CConstAlphabet "const mata::Alphabet"

@@ -164,16 +164,6 @@ cdef extern from "mata/nfa/nfa.hh" namespace "mata::nfa":
         CNfa(const CNfa&)
 
         # Public Functions
-        void make_initial(State)
-        void make_initial(vector[State])
-        bool has_initial(State)
-        void remove_initial(State)
-        void clear_initial()
-        void make_final(State)
-        void make_final(vector[State])
-        bool has_final(State)
-        void remove_final(State)
-        void clear_final()
         void unify_initial(bool)
         void unify_final(bool)
         bool is_state(State)
@@ -206,7 +196,7 @@ cdef extern from "mata/nfa/nfa.hh" namespace "mata::nfa":
         optional[State] read_word_det(CRun&)
         pair[CRun, bool] get_word_for_path(CRun&)
         cset[vector[Symbol]] get_words(size_t) except +
-        void make_complete(CAlphabet*, optional[State]) except +
+        bool make_complete(CAlphabet*, optional[State]) except +
         shared_ptr[CConstAlphabet] resolve_alphabet(CAlphabet*) except +
         COrdVector[Symbol] get_symbols_to_work_with(CAlphabet*) except +
         string print_to_mata(const CAlphabet*) except +

@@ -489,7 +489,9 @@ class Nfa:
         that is represented as graph with edges (source, target) with
         additional properties.
 
-        Each symbol is added as an property to each edge.
+        Each symbol is added as a property to each edge. If multiple symbols
+        exist on the same edge, they are accumulated into a sorted 'symbols' list.
+        Single-symbol edges retain the scalar 'symbol' attribute for compatibility.
 
         :return:
         """
@@ -570,11 +572,12 @@ class Nfa:
         """Get the set of all words in the language of the automaton whose length is <= `max_length`."""
     def get_words_lazy(self, max_length: int | None = None) -> Iterator[tuple[Symbol, ...]]:
         """Lazily enumerate the words in the language of the automaton whose length is <= `max_length`."""
-    def make_complete(self, sink_state: State, alphabet: alph.Alphabet) -> None:
+    def make_complete(self, sink_state: State, alphabet: alph.Alphabet) -> bool:
         """Makes NFA complete.
 
         :param Symbol sink_state: sink state of the automaton
         :param OnTheFlyAlphabet alphabet: alphabet to make complete against.
+        :return: True if the automaton was modified, False if already complete.
         """
     def get_symbols(self) -> set[Symbol]:
         """Return a set of symbols used on the transitions in NFA.

@@ -730,6 +730,7 @@ cdef class Nfa:
     def unify_final(self, bool force_new_state = False) -> Nfa:
         """Unify final states into a single new final state."""
         self.thisptr.get().unify_final(force_new_state)
+        return self
 
     def add_transition_object(self, Transition tr):
         """Adds transition to automaton
@@ -1001,8 +1002,10 @@ cdef class Nfa:
         result += "final_states: {}\n".format([s for s in self.thisptr.get().final])
         result += "transitions:\n"
         for trans in self.iterate():
-            symbol = trans.symbol if self.thisptr.get().alphabet.get() == NULL \
-                else self.thisptr.get().alphabet.get().reverse_translate_symbol(trans.symbol)
+            if self.thisptr.get().alphabet.get() == NULL:
+                symbol = trans.symbol
+            else:
+                symbol = self.thisptr.get().alphabet.get().reverse_translate_symbol(trans.symbol).decode('utf-8')
             result += f"{trans.source}-[{symbol}]\u2192{trans.target}\n"
         return result
 
@@ -1107,13 +1110,30 @@ cdef class Nfa:
         that is represented as graph with edges (source, target) with
         additional properties.
 
-        Each symbol is added as an property to each edge.
+        Each symbol is added as a property to each edge. If multiple symbols
+        exist on the same edge, they are accumulated into a sorted 'symbols' list.
+        Single-symbol edges retain the scalar 'symbol' attribute for compatibility.
 
         :return:
         """
-        G = nx.DiGraph()
+        # Accumulate symbols per (source, target) pair.
+        edge_symbols = {}
         for trans in self.iterate():
-            G.add_edge(trans.source, trans.target, symbol=trans.symbol)
+            key = (trans.source, trans.target)
+            if key not in edge_symbols:
+                edge_symbols[key] = []
+            edge_symbols[key].append(trans.symbol)
+
+        G = nx.DiGraph()
+        # Add edges with sorted symbols list, and scalar symbol for single-symbol edges.
+        edges_to_add = []
+        for (source, target), symbols in edge_symbols.items():
+            symbols_sorted = sorted(set(symbols))
+            attrs = {"symbols": symbols_sorted}
+            if len(symbols_sorted) == 1:
+                attrs["symbol"] = symbols_sorted[0]
+            edges_to_add.append((source, target, attrs))
+        G.add_edges_from(edges_to_add)
         return G
 
     def post_map_of(self, State st, alph.Alphabet alphabet):
@@ -1264,15 +1284,16 @@ cdef class Nfa:
         finally:
             del it
 
-    def make_complete(self, State sink_state, alph.Alphabet alphabet):
+    def make_complete(self, State sink_state, alph.Alphabet alphabet) -> bool:
         """Makes NFA complete.
 
         :param Symbol sink_state: sink state of the automaton
         :param OnTheFlyAlphabet alphabet: alphabet to make complete against.
+        :return: True if the automaton was modified, False if already complete.
         """
         if not self.thisptr.get().is_state(sink_state):
             self.thisptr.get().add_state(self.thisptr.get().num_of_states())
-        self.thisptr.get().make_complete(alphabet.as_base().get(), make_optional[State](sink_state))
+        return self.thisptr.get().make_complete(alphabet.as_base().get(), make_optional[State](sink_state))
 
     def get_symbols(self):
         """Return a set of symbols used on the transitions in NFA.

@@ -41,7 +41,7 @@ class ReplaceMode(IntEnum):
     Single = 0
     All = 1
 
-def noodlify(aut: mata_nfa.Nfa, symbol: Symbol, include_empty: bool = False) -> list[mata_nfa.Nfa]:
+def noodlify(aut: mata_nfa.Nfa, symbol: Symbol, include_empty: bool = False) -> list[list[mata_nfa.Nfa]]:
     """Create noodles from segment automaton.
 
     Segment automaton is a chain of finite automata (segments) connected via ε-transitions.
@@ -61,7 +61,7 @@ def noodlify_for_equation(
     right_side_automaton: mata_nfa.Nfa,
     include_empty: bool = False,
     params: dict[Literal["reduce"], Literal["false", "forward", "backward", "bidirectional"]] | None = None,
-) -> None:
+) -> list[list[mata_nfa.Nfa]]:
     """Create noodles for equation.
 
     Segment automaton is a chain of finite automata (segments) connected via ε-transitions.

@@ -165,14 +165,22 @@ def noodlify_for_equation(left_side_automata: list, mata_nfa.Nfa right_side_auto
     :param: bool include_empty: Whether to also include empty noodles.
     :param: dict params: Additional parameters for the noodlification:
         - "reduce": "false", "forward", "backward", "bidirectional"; Execute forward, backward or bidirectional simulation
-                    minimization before noodlification.
+                    minimization before noodlification. When "reduce" is set, the caller's left-side automata are not mutated.
     :return: List of automata: A list of all (non-empty) noodles.
     """
+    params = params or {}
+    # When reducing, the C++ side unifies the initial and final states of the left side automata in place; pass it
+    #  copies instead. `lhs_copies` keeps the copies alive while C++ holds their raw pointers.
+    copy_lhs = params.get("reduce", "false") != "false"
+    lhs_copies = []
     cdef vector[CNfa*] c_left_side_automata
     for lhs_aut in left_side_automata:
+        if copy_lhs:
+            lhs_aut = (<mata_nfa.Nfa>lhs_aut).__copy__()
+            lhs_copies.append(lhs_aut)
         c_left_side_automata.push_back((<mata_nfa.Nfa>lhs_aut).thisptr.get())
+
     noodle_segments = []
-    params = params or {}
     cdef vector[vector[shared_ptr[CNfa]]] c_noodle_segments = mata_strings.c_noodlify_for_equation(
         c_left_side_automata, dereference(right_side_automaton.thisptr.get()), include_empty,
         {

@@ -0,0 +1,50 @@
+"""Regression tests for #768: symbol width, unify_final chaining, str decoding, and noodlify_for_equation copying."""
+
+import libmata.nfa.nfa as mata_nfa
+import libmata.nfa.strings as mata_strings
+import pytest
+from libmata import alphabets
+
+
+def test_add_transition_rejects_symbol_beyond_32_bits():
+    """mata::Symbol is 32-bit; passing a larger symbol must raise instead of truncating to low bits."""
+    nfa = mata_nfa.Nfa(2)
+    with pytest.raises(OverflowError):
+        nfa.add_transition(0, 2**32 + 5, 1)
+    assert nfa.get_symbols() == set()
+
+
+def test_unify_final_returns_self_like_unify_initial():
+    nfa = mata_nfa.Nfa(3)
+    nfa.make_initial_state(0)
+    nfa.make_final_state(1)
+    nfa.make_final_state(2)
+    assert nfa.unify_initial() is nfa
+    assert nfa.unify_final() is nfa
+
+
+def test_str_decodes_symbol_names():
+    alphabet = alphabets.OnTheFlyAlphabet.from_symbol_map({"a": 0})
+    nfa = mata_nfa.Nfa(2, alphabet=alphabet)
+    nfa.add_transition(0, 0, 1)
+    text = str(nfa)
+    assert "-[a]→" in text
+    assert "b'" not in text
+
+
+def test_noodlify_for_equation_with_reduce_does_not_mutate_callers_automata():
+    lhs = mata_nfa.Nfa(3)
+    lhs.make_initial_state(0)
+    lhs.make_initial_state(1)
+    lhs.make_final_state(2)
+    lhs.add_transition(0, ord("a"), 2)
+    lhs.add_transition(1, ord("b"), 2)
+    rhs = mata_nfa.Nfa(2)
+    rhs.make_initial_state(0)
+    rhs.make_final_state(1)
+    rhs.add_transition(0, ord("a"), 1)
+    rhs.add_transition(0, ord("b"), 1)
+    states_before, initial_before = lhs.num_of_states(), sorted(lhs.initial_states)
+    noodles = mata_strings.noodlify_for_equation([lhs], rhs, params={"reduce": "forward"})
+    assert (lhs.num_of_states(), sorted(lhs.initial_states)) == (states_before, initial_before)
+    assert noodles and all(isinstance(segment, list) for segment in noodles)
@@ -30,3 +30,21 @@ def test_conversions(fa_one_divisible_by_two):
     assert len(G) == 0
     assert list(G.nodes) == []
     assert list(G.edges) == []
+
+
+def test_to_networkx_graph_keeps_parallel_symbols():
+    """All symbols between a pair of states have to survive the conversion."""
+    nfa = mata_nfa.Nfa(2)
+    for symbol in (2, 0, 1):
+        nfa.add_transition(0, symbol, 1)
+    nfa.add_transition(1, 7, 1)
+
+    G = nfa.to_networkx_graph()
+
+    # Plain (source, target) edges, so that unpacking `G.edges` keeps working.
+    assert list(G.edges) == [(0, 1), (1, 1)]
+    assert G[0][1]["symbols"] == [0, 1, 2]
+    # A single-symbol edge keeps the scalar attribute; an ambiguous one must not.
+    assert "symbol" not in G[0][1]
+    assert G[1][1]["symbols"] == [7]
+    assert G[1][1]["symbol"] == 7