Add API reference to docs

Author: Zinoex

docs/make.jl

@@ -10,14 +10,24 @@ DocMeta.setdocmeta!(
 
 makedocs(;
     modules = [IntervalMDPAbstractions],
-    authors = "Frederik Baymler Mathiesen",
+    authors = "Frederik Baymler Mathiesen <[email protected]> and contributors",
     sitename = "IntervalMDPAbstractions.jl",
     format = Documenter.HTML(;
-        canonical = "https://Zinoex.github.io/IntervalMDPAbstractions.jl",
+        prettyurls = get(ENV, "CI", "false") == "true",
+        canonical = "https://www.baymler.com/IntervalMDPAbstractions.jl",
         edit_link = "main",
         assets = String[],
     ),
-    pages = ["Home" => "index.md"],
+    pages = [
+        "Home" => "index.md"
+        "Reference" => Any[
+            "Dynamics" => "reference/dynamics.md",
+            "Specifications" => "reference/specifications.md",
+            "Abstractions" => "reference/abstractions.md",
+        ]
+    ],
+    doctest = true,
+    checkdocs = :exports
 )
 
 deploydocs(; repo = "github.com/Zinoex/IntervalMDPAbstractions.jl", devbranch = "main")

docs/src/index.md

@@ -6,9 +6,3 @@ CurrentModule = IntervalMDPAbstractions
 
 Documentation for [IntervalMDPAbstractions](https://github.com/Zinoex/IntervalMDPAbstractions.jl).
 
-```@index
-```
-
-```@autodocs
-Modules = [IntervalMDPAbstractions]
-```

docs/src/reference/abstractions.md

@@ -0,0 +1,49 @@
+# Abstractions
+To build an abstraction, in addition to the definition of the system dynamics and the specification, 
+we also need to define select inputs and partition the state space/region of interest.
+Since there are multiple options for both, we wrap them as input and state abstractions, such that
+the [`abstraction`](@ref) method to build the finite-state abstractions can ignore the details of
+the choice of input and state partitioning.
+
+## Input abstractions
+```@docs
+InputAbstraction
+InputGridSplit
+InputLinRange
+InputDiscrete
+inputs
+numinputs
+```
+
+To define a new input abstraction, introduce a new struct type that inherits from `InputAbstraction` and
+implements `inputs` and `numinputs` methods. The `inputs` method should return the set of inputs (set-based, singletons, or discrete)
+and the `numinputs` should return the number of inputs in the set.
+
+## State abstractions
+
+```@docs
+StateAbstraction
+StateUniformGridSplit
+regions
+numregions
+statespace
+```
+
+Right now, we only support state abstractions that are based on a uniform grid split of the state space. However, one
+can easily imagine a non-uniform grid or a refinement-based partitioning for heterogenous abstractions. To implement such a state abstraction,
+define a new struct type that inherits from `StateAbstraction` and implements `regions`, `numregions`, and `statespace` methods.
+
+## Target models
+```@docs
+IMDPTarget
+SparseIMDPTarget
+OrthogonalIMDPTarget
+SparseOrthogonalIMDPTarget
+MixtureIMDPTarget
+SparseMixtureIMDPTarget
+```
+
+## Constructing finite-state abstractions
+```@docs
+abstraction
+```

docs/src/reference/dynamics.md

@@ -0,0 +1,47 @@
+# Dynamics
+
+## General
+```@docs
+DiscreteTimeStochasticDynamics
+dimstate
+diminput
+System
+dynamics
+initial
+```
+
+## Additive noise systems
+```@docs
+AdditiveNoiseDynamics
+nominal
+prepare_nominal
+noise
+AffineAdditiveNoiseDynamics
+NonlinearAdditiveNoiseDynamics
+UncertainPWAAdditiveNoiseDynamics
+UncertainAffineRegion
+```
+
+### Additive noise structures
+```@docs
+AdditiveNoiseStructure
+AdditiveDiagonalGaussianNoise
+AdditiveCentralUniformNoise
+```
+
+## Abstracted Gaussian processes
+```@docs
+AbstractedGaussianProcess
+AbstractedGaussianProcessRegion
+gp_bounds
+region
+mean_lower
+mean_upper
+stddev_lower
+stddev_upper
+```
+
+## Stochastic switched systems
+```@docs
+StochasticSwitchedDynamics
+```

docs/src/reference/specifications.md

@@ -0,0 +1,21 @@
+# Specification
+
+```@docs
+FiniteTimeRegionReachability
+InfiniteTimeRegionReachability
+FiniteTimeRegionReachAvoid
+InfiniteTimeRegionReachAvoid
+FiniteTimeRegionSafety
+InfiniteTimeRegionSafety
+reach
+avoid
+dim
+```
+
+## Abstraction problem
+
+```@docs
+AbstractionProblem
+system
+specification
+```

docs/src/reference/systems.md

@@ -76,9 +76,20 @@ end
 # IMDP target #
 ###############
 """
-    abstraction(prob::AbstractionProblem, state_abstraction::StateUniformGridSplit, input_abstraction::InputAbstraction, target_model::AbstractIMDPTarget)
+    abstraction(prob, state_abstraction::StateUniformGridSplit, input_abstraction, target_model::AbstractIMDPTarget)
 
-Abstract function for creating an abstraction of a system with additive noise with an IMDP as the target model.
+Construct an abstraction of a system and a specification under a uniform grid partitioning of the state space with an arbitrary input abstraction
+and an IMDP as the target model.
+
+The argument `prob` contains both the system and the specification. The type of the system determines how the transition probability bounds are computed.
+The resulting IMDP has `numregions(state_abstraction) + 1` states, where the last state is an absorbing state, representing transitioning to outside
+the partitioned region. This absorbing state is implicitly encoded in the ambiguity sets, i.e. not stored and automatically handled by `IntervalMDP.jl`.
+
+The specification is converted based on the `state_abstraction` and `target_model` arguments in addition to whether the specification is pessimistic or optimistic.
+To encode the specification, at least one avoid state is required, i.e. the last, absorbing state. As a consequence, (concrete) reachability specifications are
+converted to (abstract) reach-avoid specifications with the last state as the avoid state.
+
+Returns `mdp` and `spec` as the abstracted IMDP and the converted specification, respectively.
 """
 function abstraction(
     prob::AbstractionProblem,
@@ -218,9 +229,21 @@ end
 # Orthogonal IMDP target #
 ##########################
 """
-    abstraction(prob::AbstractionProblem, state_abstraction::StateUniformGridSplit, input_abstraction::InputAbstraction, target_model::AbstractOrthogonalIMDPTarget)
+    abstraction(prob, state_abstraction::StateUniformGridSplit, input_abstraction, target_model::AbstractOrthogonalIMDPTarget)
+
+Construct an abstraction of a system and a specification under a uniform grid partitioning of the state space with an arbitrary input abstraction
+and an orthogonal IMDP as the target model.
+
+The argument `prob` contains both the system and the specification. The type of the system determines how the *marginal* transition probability bounds are computed.
+The resulting *orthogonal* IMDP has `IntervalMDPAbstractions.splits(state_abstraction) .+ 1` states along each axis, 
+where the last state along each axis is an absorbing state, representing transitioning to outside the partitioned region.
+This absorbing state for each axis is implicitly encoded in the ambiguity sets, i.e. not stored and automatically handled by `IntervalMDP.jl`.
 
-Abstract function for creating an abstraction of a system with additive noise with a decoupled IMDP as the target model.
+The specification is converted based on the `state_abstraction` and `target_model` arguments in addition to whether the specification is pessimistic or optimistic.
+To encode the specification, at least one avoid state is required, i.e. the last, absorbing state. As a consequence, (concrete) reachability specifications are
+converted to (abstract) reach-avoid specifications with the last state as the avoid state.
+
+Returns `mdp` and `spec` as the abstracted IMDP and the converted specification, respectively.
 """
 function abstraction(
     prob::AbstractionProblem,
@@ -411,9 +434,21 @@ end
 # Mixture IMDP target #
 #######################
 """
-    abstraction(prob::AbstractionProblem, state_abstraction::StateUniformGridSplit, input_abstraction::InputAbstraction, target_model::AbstractMixtureIMDPTarget)
+    abstraction(prob, state_abstraction::StateUniformGridSplit, input_abstraction, target_model::AbstractMixtureIMDPTarget)
+
+Construct an abstraction of a system and a specification under a uniform grid partitioning of the state space with an arbitrary input abstraction
+and a mixture of orthogonal IMDPs as the target model.
+
+The argument `prob` contains both the system and the specification. The type of the system determines how the *marginal mixture* transition probability bounds are computed.
+The resulting *mixture* IMDP has `IntervalMDPAbstractions.splits(state_abstraction) .+ 1` states along each axis, 
+where the last state along each axis is an absorbing state, representing transitioning to outside the partitioned region.
+This absorbing state for each axis is implicitly encoded in the ambiguity sets, i.e. not stored and automatically handled by `IntervalMDP.jl`.
+
+The specification is converted based on the `state_abstraction` and `target_model` arguments in addition to whether the specification is pessimistic or optimistic.
+To encode the specification, at least one avoid state is required, i.e. the last, absorbing state. As a consequence, (concrete) reachability specifications are
+converted to (abstract) reach-avoid specifications with the last state as the avoid state.
 
-Abstract function for creating an abstraction of a system with a mixture of orthogonal IMDPs as the target model.
+Returns `mdp` and `spec` as the abstracted IMDP and the converted specification, respectively.
 """
 function abstraction(
     prob::AbstractionProblem,

src/abstractions/abstraction.jl

@@ -1,8 +1,27 @@
-export InputAbstraction, InputGridSplit, InputLinRange, InputRandom, InputDiscrete
+export InputAbstraction, InputGridSplit, InputLinRange, InputDiscrete
 export inputs, numinputs
 
+"""
+    InputAbstraction
+
+Abstract type for input abstractions.
+"""
 abstract type InputAbstraction end
 
+"""
+    inputs(input::InputAbstraction)
+
+Return the set of inputs of a given input abstraction.
+"""
+function inputs end
+
+"""
+    numinputs(input::InputAbstraction)
+
+Return the number of inputs, i.e. the size of the set of inputs, of a given input abstraction.
+"""
+function numinputs end
+
 """
     InputGridSplit
 

src/abstractions/input_abstraction.jl

@@ -1,11 +1,16 @@
-export StateUniformGridSplit, numregions, statespace
+export StateAbstraction, StateUniformGridSplit, regions, numregions, statespace
 
+"""
+    StateAbstraction
+
+Abstract type for state abstractions.
+"""
 abstract type StateAbstraction end
 
 """
     StateUniformGridSplit
 
-State abstraction for splitting the state space into a grid.
+State abstraction for splitting the state space into a uniform grid.
 """
 struct StateUniformGridSplit{N,I<:Int,H<:AbstractHyperrectangle} <: StateAbstraction
     state_space::H
@@ -19,6 +24,25 @@ function StateUniformGridSplit(state_space::Hyperrectangle, splits::NTuple{N,Int
 end
 
 splits(state::StateUniformGridSplit) = state.splits
+
+"""
+    regions(state::StateUniformGridSplit)
+
+Return the regions of the state abstraction.
+"""
 regions(state::StateUniformGridSplit) = state.regions
+
+"""
+    numregions(state::StateUniformGridSplit)
+
+Return the number of regions of the state abstraction.
+"""
 numregions(state::StateUniformGridSplit) = prod(state.splits)
+
+"""
+    statespace(state::StateUniformGridSplit)
+
+Return the state space of the state abstraction. This should must be a hyperrectangle
+and should be equal to the union of the regions.
+"""
 statespace(state::StateUniformGridSplit) = state.state_space

src/abstractions/state_abstraction.jl

@@ -1,4 +1,3 @@
-export TargetAbstractionModel
 export IMDPTarget, SparseIMDPTarget
 export OrthogonalIMDPTarget, SparseOrthogonalIMDPTarget
 export MixtureIMDPTarget, SparseMixtureIMDPTarget
@@ -48,13 +47,13 @@ abstract type AbstractOrthogonalIMDPTarget <: TargetAbstractionModel end
     OrthogonalIMDPTarget
 
 A target for IMDP abstractions where, for each source state, the transition probabilities
-are orthogonally decomposed. One state is appended along each axis to capture the transitions
+are orthogonally decomposed [1]. One state is appended along each axis to capture the transitions
 to outside the partitioned region. 
 
 Benefits compared to `IMDPTarget` include less memory usage, faster computation of the
 transition probabilities and value iteration, and tighter uncertainty set (see [1] for a proof).
 
-[1] TODO: Add reference to paper.
+[1] Mathiesen, Frederik Baymler, Sofie Haesaert, and Luca Laurenti. "Scalable control synthesis for stochastic systems via structural IMDP abstractions." arXiv preprint arXiv:2411.11803 (2024).
 """
 struct OrthogonalIMDPTarget <: AbstractOrthogonalIMDPTarget end
 
@@ -82,13 +81,13 @@ abstract type AbstractMixtureIMDPTarget <: AbstractOrthogonalIMDPTarget end
     MixtureIMDPTarget
 
 A target for IMDP abstractions where, for each source state, the transition probabilities
-are Mixturely decomposed. One state is appended along each axis to capture the transitions
+are decomposed as a mixture [1]. One state is appended along each axis to capture the transitions
 to outside the partitioned region. 
 
-Benefits compared to `IMDPTarget` include less memory usage, faster computation of the
-transition probabilities and value iteration, and tighter uncertainty set (see [1] for a proof).
+Benefits compared to `IMDPTarget` include less memory usage and faster computation of the
+transition probabilities and value iteration.
 
-[1] TODO: Add reference to paper.
+[1] Mathiesen, Frederik Baymler, Sofie Haesaert, and Luca Laurenti. "Scalable control synthesis for stochastic systems via structural IMDP abstractions." arXiv preprint arXiv:2411.11803 (2024).
 """
 struct MixtureIMDPTarget <: AbstractMixtureIMDPTarget end