Collision probability computation for conjunction assessment
collision: convert fuzz suite to Alcobar generators
Rewrite fuzz_collision to use real Alcobar property tests with a
Collision.encounter generator, replacing the Random.self_init loops.
Add the missing fuzz alias rule with --gen-corpus and afl-fuzz
invocation, switch the runner module to Alcobar.run, and fix the .mli
to expose Alcobar.test_case (E700/E701 fuzz dune rules).
The hand-rolled unit-test cases that previously lived in the fuzz
suite (small_miss, head_on, monotonicity, etc.) overlap with
test_collision.ml and were dropped from the fuzz module since they
were not actually fuzzed inputs.
+92
-203
+19
-1
fuzz/dune
+19
-1
fuzz/dune
···
1
+
; Crowbar/Alcobar fuzz testing for collision Pc properties
2
+
;
3
+
; Quick check (runs tests with random inputs):
4
+
; dune build @runtest
5
+
;
6
+
; With AFL instrumentation:
7
+
; dune build @fuzz --profile=afl
8
+
1
9
(executable
2
10
(name fuzz)
3
11
(modules fuzz fuzz_collision)
4
-
(libraries collision alcotest))
12
+
(libraries collision alcobar))
5
13
6
14
(rule
7
15
(alias runtest)
···
10
18
(deps fuzz.exe)
11
19
(action
12
20
(run %{exe:fuzz.exe})))
21
+
22
+
(rule
23
+
(alias fuzz)
24
+
(enabled_if
25
+
(= %{profile} afl))
26
+
(deps fuzz.exe)
27
+
(action
28
+
(progn
29
+
(run %{exe:fuzz.exe} --gen-corpus corpus)
30
+
(run afl-fuzz -V 60 -i corpus -o _fuzz -- %{exe:fuzz.exe} @@))))
+1
-1
fuzz/fuzz.ml
+1
-1
fuzz/fuzz.ml
+71
-200
fuzz/fuzz_collision.ml
+71
-200
fuzz/fuzz_collision.ml
···
3
3
SPDX-License-Identifier: MIT
4
4
---------------------------------------------------------------------------*)
5
5
6
-
(** NASA CARA Pc test vectors.
6
+
(** NASA CARA Pc property tests.
7
7
8
-
Property-based tests using the encounter API and the 2D Foster formula.
8
+
Property-based fuzz tests using the encounter API and the 2D Foster formula.
9
9
Verifies physical invariants: Pc bounds, symmetry, scaling, monotonicity.
10
10
11
11
References:
···
13
13
Collision Probability and Maneuver Rate for Space Vehicles", 1992
14
14
- NASA Conjunction Assessment Risk Analysis (CARA) *)
15
15
16
+
open Alcobar
17
+
16
18
let check_float msg ?(eps = 1e-8) expected actual =
17
19
let diff = Float.abs (expected -. actual) in
18
20
if diff > eps then
19
-
Alcotest.failf "%s: expected %.10e, got %.10e (diff %.2e)" msg expected
20
-
actual diff
21
+
failf "%s: expected %.10e, got %.10e (diff %.2e)" msg expected actual diff
21
22
22
-
(* {1 2D Foster encounter tests}
23
+
(* Generators *)
23
24
24
-
All inputs in km (consistent with Collision.encounter). *)
25
+
(* A miss-distance component in km, in [-5, 5]. *)
26
+
let miss_gen : float gen =
27
+
map [ float ] (fun f ->
28
+
let f = if Float.is_finite f then f else 0.0 in
29
+
let scaled = Float.rem f 10.0 in
30
+
scaled -. 5.0)
25
31
26
-
(* Case 1: Small miss, moderate sigmas — Pc should be positive and bounded *)
27
-
let test_small_miss () =
28
-
let enc : Collision.encounter =
29
-
{
30
-
miss_x = 0.005;
31
-
miss_y = 0.005;
32
-
sigma_x = 0.1;
33
-
sigma_y = 1.0;
34
-
hbr = 0.020;
35
-
}
36
-
in
37
-
let pc = Collision.pc_foster enc in
38
-
if pc <= 0.0 then Alcotest.failf "Pc should be > 0, got %e" pc;
39
-
if pc >= 1.0 then Alcotest.failf "Pc should be < 1, got %e" pc;
40
-
(* Check it's in a reasonable range *)
41
-
let pc_max = Collision.pc_max enc in
42
-
if pc > pc_max *. 1.01 then
43
-
Alcotest.failf "Pc (%.2e) > Pc_max (%.2e)" pc pc_max
32
+
(* A sigma in km, in (0, 5]. *)
33
+
let sigma_gen : float gen =
34
+
map [ float ] (fun f ->
35
+
let f = if Float.is_finite f then Float.abs f else 0.5 in
36
+
0.01 +. Float.rem f 5.0)
44
37
45
-
(* Case 2: Large miss — Pc should be essentially zero *)
46
-
let test_large_miss () =
47
-
let enc : Collision.encounter =
48
-
{
49
-
miss_x = 100.0;
50
-
miss_y = 100.0;
51
-
sigma_x = 0.1;
52
-
sigma_y = 1.0;
53
-
hbr = 0.020;
54
-
}
55
-
in
38
+
(* HBR in km, in (0, 0.1]. *)
39
+
let hbr_gen : float gen =
40
+
map [ float ] (fun f ->
41
+
let f = if Float.is_finite f then Float.abs f else 0.05 in
42
+
0.001 +. Float.rem f 0.1)
43
+
44
+
let encounter_gen : Collision.encounter gen =
45
+
map [ miss_gen; miss_gen; sigma_gen; sigma_gen; hbr_gen ]
46
+
(fun miss_x miss_y sigma_x sigma_y hbr ->
47
+
({ miss_x; miss_y; sigma_x; sigma_y; hbr } : Collision.encounter))
48
+
49
+
(* Property tests on generated encounters *)
50
+
51
+
let test_pc_in_unit_interval (enc : Collision.encounter) =
56
52
let pc = Collision.pc_foster enc in
57
-
if pc > 1e-20 then Alcotest.failf "Pc should be ~0 for large miss, got %e" pc
53
+
if pc < 0.0 then failf "Pc < 0: %e" pc;
54
+
if pc > 1.0 then failf "Pc > 1: %e" pc
58
55
59
-
(* Case 3: Head-on (zero miss) — Pc should be maximal *)
60
-
let test_head_on () =
61
-
let enc : Collision.encounter =
62
-
{ miss_x = 0.0; miss_y = 0.0; sigma_x = 0.1; sigma_y = 1.0; hbr = 0.020 }
63
-
in
56
+
let test_pc_max_bounds_pc (enc : Collision.encounter) =
64
57
let pc = Collision.pc_foster enc in
65
58
let pc_max = Collision.pc_max enc in
66
-
(* For head-on collision, Pc should equal Pc_max *)
67
-
let rel_diff =
68
-
if pc_max > 1e-30 then Float.abs (pc -. pc_max) /. pc_max else 0.0
69
-
in
70
-
if rel_diff > 0.01 then
71
-
Alcotest.failf
72
-
"head-on: Pc (%.6e) should equal Pc_max (%.6e), rel_diff=%.2e" pc pc_max
73
-
rel_diff
59
+
if pc > pc_max *. 1.01 then failf "Pc (%.2e) > Pc_max (%.2e)" pc pc_max
74
60
75
-
(* Case 4: Symmetry — swapping x/y with sigma_x/sigma_y gives same Pc *)
76
-
let test_symmetry () =
77
-
let enc1 : Collision.encounter =
78
-
{ miss_x = 0.3; miss_y = 0.7; sigma_x = 0.5; sigma_y = 2.0; hbr = 0.015 }
79
-
in
80
-
let enc2 : Collision.encounter =
81
-
{ miss_x = 0.7; miss_y = 0.3; sigma_x = 2.0; sigma_y = 0.5; hbr = 0.015 }
82
-
in
83
-
let pc1 = Collision.pc_foster enc1 in
84
-
let pc2 = Collision.pc_foster enc2 in
85
-
check_float "symmetry" ~eps:1e-10 pc1 pc2
61
+
let test_sign_invariance_x (enc : Collision.encounter) =
62
+
let enc' = { enc with miss_x = -.enc.miss_x } in
63
+
let pc1 = Collision.pc_foster enc in
64
+
let pc2 = Collision.pc_foster enc' in
65
+
check_float "sign invariance x" ~eps:1e-10 pc1 pc2
86
66
87
-
(* Case 5: Scaling — double all sigmas, Pc changes predictably.
88
-
For head-on, Pc_max = hbr^2 / (2*sx*sy), so doubling sigmas divides Pc_max by 4. *)
89
-
let test_scaling_head_on () =
90
-
let enc1 : Collision.encounter =
91
-
{ miss_x = 0.0; miss_y = 0.0; sigma_x = 0.1; sigma_y = 1.0; hbr = 0.020 }
92
-
in
93
-
let enc2 : Collision.encounter =
94
-
{ miss_x = 0.0; miss_y = 0.0; sigma_x = 0.2; sigma_y = 2.0; hbr = 0.020 }
95
-
in
96
-
let pc1 = Collision.pc_foster enc1 in
97
-
let pc2 = Collision.pc_foster enc2 in
98
-
(* Ratio should be ~4 *)
99
-
let ratio = pc1 /. pc2 in
100
-
check_float "scaling ratio" ~eps:0.1 4.0 ratio
67
+
let test_sign_invariance_y (enc : Collision.encounter) =
68
+
let enc' = { enc with miss_y = -.enc.miss_y } in
69
+
let pc1 = Collision.pc_foster enc in
70
+
let pc2 = Collision.pc_foster enc' in
71
+
check_float "sign invariance y" ~eps:1e-10 pc1 pc2
101
72
102
-
(* Case 6: Pc is always in [0, 1] for many random encounters *)
103
-
let test_pc_bounds () =
104
-
Random.self_init ();
105
-
for _ = 1 to 500 do
106
-
let miss_x = Random.float 10.0 -. 5.0 in
107
-
let miss_y = Random.float 10.0 -. 5.0 in
108
-
let sigma_x = 0.01 +. Random.float 5.0 in
109
-
let sigma_y = 0.01 +. Random.float 5.0 in
110
-
let hbr = 0.001 +. Random.float 0.1 in
111
-
let enc : Collision.encounter = { miss_x; miss_y; sigma_x; sigma_y; hbr } in
112
-
let pc = Collision.pc_foster enc in
113
-
if pc < 0.0 then
114
-
Alcotest.failf "Pc < 0: miss=(%.3f,%.3f) sigma=(%.3f,%.3f) hbr=%.3f → %e"
115
-
miss_x miss_y sigma_x sigma_y hbr pc;
116
-
if pc > 1.0 then
117
-
Alcotest.failf "Pc > 1: miss=(%.3f,%.3f) sigma=(%.3f,%.3f) hbr=%.3f → %e"
118
-
miss_x miss_y sigma_x sigma_y hbr pc
119
-
done
120
-
121
-
(* Case 7: Pc_max always bounds Pc *)
122
-
let test_pc_max_always_bounds () =
123
-
Random.self_init ();
124
-
for _ = 1 to 500 do
125
-
let miss_x = Random.float 10.0 -. 5.0 in
126
-
let miss_y = Random.float 10.0 -. 5.0 in
127
-
let sigma_x = 0.01 +. Random.float 5.0 in
128
-
let sigma_y = 0.01 +. Random.float 5.0 in
129
-
let hbr = 0.001 +. Random.float 0.1 in
130
-
let enc : Collision.encounter = { miss_x; miss_y; sigma_x; sigma_y; hbr } in
131
-
let pc = Collision.pc_foster enc in
132
-
let pc_max = Collision.pc_max enc in
133
-
if pc > pc_max *. 1.01 then
134
-
Alcotest.failf "Pc (%.2e) > Pc_max (%.2e) for miss=(%.3f,%.3f)" pc pc_max
135
-
miss_x miss_y
136
-
done
137
-
138
-
(* Case 8: Foster and Chan agree *)
139
-
let test_foster_chan_agree () =
140
-
let cases =
141
-
[
142
-
(0.1, 0.2, 0.5, 1.0, 0.010);
143
-
(0.0, 0.0, 1.0, 1.0, 0.020);
144
-
(1.0, 0.5, 2.0, 3.0, 0.005);
145
-
(0.01, 0.01, 0.05, 0.5, 0.015);
146
-
(5.0, 3.0, 1.0, 1.0, 0.010);
147
-
]
73
+
let test_xy_symmetry (enc : Collision.encounter) =
74
+
let enc' =
75
+
{
76
+
Collision.miss_x = enc.miss_y;
77
+
miss_y = enc.miss_x;
78
+
sigma_x = enc.sigma_y;
79
+
sigma_y = enc.sigma_x;
80
+
hbr = enc.hbr;
81
+
}
148
82
in
149
-
List.iter
150
-
(fun (miss_x, miss_y, sigma_x, sigma_y, hbr) ->
151
-
let enc : Collision.encounter =
152
-
{ miss_x; miss_y; sigma_x; sigma_y; hbr }
153
-
in
154
-
let pc_f = Collision.pc_foster enc in
155
-
let pc_c = Collision.pc_chan enc in
156
-
let rel_diff =
157
-
if pc_f > 1e-30 then Float.abs (pc_f -. pc_c) /. pc_f else 0.0
158
-
in
159
-
if rel_diff > 0.02 then
160
-
Alcotest.failf
161
-
"Foster (%.6e) vs Chan (%.6e) disagree: rel_diff=%.2e for \
162
-
miss=(%.3f,%.3f)"
163
-
pc_f pc_c rel_diff miss_x miss_y)
164
-
cases
83
+
let pc1 = Collision.pc_foster enc in
84
+
let pc2 = Collision.pc_foster enc' in
85
+
check_float "xy symmetry" ~eps:1e-10 pc1 pc2
165
86
166
-
(* Case 9: Monotonicity — increasing miss distance decreases Pc *)
167
-
let test_monotonicity () =
168
-
let sigma_x = 0.5 in
169
-
let sigma_y = 2.0 in
170
-
let hbr = 0.015 in
171
-
let misses = [ 0.0; 0.1; 0.5; 1.0; 2.0; 5.0; 10.0 ] in
172
-
let pcs =
173
-
List.map
174
-
(fun miss_x ->
175
-
let enc : Collision.encounter =
176
-
{ miss_x; miss_y = 0.0; sigma_x; sigma_y; hbr }
177
-
in
178
-
Collision.pc_foster enc)
179
-
misses
87
+
let test_foster_chan_agree (enc : Collision.encounter) =
88
+
let pc_f = Collision.pc_foster enc in
89
+
let pc_c = Collision.pc_chan enc in
90
+
let rel_diff =
91
+
if pc_f > 1e-10 then Float.abs (pc_f -. pc_c) /. pc_f else 0.0
180
92
in
181
-
let rec check_decreasing = function
182
-
| [] | [ _ ] -> ()
183
-
| a :: (b :: _ as rest) ->
184
-
if b > a *. 1.001 then
185
-
Alcotest.failf "Pc not monotonically decreasing: %e then %e" a b;
186
-
check_decreasing rest
187
-
in
188
-
check_decreasing pcs
189
-
190
-
(* Case 10: HBR scaling — doubling HBR should roughly quadruple Pc for head-on *)
191
-
let test_hbr_scaling () =
192
-
let enc1 : Collision.encounter =
193
-
{ miss_x = 0.0; miss_y = 0.0; sigma_x = 1.0; sigma_y = 1.0; hbr = 0.010 }
194
-
in
195
-
let enc2 : Collision.encounter =
196
-
{ miss_x = 0.0; miss_y = 0.0; sigma_x = 1.0; sigma_y = 1.0; hbr = 0.020 }
197
-
in
198
-
let pc1 = Collision.pc_foster enc1 in
199
-
let pc2 = Collision.pc_foster enc2 in
200
-
let ratio = pc2 /. pc1 in
201
-
(* HBR doubled → area quadrupled → Pc should quadruple for head-on *)
202
-
check_float "HBR scaling ratio" ~eps:0.5 4.0 ratio
203
-
204
-
(* Case 11: Sign invariance — miss_x sign flip gives same Pc *)
205
-
let test_sign_invariance () =
206
-
let enc1 : Collision.encounter =
207
-
{ miss_x = 0.3; miss_y = 0.5; sigma_x = 1.0; sigma_y = 2.0; hbr = 0.010 }
208
-
in
209
-
let enc2 : Collision.encounter =
210
-
{ miss_x = -0.3; miss_y = 0.5; sigma_x = 1.0; sigma_y = 2.0; hbr = 0.010 }
211
-
in
212
-
let pc1 = Collision.pc_foster enc1 in
213
-
let pc2 = Collision.pc_foster enc2 in
214
-
check_float "sign invariance x" ~eps:1e-10 pc1 pc2;
215
-
let enc3 : Collision.encounter =
216
-
{ miss_x = 0.3; miss_y = -0.5; sigma_x = 1.0; sigma_y = 2.0; hbr = 0.010 }
217
-
in
218
-
let pc3 = Collision.pc_foster enc3 in
219
-
check_float "sign invariance y" ~eps:1e-10 pc1 pc3
93
+
if rel_diff > 0.05 then
94
+
failf "Foster (%.6e) vs Chan (%.6e) disagree: rel_diff=%.2e" pc_f pc_c
95
+
rel_diff
220
96
221
97
let suite =
222
98
( "collision",
223
99
[
224
-
Alcotest.test_case "small miss" `Quick test_small_miss;
225
-
Alcotest.test_case "large miss" `Quick test_large_miss;
226
-
Alcotest.test_case "head-on" `Quick test_head_on;
227
-
Alcotest.test_case "symmetry" `Quick test_symmetry;
228
-
Alcotest.test_case "scaling head-on" `Quick test_scaling_head_on;
229
-
Alcotest.test_case "Pc bounds" `Quick test_pc_bounds;
230
-
Alcotest.test_case "Pc_max bounds" `Quick test_pc_max_always_bounds;
231
-
Alcotest.test_case "Foster = Chan" `Quick test_foster_chan_agree;
232
-
Alcotest.test_case "monotonicity" `Quick test_monotonicity;
233
-
Alcotest.test_case "HBR scaling" `Quick test_hbr_scaling;
234
-
Alcotest.test_case "sign invariance" `Quick test_sign_invariance;
100
+
test_case "Pc in [0,1]" [ encounter_gen ] test_pc_in_unit_interval;
101
+
test_case "Pc_max bounds Pc" [ encounter_gen ] test_pc_max_bounds_pc;
102
+
test_case "sign invariance x" [ encounter_gen ] test_sign_invariance_x;
103
+
test_case "sign invariance y" [ encounter_gen ] test_sign_invariance_y;
104
+
test_case "xy symmetry" [ encounter_gen ] test_xy_symmetry;
105
+
test_case "Foster = Chan" [ encounter_gen ] test_foster_chan_agree;
235
106
] )