#!/usr/bin/env python3
"""Exact educational GPS/WFQ and deterministic service-contract replay.
No real network, variable weights, packet loss, or protocol certification.
The finite-array checker certifies integer timestamps only, through its horizon.
"""
from fractions import Fraction as Q
from heapq import heappush, heappop
from collections import deque
from random import Random
import json


def require(ok, why):
    if not ok:
        raise ValueError(why)


def rational(x):
    require(type(x) in (int, Q), 'exact int or Fraction required')
    return Q(x)


def normalize(packets, weights, capacity, max_packet):
    c, limit = rational(capacity), rational(max_packet)
    require(c > 0 and limit > 0, 'positive capacity and packet bound')
    require(all(type(i) is str for i in weights), 'string flow identities')
    w = {i: rational(v) for i, v in weights.items()}
    require(all(v > 0 for v in w.values()), 'positive weights')
    seen, rows = set(), []
    for serial, row in enumerate(packets):
        name, flow, at, length = row
        require(type(name) is str and name not in seen, 'unique string packet identity')
        require(type(flow) is str and flow in w, 'known flow')
        at, length = rational(at), rational(length)
        require(at >= 0 and 0 < length <= limit, 'time or packet length outside contract')
        seen.add(name)
        rows.append((at, serial, flow, length, name))
    rows.sort()  # At one time, the input serial preserves per-flow arrival order.
    return rows, w, c, limit


def schedule(packets, weights, capacity, max_packet):
    rows, w, c, limit = normalize(packets, weights, capacity, max_packet)
    t, v, active = Q(0), Q(0), Q(0)
    counts = {i: 0 for i in w}
    tail = {i: Q(0) for i in w}
    heap, events, tags, gps = [], [], {}, {}

    def advance(stop=None):
        nonlocal t, v, active
        while heap:
            finish, serial, flow, name = heap[0]
            due = t + (finish - v) * active / c
            if stop is not None and due > stop:
                break
            t, v = due, finish
            heappop(heap)
            counts[flow] -= 1
            if counts[flow] == 0:
                active -= w[flow]
            gps[name] = t
            events.append({'kind': 'GPS_END', 'packet': name, 'at': t,
                           'virtual': v, 'active_weight_after': active})
        if stop is not None:
            if heap:
                v += (stop - t) * c / active
            t = stop

    for at, serial, flow, length, name in rows:
        advance(at)
        finish = max(tail[flow], v) + length / w[flow]
        tail[flow] = finish
        tags[name] = finish
        if counts[flow] == 0:
            active += w[flow]
        counts[flow] += 1
        heappush(heap, (finish, serial, flow, name))
        events.append({'kind': 'ARRIVE', 'packet': name, 'at': at,
                       'virtual': v, 'finish_tag': finish,
                       'active_weight_after': active})
    advance()

    pending, k, now, real, runs = [], 0, Q(0), {}, []
    while k < len(rows) or pending:
        if not pending:
            now = max(now, rows[k][0])
        # Include every arrival at the dispatch timestamp, not just the first.
        while k < len(rows) and rows[k][0] <= now:
            at, serial, flow, length, name = rows[k]
            heappush(pending, (tags[name], serial, length, name))
            k += 1
        finish, serial, length, name = heappop(pending)
        start = now
        now += length / c
        real[name] = now
        runs.append({'packet': name, 'start': start, 'end': now})
    require(all(real[p] <= gps[p] + limit / c for p in real), 'one-sided GPS finish bound')
    return {'tags': tags, 'gps_finish': gps, 'wfq_finish': real,
            'virtual_events': events, 'physical_runs': runs}


def direct_fluid(packets, weights, capacity, max_packet):
    """Slow test oracle: actual remaining bytes, not virtual finish tags."""
    rows, w, c, _ = normalize(packets, weights, capacity, max_packet)
    q = {i: deque() for i in w}
    at, k, result = Q(0), 0, {}
    while k < len(rows) or any(q.values()):
        busy = [i for i in w if q[i]]
        nxt = rows[k][0] if k < len(rows) else None
        if busy:
            total = sum(w[i] for i in busy)
            end = min(at + q[i][0][1] * total / (c * w[i]) for i in busy)
            stop = end if nxt is None else min(end, nxt)
            for i in busy:
                q[i][0][1] -= (stop - at) * c * w[i] / total
            at = stop
            for i in busy:
                if q[i][0][1] == 0:
                    name, _ = q[i].popleft()
                    result[name] = at
        else:
            at = nxt
        while k < len(rows) and rows[k][0] == at:
            _, _, flow, length, name = rows[k]
            q[flow].append([name, length])
            k += 1
    return result


def guaranteed_finishes(packets, weights, capacity, max_packet):
    rows, w, c, _ = normalize(packets, weights, capacity, max_packet)
    total = sum(w.values(), Q(0))
    clocks, out = {i: Q(0) for i in w}, {}
    for at, _, flow, length, name in rows:
        rate = c * w[flow] / total
        clocks[flow] = max(clocks[flow], at) + length / rate
        out[name] = clocks[flow]
    return out


def parameters(b, rho, rate, latency):
    b, rho, rate, latency = map(rational, (b, rho, rate, latency))
    require(b >= 0 and rho >= 0 and rate > 0 and latency >= 0, 'invalid curve parameters')
    return b, rho, rate, latency


def bounds(b, rho, rate, latency):
    b, rho, rate, latency = parameters(b, rho, rate, latency)
    if rho > rate:
        return {'status': 'NO_FINITE_UNIFORM_BOUND'}
    return {'status': 'BOUNDED', 'backlog': b + rho * latency,
            'virtual_delay': latency + b / rate, 'output_burst': b + rho * latency}


def beta(rate, latency, t):
    return rate * max(Q(0), t - latency)


def saturated_output(b, rho, rate, latency, t):
    """A(0)=0, A(t)=b+rho*t for t>0; D=A tensor beta exactly."""
    return min(rate * max(Q(0), t - latency),
               b + rho * max(Q(0), t - latency))


def tandem_output(b, rho, r1, t1, r2, t2, t):
    """Exact minimum of continuous piecewise-affine D1(s)+beta2(t-s).
    Check endpoints, D1 slope changes, and the reflected beta2 breakpoint.
    """
    b, rho, r1, t1 = parameters(b, rho, r1, t1)
    _, _, r2, t2 = parameters(b, rho, r2, t2)
    t = rational(t)
    require(t >= 0, 'nonnegative query time')
    cuts = {Q(0), t, t1, t - t2}
    if r1 > rho:
        cuts.add(t1 + b / (r1 - rho))
    cuts = [s for s in cuts if 0 <= s <= t]
    candidates = [(saturated_output(b, rho, r1, t1, s) + beta(r2, t2, t-s), s)
                  for s in cuts]
    value, split = min(candidates)
    return value, split


def finite_contract(arrivals, departures, service, envelope):
    """Only discrete times 0..N; no interpolation or unseen-future claim."""
    a, d, b, alpha = [list(map(rational, x)) for x in
                       (arrivals, departures, service, envelope)]
    size = len(a)
    require(size > 0 and all(len(x) == size for x in (d, b, alpha)), 'matching nonempty arrays')
    require(a[0] == d[0] == b[0] == alpha[0] == 0, 'zero initial state')
    require(all(x[t] >= 0 and (t == 0 or x[t] >= x[t-1])
                for x in (a, d, b, alpha) for t in range(size)), 'nonnegative monotone arrays')
    for t in range(size):
        if d[t] > a[t]:
            return {'status': 'CAUSALITY_FAIL', 'time': t}
        for s in range(t+1):
            if a[t]-a[s] > alpha[t-s]:
                return {'status': 'ARRIVAL_FAIL', 'start': s, 'end': t,
                        'actual': a[t]-a[s], 'limit': alpha[t-s]}
        value, split = min((a[s]+b[t-s], s) for s in range(t+1))
        if d[t] < value:
            return {'status': 'SERVICE_FAIL', 'time': t, 'minimum_split': split,
                    'required': value, 'actual': d[t]}
    return {'status': 'PASS_FINITE_INTEGER_DOMAIN', 'horizon': size-1,
            'backlog': [a[t]-d[t] for t in range(size)]}


def finite_delay(arrivals, departures, t):
    require(type(t) is int and 0 <= t < len(arrivals), 'integer query in horizon')
    require(len(arrivals) == len(departures), 'matching arrays')
    for end in range(t, len(departures)):
        if departures[end] >= arrivals[t]:
            return {'status': 'OBSERVED', 'completion': end, 'delay': end-t}
    return {'status': 'INCOMPLETE', 'through': len(departures)-1}


def main():
    packets = [('A1','A',0,6),('B1','B',0,6),('A2','A',1,2),
               ('C1','C',2,3),('A3','A',4,4),('B2','B',Q(21,5),2)]
    weights = {'A':2,'B':1,'C':1}
    principal = schedule(packets, weights, 6, 6)
    require(principal['tags'] == dict(zip(['A1','B1','A2','C1','A3','B2'],
                 map(Q,[3,6,4,7,9,Q(48,5)]))), 'main tags')
    require(principal['gps_finish'] == direct_fluid(packets,weights,6,6), 'main fluid')
    long = [('A','A',0,12),('B','B',Q(1,10),1)]
    late = schedule(long,{'A':1,'B':1},1,12)
    simultaneous = schedule([('A','A',0,12),('B','B',0,1)],{'A':1,'B':1},1,12)
    require(late['gps_finish']['B']==Q(21,10) and late['wfq_finish']['B']==13,
            'nonpreemptive boundary')
    require(simultaneous['physical_runs'][0]['packet']=='B', 'batch timestamp')
    table = []
    for t in map(Q,[0,1,2,3,4,6,9,10]):
        value,split=tandem_output(12,2,6,1,4,2,t)
        require(value==saturated_output(Q(12),Q(2),Q(4),Q(3),t), 'main convolution')
        arrived=Q(0) if t==0 else 12+2*t
        mid=saturated_output(Q(12),Q(2),Q(6),Q(1),t)
        table.append({'time':t,'input':arrived,'middle':mid,'output':value,
                      'split':split,'total_backlog':arrived-value,
                      'queue1':arrived-mid,'queue2':mid-value})
    arrivals=[Q(0)]+[Q(12+2*t) for t in range(1,11)]
    service=[beta(Q(4),Q(3),Q(t)) for t in range(11)]
    dep=[saturated_output(Q(12),Q(2),Q(4),Q(3),Q(t)) for t in range(11)]
    env=[Q(0)]+[Q(12+2*t) for t in range(1,11)]
    discrete=finite_contract(arrivals,dep,service,env)
    require(discrete['status']=='PASS_FINITE_INTEGER_DOMAIN','finite contract')
    broken=dep[:];broken[4]=Q(3)
    fail=finite_contract(arrivals,broken,service,env)
    require(fail['status']=='SERVICE_FAIL' and fail['time']==4,'counterexample witness')
    unfinished=finite_delay(arrivals[:5],dep[:5],3)
    require(unfinished['status']=='INCOMPLETE','unknown future')
    rng=Random(1809);tested=0;queries=0
    for _ in range(700):
        f=rng.randrange(1,6);w={str(i):rng.randrange(1,6) for i in range(f)}
        rows=[(str(j),str(rng.randrange(f)),Q(rng.randrange(30),4),rng.randrange(1,13))
              for j in range(rng.randrange(0,30))]
        c=Q(rng.randrange(1,15),3);out=schedule(rows,w,c,12)
        require(out['gps_finish']==direct_fluid(rows,w,c,12),'random literal fluid')
        guarantee=guaranteed_finishes(rows,w,c,12)
        require(all(out['gps_finish'][p]<=guarantee[p] for p in guarantee),'reserved rate')
        tested+=len(rows)
    for _ in range(500):
        b=Q(rng.randrange(20));rho=Q(rng.randrange(7),2)
        r1=Q(rng.randrange(1,20),2);r2=Q(rng.randrange(1,20),2)
        t1=Q(rng.randrange(10),2);t2=Q(rng.randrange(10),2)
        for t in [Q(rng.randrange(100),3) for _ in range(6)]:
            got,_=tandem_output(b,rho,r1,t1,r2,t2,t)
            expected=saturated_output(b,rho,min(r1,r2),t1+t2,t)
            require(got==expected,'tandem breakpoint minimum');queries+=1
    return {'status':'PASS','wfq':principal,'late_short_packet':late,
            'simultaneous_arrival':simultaneous,'flow_A_delay_bound':Q(6,3)+Q(6,6),
            'tandem':table,'end_to_end':bounds(12,2,4,3),
            'separate_delay_sum':Q(3)+Q(11,2),'overload':bounds(12,5,4,3),
            'finite_trace':discrete,'broken_service':fail,'unfinished':unfinished,
            'self_checks':{'random_schedules':700,'packets':tested,'tandem_queries':queries}}


if __name__=='__main__':
    print(json.dumps(main(),ensure_ascii=False,indent=2,
                     default=lambda x:str(x) if isinstance(x,Q) else x))