Property and metamorphic test suite (2/4, landing #24 on main)

.github/workflows/build.yml

@@ -1,6 +1,15 @@
 name: Build
 
-on: [push, pull_request, workflow_dispatch]
+on:
+  push:
+    branches: [main]
+  pull_request:
+  workflow_dispatch:
+
+# A newer commit on the same PR or branch supersedes runs still queued for older ones.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
 
 jobs:
   test:
@@ -30,7 +39,7 @@ jobs:
         uses: ts-graphviz/setup-graphviz@v2
 
       - name: Install package and dependencies
-        run: uv sync --extra test
+        run: uv sync --extra test --extra symbolic
 
       - name: Run tests
         run: uv run pytest --cov-report=xml
@@ -43,6 +52,30 @@ jobs:
           files: coverage.xml
           fail_ci_if_error: false
 
+  test-without-symbolic:
+    # sympy is optional; this keeps the import guards and pytest.importorskip paths honest.
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v6
+
+      - name: Set up uv
+        uses: astral-sh/setup-uv@v8.1.0
+        with:
+          version: "latest"
+
+      - name: Install Python
+        run: uv python install 3.13
+
+      - name: Install Graphviz
+        uses: ts-graphviz/setup-graphviz@v2
+
+      - name: Install package and dependencies
+        run: uv sync --extra test
+
+      - name: Run tests
+        run: uv run pytest --no-cov
+
   lint:
     runs-on: ubuntu-latest
     steps:

CHANGELOG.md

@@ -54,13 +54,27 @@ brute-force reference or a closed-form value and has a regression test.
   `reverse()` returns the mirror-image shift; `from_adjacency` assigns symbols in
   sorted order and honors subclasses; the synchronization methods on
   `SoficShift` (`markov_order`, `reset_threshold`, ...) no longer raise
-  `AttributeError`.
+  `AttributeError`; the Fischer cover raises on reducible shifts instead of
+  returning a single terminal component; the Parry measure drops transient
+  states.
 - **Generators:** `cryptic_order` is 0 for zero-crypticity processes (even,
   periodic) via a new algorithm checked against brute force;
   `log_word_probability` no longer underflows; channel statistical complexity
   uses the driven process's occupation law (it was hash-seed dependent);
   mixed-state enumeration of infinite belief sets fails in under a second;
-  numeric stationary distributions warn when not unique.
+  numeric stationary distributions warn when not unique;
+  `EpsilonMachine.from_hmm` handles more than 26 causal states;
+  `word_probability` no longer returns 0 below 1e-15 (and
+  `conditional_word_probability` no longer raises `ZeroDivisionError` there);
+  `backward(normalize=True)` normalizes the final row; `reverse_is_finite` is
+  documented as deciding finiteness of the reverse mixed states, a sufficient
+  but not necessary condition for a finite reverse ε-machine (alternating
+  biased coins has infinitely many reverse beliefs but a two-state reverse
+  machine); `from_time_reversed` and `to_bidirectional` warn when numeric belief
+  merging returns a finite truncation of an infinite reverse machine; the bidirectional machine's choice
+  between joint classes that tie on the anatomy identity no longer depends on
+  floating-point round-off (it chose a wrong class on x86-64, giving E = 1.0
+  instead of 1.5 for a 3-state machine).
 - **Inference:** Bayesian posterior machines start where the data start (they
   started in its final state, giving −∞ likelihoods and infinite BIC); WAIC
   scores from the stationary distribution; `learn_stack_hmm_mle` and the stack
@@ -75,6 +89,8 @@ brute-force reference or a closed-form value and has a regression test.
   `wheeler_index`, word counting, empty marks, `minimize_wheeler` on dead
   states, and `colex_width`; modular VPA `minimize` on valid well-matched VPAs;
   intersection, difference and complement with empty-language operands;
+  `complete()` no longer reuses an accepting trap left by a previous
+  complement (double complement could return the wrong language);
   `right_quotient` by the empty word; `sofic.automata.languages.residuals`
   callable again; IDFA enumeration includes missing transitions before the first
   flag (`count_accessible_idfa(2, 2)` is 45), which changes some canonical
@@ -88,13 +104,21 @@ brute-force reference or a closed-form value and has a regression test.
 - **Serialization and viz:** YAML stores observation, output and stack
   alphabets and supports sympy and `Fraction` values; `copy()` deep-copies
   attributes; Graphviz/TikZ node names are unique; TikZ escapes `^`, `~`, `\`
-  for math mode.
+  for math mode and handles newlines in labels; YAML uses libyaml's C loader
+  and dumper when available.
 
 ### New
 
 - Hypothesis strategies in `sofic.testing` for NFAs, Büchi automata and lassos,
   Wheeler NFAs, Markov chains, Mealy HMMs, sofic shifts, SFTs, VPAs, NWAs, and
   Mealy transducers; `ci` and `nightly` Hypothesis profiles (`HYPOTHESIS_PROFILE`).
+- Experimental `EpsilonMachine.reverse_epsilon_machine_is_finite()` (and
+  `sofic.generators.reversal.reverse_epsilon_machine_is_finite`): decides whether
+  the reverse ε-machine has finitely many *recurrent* causal states, which
+  `reverse_is_finite` only bounds from one side.
+- A property and metamorphic test suite (`tests/test_properties_*.py`) checking
+  shifts, generators, inference, automata, serialization, viz and examples
+  against brute-force oracles and invariants.
 
 ## 0.3.0
 

docs/generators/epsilon_machine.rst

@@ -75,12 +75,21 @@ infinite — that is the entropy of the retrodictive stationary distribution, an
 it converges when those weights decay geometrically, as in the example above.
 The obstruction here is cardinality, not divergence.
 
-:meth:`reverse_is_finite` decides this in polynomial time without enumerating
-beliefs. Since the retrodictive causal states are the normalized vectors
-:math:`(\Pr(x \mid s))_s`, the reverse machine is finite exactly when every
-cycle of the pair graph on :math:`S \times S`, weighted by
+:meth:`reverse_is_finite` gives a polynomial-time sufficient condition without
+enumerating beliefs. The reverse mixed states are the normalized vectors
+:math:`(\Pr(x \mid s))_s`, and they are finite exactly when every cycle of the
+pair graph on :math:`S \times S`, weighted by
 :math:`p(a \mid s) / p(a \mid s')`, has weight one — the twins property
-:cite:`Mohri2009` :cite:`AllauzenMohri2003`.
+:cite:`Mohri2009` :cite:`AllauzenMohri2003`. Finitely many mixed states implies
+a finite reverse machine, but not conversely: for alternating biased coins the
+mixed states are infinite, yet they converge to two recurrent causal states.
+
+:meth:`reverse_epsilon_machine_is_finite` (experimental) decides the recurrent
+question instead: the reverse machine is infinite exactly when a pair-graph
+component with a non-unit cycle can reach the diagonal, so that a grown ratio
+is frozen by the two forward paths merging. :meth:`from_time_reversed` warns
+when it says infinite but numeric belief merging closed the construction
+anyway.
 
 This is not a structural property: two machines with identical transition
 structure can differ, because a cycle weight may equal one only by algebraic
@@ -93,10 +102,12 @@ API
 ===
 
 .. autoclass:: EpsilonMachine
-   :members: from_hmm, from_sequence, from_time_reversed, to_bidirectional, block_entropy_diagram, block_entropy_estimates, plot_block_entropy_diagram, block_convergence_diagram, block_convergence_estimates, plot_block_convergence_diagram, caekl_block_information, caekl_rate, caekl_intercept, caekl_rate_converged, approximate_entropy_rate, approximate_excess_entropy, approximate_information_anatomy, statistical_complexity, bidirectional_statistical_complexity, excess_entropy, predicted_information, bound_information, ephemeral_information, information_anatomy, caekl_causal_information, crypticity, bidirectional_crypticity, causal_irreversibility, stored_information_decomposition, transient_information, oracular_information, gauge_information, predictability_gain, structural_information, thermodynamic_depth, spectral_complexity, markov_order, is_markov, cryptic_order, reset_threshold, synchronizing_word, is_exactly_synchronizable, is_asymptotically_synchronizable, is_definite, reverse_is_finite
+   :members: from_hmm, from_sequence, from_time_reversed, to_bidirectional, block_entropy_diagram, block_entropy_estimates, plot_block_entropy_diagram, block_convergence_diagram, block_convergence_estimates, plot_block_convergence_diagram, caekl_block_information, caekl_rate, caekl_intercept, caekl_rate_converged, approximate_entropy_rate, approximate_excess_entropy, approximate_information_anatomy, statistical_complexity, bidirectional_statistical_complexity, excess_entropy, predicted_information, bound_information, ephemeral_information, information_anatomy, caekl_causal_information, crypticity, bidirectional_crypticity, causal_irreversibility, stored_information_decomposition, transient_information, oracular_information, gauge_information, predictability_gain, structural_information, thermodynamic_depth, spectral_complexity, markov_order, is_markov, cryptic_order, reset_threshold, synchronizing_word, is_exactly_synchronizable, is_asymptotically_synchronizable, is_definite, reverse_is_finite, reverse_epsilon_machine_is_finite
 
 .. autofunction:: sofic.generators.reversal.reverse_is_finite
 
+.. autofunction:: sofic.generators.reversal.reverse_epsilon_machine_is_finite
+
 .. autoclass:: sofic.generators.block_entropy.BlockEntropyDiagram
    :members: plot, transient_information
 .. autoclass:: sofic.generators.block_entropy.BlockEntropyEstimates

sofic/automata/algorithms.py

@@ -37,10 +37,22 @@ def trim(aut: L) -> L:  # noqa: UP047 - keep Python 3.11 compatibility.
 
 def complete(dfa: DFA, alphabet: frozenset[Any] | None = None) -> DFA:
     """Add a trap state so every state has one outgoing transition per symbol."""
+    return _complete_with_trap(dfa, alphabet)[0]
+
+
+def _complete_with_trap(dfa: DFA, alphabet: frozenset[Any] | None = None) -> tuple[DFA, Hashable | None]:
+    """Complete ``dfa``; also return the trap state if it was newly added.
+
+    An existing ``_TRAP`` state is reused only while it is still a rejecting
+    sink: a complemented DFA keeps its trap but makes it accepting.
+    """
     symbols = alphabet if alphabet is not None else _effective_alphabet(dfa)
     result = dfa.copy()
-    trap = _TRAP
-    if trap not in result.graph.nx:
+    trap: Hashable = _TRAP
+    if trap in result.graph.nx and not _is_rejecting_sink(result, trap):
+        trap = Sentinel("trap")
+    added = trap not in result.graph.nx
+    if added:
         result.graph.add_state(trap)
 
     for state in list(result.states()):
@@ -51,11 +63,18 @@ def complete(dfa: DFA, alphabet: frozenset[Any] | None = None) -> DFA:
                 result.add_transition(state, trap, symbol)
 
     for symbol in symbols:
-        result.add_transition(trap, trap, symbol)
+        if not result.delta(trap, symbol):
+            result.add_transition(trap, trap, symbol)
 
     if symbols:
         result.input_alphabet = frozenset(symbols) | result.input_alphabet
-    return result
+    return result, trap if added else None
+
+
+def _is_rejecting_sink(dfa: DFA, state: Hashable) -> bool:
+    return state not in dfa.accepting_states and all(
+        transition.target == state for transition in dfa.graph.out_transitions(state)
+    )
 
 
 def reverse(aut: NFA | DFA) -> NFA:
@@ -160,13 +179,13 @@ def nerode_partition(
     -- need that distinction.
     """
     symbols = alphabet if alphabet is not None else _effective_alphabet(dfa)
-    work = complete(dfa, symbols)
+    work, trap = _complete_with_trap(dfa, symbols)
     states = sorted(work.states(), key=repr)
     if not states:
         return ()
 
     partition = _moore_refine(work, states, symbols)
-    blocks = (frozenset(block) - {_TRAP} for block in partition)
+    blocks = (frozenset(block) - {trap} for block in partition)
     return tuple(block for block in blocks if block)
 
 

sofic/generators/bidirectional_construction.py

@@ -23,7 +23,7 @@
     sum_probs,
     zeros,
 )
-from sofic.generators.reversal import time_reverse_stochastic
+from sofic.generators.reversal import time_reverse_stochastic, warn_if_reverse_truncated
 from sofic.generators.stationary import (
     stationary_distribution_from_transition,
     stationary_distribution_hmm,
@@ -389,6 +389,7 @@ def _joint_pi_minimum_support(
     *,
     tol: float = 1e-12,
     marginal_tol: float = 1e-6,
+    anatomy_tol: float = 1e-9,
 ) -> dict[tuple[Hashable, Hashable], Any]:
     """Pick the closed undirected component that is the true bidirectional class.
 
@@ -431,10 +432,12 @@ class is the one whose forward/reverse marginals equal the forward/reverse
         matching = [candidate for candidate in candidates if candidate[0] == 0.0]
     else:
         matching = [candidate for candidate in candidates if candidate[0] <= marginal_tol]
-    if matching:
-        best = min(matching, key=lambda candidate: (candidate[1], candidate[2]))
-    else:
-        best = min(candidates, key=lambda candidate: (candidate[0], candidate[1], candidate[2]))
+    pool = matching or [min(candidates, key=lambda candidate: candidate[0])]
+    # Anatomy gaps that agree to round-off are ties; comparing them exactly made
+    # the choice depend on the platform's floating-point kernels.
+    best_gap = min(candidate[1] for candidate in pool)
+    tied = [candidate for candidate in pool if candidate[1] <= best_gap + anatomy_tol]
+    best = min(tied, key=lambda candidate: (candidate[2], sorted(map(repr, candidate[3]))))
     return best[3]
 
 
@@ -539,6 +542,7 @@ def infer_reverse_epsilon_machine(forward: EpsilonMachine) -> EpsilonMachine:
     """
     rev_hmm = time_reverse_stochastic(forward)
     reverse = EpsilonMachine.from_hmm(rev_hmm)
+    warn_if_reverse_truncated(forward)
     return _relabel_collision_free(reverse, forward)
 
 

sofic/generators/epsilon_construction.py

@@ -135,7 +135,8 @@ def _quotient_machine(
             state_map[state] = index
 
     graph = TransitionGraph()
-    labels = sequential_labels(len(partitions))
+    count = len(partitions)
+    labels = sequential_labels(count) if count <= 26 else tuple(range(count))
     for label in labels:
         graph.add_state(label)
     label_for_index = {index: labels[index] for index in range(len(partitions))}

sofic/generators/epsilon_machine.py

@@ -526,20 +526,34 @@ def is_asymptotically_synchronizable(self) -> bool:
         return is_asymptotically_synchronizable_from_graph(graph_from_epsilon_machine(self))
 
     def reverse_is_finite(self) -> bool:
-        """Return whether the reverse ε-machine has finitely many causal states.
+        """Return whether the reverse mixed-state presentation is finite.
 
         Decided in polynomial time by the twins property rather than by
         enumerating beliefs; see
-        :func:`~sofic.generators.reversal.reverse_is_finite`. Use this before
-        :meth:`from_time_reversed` or :meth:`causal_irreversibility`, both of
-        which raise
-        :class:`~sofic.exceptions.MixedStateExplosionError` when it returns
-        ``False``.
+        :func:`~sofic.generators.reversal.reverse_is_finite`. ``True``
+        guarantees that :meth:`from_time_reversed` and
+        :meth:`causal_irreversibility` succeed. ``False`` means infinitely many
+        reverse beliefs, which may still converge to a finite reverse
+        ε-machine; those methods raise
+        :class:`~sofic.exceptions.MixedStateExplosionError` only when the
+        recurrent part does not close.
         """
         from sofic.generators.reversal import reverse_is_finite
 
         return reverse_is_finite(self)
 
+    def reverse_epsilon_machine_is_finite(self) -> bool:
+        """Return whether the reverse ε-machine has finitely many recurrent causal states.
+
+        Experimental; see
+        :func:`~sofic.generators.reversal.reverse_epsilon_machine_is_finite`.
+        Unlike :meth:`reverse_is_finite` it ignores transient beliefs, so it is
+        ``True`` for alternating biased coins.
+        """
+        from sofic.generators.reversal import reverse_epsilon_machine_is_finite
+
+        return reverse_epsilon_machine_is_finite(self)
+
     def is_definite(self) -> bool:
         """Return whether the ε-machine is a definite automaton (finite Markov order).
 
@@ -562,24 +576,35 @@ def from_time_reversed(cls, forward: EpsilonMachine) -> EpsilonMachine:
             ε-machine does not imply a finite reverse one -- the "explosive
             irreversibility" of :cite:`Ellison2011` -- and when the reverse is
             infinite there is no presentation to return.
+
+        Warns
+        -----
+        RuntimeWarning
+            If the belief set closed only because numeric beliefs merge within
+            tolerance while
+            :func:`~sofic.generators.reversal.reverse_epsilon_machine_is_finite`
+            says the reverse machine is infinite; the result is then a finite
+            approximation.
         """
         from sofic.exceptions import (
             MixedStateExplosionError,
             StochasticValidationError,
             UnifilarityError,
         )
-        from sofic.generators.reversal import time_reverse_stochastic
+        from sofic.generators.reversal import time_reverse_stochastic, warn_if_reverse_truncated
 
         rev_hmm = time_reverse_stochastic(forward)
         try:
-            return cls.from_hmm(rev_hmm)
+            reverse = cls.from_hmm(rev_hmm)
         except MixedStateExplosionError:
             # Row-normalizing would return a non-unifilar machine whose state
             # entropy coincides with the forward C_mu, reporting Delta C_mu = 0
             # for a process whose reverse machine is infinite.
             raise
         except (StochasticValidationError, UnifilarityError):
             return _row_normalized_presentation(rev_hmm)
+        warn_if_reverse_truncated(forward)
+        return reverse
 
 
 def _row_normalized_presentation(hmm: MealyHMM) -> EpsilonMachine: