% Evidence-backed spacecraft battery diagnosis.
%
% This compact engineering model combines telemetry, derived physical
% quantities, threshold checks, redundant sensing, diagnosis, and response.
% The values and limits are illustrative; they are not operational flight
% rules.

query(metric(X0, X1, X2)).
query(diagnosis(X0, X1)).
query(action(X0, X1)).

% Primary telemetry for battery pack bp1.
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).

% An independent temperature channel provides corroborating evidence.
redundant_telemetry(bp1, temperature_c, 76.0).

% Illustrative engineering limits and available cooling power.
limit(max_safe_temperature_c, 60.0).
limit(max_temperature_rise_c_per_min, 1.5).
limit(max_cell_delta_v, 0.08).
cooling_capacity_w(bp1, 12.0).

% Thermal margin is positive below the limit and negative above it.
metric(Pack, thermal_margin_c, Margin) :-
  limit(max_safe_temperature_c, Maximum),
  telemetry(Pack, temperature_c, Temperature),
  sub(Maximum, Temperature, Margin).

% Resistive heating follows P = I^2 R.
metric(Pack, resistive_heating_w, Heating) :-
  telemetry(Pack, current_a, Current),
  telemetry(Pack, internal_resistance_ohm, Resistance),
  mul(Current, Current, CurrentSquared),
  mul(CurrentSquared, Resistance, Heating).

over_temperature(Pack) :-
  telemetry(Pack, temperature_c, Temperature),
  limit(max_safe_temperature_c, Maximum),
  gt(Temperature, Maximum).

rapid_heating(Pack) :-
  telemetry(Pack, temperature_rise_c_per_min, Rate),
  limit(max_temperature_rise_c_per_min, Maximum),
  gt(Rate, Maximum).

cell_imbalance(Pack) :-
  telemetry(Pack, cell_delta_v, Delta),
  limit(max_cell_delta_v, Maximum),
  gt(Delta, Maximum).

heating_exceeds_cooling(Pack) :-
  metric(Pack, resistive_heating_w, Heating),
  cooling_capacity_w(Pack, Capacity),
  gt(Heating, Capacity).

% Require two independent temperature channels above the same safety limit.
corroborated_over_temperature(Pack) :-
  telemetry(Pack, temperature_c, Primary),
  redundant_telemetry(Pack, temperature_c, Redundant),
  limit(max_safe_temperature_c, Maximum),
  gt(Primary, Maximum),
  gt(Redundant, Maximum).

% A diagnosis needs multiple independent signatures, not one threshold alone.
diagnosis(Pack, thermal_runaway_precursor) :-
  over_temperature(Pack),
  rapid_heating(Pack),
  cell_imbalance(Pack),
  heating_exceeds_cooling(Pack).

% The safety action additionally requires redundant temperature corroboration.
action(Pack, isolate_and_cool) :-
  diagnosis(Pack, thermal_runaway_precursor),
  corroborated_over_temperature(Pack).