prop/test/microwaveprop/geo_property_test.exs
Graham McIntire 4c1013cdbd
test(property): add property tests for terrain + atmospheric math
Cover the pure-math invariants of the ITU-R P.526-16 diffraction
helpers, the haversine metric on Geo, and the Magnus / dry-adiabat
helpers in the skew-T renderer. 29 properties, one invariant each.
2026-04-21 13:56:39 -05:00

97 lines
3.3 KiB
Elixir

defmodule Microwaveprop.GeoPropertyTest do
@moduledoc """
StreamData property tests for `Microwaveprop.Geo`.
The haversine formula defines a metric on the surface of the Earth,
so it must satisfy the three metric axioms: non-negativity with
identity-of-indiscernibles, symmetry, and the triangle inequality.
These properties encode those axioms directly, plus the global
bound of half the Earth's circumference.
"""
use ExUnit.Case, async: true
use ExUnitProperties
alias Microwaveprop.Geo
@half_circumference_km 20_015.1
describe "haversine_km/4 metric axioms" do
property "distance from a point to itself is exactly 0" do
check all(
lat <- float(min: -89.9, max: 89.9),
lon <- float(min: -179.9, max: 179.9)
) do
assert Geo.haversine_km(lat, lon, lat, lon) == 0.0
end
end
property "is non-negative for every pair of points" do
check all(
lat1 <- float(min: -89.9, max: 89.9),
lon1 <- float(min: -179.9, max: 179.9),
lat2 <- float(min: -89.9, max: 89.9),
lon2 <- float(min: -179.9, max: 179.9)
) do
assert Geo.haversine_km(lat1, lon1, lat2, lon2) >= 0
end
end
property "is symmetric in its endpoints" do
check all(
lat1 <- float(min: -89.9, max: 89.9),
lon1 <- float(min: -179.9, max: 179.9),
lat2 <- float(min: -89.9, max: 89.9),
lon2 <- float(min: -179.9, max: 179.9)
) do
forward = Geo.haversine_km(lat1, lon1, lat2, lon2)
reverse = Geo.haversine_km(lat2, lon2, lat1, lon1)
assert_in_delta forward, reverse, 1.0e-9
end
end
property "satisfies the triangle inequality for any three points" do
check all(
lat1 <- float(min: -89.9, max: 89.9),
lon1 <- float(min: -179.9, max: 179.9),
lat2 <- float(min: -89.9, max: 89.9),
lon2 <- float(min: -179.9, max: 179.9),
lat3 <- float(min: -89.9, max: 89.9),
lon3 <- float(min: -179.9, max: 179.9)
) do
d_ab = Geo.haversine_km(lat1, lon1, lat2, lon2)
d_bc = Geo.haversine_km(lat2, lon2, lat3, lon3)
d_ac = Geo.haversine_km(lat1, lon1, lat3, lon3)
# Small epsilon for accumulated floating-point error.
assert d_ac <= d_ab + d_bc + 1.0e-6
end
end
property "is bounded above by half the Earth's circumference" do
check all(
lat1 <- float(min: -89.9, max: 89.9),
lon1 <- float(min: -179.9, max: 179.9),
lat2 <- float(min: -89.9, max: 89.9),
lon2 <- float(min: -179.9, max: 179.9)
) do
assert Geo.haversine_km(lat1, lon1, lat2, lon2) <= @half_circumference_km
end
end
end
describe "bearing_deg/4" do
property "result is always in [0, 360) for distinct points" do
check all(
lat1 <- float(min: -80.0, max: 80.0),
lon1 <- float(min: -179.0, max: 179.0),
# Ensure a nonzero displacement.
dlat <- float(min: 0.1, max: 5.0),
dlon <- float(min: 0.1, max: 5.0)
) do
b = Geo.bearing_deg(lat1, lon1, lat1 + dlat, lon1 + dlon)
assert b >= 0.0
assert b < 360.0
end
end
end
end