A spacecraft battery pack is running hot. This example turns telemetry into physical quantities, checks them against limits, requires several independent signs before diagnosing a problem, and requires a second temperature sensor to agree before recommending action.
Run it in the playground · Source
Thermal runaway is a battery failure in which heat causes reactions that release more heat. Catching its precursors early matters, but so does not reacting to one faulty sensor. When is the evidence strong enough to isolate and cool the pack?
The values and limits in the example are illustrative, not flight rules.
telemetry(bp1, temperature_c, 78.0).
telemetry(bp1, temperature_rise_c_per_min, 4.2).
telemetry(bp1, current_a, 32.0).
telemetry(bp1, internal_resistance_ohm, 0.015625).
telemetry(bp1, cell_delta_v, 0.19).
redundant_telemetry(bp1, temperature_c, 76.0).
safety_limit(max_safe_temperature_c, 60.0).
cooling_capacity_w(bp1, 12.0).
Readings from the pack, an independent second temperature channel, and the limits they are judged against.
metric(Pack, resistive_heating_w, Heating) :-
telemetry(Pack, current_a, Current),
telemetry(Pack, internal_resistance_ohm, Resistance),
(CurrentSquared is Current * Current),
(Heating is CurrentSquared * Resistance).
diagnosis(Pack, thermal_runaway_precursor) :-
over_temperature(Pack),
rapid_heating(Pack),
cell_imbalance(Pack),
heating_exceeds_cooling(Pack).
action(Pack, isolate_and_cool) :-
diagnosis(Pack, thermal_runaway_precursor),
corroborated_over_temperature(Pack).
Heating follows P = I²R. The diagnosis needs four independent signatures, and the action additionally needs both temperature channels above the limit. Each layer is its own predicate, so each shows up separately in the proof.
eyeprolog examples/spacecraft-battery-diagnosis.pl
metric(bp1, thermal_margin_c, -18.0).
metric(bp1, resistive_heating_w, 16.0).
diagnosis(bp1, thermal_runaway_precursor).
action(bp1, isolate_and_cool).
The pack is 18 °C over its limit and generates 16 W of resistive heat against 12 W of cooling. All four signatures are present, both sensors agree, and the recommendation is to isolate and cool.
step(heating_exceeds_cooling(bp1),
rule(16),
['Pack' = bp1, 'Heating' = 16.0, 'Capacity' = 12.0],
[metric(bp1, resistive_heating_w, 16.0), cooling_capacity_w(bp1, 12.0), 16.0 > 12.0]).
step(corroborated_over_temperature(bp1),
rule(17),
['Pack' = bp1, 'Primary' = 78.0, 'Redundant' = 76.0, 'Maximum' = 60.0],
[telemetry(bp1, temperature_c, 78.0),
redundant_telemetry(bp1, temperature_c, 76.0),
(second step shortened.) Each conclusion names the numbers it used: 16 W against 12 W, and 78 °C and 76 °C against 60 °C. A reviewer can dispute a limit without re-deriving the physics.
condition('C1', resolution, ok, 19).
condition('C5', re_decision, ok, 8).
verdict(checked).
The 19 rule and fact steps replay against the model, and the 8 arithmetic and comparison steps are recomputed. Nothing is trusted. What the proof cannot vouch for is the telemetry itself: the sensors’ calibration lies outside the logic.
58.0. The diagnosis stays, but the
action disappears: one hot sensor is not enough to act.20.0. Now there is no diagnosis at all.
Which signature failed?metric(Pack, heating_surplus_w, Surplus) rule for heating minus
cooling.Learn more in The Art of EyeProlog, Chapter 14.