From 5c1013950dfd72416473fc4b1da3b2904b0b072e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 2 Feb 2024 15:25:53 +0100
Subject: [PATCH] [kernel] Minor fixes to Linear_filter documentation.

---
 .../analysis/filter/linear_filter.mli            | 16 +++++++++-------
 .../analysis/filter/linear_filter_test.ml        | 10 ++++++++--
 .../analysis/filter/linear_filter_test.mli       |  1 +
 3 files changed, 18 insertions(+), 9 deletions(-)

diff --git a/src/kernel_services/analysis/filter/linear_filter.mli b/src/kernel_services/analysis/filter/linear_filter.mli
index e22d3f7bfb2..352c681ada8 100644
--- a/src/kernel_services/analysis/filter/linear_filter.mli
+++ b/src/kernel_services/analysis/filter/linear_filter.mli
@@ -26,17 +26,19 @@ open Finite
 (* A filter corresponds to the recursive equation
    X[k + 1] = AX[k] + Bε[k + 1] + C where :
    - n is the filter's order and m its number of inputs ;
-   - X[k]∈ ℝ^n is the filter's state at iteration [k] ;
-   - ε[k]∈ ℝ^m is the filters's inputs at iteration [k] ;
-   - A∈ ℝ^(n×n) is the filter's state matrix ;
-   - B∈ ℝ^(n×m) is the filter's input matrix ;
-   - C∈ ℝ^n is the filter's center.
+   - X[k] ∈ ℝ^n is the filter's state at iteration [k] ;
+   - ε[k] ∈ ℝ^m is the filters's inputs at iteration [k] ;
+   - A ∈ ℝ^(n×n) is the filter's state matrix ;
+   - B ∈ ℝ^(n×m) is the filter's input matrix ;
+   - C ∈ ℝ^n is the filter's center.
 
    The goal of this module is to compute filters invariants, i.e bounds for
    each of the filter's state dimensions when the iterations goes to infinity.
    To do so, it only suppose that, at each iteration, each input εi is bounded
    by [-λi .. λi]. Each input is thus supposed centered around zero but each
-   one can have different bounds. *)
+   one can have different bounds.
+
+   {!Linear_filter_test} is an example using this module. *)
 module Make (Field : Field.S) : sig
 
   module Linear : module type of Linear.Space (Field)
@@ -71,7 +73,7 @@ module Make (Field : Field.S) : sig
      lower than one. For the filter to converge, there must exist an α such as,
      for every β greater than α, ||A^β|| < 1 with A the filter's state matrix.
      As such, the search does not have to find α, but instead any exponent such
-     as the property is satisfies. As the computed invariant will be more
+     as the property is satisfied. As the computed invariant will be more
      precise with a larger exponent, the computation always uses [k], the
      largest authorized exponent, and thus only check that indeed ||A^k|| < 1.
      If the property is not verified, the function returns None as it cannot
diff --git a/src/kernel_services/analysis/filter/linear_filter_test.ml b/src/kernel_services/analysis/filter/linear_filter_test.ml
index 6634aef53e7..f239d3adbee 100644
--- a/src/kernel_services/analysis/filter/linear_filter_test.ml
+++ b/src/kernel_services/analysis/filter/linear_filter_test.ml
@@ -20,8 +20,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
-
 module Rational = struct
 
   type scalar = Q.t
@@ -80,6 +78,10 @@ let pretty_invariant order fmt = function
 
 
 
+(* Invariant computation for the filter:
+     X = 0.68 * X - 0.68 * Y + E1;
+     Y = 0.68 * X + 0.68 * Y + E2;
+   with E1 ∈ [-1 .. 1] and E2 ∈ [-1 .. 1]. *)
 module Circle = struct
 
   let order = Nat.(succ one)
@@ -106,6 +108,10 @@ end
 
 
 
+(* Invariant computation for the filter:
+     X = 1.5 * X - 0.7 * Y + E + 1;
+     Y = X + 1;
+   with E ∈ [-0.1 .. 0.1]. *)
 module Simple = struct
 
   let order = Nat.(succ one)
diff --git a/src/kernel_services/analysis/filter/linear_filter_test.mli b/src/kernel_services/analysis/filter/linear_filter_test.mli
index cc9eb1f5468..e973f651b1a 100644
--- a/src/kernel_services/analysis/filter/linear_filter_test.mli
+++ b/src/kernel_services/analysis/filter/linear_filter_test.mli
@@ -20,4 +20,5 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Tests the Linear_filter module: invariant computation of filters. *)
 val run : unit -> unit
-- 
GitLab