triz_dynamics
Explores bounded dynamics of finite-state function models via breadth-first search, checking reachability, safety, timed separation, loop classes, and cycle-cost bounds with witness traces.
Instructions
Costed transition rows add exact per-dimension cycle mean ranges, rational potential bounds and rechecked witnesses on closed components; max_cost_work caps these. Bounded dynamics of a function model whose boxes declare state, initial, and transition rows (state, inputs) → (next state, outputs): each such box is a nondeterministic Mealy machine (a lens with a residual is one, with the residual as state); boxes with behavior are stateless. Boxes compose synchronously along the wiring: wires are instantaneous, memory lives only in declared state, and a loop through stateless boxes resolves within a step as in triz_behavior. From the initial states, over the boundary inputs you allow at each time (default: every value), every run is explored breadth first up to horizon steps; the result lists the reachable states, the fixed points among them, and the runs that block (a state with no row for its inputs). unsafe decides escalation: reachable (with a shortest trace), unreachable (the reachable set stopped growing, so at no horizon), or unreachable-within-horizon. safe decides invariance: violated (shortest trace), invariant, or invariant-within-horizon. Without inputs the configurations are finite, so each verdict also carries unbounded, decided at every horizon by continuing the search past the horizon within the same state cap: reachable or violated (with the time and, past the horizon, a shortest trace), unreachable or invariant (with completeAfter), or undecided (cap-exceeded past the horizon, or blocked); the bounded verdict beside it is unchanged. A blocked state meets a target by its state conditions; a port condition there leaves the verdict undecided (reason blocked), never safe. separation takes two to four demands, each a target set with a time window, and decides whether one run visits each within its window (separation in time along a trajectory, Principle 15): realizable with a witness trace, unrealizable (a demand never met, or no single run meets them all), or undecided (a blocked run might meet them all). Without inputs, loops classifies the closed components (no step leaves them) of the reachable graph of the global states of boxes that declare transition, explored without a horizon up to the cap, from the initial states and every state meeting safe's state conditions: bistable (fixed points in two or more closed components), trapped (a closed component every configuration of which meets unsafe: an absorbing trap, with a shortest trace into it), recurrent (a closed component that meets unsafe and also holds a safe configuration: the run can recover but never leaves it, with a shortest trace into it and the safe configuration), oscillating (a cycle and no fixed point, with its period and one cycle); each closed component reports unsafe (it meets the set) and allUnsafe (it lies inside it); classes can coexist, and 'none' means no closed component was found within the cap. Behavior rows are never read as transitions. Every trace is re-checked against the declared rows. Fails closed on ill-typed rows, unknown targets, and past the state cap. Verdicts hold for the rows as declared; continuous dynamics, convergence rates, and control are not modelled.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| safe | No | Invariance: does every reachable configuration meet every condition? | |
| model | Yes | ||
| inputs | No | Entry t lists the values allowed at time t on unwired input ports; an unlisted port takes every value. Omit for every value at every time | |
| unsafe | No | Escalation: is a configuration where every condition holds reachable? e.g. [{ box: 'bearing', port: 'friction', values: ['high'] }] | |
| horizon | No | Steps to explore (times 0 to horizon); default: the length of inputs minus one, else 20 | |
| initial | No | Box id → initial states, overriding the box's initial | |
| max_states | No | Cap on configurations and search states (default and maximum 100000) | |
| separation | No | Separation in time: does one run visit each demand's target set within its window? | |
| max_cost_work | No | Exact cycle-cost work cap; past it meanCost is undecided |