triz_abstraction
Check whether a coarse function model correctly abstracts a detailed one under a typed box, port, and carrier map, and report failing checks, hidden functions, and harm loops.
Instructions
Check that a coarse function model (few boxes, e.g. with declared behaviour) is an abstraction of a detailed one of the same system (many boxes, e.g. with costs and feasibility) under a typed map: detailed box → coarse box (several may share one; a box left out is outside the abstraction), per box detailed port → coarse port (default: the same id and side), detailed carrier → coarse carrier (default: the same id). A function between two mapped ports is mapped; one between unmapped ports of boxes with the same image is hidden inside that coarse box; one between boxes with different images and an unmapped port is forgotten. Four checks: total (every mapped port's carrier has an image, and every mapped function has an image coarse function with the mapped endpoints, the mapped carrier, and the same polarity class: negative = harmful or excessive, or not), typed (each mapped port lands on a port of the same side whose carrier is its carrier's image, of the same layer; typed_map), wires (every coarse function is the image of a mapped detailed function of its class), harm loops (every coarse harm loop is the image of a detailed one: each harmful or excessive coarse function on it has such a preimage whose object reaches its performer along mapped and hidden functions; cycle_map, with the detailed cycle as witness). Verdict abstraction or not-an-abstraction with the failing checks. Also reports the functions hidden, forgotten, and left out (harms listed apart), the detailed harm loops the coarse model hides or loses, whether reachability among mapped boxes passes to the coarse model (reach_map, when nothing is forgotten), and, where a coarse box with behaviour has one preimage box with feasibility, whether that box's feasibility amounts read through the coarse carriers' levels fall in the coarse behaviour. When either model declares flows, each detailed flow's runs inside the mapped boxes are sent through the map like a merge and matched step by step against the coarse flows of the image carrier (flows.images), and coarse flow steps no detailed step maps to are listed (flows.unbacked); flows do not change the verdict. Fails closed on a model that does not type-check and on map ids that do not exist. Whether the coarse rows are true of their preimages is substantiated outside the kernel.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| map | Yes | ||
| coarse | Yes | The coarse model of the same system | |
| detailed | Yes | The detailed model |