Merge pull request #748 from JuliaReach/schillic/spellcheck

Spell check

.github/workflows/SpellCheck.yml

@@ -0,0 +1,13 @@
+name: Spell Check
+
+on: [pull_request]
+
+jobs:
+  typos-check:
+    name: check spelling
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Actions Repository
+        uses: actions/checkout@v4
+      - name: Check spelling
+        uses: crate-ci/typos@master

.typos.toml

@@ -0,0 +1,13 @@
+[default.extend-words]
+# do not correct the following strings:
+fpr = "fpr"
+PLAD = "PLAD"
+Childs = "Childs"
+OT = "OT"
+ND = "ND"
+GIR = "GIR"
+AKS = "AKS"
+
+[files]
+# do not check the following files:
+extend-exclude = ["references.md"]

README.md

@@ -168,13 +168,13 @@ plot(sol, vars=(1, 2), xlab="x", ylab="v", lw=0.5, color=:red)
 
 ## :blue_book: Publications
 
-This library has been applied in a number of scientic works. 
+This library has been applied in a number of scientific works.
 
 <details>
 <summary>Click to see the full list of publications that use ReachabilityAnalysis.jl.</summary>
-  
+
 We list them in reverse chronological order.
-  
+
 [11] **Combining Set Propagation with Finite Element Methods for Time Integration in Transient Solid Mechanics Problems.** Forets, Marcelo, Daniel Freire Caporale, and Jorge M. Pérez Zerpa. arXiv preprint [arXiv:2105.05841](https://arxiv.org/abs/2105.05841). Accepted in Computers & Structures (2021).
 
 [10] **Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions.** Marcelo Forets, Daniel Freire, Christian Schilling, 2020. [arXiv: 2006.12325](https://arxiv.org/abs/2006.12325). Published in
@@ -203,7 +203,7 @@ Schilling (2020) ARCH20. To appear in 7th International Workshop on Applied Veri
 *Note:* Articles [1-7] use the former codebase `Reachability.jl`.
 
 </details>
-  
+
 ## 📜  How to cite
 
 Research credit and full references to the scientific papers presenting the algorithms implemented in this package can be found in the source code for each algorithm and in the [References](https://juliareach.github.io/ReachabilityAnalysis.jl/dev/references/) section of the online documentation.

docs/src/lib/discretize.md

@@ -38,7 +38,7 @@ compute exponential matrices. There are distinct ways to compute the matrix
 exponential $e^{A\delta}$ depending on the type of $A$
 (see e.g. [^HIH08]). The available methods can be used through the (unexported) function `_exp`.
 
-For high dimensional systems (typicall `n > 2000`), computing the matrix exponential
+For high dimensional systems (typically `n > 2000`), computing the matrix exponential
 is expensive hence it is preferable to compute the action of the matrix exponential
 over vectors when needed, that is, $e^{δA} v$ for each $v$. This method is particularly
 well-suited if `A` is vert sparse. Use the option `exp=:krylov` (or `exp=:lazy`) for this purpose.

docs/src/lib/systems.md

@@ -11,7 +11,7 @@ Depth = 3
 
 ## Types and macros
 
-The API reference for systms types and macros can be found in the
+The API reference for systems types and macros can be found in the
 [MathematicalSystems.jl](https://juliareach.github.io/MathematicalSystems.jl/latest/man/systems/)
 documentation. Two commonly used macros are `@system` and `@ivp`, used to
 define a system and an initial-value problem respectively.

docs/src/man/algorithms/LGG09.md

@@ -98,7 +98,7 @@ using the methods described above. Once both computations have finished, we can
 the resulting support functions in the same array. Use the flag `threaded=true` to
 use this method.
 
-Implementation-wise the function `_reach_homog_dir_LGG09!` spawns differen threads
+Implementation-wise the function `_reach_homog_dir_LGG09!` spawns different threads
 which populate the matrix `ρℓ::Matrix{N}(undef, length(dirs), NSTEPS)` with the computed
 values. Hence each thread computes a subset of distinct rows of `ρℓ`.
 
@@ -145,6 +145,6 @@ $\lambda^k$ is positive if $k$ is even, otherwise it is negative. So we can writ
 ```math
 \rho(d, X_k) = (-\lambda)^k \rho((-1)^k d, X_0) + \sum_{i=0}^{k-1} (-\lambda)^{k-i-1} \rho((-1)^{k-i-1} d, V_i).
 ```
-The main difference between this case and the previus one is that now we have to evaluate
+The main difference between this case and the previous one is that now we have to evaluate
 support functions $\rho(\pm d, X_0)$ and $\rho(\pm d, V_i)$. Again, simplification takes place
 if the $V_i$'s are constant and such special case is considered in the implementation.

docs/src/man/algorithms/ORBIT.md

@@ -48,7 +48,7 @@ The matrix $\Phi = e^{A\delta}$ can be evaluated in different ways, using the fu
 
 (1) `method=:base` uses Julia's built-in implementation (if `method = :base`),
 
-(2) `method = :lazy` uses a lazy wrapper of the matrix exponential which is then evaluted using Krylov subspace methods.
+(2) `method = :lazy` uses a lazy wrapper of the matrix exponential which is then evaluated using Krylov subspace methods.
 
 Method (1) is the default method. Method (2) is particularly useful to work with very large and sparse matrices (e.g. typically of order `n > 2000`). Evaluation of $\Phi_1(u, \delta)$ is available through the function [`Φ₁`](@ref). Two implementations are available:
 

docs/src/man/algorithms/VREP.md

@@ -33,7 +33,7 @@ polygons (e.g. convex hull, Minkowski sum) implemented in
 [LazySets.jl](https://github.com/JuliaReach/LazySets.jl/).
 On the other hand, for systems of dimension higher than two, concrete polyhedral
 computations use the [Polyhedra.jl](https://github.com/JuliaPolyhedra/Polyhedra.jl)
-libary which itself relies on specific *backends*, which
+library which itself relies on specific *backends*, which
 can be specified with the `backend` keyword argument in the `VREP` algorithm constructor.
 Such backend is used in the discretization phase. Actually, `Polyhedra.jl` features a default
 solver (hence it doesn't require additional packages apart from `Polyhedra.jl` itself),

docs/src/man/benchmarks/filtered_oscillator.md

@@ -12,7 +12,7 @@ model from [[FRE11]](@ref). The model consists of a two-dimensional switched osc
 and a parametric number of filters which are used to *smooth* the oscilllator's state.
 An interesting aspect of the model is that it is scalable: the total number of continuous
 variables can be made arbitrarily large. Moreover, this is a challenging benchmark
-since several dozens of reach-sets may take each discrete jumps, hence clustering methods are indispensible.
+since several dozens of reach-sets may take each discrete jumps, hence clustering methods are indispensable.
 
 The continuous variables ``x`` and ``y`` are used to denote the state of the oscillator,
 and the remaining ``m`` variables are used for the state of the filters.

docs/src/man/examples_overview.md

@@ -9,7 +9,7 @@ We organize the models by the type of nonlinearities (if there are some), and
 whether they are purely continuous or present discrete transitions, i.e. hybrid systems.
 We have added a column with the associated scientific domain, and another column with
 the number of state variables. Roughly speaking, a higher number of state variables
-usually correspnds to problems which are harder to solve, altough strictly speaking,
+usually corresponds to problems which are harder to solve, although strictly speaking,
 this usually depends on the property to be verified.
 
 Column `P.V.` refers to the cases

docs/src/man/faq.md

@@ -204,7 +204,7 @@ As it is seen in the question *Can I solve a for a single initial condition?*,
 even if the initial condition is a singleton, the obtained flowpipe is a sequence
 of boxes in the `x-t` plane, i.e. we obtain sets with non-zero width both in time
 and in space. This behavior may seem confusing at first, because the initial conditions
-where determinitic. The catch is that reach-sets represents a set of states
+where deterministic. The catch is that reach-sets represents a set of states
 reachable over a *time interval*, that certainly contains the exact solution for
 the time-span associated to the reach-set, `tspan(R)`. The projection of the flowpipe
 on the time axis thus returns a sequence of intervals, their width being the

docs/src/man/introduction.md

@@ -28,7 +28,7 @@ f(t, x0) = x0 * exp(-t)
 plot!(t -> f(t, 0.45), xlims=(0, 4), label="Analytic sol., x(0) = 0.45", color="red")
 plot!(t -> f(t, 0.55), xlims=(0, 4), label="Analytic sol., x(0) = 0.55", color="red")
 ```
-In practice, analytic solutons of ODEs are unknown. However, in this simple case
+In practice, analytic solutions of ODEs are unknown. However, in this simple case
 we knew that for an initial point $x_0 \in \mathbb{R}$, the solution is
 $x(t) = x_0 e^{-t}$ so we plotted the trajectories associated to the extremal
 values in the given initial interval.

docs/src/man/structure.md

@@ -15,7 +15,7 @@ that we want to perform on the outputs.
 of a given linear system.
 
 - Method to lazily compute the flowpipe when we are only interested in outputs.
-- Example with linear combination of state varibles with LGG09 (eg. some of SLICOT benchmaris properties).
+- Example with linear combination of state variables with LGG09 (eg. some of SLICOT benchmarks properties).
 
 ## State-space decomposition
 

docs/src/man/systems.md

@@ -8,7 +8,7 @@ from `AbstractSystem`.
 
 ## Linear systems
 
-Two commonly used types of systems are discrete and continous systems.
+Two commonly used types of systems are discrete and continuous systems.
 
 **Discrete systems.** A discrete system consists of a matrix representing the system dynamics, a set
 of initial states, a set of nondeterministic inputs, and a discretization step

docs/src/tutorials/linear_methods/discrete_time.md

@@ -202,7 +202,7 @@ fig = plot(F, vars=(1, 2), ratio=1.)
 fig = DisplayAs.Text(DisplayAs.PNG(fig))  # hide
 ```
 
-Flowpipes implement Julia's array inteface.
+Flowpipes implement Julia's array interface.
 
 ```@example discrete_propagation
 length(F)

docs/src/tutorials/set_representations/distances.md

@@ -7,7 +7,7 @@ CurrentModule = ReachabilityAnalysis
 
 ## Hausdorff distance
 
-Tthe notion of Hausdorff distance can be used to *measure* the distance between sets.
+The notion of Hausdorff distance can be used to *measure* the distance between sets.
 It constitutes a practical theoretical tool to quantify the quality of an approximation.
 
 ```math

docs/src/tutorials/set_representations/polyhedral_computations.md

@@ -11,10 +11,8 @@ CurrentModule = ReachabilityAnalysis
 
 ## Limitations
 
-Computing with concrete polyhedra in high dimensions is generally expensive. In particular, converting between vertex and constraint reprsentations (so-called dual representations) should be used only if it is strictly necessary. However, there are some operations that are cheap:
+Computing with concrete polyhedra in high dimensions is generally expensive. In particular, converting between vertex and constraint representations (so-called dual representations) should be used only if it is strictly necessary. However, there are some operations that are cheap:
 
 - Intersecting two (or more) sets in constraint representation, or whose `constraints_list` can be computed efficiently. Such computation only requires concatenating the constraints and removing redundant inequalities (operation that requires the solution of linear programs).
 
 - Taking linear maps of sets in vertex representation, $MX$. This operation requires to map each vertex of $X$ under the transformation $M$. Linear transformations can also be done efficiently in constraint representation provided that the matrix $M$ is invertible. LazySets handles other cases ($M$ not invertible, and the sets either in constraint or in vertex representation), but they are generally expensive in high dimensions. However, using specific classes of sets (e.g. zonotopes).
-
--

docs/src/tutorials/set_representations/zonotopes.md

@@ -28,7 +28,7 @@ a finite number of generators $g_1, . . . , g_p ∈ \mathbb{R}^n$ such that
 Z = \left\{ c + \sum_{i=1}^{p} \xi_i g_i | \xi_i ∈ [−1, 1]\right\}.
 ```
 It is common to note $Z = (c, \langle g_1 . . . , g_p \rangle)$ or simply
-$Z = (c, G)$, where $g_i$ is the $i$-th column of $G$. In the examle of above,
+$Z = (c, G)$, where $g_i$ is the $i$-th column of $G$. In the example above,
 
 ```@example zonotope_definition
 @show center(Z)

examples/ISS/ISS.jl

@@ -18,7 +18,7 @@
 #   y(t) & = & C x(t)
 #   \end{array}
 # ```
-# It was proposed as a benchmark in ARCH 2016 [^TLT16]. The matrix dimensiones are
+# It was proposed as a benchmark in ARCH 2016 [^TLT16]. The matrix dimensions are
 # ``A ∈ \mathbb{R}^{270\times 270}``, ``B ∈ \mathbb{R}^{270\times 3}`` and
 # ``C ∈ \mathbb{R}^{3\times 270}``.
 

examples/Lorenz/Lorenz.jl

@@ -85,7 +85,7 @@ fig = plot(solz; vars=(0, 2), xlab="t", ylab="y")
 #!jl DisplayAs.Text(DisplayAs.PNG(fig))  #hide
 
 # Since we have computed overapproximations of the exact flowipe, the following
-# quantities are a lower bound on the exact minimum (resp. an uppper bound on the
+# quantities are a lower bound on the exact minimum (resp. an upper bound on the
 # exact maximum):
 
 -ρ([0.0, -1.0, 0.0], solz)

examples/OpAmp/OpAmp.jl

@@ -230,7 +230,7 @@ X0 = Singleton(zeros(2));
 
 #-
 
-# We solve both instances by choosing som values of ``δ`` and ``γ``:
+# We solve both instances by choosing some values for ``δ`` and ``γ``:
 
 ## linearly increasing input signal
 prob_lin = opamp_with_saturation(; X0=X0, γ=0.0, δ=100.0, Es=1.0);

examples/Platoon/Platoon.jl

@@ -154,7 +154,7 @@ function platoon(; deterministic_switching::Bool=true,
 
     H = HybridSystem(automaton, modes, resetmaps, [AutonomousSwitching()])
 
-    ## initial condition is at the orgin in mode 1
+    ## initial condition is at the origin in mode 1
     X0 = BallInf(zeros(n), 0.0)
     initial_condition = [(1, X0)]
 
@@ -217,7 +217,7 @@ sol_PLAD01_BND42 = solve(prob_PLAD01;
 dmin_specification(sol_PLAD01_BND42, 42)
 
 # In more detail we can check how is the flowpipe from violating the property.
-# The specification requires that each of the follwing quantities is greater
+# The specification requires that each of the following quantities is greater
 # than `-dmin = -42`.
 
 # Minimum of ``x_1(t)``:

examples/ProductionDestruction/ProductionDestruction.jl

@@ -68,7 +68,7 @@ using ReachabilityAnalysis, Symbolics, Plots
 const positive_orthant = HPolyhedron([x >= 0, y >= 0, z >= 0], [x, y, z])
 
 # Given a set $X \subseteq \mathbb{R}^n$, to check whether the positivity constraint
-# holds correspnods to checking wheter ``X`` is included in the positive orthant.
+# holds corresponds to checking whether ``X`` is included in the positive orthant.
 # This computation can be done efficiently using support functions, and it is available
 # in `LazySets.jl`. Multiple dispatch takes care based on the types of the arguments
 # in the call `X ⊆ positive_orthant` depending on the type of ``X``.
@@ -173,7 +173,7 @@ fig = plot(solP; vars=(0, 3), linecolor=:blue, color=:blue, alpha=0.3, lab="P")
 
 # ## Case I & P
 
-# When uncertainty in both the intial states and the paramters are present, we can
+# When uncertainty in both the initial states and the parameters are present, we can
 # reuse the function `prod_dest_IP!`, but setting an uncertain initial condition
 # and an uncertain parameter.
 # Recall that we are interested in ``x(0) \in [9.5, 10.0]`` and ``a \in [0.296, 0.304]``.

examples/TransmissionLine/TransmissionLine.jl

@@ -111,7 +111,7 @@ function tline(; η=3, R=1.00, Rd=10.0, L=1e-10, C=1e-13 * 4.00)
     return A, B
 end
 
-# We can visualize the structure of the cofficients matrix ``A`` for the case
+# We can visualize the structure of the coefficients matrix ``A`` for the case
 # $\eta = 20$ with `spy` plot:
 
 using Plots

src/Algorithms/ASB07/post.jl

@@ -43,7 +43,7 @@ function post(alg::ASB07{N}, ivp::IVP{<:AbstractContinuousSystem}, tspan;
         reach_homog_ASB07!(F, Ω0, Φ, NSTEPS, δ, max_order, X, recursive, reduction_method, Δt0)
     else
         U = inputset(ivp_discr)
-        @assert isa(U, LazySet) "expcted input of type `<:LazySet`, but got $(typeof(U))"
+        @assert isa(U, LazySet) "expected input of type `<:LazySet`, but got $(typeof(U))"
         U = _convert_or_overapproximate(Zonotope, U)
         reach_inhomog_ASB07!(F, Ω0, Φ, NSTEPS, δ, max_order, X, U, recursive, reduction_method, Δt0)
     end

src/Algorithms/BFFPSV18/BFFPSV18.jl

@@ -18,7 +18,7 @@ Implementation of the reachability method for linear systems using block decompo
                       after discretization
 - `sparse`        -- (optional, default: `false`) if `true`, assume that the state transition
                       matrix is sparse
-- `view`          -- (optional, default: `false`) if `true`, use implementaton that
+- `view`          -- (optional, default: `false`) if `true`, use implementation that
                      uses arrays views
 
 matrix is sparse
@@ -53,7 +53,7 @@ TODO:
 ### References
 
 This algorithm is essentially an extension of the method in [[BFFPSV18]](@ref).
-Blocks can have different dimensions and the set represenation can be different
+Blocks can have different dimensions and the set representation can be different
 for each block.
 
 For a general introduction we refer to the dissertation [[SCHI18]](@ref).

src/Algorithms/BOX/post.jl

@@ -32,7 +32,7 @@ function post(alg::BOX{N}, ivp::IVP{<:AbstractContinuousSystem}, tspan;
     Ω0 = _overapproximate(Ω0, Hyperrectangle)
 
     # reconvert the set of initial states and state matrix, if needed
-    #static = haskey(kwargs, :static) ? kwargs[:static] : alg.stati
+    #static = haskey(kwargs, :static) ? kwargs[:static] : alg.static
 
     Ω0 = _reconvert(Ω0, static, dim)
     Φ = _reconvert(Φ, static, dim)
@@ -46,7 +46,7 @@ function post(alg::BOX{N}, ivp::IVP{<:AbstractContinuousSystem}, tspan;
         reach_homog_BOX!(F, Ω0, Φ, NSTEPS, δ, X, recursive, Δt0)
     else
         U = inputset(ivp_discr)
-        @assert isa(U, LazySet) "expcted input of type `<:LazySet`, but got $(typeof(U))"
+        @assert isa(U, LazySet) "expected input of type `<:LazySet`, but got $(typeof(U))"
         # TODO: can we use support function evaluations for the input set?
         U = overapproximate(U, Hyperrectangle)
         reach_inhomog_BOX!(F, Ω0, Φ, NSTEPS, δ, X, U, recursive, Δt0)

src/Algorithms/GLGM06/reach_homog.jl

@@ -75,7 +75,7 @@ function reach_homog_GLGM06!(F::Vector{ReachSet{N,Zonotope{N,Vector{N},Matrix{N}
     return F
 end
 
-# check interection with invariant on the loop
+# check intersection with invariant on the loop
 function reach_homog_GLGM06!(F::Vector{ReachSet{N,Zonotope{N,VN,MN}}},
                              Ω0::Zonotope{N,VN,MN},
                              Φ::AbstractMatrix,
@@ -104,7 +104,7 @@ function reach_homog_GLGM06!(F::Vector{ReachSet{N,Zonotope{N,VN,MN}}},
     return F
 end
 
-# check interection with invariant on the loop, implementation with zonotope preallocation
+# check intersection with invariant on the loop, implementation with zonotope preallocation
 function reach_homog_GLGM06!(F::Vector{ReachSet{N,Zonotope{N,Vector{N},Matrix{N}}}},
                              Ω0::Zonotope{N,Vector{N},Matrix{N}},
                              Φ::AbstractMatrix,

src/Algorithms/TMJets/common.jl

@@ -4,7 +4,7 @@ using TaylorModels: TaylorModelN
 using TaylorModels: fp_rpa, remainder, initialize!
 
 # =================================
-# Defaut values for the parameters
+# Default values for the parameters
 # =================================
 
 const DEFAULT_MAX_STEPS_TMJETS = 2000
@@ -20,7 +20,7 @@ The algorithm TMJets defaults to `TMJets21b`.
 const TMJets = TMJets21b
 
 # =======================================================================
-# Initialization funtions to prepare the input for validated integration
+# Initialization functions to prepare the input for validated integration
 # =======================================================================
 
 # fallback

src/Algorithms/VREP/post.jl

@@ -1,5 +1,5 @@
 # ===========================
-# Continous post interface
+# Continuous post interface
 # ===========================
 
 # this algorithm uses polygons (two dimensions) or polytopes (any dimension) in vertex representation

src/Continuous/fields.jl

@@ -56,7 +56,7 @@ end
 function outofplace_field(ivp::InitialValueProblem)
     vf = VectorField(ivp)
 
-    # function closure over the inital-value problem
+    # function closure over the initial-value problem
     f = function f_outofplace(x, p, t)
         return vf(x)
     end
@@ -67,7 +67,7 @@ end
 function inplace_field!(ivp::InitialValueProblem)
     vf = VectorField(ivp)
 
-    # function closure over the inital-value problem
+    # function closure over the initial-value problem
     f! = function f_inplace!(dx, x, p, t)
         return dx .= vf(x)
     end