Computation engine

Two solvers that must agree.

The fault-tree mathematics is where a technical evaluator goes first — so here is what the engine computes, how it is checked, and where its boundaries are.

How the mathematics is checked.

Minimal cut sets are computed by two solvers that share no algorithmic ancestry: MOCUS top-down expansion, and a reduced ordered binary decision diagram built from scratch. The engine selects by tree size; the regression suite runs both and requires identical minimal cut sets.

You will not find a "validated to within 1%" claim here. Agreement between independent implementations, on every tree in the suite, is a stronger check than a tolerance against a textbook — and it does not collapse when someone opens the test file.

The engine implements a written mathematical specification, clause by clause, with a conformance brief governing what the implementation may and may not do. Every computation is a recorded run; each tree pins the run it currently cites.

Regression invariant illustrative
solver=MOCUSmcs=14Q=4.5e-8
solver=ROBDDmcs=14Q=4.5e-8
assert identical(mcs_a, mcs_b) ✓

What it quantifies.

Unavailability

Fixed-probability, exponential, repairable steady-state and dormant models — so a free-fall extension mechanism checked every 600 flight hours carries its latent exposure between checks.

Importance

Five measures per basic event — Fussell-Vesely, Birnbaum, RAW, RRW and criticality — ranked in the workbook export.

Common cause

Beta-factor CCF groups across basic events. MGL and alpha-factor requests are rejected outright — the engine refuses to approximate a model it does not implement.

What happens on a 500-node tree.

Background computations run in isolated child processes with database-cooperative cancellation, a heartbeat, and an orphan reaper. A long background solve cannot wedge the instance, and can be cancelled across workers — the kill path itself is tested.

Known limit: the synchronous compute route still solves in-process. Isolating it the same way is a queued work item, so until then a large tree through that one endpoint can occupy a worker.

Where the boundaries are.

The specification the engine implements is SPARC-SPEC-FTA-MATH-001 v1.3 — a draft, not approved for compliance use, with sixteen release gates still to meet and a register of known implementation gaps. It computes unavailability, importance and common-cause contributions; it does not compute an Average Probability per Flight Hour, and it issues no compliance verdict — every comparison path fails closed and says why.

The acceptance criteria are published in advance — each validation vector, its inputs and its expected value — as the target the engine is being built to meet. That is a stronger and rarer claim than an accuracy figure, and it is checkable in the repository.

The SPARC FTA mathematics specification (SPARC-SPEC-FTA-MATH-001) was independently reviewed on 16 August 2026. That review covered the specification and a static composition review of the implementation at a pinned baseline. It was a technical review, not a certification approval.

The full claim boundary is on the evidence page.