triz_behavior

Compose declared box behaviour (carrier values, box behavior rows) into the model's external relation: boundary inputs (unwired input ports) to deliverables (product input ports fed by a non-harmful function). The default upstream scope composes boxes that can reach a deliverable and explicitly assumes omitted boxes accept everything; scope whole composes every box, including downstream and disconnected constraints. full_relation returns all rows within the search cap. Feedback loops compose by the relational trace, so every consistent steady state counts, and the steady states are listed. factorisations lists each composed box whose relation is the product of its projections onto two or more groups of ports, with the finest groups, in box order (decided:false past a per-box cap): segment it into them, or unions of them, and each part keeps its projection. The hint describes the declared rows, not a physical split, and changes no verdict. This is steady-state semantics, not dynamics. With compare_to, decide whether the model (a concept, e.g. a triz_transform result) has the baseline's input→deliverable relation; pass segment's or take_out's boxMap as box_map. trim is shorthand: perform the trim as triz_transform does and compare the result with the model. Verdict preserved; changed (a lost deliverable, or a counterexample input with the differing outputs and which relation contains which); or undecided (reason missing-behavior: the boxes that can reach a deliverable and declare no behaviour; reason no-steady-state: neither model has a steady state at any input, so equal empty relations say nothing). With joint_boxes and weakest_spec, select every composed box without behavior and compute one coupled residual over their combined ports. The joint rows are a single relation: independentSafe checks whether independently declaring their per-box projections stays inside the target, factorizes checks whether their product equals the joint relation, and a counterexample explains unsafe coupling. The exact search is bounded by max_states; row_costs are unsupported in this mode. With weakest_spec (and compare_to or trim), give the weakest box specification (residual in Rel) for the one box of the concept that can reach a deliverable and declares no behaviour, against the same target: spec, every row of that box whose composite stays inside the target, with preserves:true when declaring it gives exactly the target (any behaviour that does is contained in it); impossible, when the spec's composite misses part of the target (an uncovered input is given; no behaviour of that box gives the target, and the empty relation, which always stays inside, is never read as preserving) or a deliverable is lost; undecided for three or more unknown boxes when joint_boxes is omitted (several-holes), missing baseline behaviour, an empty target, or past the cap (state-cap). When the box to specify declares producible rows (what it can physically produce), the spec is the residual cut down to them: spec when that still covers the target (producible.infeasible lists the residual rows left out); impossible with reason infeasible when the residual covers the target but its producible rows do not, with requiredInfeasible giving, per missing target pair, the residual rows that deliver it, none producible (every relation that gives the target contains one of each); impossible with reason not-covered when the residual itself does not cover. With exactly two boxes without behaviour (boxes), a pair of relations stays inside the target iff every pair of rows, one of each, does, and the maximal such pairs are the formal concepts of the safe row pairs: spec lists those whose composite covers the target (specs, each declared and re-checked to give exactly the target; every pair that gives the target lies inside one), with weakest:true when there is one and weakest:false when several are incomparable; impossible (not-covered) when none covers, with each maximal pair's uncovered input (pairs); undecided (concept-cap) past the cap on concepts. Producible rows cut each box first; impossible with reason infeasible then means some pair over all rows (wouldGive) would give the target. Fails closed on ill-typed behaviour, an ambiguous or mismatched box_map, inputs whose values differ between the models, and past the state cap. With row_costs in the one-hole mode, cheapestExtension gives an exact least-cost set of safe nonproducible rows to add, using the complete target relation and explicit integer costs, or reports an undecided capped search; it is not-applicable (target-not-covered-by-residual) when the residual itself misses the target, and row_costs fail with invalid-row-costs wherever no one-box residual is computed; the Boolean verdict is unchanged. The verdict holds for the relations as declared; substantiating them, the absorber's or mediator's first, is outside the kernel.