#!/usr/bin/env python3
"""Finite audit for the live-quotient pumping corollary.

The exhaustive checks corroborate the finite constructions.  The unrestricted
no-resurrection and bounded-quotient arguments are proved in the note.
"""

import itertools
import json
from collections import defaultdict, deque
from pathlib import Path


BASE = (("B", (-1,)),)
ROWS = tuple(itertools.product(("0", "1"), ("missing", "self", 0, 1, 2)))


def follow(graph, node, length):
    for _ in range(length):
        node = -1 if node == -1 else graph[node][1][0]
    return node


def append(graph, row):
    label, address = row
    if address == "missing":
        target = -1
    elif address == "self":
        target = len(graph)
    else:
        target = follow(graph, len(graph) - 1, address)
    return graph + ((label, (target,)),)


def reachable(graph, root=None):
    root = len(graph) - 1 if root is None else root
    todo = [root]
    seen = set()
    while todo:
        node = todo.pop()
        if node == -1 or node in seen:
            continue
        seen.add(node)
        todo.extend(graph[node][1])
    return seen


def minimal_figure(graph):
    """Canonical rooted greatest-bisimulation quotient."""
    live = sorted(reachable(graph))
    classes = {node: graph[node][0] for node in live}
    while True:
        signatures = {
            node: (
                graph[node][0],
                tuple(-1 if target == -1 else classes[target]
                      for target in graph[node][1]),
            )
            for node in live
        }
        palette = {signature: index for index, signature in enumerate(sorted(set(signatures.values()), key=repr))}
        refined = {node: palette[signatures[node]] for node in live}
        stable = all(
            (classes[u] == classes[v]) == (refined[u] == refined[v])
            for u in live for v in live
        )
        classes = refined
        if stable:
            break

    members = defaultdict(list)
    for node, cls in classes.items():
        members[cls].append(node)

    root_class = classes[len(graph) - 1]
    order = []
    names = {root_class: 0}
    queue = deque([root_class])
    while queue:
        cls = queue.popleft()
        order.append(cls)
        representative = members[cls][0]
        for target in graph[representative][1]:
            if target == -1:
                continue
            target_class = classes[target]
            if target_class not in names:
                names[target_class] = len(names)
                queue.append(target_class)

    result = []
    for cls in order:
        representative = members[cls][0]
        label, ports = graph[representative]
        result.append((label, tuple(-1 if target == -1 else names[classes[target]] for target in ports)))
    return tuple(result)


def configuration(machine_state, graph):
    return machine_state, minimal_figure(graph)


def counting_bound(q, g, d, bound):
    return q * sum(
        b * (g + 1) ** b * (b + 1) ** (d * b)
        for b in range(1, bound + 1)
    )


def regular_step(state, graph, letter):
    # Parity of a's in finite control.  The graph deliberately allocates a
    # fresh self-loop on every letter; all earlier nodes immediately become
    # unreachable.
    next_state = state ^ (letter == "a")
    return int(next_state), graph + (("0", (len(graph),)),)


def regular_run(word):
    state, graph = 0, BASE
    configurations = [configuration(state, graph)]
    for letter in word:
        state, graph = regular_step(state, graph, letter)
        configurations.append(configuration(state, graph))
    return state, graph, configurations


def main():
    layers = {BASE}
    graphs = set(layers)
    for _ in range(4):
        layers = {append(graph, row) for graph in layers for row in ROWS}
        graphs.update(layers)

    by_figure = defaultdict(list)
    no_resurrection_checks = 0
    for graph in graphs:
        by_figure[minimal_figure(graph)].append(graph)
        old_live = reachable(graph)
        for row in ROWS:
            extended = append(graph, row)
            resurrected_old = {node for node in reachable(extended) if node < len(graph)}
            assert resurrected_old <= old_live
            no_resurrection_checks += 1

    quotient_extension_checks = 0
    for members in by_figure.values():
        for row in ROWS:
            expected = minimal_figure(append(members[0], row))
            for graph in members[1:]:
                assert minimal_figure(append(graph, row)) == expected
                quotient_extension_checks += 1

    # The explicit formula is an overcount of all rooted labelled partial
    # port graphs.  It must dominate the distinct quotients in every observed
    # size stratum.
    quotient_count_checks = 0
    observed_by_bound = {}
    for bound in range(1, 6):
        observed = sum(1 for figure in by_figure if len(figure) <= bound)
        formula = counting_bound(q=1, g=2, d=1, bound=bound)
        assert observed <= formula
        observed_by_bound[str(bound)] = {"observed": observed, "formula_bound": formula}
        quotient_count_checks += 1

    # Exhaustively find a repeated canonical configuration and pump the loop
    # for the parity language.  Three canonical configurations are reachable:
    # the initial base and the two parity controls over the one-node loop.
    pump_witnesses = 0
    pumped_words = 0
    for length in range(3, 9):
        for letters in itertools.product("ab", repeat=length):
            word = "".join(letters)
            accepted, graph, configs = regular_run(word)
            assert len(graph) == length + 1
            assert len(minimal_figure(graph)) == 1
            pair = next(
                (i, j)
                for j in range(1, 4)
                for i in range(j)
                if configs[i] == configs[j]
            )
            i, j = pair
            x, y, z = word[:i], word[i:j], word[j:]
            assert y
            for repeats in range(5):
                pumped_acceptance, _, _ = regular_run(x + y * repeats + z)
                assert pumped_acceptance == accepted
                pumped_words += 1
            pump_witnesses += 1

    result = {
        "status": "pass",
        "scope": "degree-one legal histories through four appends, two labels, path length at most two",
        "graphs": len(graphs),
        "minimal_figures": len(by_figure),
        "no_resurrection_checks": no_resurrection_checks,
        "quotient_extension_checks": quotient_extension_checks,
        "quotient_count_checks": quotient_count_checks,
        "observed_by_bound": observed_by_bound,
        "regular_example_configuration_classes": 3,
        "regular_example_formula_bound": counting_bound(q=2, g=1, d=1, bound=1),
        "pump_witnesses": pump_witnesses,
        "pumped_words": pumped_words,
        "does_not_verify": [
            "the unrestricted no-resurrection theorem",
            "the unrestricted bounded-quotient regularity criterion",
            "minimality of the explicit counting bound",
            "a pumping theorem for nonregular scaffold languages",
        ],
    }
    output = json.dumps(result, indent=2) + "\n"
    Path(__file__).with_name("live-quotient-checker-output.json").write_text(output)
    print(output, end="")


if __name__ == "__main__":
    main()