#!/usr/bin/env python3
"""Finite, exact models for sporadic deadlines, EDF demand, FP RTA and mutex PIP.
Only standard library. Explicit checks execute with or without -O. JSON goes
only to stdout. Bounds assume the page's single-CPU model, not a real machine.
"""
import sys
sys.dont_write_bytecode=True
from dataclasses import dataclass
from fractions import Fraction
from functools import lru_cache
from heapq import heappush,heappop
from itertools import product,combinations
from math import lcm
from random import Random
import json

def require(ok,why):
    if not ok:raise ValueError(why)
def check(ok,why):
    if not ok:raise AssertionError(why)
@dataclass(frozen=True)
class Task:
    name:str
    C:int
    D:int
    T:int
@dataclass(frozen=True)
class Job:
    task:str
    number:int
    r:int
    c:int
    d:int
    @property
    def id(self):return f'{self.task}:{self.number}'

def validate_tasks(tasks):
    require(len({t.name for t in tasks})==len(tasks),'distinct task names')
    for t in tasks:
        require(isinstance(t.name,str) and bool(t.name),'nonempty string name')
        require(all(type(x) is int and x>0 for x in (t.C,t.D,t.T)),'positive integer C/D/T')
        require(t.D<=t.T,'model unsupported: D>T')

def periodic_jobs(tasks,horizon):
    validate_tasks(tasks);require(type(horizon) is int and horizon>=0,'horizon')
    return [Job(t.name,k,r,t.C,r+t.D) for t in tasks for k,r in enumerate(range(0,horizon,t.T))]

def validate_jobs(tasks,jobs):
    validate_tasks(tasks);table={t.name:t for t in tasks};last={}
    require(len({j.id for j in jobs})==len(jobs),'distinct job identities')
    for j in sorted(jobs,key=lambda j:(j.task,j.r,j.number)):
        require(j.task in table,'known task');t=table[j.task]
        require(all(type(x) is int for x in (j.r,j.c,j.d,j.number)) and j.r>=0 and j.number>=0,'job integers')
        require(0<j.c<=t.C and j.d==j.r+t.D,'job C/D contract')
        require(j.task not in last or j.r-last[j.task]>=t.T,'minimum separation')
        last[j.task]=j.r

def schedule(tasks,jobs,policy='EDF'):
    """O(1+n+J log(1+J)) including task input, event queues and trace.
    Continues after a deadline miss, recording the first miss for each job.
    No all-job invariant scan occurs inside the event loop.
    """
    validate_jobs(tasks,jobs);require(policy in ('EDF','FP'),'policy')
    rank={t.name:i for i,t in enumerate(tasks)}
    events=sorted(jobs,key=lambda j:(j.r,j.task,j.number))
    ready=[];deadlines=[];left={j.id:j.c for j in jobs};done={};miss=[];segments=[];idx=0;t=0
    byid={j.id:j for j in jobs}
    def put(j):heappush(ready,((j.d if policy=='EDF' else rank[j.task],j.task,j.number),j.id))
    def segment(start,end,who):
        if start==end:return
        if segments and segments[-1]['job']==who and segments[-1]['end']==start:segments[-1]['end']=end
        else:segments.append(dict(start=start,end=end,job=who))
    while idx<len(events) or ready or deadlines:
        # Completed work was accounted for on arrival at this event time.
        while deadlines and deadlines[0][0]<=t:
            d,key=heappop(deadlines)
            if key not in done:miss.append(dict(job=key,deadline=d,remaining=left[key]))
        while idx<len(events) and events[idx].r==t:
            j=events[idx];put(j);heappush(deadlines,(j.d,j.id));idx+=1
        if not ready:
            times=([events[idx].r] if idx<len(events) else [])+([deadlines[0][0]] if deadlines else [])
            if not times:break
            nxt=min(times);segment(t,nxt,None);t=nxt;continue
        _,key=heappop(ready);j=byid[key]
        nxt=t+left[key]
        if idx<len(events):nxt=min(nxt,events[idx].r)
        if deadlines:nxt=min(nxt,deadlines[0][0])
        require(nxt>t,'positive event advance')
        segment(t,nxt,key);left[key]-=nxt-t;t=nxt
        if left[key]==0:done[key]=t
        else:put(j)
    return dict(policy=policy,segments=segments,completion=done,misses=miss)

def verify_trace(jobs,result):
    """Linear pass over sorted service certificate; independent of policy choice."""
    js={j.id:j for j in jobs};service={k:0 for k in js};last_end={};end=0
    for s in result['segments']:
        check(s['start']==end and s['end']>s['start'],'contiguous exclusive CPU segments');end=s['end']
        key=s['job']
        if key is not None:
            check(key in js and s['start']>=js[key].r,'no early service')
            service[key]+=s['end']-s['start'];last_end[key]=s['end']
    check(all(service[k]==j.c and last_end[k]==result['completion'][k] for k,j in js.items()),'exact service and completion')
    expected={k for k,j in js.items() if result['completion'][k]>j.d}
    check({x['job'] for x in result['misses']}==expected,'miss equals late completion')

def demand(tasks,t):return [max(0,(t-x.D)//x.T+1) for x in tasks]
def edf_test(tasks,budget=200000):
    validate_tasks(tasks);require(type(budget) is int and budget>=0,'nonnegative deadline enumeration budget')
    if not tasks:return dict(status='FEASIBLE',H=1,U='0',rows=[])
    H=lcm(*(x.T for x in tasks));U=sum((Fraction(x.C,x.T) for x in tasks),Fraction())
    # A certificate found from H avoids enumerating the potentially huge horizon.
    if U>1:
        counts=demand(tasks,H);return dict(status='INFEASIBLE',H=H,U=str(U),witness=dict(t=H,counts=counts,demand=sum(c*x.C for c,x in zip(counts,tasks))))
    Q=sum(H//x.T for x in tasks)
    if Q+1>budget:return dict(status='UNKNOWN',H=H,U=str(U),candidate_bound=Q+1,budget=budget)
    points=sorted({H}|{x.D+k*x.T for x in tasks for k in range(H//x.T)})
    rows=[]
    for t in points:
        counts=demand(tasks,t);d=sum(c*x.C for c,x in zip(counts,tasks));row=dict(t=t,counts=counts,demand=d);rows.append(row)
        if d>t:return dict(status='INFEASIBLE',H=H,U=str(U),rows=rows,witness=row)
    return dict(status='FEASIBLE',H=H,U=str(U),rows=rows)

def response_times(tasks):
    validate_tasks(tasks);results=[]
    for i,x in enumerate(tasks):
        w=x.C;seq=[w];counts=[]
        while w<=x.D:
            num=[(w+y.T-1)//y.T for y in tasks[:i]]
            q=x.C+sum(c*y.C for c,y in zip(num,tasks[:i]));counts.append(num);seq.append(q)
            if q==w:break
            w=q
        ok=seq[-1]<=x.D
        results.append(dict(task=x.name,status='PASS' if ok else 'FAIL',iterations=seq,interference_counts=counts,response=seq[-1] if ok else None))
        if not ok:return dict(status='FAIL',tasks=results,failed_task=x.name)
    return dict(status='PASS',tasks=results)

class Inheritance:
    """Current-graph priority donation. State manager, not an OS implementation.
    Public operations include complete snapshots for review, O(n + locks) extra.
    """
    def __init__(self,priorities,locks,enabled=True):
        require(all(type(x) is int and x>0 for x in priorities.values()),'positive priorities')
        require(len(set(priorities.values()))==len(priorities),'distinct base priorities')
        self.base=dict(priorities);self.owner={m:None for m in locks};self.pending={p:None for p in priorities}
        self.held={p:set() for p in priorities};self.done=set();self.enabled=enabled;self.effective=dict(priorities)
    def recalc(self):
        edges=[(p,self.owner[m]) for p,m in self.pending.items() if m is not None]
        self.effective=dict(self.base)
        if self.enabled:
            changed=False
            for _ in range(len(self.base)):
                changed=False
                for u,v in edges:
                    if self.effective[v]>self.effective[u]:self.effective[v]=self.effective[u];changed=True
                if not changed:break
            check(not changed,'finite donation closure')
    def ready(self,p):return p in self.base and p not in self.done and self.pending[p] is None
    def snapshot(self):
        return dict(owner=dict(self.owner),pending=dict(self.pending),effective=dict(self.effective),done=[p for p in self.base if p in self.done])
    def acquire(self,p,m):
        require(self.ready(p) and m in self.owner,'ready known requester/lock')
        if self.owner[m] is None:self.owner[m]=p;self.held[p].add(m)
        else:self.pending[p]=m # Recursive request intentionally records self-deadlock.
        self.recalc();return self.snapshot()
    def release(self,p,m):
        require(self.ready(p) and self.owner.get(m)==p,'ready owner release')
        waiters=[u for u,x in self.pending.items() if x==m]
        target=min(waiters,key=lambda u:(self.effective[u],u)) if waiters else None
        self.held[p].remove(m);self.owner[m]=target
        if target is not None:self.held[target].add(m);self.pending[target]=None
        self.recalc();return self.snapshot()
    def cancel(self,p):
        require(p in self.pending and self.pending[p] is not None,'pending request to cancel')
        self.pending[p]=None;self.recalc();return self.snapshot()
    def finish(self,p):
        require(self.ready(p) and not self.held[p],'finish without held or pending')
        self.done.add(p);self.recalc();return self.snapshot()
    def select(self,candidates):
        eligible=[p for p in candidates if self.ready(p)]
        return min(eligible,key=lambda p:(self.effective[p],p)) if eligible else None

def inversion_trace(enabled):
    p=Inheritance({'H':1,'M':2,'L':3},['m'],enabled)
    p.acquire('L','m');remaining={'L':4,'H':1,'M':5};released={'L'};out=[];finish={};events=[]
    for t in range(10):
        if t==1:released.add('H');events.append(dict(t=t,action='H acquire m',state=p.acquire('H','m')))
        if t==2:released.add('M')
        who=p.select(released);check(who is not None,'inversion example work available')
        out.append(who);remaining[who]-=1
        if remaining[who]==0:
            if p.owner['m']==who:events.append(dict(t=t+1,action=f'{who} release m',state=p.release(who,'m')))
            p.finish(who);released.remove(who);finish[who]=t+1
    return dict(inheritance=enabled,ticks=out,completion=finish,lock_events=events)

# Independent self-checks below are intentionally slower than public algorithms.
def slot_feasible(jobs):
    """Finite exact schedule existence by memoized alternatives, no EDF choices."""
    if not jobs:return True
    stop=max(j.d for j in jobs)
    @lru_cache(None)
    def go(t,remaining):
        if any(x>0 and j.d<=t for x,j in zip(remaining,jobs)):return False
        if not any(remaining):return True
        if t>=stop:return False
        choices=[i for i,(x,j) in enumerate(zip(remaining,jobs)) if x and j.r<=t<j.d]
        # Unit integer windows and preemption admit an integer-slot schedule.
        for i in choices:
            q=list(remaining);q[i]-=1
            if go(t+1,tuple(q)):return True
        return go(t+1,remaining) if not choices else False
    return go(0,tuple(j.c for j in jobs))

def graph_priority_oracle(p):
    expected={}
    for target in p.base:
        reaching=[]
        for source in p.base:
            current=source;seen=set()
            while current not in seen:
                if current==target:reaching.append(p.base[source]);break
                seen.add(current);m=p.pending[current]
                if m is None:break
                current=p.owner[m]
        expected[target]=min(reaching)
    check(p.effective==expected,'independent reachability donor set')
    for m,owner in p.owner.items():
        check((owner is None)==all(m not in h for h in p.held.values()),'free lock iff no holder')
        if owner is not None:check(m in p.held[owner] and sum(m in h for h in p.held.values())==1,'one owner')
    for u,m in p.pending.items():
        if m is not None:check(p.owner[m] is not None and u not in p.done,'pending has current owner')

MAIN=[Task('A',1,3,4),Task('B',2,5,5),Task('C',2,7,10)]
def main():
    rng=Random(9102026);jobs=periodic_jobs(MAIN,20)
    edf=schedule(MAIN,jobs);fp=schedule(MAIN,jobs,'FP');verify_trace(jobs,edf);verify_trace(jobs,fp)
    test=edf_test(MAIN);rta=response_times(MAIN)
    check(test['status']=='FEASIBLE' and [x['demand'] for x in test['rows']]==[1,3,6,8,9,12,14,15,17],'main demand table')
    check(edf['completion']['C:0']==6 and fp['completion']['C:0']==8,'same input EDF/FP split')
    check(rta['tasks'][-1]['iterations']==[2,5,6,8] and rta['status']=='FAIL','RTA stop at deadline')
    relaxed=[*MAIN[:2],Task('C',2,9,10)];check(response_times(relaxed)['tasks'][-1]['iterations']==[2,5,6,8,8],'relaxed deadline fixed point')
    impossible=[Task('X',2,2,10),Task('Y',2,2,10)];bad=edf_test(impossible)
    check(bad['witness']['t']==2 and bad['witness']['demand']==4 and bad['U']=='2/5','low utilization impossible window')
    unknown=edf_test([Task('X',1,2,101),Task('Y',1,3,103)],10);check(unknown['status']=='UNKNOWN','budget is not feasibility')
    same=[Task('A',2,5,5),Task('B',4,7,7)];check(edf_test(same)['status']=='FEASIBLE' and response_times(same)['status']=='FAIL','implicit EDF vs RM')
    off=inversion_trace(False);on=inversion_trace(True);check(off['completion']['H']==10 and on['completion']['H']==5,'inversion timeline')
    # Exact EDF finite-job oracle, including sporadic gaps and shorter actual work.
    finite_cases=0
    for _ in range(3500):
        ts=[Task(chr(65+i),rng.randrange(1,4),rng.randrange(1,6),6) for i in range(rng.randrange(1,4))]
        js=[]
        for x in ts:
            r=rng.randrange(4)
            for k in range(rng.randrange(1,3)):
                js.append(Job(x.name,k,r,rng.randrange(1,x.C+1),r+x.D));r+=x.T+rng.randrange(3)
        z=schedule(ts,js);verify_trace(js,z);check((not z['misses'])==slot_feasible(js),'EDF versus complete slot search');finite_cases+=1
    # Every two-task constrained model with T<=5, C<=T+1 (including C>D).
    shapes=[(c,d,t) for t in range(1,6) for d in range(1,t+1) for c in range(1,t+2)]
    exact_sets=fp_checks=demand_intervals=0
    for x,y in product(shapes,repeat=2):
        ts=[Task('A',*x),Task('B',*y)];H=lcm(x[2],y[2]);js=periodic_jobs(ts,H);z=schedule(ts,js);verify_trace(js,z)
        dec=edf_test(ts);check((dec['status']=='FEASIBLE')==(not z['misses']),'demand versus full synchronous horizon')
        for t in range(H+1):
            literal=sum(j.c for j in js if j.d<=t)
            check(literal==sum(k*q.C for k,q in zip(demand(ts,t),ts)),'literal deadline list versus dbf');demand_intervals+=1
        rr=response_times(ts);fixed=schedule(ts,js,'FP');verify_trace(js,fixed)
        check((rr['status']=='PASS')==(not fixed['misses']),'RTA versus complete fixed-priority horizon')
        if rr['status']=='PASS':
            for row in rr['tasks']:
                worst=max(fixed['completion'][j.id]-j.r for j in js if j.task==row['task'])
                check(worst==row['response'],'synchronous first job realizes worst response')
        fp_checks+=1;exact_sets+=1
    # State regression: chain, partial unlock, cancellation, deadlock closure.
    p=Inheritance({'H':1,'M':2,'L':4,'Q':3},['a','b']);p.acquire('L','a');p.acquire('M','b');p.acquire('M','a');chain=p.acquire('H','b');graph_priority_oracle(p)
    check(chain['effective']['L']==chain['effective']['M']==1,'transitive donation')
    cancelled=p.cancel('H');graph_priority_oracle(p);check(cancelled['effective']['L']==cancelled['effective']['M']==2,'cancel removes only one donor')
    p=Inheritance({'H':1,'M':2,'L':4},['a','b']);p.acquire('L','a');p.acquire('L','b');p.acquire('H','a');p.acquire('M','b');partial=p.release('L','a');graph_priority_oracle(p);check(partial['effective']['L']==2,'one unlock retains other donation')
    p=Inheritance({'X':1,'Y':2},['a','b']);p.acquire('X','a');p.acquire('Y','b');p.acquire('X','b');deadlock=p.acquire('Y','a');graph_priority_oracle(p);check(p.select(p.base) is None,'priority closure cannot break deadlock')
    p=Inheritance({'H':1,'M':2,'L':4},['a']);p.acquire('L','a');p.acquire('H','a');p.acquire('M','a');handoff=p.release('L','a');graph_priority_oracle(p)
    check(handoff['owner']['a']=='H' and handoff['pending']['M']=='a' and handoff['effective']['L']==4,'other waiter resolves new owner after handoff')
    p.release('H','a');graph_priority_oracle(p);check(p.owner['a']=='M' and p.pending['M'] is None,'second handoff')
    p=Inheritance({},[]);p.recalc();check(p.snapshot()['effective']=={},'empty graph closure')
    # Release exactly at the response endpoint does not interfere with completion.
    boundary=[Task('A',1,2,2),Task('B',1,2,2)]
    check(response_times(boundary)['tasks'][1]['iterations']==[1,2,2],'ceil endpoint w=kT')
    check(not schedule(boundary,periodic_jobs(boundary,6),'FP')['misses'],'complete before equal-time arrival')
    operations=0
    for _ in range(1000):
        p=Inheritance({f'T{i}':i+1 for i in range(5)},[f'L{i}' for i in range(4)])
        for step in range(60):
            choices=[]
            for u in p.base:
                if p.pending[u] is not None:choices.append(('cancel',u,None))
                elif u not in p.done:
                    choices.extend(('acquire',u,m) for m in p.owner)
                    choices.extend(('release',u,m) for m in p.owner if m in p.held[u])
            act,u,m=rng.choice(choices)
            if act=='cancel':p.cancel(u)
            elif act=='acquire':p.acquire(u,m)
            else:p.release(u,m)
            graph_priority_oracle(p);operations+=1
    # Minimal API boundaries and completion-before-release convention.
    edge=[Task('X',1,1,1)];z=schedule(edge,periodic_jobs(edge,3));check(not z['misses'] and z['completion']=={'X:0':1,'X:1':2,'X:2':3},'equality deadline boundaries')
    invalid=[lambda:response_times([Task('X',1,3,2)]),lambda:edf_test([Task('X',0,1,1)]),lambda:schedule(edge,[Job('X',0,0,1,1),Job('X',1,0,1,1)])]
    for f in invalid:
        try:f()
        except ValueError:pass
        else:raise AssertionError('bad interface accepted')
    result=dict(status='PASS',checks=dict(finite_job_DFS_cases=finite_cases,two_task_models=exact_sets,literal_demand_intervals=demand_intervals,fixed_priority_horizon_cases=fp_checks,priority_graph_actions=operations),examples=dict(tasks=[vars(t) for t in MAIN],jobs=[vars(j) for j in jobs],EDF=edf,fixed_priority=fp,demand=test,RTA=rta,relaxed_RTA=response_times(relaxed),impossible=bad,budget_unknown=unknown,without_inheritance=off,with_inheritance=on,transitive_chain=chain,cancelled_chain=cancelled,partial_unlock=partial,handoff=handoff,deadlock=deadlock),scope='Exact finite models and own invariants; no WCET measurement, kernel implementation, or physical hard-real-time certification.')
    print(json.dumps(result,ensure_ascii=False,indent=2))
if __name__=='__main__':main()