"""Model checker for "Work Order Scheduling: Reserving Output at Run Start".

    python checker.py theorems          replay every stepper on the page and check its claim
    python checker.py weld              the "what it buys" table
    python checker.py search SEED N     N random factories from SEED under every rule
        env MULTIKIND=1 (recipes may put out a second kind), MAXOPS (default 7), LIMIT (default 40000)

The model is the one the page states. Components are fungible by kind; source kinds arrive at
assignment; sink kinds leave at resolve; a component departs the moment a waiting operation needs
its kind. Every order of transitions is explored breadth first.

Operation status: 0 planned, 1 waiting, 2 running, 3 holding, 4 done.
"""
from collections import deque
import os
import random
import sys


class Factory:
    def __init__(self, machines, recipes, ops, name=''):
        self.name = name
        self.mnames = list(machines)
        self.cin = [machines[m]['cin'] for m in self.mnames]
        self.cout = [machines[m]['cout'] for m in self.mnames]
        self.mrec = [set(machines[m]['recipes']) for m in self.mnames]
        self.recipes = recipes
        consumed = {k for r in recipes.values() for k in r['in']}
        produced = {k for r in recipes.values() for k in r['out']}
        self.raw = consumed - produced
        self.final = produced - consumed
        self.opname = [o[0] for o in ops]
        self.orec = [o[1] for o in ops]
        self.inkinds = [sorted(recipes[r]['in']) for r in self.orec]
        self.outkinds = [sorted(recipes[r]['out']) for r in self.orec]
        self.nin = [sum(recipes[r]['in'].values()) for r in self.orec]
        self.nout = [sum(recipes[r]['out'].values()) for r in self.orec]
        self.reach = [[i for i in range(len(self.mnames)) if r in self.mrec[i]] for r in self.orec]


class Rules:
    """reserve: 'assign' (current) or 'start' (proposal).
    cover: 'op' (an assigned operation covers its recipe, as the current doc states) or 'units'.
    check_start: the start is a checked event. needed: 'not-started' (page) or 'all'.
    eager: a start that can happen always happens before anything else."""
    def __init__(self, reserve, cover, check_start=False, needed='not-started', eager=False, ledger_only=False,
                 assign_full=False, short_no_lend=False):
        self.reserve, self.cover, self.check_start = reserve, cover, check_start
        self.needed, self.eager, self.ledger_only = needed, eager, ledger_only
        self.assign_full, self.short_no_lend = assign_full, short_no_lend


RULES = {
    'current':              Rules('assign', 'op'),
    'current-units':        Rules('assign', 'units'),
    'proposal':             Rules('start', 'op'),
    'proposal-startcheck':  Rules('start', 'op', check_start=True),
    'proposal-units':       Rules('start', 'units'),
    'amended':              Rules('start', 'units', check_start=True),
    'amended-needed-all':   Rules('start', 'units', check_start=True, needed='all'),
    'amended-assign-full':  Rules('start', 'units', check_start=True, assign_full=True),
    'amended-short-no-lend': Rules('start', 'units', check_start=True, short_no_lend=True),
}


def init_state(F):
    return tuple((0, -1, tuple(0 for _ in F.inkinds[i]), tuple(0 for _ in F.outkinds[i])) for i in range(len(F.orec)))


def setop(S, i, v):
    L = list(S); L[i] = v; return tuple(L)


def free(F, R, S):
    fin, fout = list(F.cin), list(F.cout)
    for i, (st, m, dl, hd) in enumerate(S):
        if st == 1:
            fin[m] -= F.nin[i]
            if R.reserve == 'assign':
                fout[m] -= F.nout[i]
        elif st == 2:
            fout[m] -= F.nout[i]
        elif st == 3:
            fout[m] -= sum(hd)
    return fin, fout


def needed_set(F, R, S):
    n = len(S)

    def pend_out(i):
        st, m, dl, hd = S[i]
        if st == 4: return set()
        if st == 3: return {k for j, k in enumerate(F.outkinds[i]) if hd[j] > 0 and k not in F.final}
        return {k for k in F.outkinds[i] if k not in F.final}

    def need(i):
        st, m, dl, hd = S[i]
        if st not in (0, 1): return set()
        return {k for j, k in enumerate(F.inkinds[i]) if k not in F.raw and F.recipes[F.orec[i]]['in'][k] - dl[j] > 0}

    po = [pend_out(i) for i in range(n)]
    nd = [need(i) for i in range(n)]
    seen = {i for i in range(n) if S[i][0] in (1, 2, 3)}
    dq = deque(seen)
    while dq:
        x = dq.popleft()
        for y in range(n):
            if y in seen or S[y][0] == 4: continue
            if po[x] & nd[y] or po[y] & nd[x]:
                seen.add(y); dq.append(y)
    if R.needed == 'not-started':
        return {F.orec[i] for i in seen if S[i][0] in (0, 1)}
    return {F.orec[i] for i in seen}


def fits(reqs, fin, fout):
    """reqs: per recipe, a list of (machine, in units, out units) options; pick one each."""
    if not reqs:
        return all(x >= 0 for x in fin) and all(x >= 0 for x in fout)
    for (mi, a, b) in reqs[0]:
        if fin[mi] >= a and fout[mi] >= b:
            fin[mi] -= a; fout[mi] -= b
            ok = fits(reqs[1:], fin, fout)
            fin[mi] += a; fout[mi] += b
            if ok:
                return True
    return False


def covered(F, R, S):
    if R.ledger_only:
        return True
    need = needed_set(F, R, S)
    fin, fout = free(F, R, S)
    nm = len(F.mnames)
    size = lambda r, side: sum(F.recipes[r][side].values())
    if R.cover == 'op':
        assigned = {F.orec[i] for i in range(len(S)) if S[i][0] in (1, 2, 3)}
        reqs = [[(mi, size(r, 'in'), size(r, 'out')) for mi in range(nm) if r in F.mrec[mi]] for r in sorted(need - assigned)]
        return fits(reqs, fin, fout)
    lend_in, held, waiting = {}, {}, set()
    for i, (st, m, dl, hd) in enumerate(S):
        r = F.orec[i]
        if st == 1:
            full = all(dl[j] >= F.recipes[r]['in'][k] for j, k in enumerate(F.inkinds[i]))
            if full or not R.short_no_lend:
                lend_in[(r, m)] = lend_in.get((r, m), 0) + F.nin[i]
            waiting.add((r, m))
            if R.reserve == 'assign':
                held[(r, m)] = held.get((r, m), 0) + F.nout[i]
        elif st == 2:
            held[(r, m)] = held.get((r, m), 0) + F.nout[i]
        elif st == 3:
            held[(r, m)] = held.get((r, m), 0) + sum(hd)
    kept = set()
    if R.reserve == 'start':
        # a waiting run keeps one run of its recipe's output where it waits
        for (r, m) in waiting:
            fout[m] -= max(0, size(r, 'out') - held.get((r, m), 0))
            kept.add((r, m))
    reqs = []
    for r in sorted(need):
        opts = []
        for mi in range(nm):
            if r in F.mrec[mi]:
                a = 0 if lend_in.get((r, mi), 0) > 0 else size(r, 'in')
                b = 0 if (r, mi) in kept else max(0, size(r, 'out') - held.get((r, mi), 0))
                opts.append((mi, a, b))
        reqs.append(opts)
    if any(x < 0 for x in fout):
        return False
    return fits(reqs, fin, fout)


def departures(F, S, consumer=None, producer=None):
    """Every way of moving held components into waiting operations that need them, to saturation."""
    pairs = []
    for c, (st, m, dl, hd) in enumerate(S):
        if st != 1 or (consumer is not None and c != consumer): continue
        for j, k in enumerate(F.inkinds[c]):
            if F.recipes[F.orec[c]]['in'][k] - dl[j] <= 0: continue
            for p, (pst, pm, pdl, phd) in enumerate(S):
                if pst != 3 or (producer is not None and p != producer): continue
                for jj, kk in enumerate(F.outkinds[p]):
                    if kk == k and phd[jj] > 0:
                        pairs.append((c, j, p, jj))
    if not pairs:
        return [S]
    out = []
    for (c, j, p, jj) in pairs:
        st, m, dl, hd = S[c]
        dl2 = list(dl); dl2[j] += 1
        S2 = setop(S, c, (st, m, tuple(dl2), hd))
        pst, pm, pdl, phd = S2[p]
        phd2 = list(phd); phd2[jj] -= 1
        S2 = setop(S2, p, (4 if sum(phd2) == 0 else 3, pm, pdl, tuple(phd2)))
        for S3 in departures(F, S2, consumer, producer):
            if S3 not in out:
                out.append(S3)
    return out


def successors(F, R, S):
    fin, fout = free(F, R, S)
    n = len(S)
    starts, others = [], []
    for i, (st, m, dl, hd) in enumerate(S):
        rec = F.recipes[F.orec[i]]
        if st == 0:
            exists = any(k in F.raw for k in F.inkinds[i]) or any(
                S[p][0] == 3 and any(F.outkinds[p][jj] == k and S[p][3][jj] > 0 for jj in range(len(F.outkinds[p])))
                for k in F.inkinds[i] for p in range(n))
            if not exists: continue
            if R.assign_full:
                avail = {}
                for p, (pst, pm, pdl, phd) in enumerate(S):
                    if pst == 3:
                        for jj, kk in enumerate(F.outkinds[p]): avail[kk] = avail.get(kk, 0) + phd[jj]
                if any(k not in F.raw and avail.get(k, 0) < rec['in'][k] for k in F.inkinds[i]): continue
            for mi in F.reach[i]:
                if fin[mi] < F.nin[i]: continue
                if R.reserve == 'assign' and fout[mi] < F.nout[i]: continue
                dl0 = tuple(rec['in'][k] if k in F.raw else 0 for k in F.inkinds[i])
                S1 = setop(S, i, (1, mi, dl0, tuple(0 for _ in F.outkinds[i])))
                for S2 in departures(F, S1, consumer=i):
                    if covered(F, R, S2):
                        others.append((f"assign {F.opname[i]}@{F.mnames[mi]}", S2))
        elif st == 1:
            if all(dl[j] >= rec['in'][k] for j, k in enumerate(F.inkinds[i])):
                if R.reserve == 'start' and fout[m] < F.nout[i]: continue
                S1 = setop(S, i, (2, m, dl, hd))
                if R.check_start and not covered(F, R, S1): continue
                starts.append((f"start {F.opname[i]}", S1))
        elif st == 2:
            hd2 = tuple(0 if k in F.final else rec['out'][k] for k in F.outkinds[i])
            S1 = setop(S, i, (4 if sum(hd2) == 0 else 3, m, dl, hd2))
            for S2 in departures(F, S1, producer=i):
                others.append((f"resolve {F.opname[i]}", S2))
    if R.eager and starts:
        return starts
    return starts + others


def explore(F, R, limit=10 ** 9):
    """('live'|'LOCK'|'limit', states, shortest trace to a lock)."""
    s0 = init_state(F)
    parent = {s0: None}
    dq = deque([s0])
    while dq:
        S = dq.popleft()
        succ = successors(F, R, S)
        if not succ and any(x[0] != 4 for x in S):
            trace, cur = [], S
            while parent[cur] is not None:
                prev, lbl = parent[cur]
                trace.append((lbl, cur)); cur = prev
            return 'LOCK', len(parent), trace[::-1]
        for lbl, S2 in succ:
            if S2 not in parent:
                parent[S2] = (S, lbl); dq.append(S2)
        if len(parent) > limit:
            return 'limit', len(parent), None
    return 'live', len(parent), None


def describe_state(F, R, S):
    fin, fout = free(F, R, S)
    names = ['planned', 'waiting', 'running', 'holding', 'done']
    ops = ', '.join(f"{F.opname[i]} {names[st]}" for i, (st, m, dl, hd) in enumerate(S) if st in (1, 2, 3))
    cap = ' '.join(f"{F.mnames[i]} free in {fin[i]}/{F.cin[i]} out {fout[i]}/{F.cout[i]}" for i in range(len(F.mnames)))
    return f"{cap} | {ops} | needed {sorted(needed_set(F, R, S))}"


# ── The factories and schedules on the page ──

def chains(pairs):
    return [(f"{r}{i}", r) for r, n in pairs for i in range(1, n + 1)]

AB = {'A': {'in': {'ore': 1}, 'out': {'ingot': 1}}, 'B': {'in': {'ingot': 1}, 'out': {'plate': 1}}}

def one_machine(n):
    return Factory({'M': {'cin': 2, 'cout': 2, 'recipes': {'A', 'B'}}}, AB, chains([('A', n), ('B', n)]), f"A->B on M(2,2), {n} plates")

def coal_factory():
    rec = {'A': {'in': {'ore': 1}, 'out': {'ingot': 1}}, 'B': {'in': {'coal': 1, 'ingot': 2}, 'out': {'plate': 1}}}
    return Factory({'M': {'cin': 6, 'cout': 3, 'recipes': {'A', 'B'}}}, rec, chains([('A', 4), ('B', 2)]), 'Theorem 3 factory')

def coal_two_machines():
    rec = {'A': {'in': {'ore': 1}, 'out': {'ingot': 1}}, 'B': {'in': {'coal': 1, 'ingot': 2}, 'out': {'plate': 1}}}
    return Factory({'M': {'cin': 3, 'cout': 2, 'recipes': {'A', 'B'}}, 'N': {'cin': 3, 'cout': 1, 'recipes': {'B'}}},
                   rec, chains([('A', 2), ('B', 1)]), 'Theorem 3, two machines')

def double_ingot():
    rec = {'A': {'in': {'ore': 1}, 'out': {'ingot': 2}}, 'B': {'in': {'ingot': 3}, 'out': {'plate': 1}}}
    return Factory({'M': {'cin': 4, 'cout': 3, 'recipes': {'A', 'B'}}}, rec, chains([('A', 3), ('B', 2)]), 'Theorem 4 factory')

T1 = ['assign A1@M', 'start A1', 'resolve A1', 'assign B1@M', 'start B1', 'assign A2@M', 'start A2', 'resolve A2',
      'assign A3@M', 'assign B2@M', 'start A3', 'resolve A3', 'assign A4@M', 'resolve B1', 'start A4', 'resolve A4', 'assign A5@M']

THEOREMS = [
    ('Theorem 1', one_machine(5), Rules('start', 'op', eager=True), T1, 'lock'),
    ('Theorem 2', one_machine(4), Rules('start', 'op', check_start=True, eager=True),
     ['assign A1@M', 'start A1', 'resolve A1', 'assign B1@M', 'start B1', 'assign A2@M', 'start A2', 'resolve A2',
      'assign A3@M', 'assign A4@M', 'resolve B1'], 'lock'),
    ('Theorem 3', coal_factory(), Rules('assign', 'op', eager=True),
     ['assign A1@M', 'start A1', 'assign B1@M', 'assign B2@M', 'resolve A1'], 'lock'),
    ('Theorem 3, two machines', coal_two_machines(), Rules('assign', 'op', eager=True),
     ['assign A1@M', 'start A1', 'assign B1@M', 'resolve A1'], 'lock'),
    ('Theorem 4', double_ingot(), Rules('start', 'units', eager=True),
     ['assign A1@M', 'start A1', 'resolve A1', 'assign A2@M', 'assign B1@M', 'start A2', 'assign A3@M', 'resolve A2',
      'start A3', 'resolve A3'], 'lock'),
    ('Replay under the amended rule', one_machine(5), Rules('start', 'units', check_start=True),
     T1[:14] + ['!start A4', 'start B2', 'resolve B2', 'assign B3@M', 'start B3', 'resolve B3', 'start A4', 'resolve A4',
                'assign B4@M', 'start B4', 'resolve B4', 'assign A5@M', 'start A5', 'resolve A5', 'assign B5@M',
                'start B5', 'resolve B5'], 'done'),
]


def theorems():
    ok_all = True
    for name, F, R, events, expect in THEOREMS:
        print(f"\n== {name}: {F.name}")
        S, ok = init_state(F), True
        for ev in events:
            succ = successors(F, R, S)
            if ev.startswith('!'):
                allowed = any(l == ev[1:] for l, _ in succ)
                print(f"   {ev[1:]:18s} {'ALLOWED (expected refused)' if allowed else 'refused'}")
                ok &= not allowed
                continue
            nxt = [s for l, s in succ if l == ev]
            if not nxt:
                print(f"   {ev:18s} NOT ALLOWED; allowed: {[l for l, _ in succ]}")
                ok = False; break
            S = nxt[0]
            print(f"   {ev:18s} {describe_state(F, R, S)}")
        left = successors(F, R, S)
        if expect == 'lock':
            ok &= not left and any(x[0] != 4 for x in S)
            print(f"   final state: {'no transition allowed (lock)' if not left else 'allowed: ' + str([l for l, _ in left])}")
        else:
            ok &= all(x[0] == 4 for x in S)
        amended = explore(F, RULES['amended'])[0]
        print(f"   {name}: {'OK' if ok else 'FAILED'} - same factory under the amended rule: {amended}")
        ok_all &= ok
    print('\nall claims hold' if ok_all else '\nSOME CLAIMS FAILED')


def weld():
    rec = {'Press': {'in': {'ore': 1}, 'out': {'plate': 1}},
           'Weld': {'in': {'plate': 2}, 'out': {'frame': 1}},
           'Paint': {'in': {'frame': 1}, 'out': {'painted': 1}}}
    F = Factory({'P': {'cin': 2, 'cout': 2, 'recipes': {'Press'}}, 'W': {'cin': 6, 'cout': 1, 'recipes': {'Weld'}},
                 'T': {'cin': 1, 'cout': 1, 'recipes': {'Paint'}}}, rec, chains([('Press', 6), ('Weld', 3), ('Paint', 3)]), 'weld')
    for name in ('current', 'current-units', 'amended'):
        R = RULES[name]
        s0 = init_state(F); seen = {s0}; dq = deque([s0]); most = 0; locks = 0
        while dq:
            S = dq.popleft()
            most = max(most, sum(1 for i, x in enumerate(S) if x[0] == 1 and F.orec[i] == 'Weld'))
            succ = successors(F, R, S)
            locks += not succ and any(x[0] != 4 for x in S)
            for _, S2 in succ:
                if S2 not in seen: seen.add(S2); dq.append(S2)
        print(f"{name:14s} most welds gathering plates at once: {most} - states {len(seen)} - locks {locks}")


# ── Random factories ──

def generate(rng, multikind, maxops):
    nrec = rng.randint(2, 4)
    names = [chr(ord('A') + i) for i in range(nrec)]
    recipes, producer = {}, {}
    for i, r in enumerate(names):
        ins = {}
        for _ in range(rng.randint(1, 2)):
            if i > 0 and rng.random() < 0.8:
                k = rng.choice([k for k in producer if names.index(producer[k]) < i])
            else:
                k = f"raw{rng.randint(1, 2)}"
            ins[k] = ins.get(k, 0) + (2 if rng.random() < 0.25 else 1)
        outs = {f"k{r}": (2 if rng.random() < 0.2 else 1)}
        if multikind and rng.random() < 0.4:
            outs[f"j{r}"] = 1
        for k in outs:
            producer[k] = r
        recipes[r] = {'in': ins, 'out': outs}
    count = {r: 0 for r in names}
    count[names[-1]] = rng.randint(1, 3)
    for i in range(nrec - 2, -1, -1):
        r = names[i]
        need_ops = 0
        for k, v in recipes[r]['out'].items():
            d = sum(count[q] * recipes[q]['in'].get(k, 0) for q in names)
            if d:
                need_ops = max(need_ops, -(-d // v))
        count[r] = need_ops
    used = [r for r in names if count[r] > 0]
    for r in used:
        for k, v in recipes[r]['out'].items():
            consumed = sum(count[q] * recipes[q]['in'].get(k, 0) for q in used)
            if consumed and consumed != count[r] * v:
                return None
    total = sum(count.values())
    if total > maxops or total < 2:
        return None
    recipes = {r: recipes[r] for r in used}
    nm = rng.randint(1, 3)
    mnames = ['M', 'N', 'K'][:nm]
    mrec = {m: set() for m in mnames}
    for r in used:
        for m in rng.sample(mnames, rng.randint(1, min(2, nm))):
            mrec[m].add(r)
    mnames = [m for m in mnames if mrec[m]]
    alloc = {m: [0, 0] for m in mnames}
    for r in used:
        m = rng.choice([m for m in mnames if r in mrec[m]])
        alloc[m][0] += sum(recipes[r]['in'].values())
        alloc[m][1] += sum(recipes[r]['out'].values())
    machines = {}
    for m in mnames:
        ci = max(alloc[m][0], max(sum(recipes[r]['in'].values()) for r in mrec[m])) + (rng.random() < 0.35)
        co = max(alloc[m][1], max(sum(recipes[r]['out'].values()) for r in mrec[m])) + (rng.random() < 0.35)
        machines[m] = {'cin': ci, 'cout': co, 'recipes': mrec[m]}
    F = Factory(machines, recipes, chains([(r, count[r]) for r in used]), 'random')
    # precondition P: the empty factory fits one run of every recipe at once
    reqs = [[(mi, sum(recipes[r]['in'].values()), sum(recipes[r]['out'].values())) for mi in range(len(F.mnames)) if r in F.mrec[mi]] for r in used]
    return F if fits(reqs, list(F.cin), list(F.cout)) else None


def recipe_cycle(recipes):
    """True when some recipe consumes, directly or through others, a kind it makes."""
    makes = {r: set(v['out']) for r, v in recipes.items()}
    feeds = {r: {q for q, w in recipes.items() if makes[r] & set(w['in'])} for r in recipes}
    for start in recipes:
        seen, stack = set(), list(feeds[start])
        while stack:
            q = stack.pop()
            if q == start:
                return True
            if q not in seen:
                seen.add(q); stack.extend(feeds[q])
    return False


def feasible(F):
    """Ignoring buffers, can the operations be run one at a time in some order?"""
    n = len(F.orec)
    full = (1 << n) - 1
    seen, stack = {0}, [0]
    while stack:
        mask = stack.pop()
        if mask == full:
            return True
        pool = {}
        for i in range(n):
            if mask >> i & 1:
                for k, v in F.recipes[F.orec[i]]['out'].items(): pool[k] = pool.get(k, 0) + v
                for k, v in F.recipes[F.orec[i]]['in'].items(): pool[k] = pool.get(k, 0) - v
        for i in range(n):
            if mask >> i & 1: continue
            if all(k in F.raw or pool.get(k, 0) >= v for k, v in F.recipes[F.orec[i]]['in'].items()):
                m2 = mask | 1 << i
                if m2 not in seen:
                    seen.add(m2); stack.append(m2)
    return False


def generate_general(rng, cycles, multikind, maxops, need_cycle, need_multi, unique=False):
    """Recipes draw inputs and outputs from a shared pool of kinds, so a kind can have several
    makers (ingots from ore, or from offcuts) and recipes can form cycles. Operation counts are
    drawn first; output counts are then set so the work balances."""
    nrec = rng.randint(2, 4)
    names = [chr(ord('A') + i) for i in range(nrec)]
    kinds = [f"k{i}" for i in range(rng.randint(2, 4))]
    outs, ins = {}, {}
    for i, r in enumerate(names):
        pick = kinds if cycles else kinds[:i + 1]
        taken = {k for q in outs for k in outs[q]} if unique else set()
        first = [k for k in (kinds[i % len(kinds):] if not cycles else kinds) if k not in taken]
        if not first:
            return None
        outs[r] = rng.sample(first, 1)
        if multikind and rng.random() < 0.5:
            extra = [k for k in kinds if k not in outs[r] and k not in taken]
            if extra:
                outs[r].append(rng.choice(extra))
        d = {}
        for _ in range(rng.randint(1, 2)):
            usable = [k for k in kinds if k not in outs[r]] if not cycles else kinds
            if not cycles:
                usable = [k for k in usable if all(names.index(q) < i for q in names if k in outs.get(q, []))]
            if usable and rng.random() < 0.75:
                k = rng.choice(usable)
            else:
                k = f"raw{rng.randint(1, 2)}"
            d[k] = d.get(k, 0) + (2 if rng.random() < 0.25 else 1)
        ins[r] = d
    count = {r: rng.randint(1, 3) for r in names}
    if sum(count.values()) > maxops:
        return None
    out_counts = {r: {} for r in names}
    for k in kinds:
        makers = [r for r in names if k in outs[r]]
        consumed = sum(count[q] * ins[q].get(k, 0) for q in names)
        if not makers:
            if consumed:
                return None          # consumed but never made, and not a source kind
            continue
        if consumed == 0:
            for r in makers:
                out_counts[r][k] = rng.randint(1, 2)
            continue
        left = consumed - sum(count[r] for r in makers)
        if left < 0:
            return None
        oc = {r: 1 for r in makers}
        while left > 0:
            fit = [r for r in makers if count[r] <= left and oc[r] < 4]
            if not fit:
                return None
            r = rng.choice(fit)
            oc[r] += 1; left -= count[r]
        for r in makers:
            out_counts[r][k] = oc[r]
    recipes = {r: {'in': ins[r], 'out': out_counts[r]} for r in names}
    if any(not v['out'] for v in recipes.values()):
        return None
    consumed_kinds = {k for v in recipes.values() for k in v['in']}
    if need_cycle and not recipe_cycle(recipes):
        return None
    if not cycles and recipe_cycle(recipes):
        return None
    if os.environ.get('NEED_SHARED') == '1' and not any(sum(1 for v in recipes.values() if k in v['out']) >= 2 for k in consumed_kinds):
        return None
    if need_multi and not any(sum(1 for k in v['out'] if k in consumed_kinds) >= 2 for v in recipes.values()):
        return None
    nm = rng.randint(1, 3)
    mnames = ['M', 'N', 'K'][:nm]
    mrec = {m: set() for m in mnames}
    for r in names:
        for m in rng.sample(mnames, rng.randint(1, min(2, nm))):
            mrec[m].add(r)
    mnames = [m for m in mnames if mrec[m]]
    alloc = {m: [0, 0] for m in mnames}
    for r in names:
        m = rng.choice([m for m in mnames if r in mrec[m]])
        alloc[m][0] += sum(recipes[r]['in'].values())
        alloc[m][1] += sum(recipes[r]['out'].values())
    machines = {}
    for m in mnames:
        ci = max(alloc[m][0], max(sum(recipes[r]['in'].values()) for r in mrec[m])) + (rng.random() < 0.35)
        co = max(alloc[m][1], max(sum(recipes[r]['out'].values()) for r in mrec[m])) + (rng.random() < 0.35)
        machines[m] = {'cin': ci, 'cout': co, 'recipes': mrec[m]}
    F = Factory(machines, recipes, chains([(r, count[r]) for r in names]), 'random')
    reqs = [[(mi, sum(recipes[r]['in'].values()), sum(recipes[r]['out'].values())) for mi in range(len(F.mnames)) if r in F.mrec[mi]] for r in names]
    if not fits(reqs, list(F.cin), list(F.cout)) or not feasible(F):
        return None
    return F


def describe_factory(F):
    rec = '; '.join(f"{r}: {v['in']} -> {v['out']}" for r, v in F.recipes.items())
    mach = '; '.join(f"{F.mnames[i]}(in {F.cin[i]}, out {F.cout[i]}) {sorted(F.mrec[i])}" for i in range(len(F.mnames)))
    ops = {r: F.orec.count(r) for r in F.recipes}
    return f"{rec} | {mach} | ops {ops}"


def search(seed, n):
    multikind = os.environ.get('MULTIKIND') == '1'
    maxops = int(os.environ.get('MAXOPS', '7'))
    limit = int(os.environ.get('LIMIT', '40000'))
    general = os.environ.get('GEN') == 'general'
    cycles = os.environ.get('CYCLES') == '1'
    need_cycle = os.environ.get('NEED_CYCLE') == '1'
    need_multi = os.environ.get('NEED_MULTI') == '1'
    only = os.environ.get('RULES')
    rules = {k: v for k, v in RULES.items() if not only or k in only.split(',')}
    rng = random.Random(seed)
    stats = {k: {'live': 0, 'LOCK': 0, 'limit': 0} for k in rules}
    tried = 0
    while tried < n:
        if general:
            F = generate_general(rng, cycles, multikind, maxops, need_cycle, need_multi, os.environ.get('UNIQUE') == '1')
        else:
            F = generate(rng, multikind, maxops)
        if F is None:
            continue
        tried += 1
        for k, R in rules.items():
            res, states, trace = explore(F, R, limit)
            stats[k][res] += 1
            if res == 'LOCK' and (k.startswith('amended') or k == 'current-units'):
                print(f"LOCK under {k}: {describe_factory(F)}", flush=True)
                for lbl, S in trace:
                    print('  ', lbl, describe_state(F, R, S), flush=True)
    for k, v in stats.items():
        print(f"{k:22s} locks {v['LOCK']:4d} - explored {v['live'] + v['LOCK']:5d} - capped {v['limit']}")


if __name__ == '__main__':
    cmd = sys.argv[1] if len(sys.argv) > 1 else 'theorems'
    if cmd == 'theorems':
        theorems()
    elif cmd == 'weld':
        weld()
    elif cmd == 'search':
        search(int(sys.argv[2]), int(sys.argv[3]))