#!/usr/bin/env python3
"""Bounded implementation of family 104 deterministic Procedure 4.1.

No source proof is accepted here. Completed labels remain source-conditional.
Separate positional certificates can certify threshold regions through finite
closure and Bellman-Ford checks, independently of the recursion theorem.
"""
import argparse
import json
from fractions import Fraction
from pathlib import Path

MODEL={'arena':'turn_based_deterministic','reward':'signed_integer_edge',
       'objective':'liminf_mean_at_least_zero','opponents':'full_history'}


def parse(data):
    if not isinstance(data,dict) or set(data)!={'model','owners','edges'}:
        raise ValueError('Expected exactly model, owners and edges')
    if data['model']!=MODEL:raise ValueError('Unsupported model declaration')
    owners=data['owners'];edges=data['edges']
    if not isinstance(owners,list) or not 1<=len(owners)<=12 or any(x not in ('max','min') for x in owners):
        raise ValueError('Use 1..12 explicit max/min vertices')
    n=len(owners)
    if not isinstance(edges,list) or not 1<=len(edges)<=96:raise ValueError('Use 1..96 explicit edges')
    out=[[] for _ in owners]
    for k,e in enumerate(edges):
        if not isinstance(e,list) or len(e)!=3 or any(type(v) is not int for v in e):
            raise ValueError('An edge is [tail,head,signed integer weight]; booleans excluded')
        u,v,w=e
        if not 0<=u<n or not 0<=v<n or abs(w).bit_length()>256:raise ValueError('Endpoint/weight outside limits')
        out[u].append(k)
    if any(not a for a in out):raise ValueError('Every vertex needs an outgoing edge')
    return tuple(owners),tuple(tuple(e) for e in edges),tuple(tuple(a) for a in out)


class Exhausted(Exception):pass


class Labeler:
    def __init__(self,data,work_limit=200_000,depth_limit=128):
        self.owners,self.edges,self.out=parse(data);self.n=len(self.owners)
        if type(work_limit) is not int or not 0<=work_limit<=2_000_000:raise ValueError('Work limit must be 0..2000000')
        if type(depth_limit) is not int or not 1<=depth_limit<=128:raise ValueError('Depth limit must be 1..128')
        self.work_limit=work_limit;self.depth_limit=depth_limit
        self.weights=tuple((self.n+1)*e[2]+1 for e in self.edges)
        self.W=max(map(abs,self.weights))
        threshold=64*(self.n+1)*(self.W+1)
        self.D=1<<(threshold-1).bit_length()
        self.stats=dict(work=0,calls=0,nonbase_calls=0,mass_base_calls=0,width_base_calls=0,
                        operator_evaluations=0,edge_scans=0,pivot_updates=0,max_depth=0)

    def charge(self,n):
        if self.stats['work']+n>self.work_limit:raise Exhausted('work_limit')
        self.stats['work']+=n

    def basic(self,A,D):
        z=A
        while True:
            self.charge(len(self.edges)+self.n)
            self.stats['operator_evaluations']+=1;self.stats['edge_scans']+=len(self.edges)
            q=[]
            for i in range(self.n):
                vals=[self.weights[e]+z[self.edges[e][1]] for e in self.out[i]]
                v=(max if self.owners[i]=='max' else min)(vals)
                q.append(min(A[i]+D,max(A[i],v)))
            q=tuple(q)
            if q==z:return z
            z=q

    def label(self,A,D,a,b,depth=0):
        if depth>self.depth_limit:raise Exhausted('depth_limit')
        self.charge(self.n);self.stats['calls']+=1
        self.stats['max_depth']=max(self.stats['max_depth'],depth)
        if all(a[i]*b[i]>1 for i in range(self.n)):
            self.stats['mass_base_calls']+=1
            return tuple(x>1 for x in b)
        if D<4096:
            self.stats['width_base_calls']+=1;z=self.basic(A,D)
            return tuple(2*z[i]>2*A[i]+D for i in range(self.n))
        self.stats['nonbase_calls']+=1
        c=tuple(x+D//2 for x in A);M=D//8;q=D//128;p=D//4096;P=D//32
        k=c
        scaled_b=tuple(x*Fraction(4,3) for x in b)
        while True:
            labels=self.label(tuple(x-q//2 for x in k),q,a,scaled_b,depth+1)
            self.charge(self.n);self.stats['pivot_updates']+=1
            nxt=tuple(k[i] if labels[i] else max(c[i]-M,k[i]-p) for i in range(self.n))
            if nxt==k:break
            k=nxt
        minus=tuple(k[i]<c[i]-P for i in range(self.n))
        scaled_a=tuple(x*Fraction(4,3) for x in a)
        while True:
            labels=self.label(tuple(x-q//2 for x in k),q,scaled_a,b,depth+1)
            self.charge(self.n);self.stats['pivot_updates']+=1
            nxt=tuple(min(c[i]+M,k[i]+p) if labels[i] else k[i] for i in range(self.n))
            if nxt==k:break
            k=nxt
        plus=tuple(k[i]>c[i]+P for i in range(self.n))
        labels=self.label(tuple(x-D//4 for x in k),D//2,a,b,depth+1)
        aa=tuple(a[i]*Fraction(4 if labels[i] else 8,5) for i in range(self.n))
        bb=tuple(b[i]*Fraction(8 if labels[i] else 4,5) for i in range(self.n))
        labels=self.label(A,D,aa,bb,depth+1)
        return tuple(False if minus[i] else True if plus[i] else labels[i] for i in range(self.n))

    def run(self):
        out=dict(algorithm='deterministic_paper_procedure_4_1_bounded_reference',model=MODEL,
                 vertices=self.n,initial_width=str(self.D),transformed_max_weight=str(self.W),
                 limits=dict(work=self.work_limit,depth=self.depth_limit),
                 source_proof_accepted=False,outputs_values_or_strategies=False)
        try:
            a=tuple(Fraction(1,self.n) for _ in range(self.n))
            labels=self.label((0,)*self.n,self.D,a,a)
            out.update(status='complete_labels_source_conditional',winning_vertices=[i for i,v in enumerate(labels) if v])
        except Exhausted as e:out.update(status='unknown',reason=str(e),winning_vertices=None)
        out['counts']=dict(self.stats)
        out['counter_scope']='vertex visits at call/pivot and edge+vertex visits at operator evaluations; excludes bit cost, preprocessing, allocation, parsing and wall time'
        return out


def solve(data,work_limit=200_000,depth_limit=128):return Labeler(data,work_limit,depth_limit).run()


def certify_regions(data,winning,max_edges,min_edges):
    """Check total positional region certificates without executing source recursion.

    For Max, retained original edges have no negative cycle. For Min, negate the
    perturbed weights (n+1)*w+1 and check the same. Closed finite regions and
    cycle decomposition then imply >=0 and <=-1/n against arbitrary histories.
    Strategies outside the relevant region are intentionally not claimed.
    """
    owners,edges,out=parse(data);n=len(owners)
    if not isinstance(winning,list) or any(type(i) is not int or not 0<=i<n for i in winning) or len(set(winning))!=len(winning):
        raise ValueError('Invalid winning list')
    U=set(winning)
    if any(not isinstance(a,dict) for a in (max_edges,min_edges)):raise ValueError('Use edge-index dictionaries keyed by vertex strings')
    results=[]
    for player,region,policy in [('max',U,max_edges),('min',set(range(n))-U,min_edges)]:
        needed={str(i) for i in region if owners[i]==player}
        if set(policy)!=needed:return dict(accepted=False,reason='policy_keys',player=player)
        selected=[]
        for i in sorted(region):
            if owners[i]==player:
                k=policy[str(i)]
                if type(k) is not int or k not in out[i]:return dict(accepted=False,reason='invalid_edge_choice',player=player)
                candidates=[k]
            else:candidates=out[i]
            for k in candidates:
                u,v,w=edges[k]
                if v not in region:return dict(accepted=False,reason='region_not_closed',player=player,edge=k)
                selected.append((u,v,w if player=='max' else -((n+1)*w+1)))
        distances={i:0 for i in region}
        changed=False
        for _ in range(len(region)):
            changed=False
            for u,v,w in selected:
                if distances[v]>distances[u]+w:
                    distances[v]=distances[u]+w;changed=True
            if not changed:break
        if changed:return dict(accepted=False,reason='adverse_cycle',player=player)
        results.append(dict(player=player,vertices=sorted(region),distance_potential={str(i):str(v) for i,v in distances.items()},retained_edges=len(selected)))
    return dict(accepted=True,status='threshold_regions_finitely_certified',winning_vertices=sorted(U),checks=results,
                scope='zero-threshold region strategies only; no exact value-optimality, stochastic, parity, or initial-credit claim')


def main():
    p=argparse.ArgumentParser(description=__doc__);p.add_argument('input',type=Path)
    p.add_argument('--work-limit',type=int,default=200_000);p.add_argument('--depth-limit',type=int,default=128);args=p.parse_args()
    with args.input.open('rb') as f:raw=f.read(2*1024*1024+1)
    if len(raw)>2*1024*1024:raise ValueError('Input exceeds 2 MiB')
    print(json.dumps(solve(json.loads(raw),args.work_limit,args.depth_limit),indent=2))


if __name__=='__main__':main()