tms-core-is-crash-safe
IN derived (depth 2)
The TMS core provides crash-free truth maintenance: deterministic termination, pure evaluation, and conservative failure semantics ensure correct results across all reachable nodes.
Summary
The truth maintenance engine will always finish its work and never crash, hang, or produce corrupt results. This guarantee comes from two properties working together: the propagation algorithm always reaches a stable stopping point in bounded time, and the justification logic is a simple pure function with no hidden state that could cause unexpected failures.
Justifications
SL — The engine's correctness guarantees (purity, termination, conservatism) hold only if all dependent references resolve — a dangling entry in `node.dependents` triggers an uncaught KeyError
Antecedents (all must be IN):
- justification-evaluation-is-uniform-and-pure — All justification types (SL and CP) use the same validity rule (antecedents IN, outlist OUT), evaluated as a pure function with no side effects
- propagation-terminates-deterministically — Truth propagation is guaranteed to terminate: BFS prevents stack overflow, stop-on-unchanged prevents oscillation, and fixpoint iteration bounds the outer loop
Unless (any of these IN defeats this justification):
- propagate-assumes-dependents-exist — Every ID in `node.dependents` is accessed via `self.nodes[dep_id]` without a membership check; a dangling dependent reference will raise `KeyError` — this is intentional (broken invariant = bug)
Dependents
These beliefs depend on this one:
- tms-handles-all-conditions-safely — The TMS core handles both normal operation (crash-free truth propagation via BFS with stop-on-unchanged) and exceptional conditions (deterministic contradiction resolution via backtracking with least-entrenched selection) through shared propagation infrastructure — no reachable execution state leads to undefined behavior.