Jc/update doc

docs/make.jl

@@ -2,14 +2,25 @@ using Dionysos
 using Documenter, Literate
 
 const EXAMPLES_DIR = joinpath(@__DIR__, "src", "examples")
+const EXAMPLES_SOLVERS_DIR = joinpath(@__DIR__, "src", "examples", "solvers")
+const EXAMPLES_UTILS_DIR = joinpath(@__DIR__, "src", "examples", "utils")
+
 const REFERENCE_DIR = joinpath(@__DIR__, "src", "reference")
 const OUTPUT_DIR = joinpath(@__DIR__, "src", "generated")
 
 const EXAMPLES = readdir(EXAMPLES_DIR)
+const EXAMPLES_SOLVERS = readdir(EXAMPLES_SOLVERS_DIR)
+const EXAMPLES_UTILS = readdir(EXAMPLES_UTILS_DIR)
 const REFERENCE = readdir(REFERENCE_DIR)
 
-for example in EXAMPLES
-    example_filepath = joinpath(EXAMPLES_DIR, example)
+for example in EXAMPLES_SOLVERS
+    example_filepath = joinpath(EXAMPLES_SOLVERS_DIR, example)
+    Literate.markdown(example_filepath, OUTPUT_DIR)
+    Literate.notebook(example_filepath, OUTPUT_DIR)
+    Literate.script(example_filepath, OUTPUT_DIR)
+end
+for example in EXAMPLES_UTILS
+    example_filepath = joinpath(EXAMPLES_UTILS_DIR, example)
     Literate.markdown(example_filepath, OUTPUT_DIR)
     Literate.notebook(example_filepath, OUTPUT_DIR)
     Literate.script(example_filepath, OUTPUT_DIR)
@@ -18,7 +29,13 @@ end
 const _PAGES = [
     "Index" => "index.md",
     "Manual" => ["manual/abstraction-based-control.md", "manual/manual.md"],
-    "Examples" => map(EXAMPLES) do jl_file
+    "Getting Started" => "generated/Getting Started.md",
+    "Solvers" => map(EXAMPLES_SOLVERS) do jl_file
+        # Need `string` as Documenter fails if `name` is a `SubString{String}`.
+        name = string(split(jl_file, ".")[1])
+        return name => "generated/$name.md"
+    end,
+    "Utils" => map(EXAMPLES_UTILS) do jl_file
         # Need `string` as Documenter fails if `name` is a `SubString{String}`.
         name = string(split(jl_file, ".")[1])
         return name => "generated/$name.md"

docs/src/examples/DC-DC converter.jl → docs/src/examples/solvers/DC-DC converter.jl

@@ -1,5 +1,5 @@
 using Test     #src
-# # Example: DC-DC converter
+# # Example: DC-DC converter solved by [Naive abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/DC-DC converter.ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/DC-DC converter.ipynb)
@@ -19,24 +19,13 @@ using Test     #src
 # A_1 = \begin{bmatrix} -\frac{r_l}{x_l} &0 \\ 0 & -\frac{1}{x_c}\frac{1}{r_0+r_c}  \end{bmatrix}, A_2= \begin{bmatrix} -\frac{1}{x_l}\left(r_l+\frac{r_0r_c}{r_0+r_c}\right) & -\frac{1}{x_l}\frac{r_0}{r_0+r_c}  \\ \frac{1}{x_c}\frac{r_0}{r_0+r_c}   & -\frac{1}{x_c}\frac{1}{r_0+r_c}  \end{bmatrix}, b = \begin{bmatrix} \frac{v_s}{x_l}\\0\end{bmatrix}.
 # ```
 # The goal is to design a controller to keep the state of the system in a safety region around the reference desired value, using as input only the switching
-# signal.
-#
-#
-# In order to study the concrete system and its symbolic abstraction in a unified framework, we will solve the problem
-# for the sampled system with a sampling time $\tau$.
-#
-# The abstraction is based on a feedback refinment relation [4,V.2 Definition].
-# Basically, this is equivalent to an alternating simulation relationship with the additional constraint that the input of the
-# concrete and symbolic system preserving the relation must be identical.
-# This allows to easily determine the controller of the concrete system from the abstraction controller by simply adding a quantization step.
-#
-# For the construction of the relations in the abstraction, it is necessary to over-approximate attainable sets of
-# a particular cell. In this example, we consider the used of a growth bound function  [4, VIII.2, VIII.5] which is one of the possible methods to over-approximate
-# attainable sets of a particular cell based on the state reach by its center. Therefore, it is used
-# to compute the relations in the abstraction based on the feedback refinement relation.
+# signal. In order to study the concrete system and its symbolic abstraction in a unified framework, we will solve the problem
+# for the sampled system with a sampling time $\tau$. For the construction of the relations in the abstraction, it is necessary to over-approximate attainable sets of
+# a particular cell. In this example, we consider the use of a growth bound function  [4, VIII.2, VIII.5] which is one of the possible methods to over-approximate
+# attainable sets of a particular cell based on the state reach by its center.
 #
 
-# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots].
+# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots](https://github.com/JuliaPlots/Plots.jl).
 
 using StaticArrays, Plots
 
@@ -66,7 +55,7 @@ hu = SVector(1)
 input_grid = DO.GridFree(u0, hu)
 
 using JuMP
-optimizer = MOI.instantiate(AB.SCOTSAbstraction.Optimizer)
+optimizer = MOI.instantiate(AB.NaiveAbstraction.Optimizer)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), concrete_problem)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), state_grid)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("input_grid"), input_grid)

docs/src/examples/Gol, Lazar & Belta (2013).jl → docs/src/examples/solvers/Gol, Lazar & Belta (2013).jl

@@ -1,5 +1,5 @@
 using Test     #src
-# # Example: Gol, Lazar and Belta (2013)
+# # Example: Gol, Lazar and Belta (2013) solved by [Bemporad Morari](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/Gol%2C Lazar %26 Belta (2013).ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/Gol%2C Lazar %26 Belta (2013).ipynb)

docs/src/examples/Hierarchical-abstraction.jl → docs/src/examples/solvers/Hierarchical-abstraction.jl

@@ -1,4 +1,4 @@
-# # Hierarchical-abstraction
+# # Example: Reachability problem solved by [Hierarchical abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/Hierarchical-abstraction.ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/Hierarchical-abstraction.ipynb)
@@ -17,7 +17,7 @@ const PR = DI.Problem
 const OP = DI.Optim
 const AB = OP.Abstraction
 
-include("../../../problems/simple_problem.jl")
+include(joinpath(dirname(dirname(pathof(Dionysos))), "problems", "simple_problem.jl"))
 
 ## specific functions
 function post_image(abstract_system, concrete_system, xpos, u)
@@ -125,11 +125,11 @@ AB.LazyAbstraction.set_optimizer_parameters!(
 )
 
 # Global optimizer parameters
-hx_global = [10.0, 10.0] #[15.0, 15.0]
+hx_global = [10.0, 10.0]
 u0 = SVector(0.0, 0.0)
 hu = SVector(0.5, 0.5)
 Ugrid = DO.GridFree(u0, hu)
-max_iter = 6 # 9
+max_iter = 6
 max_time = 1000
 
 optimizer = MOI.instantiate(AB.HierarchicalAbstraction.Optimizer)

docs/src/examples/Lazy-Ellipsoids-Abstraction.jl → docs/src/examples/solvers/Lazy-Ellipsoids-Abstraction.jl

@@ -1,3 +1,6 @@
+# # Example: Reachability problem solved by [Lazy ellipsoid abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
+#
+
 using StaticArrays, LinearAlgebra, Random, IntervalArithmetic
 using MathematicalSystems, HybridSystems
 using JuMP, Mosek, MosekTools
@@ -15,7 +18,7 @@ const PR = DI.Problem
 const OP = DI.Optim
 const AB = OP.Abstraction
 
-include("../../../problems/non_linear.jl")
+include(joinpath(dirname(dirname(pathof(Dionysos))), "problems", "non_linear.jl"))
 
 # # First example
 
@@ -95,23 +98,24 @@ fig = plot(;
     ytickfontsize = 10,
     guidefontsize = 16,
     titlefontsize = 14,
+    label = false,
 );
 xlabel!("\$x_1\$");
 ylabel!("\$x_2\$");
 title!("Specifictions and domains");
 
 #Display the concrete domain
-plot!(concrete_system.X; color = :yellow, opacity = 0.5);
+plot!(concrete_system.X; color = :yellow, opacity = 0.5, label = false);
 for obs in concrete_system.obstacles
-    plot!(obs; color = :black)
+    plot!(obs; color = :black, label = false)
 end
 
 #Display the abstract domain
-plot!(abstract_system; arrowsB = false, cost = false);
+plot!(abstract_system; arrowsB = false, cost = false, label = false);
 
 #Display the concrete specifications
-plot!(concrete_problem.initial_set; color = :green);
-plot!(concrete_problem.target_set; color = :red)
+plot!(concrete_problem.initial_set; color = :green, label = false);
+plot!(concrete_problem.target_set; color = :red, label = false)
 
 # # Display the abstraction
 fig = plot(;

docs/src/examples/Lazy-abstraction-reachability.jl → docs/src/examples/solvers/Lazy-abstraction-reachability.jl

@@ -1,4 +1,4 @@
-# # Lazy-abstraction-reachability
+# # Example: Reachability problem solved by [Lazy abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/Lazy-abstraction-reachability.ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/Lazy-abstraction-reachability.ipynb)
@@ -8,19 +8,14 @@
 #
 # In order to study the concrete system and its symbolic abstraction in a unified framework, we will solve the problem
 # for the sampled system with a sampling time $\tau$.
-#
-# The abstraction is based on a feedback refinment relation [1,V.2 Definition].
-# This allows to easily determine the controller of the concrete system from the abstraction controller by simply adding a quantization step.
-#
 # For the construction of the relations in the abstraction, it is necessary to over-approximate attainable sets of
 # a particular cell. In this example, we consider the used of a growth bound function  [1, VIII.2, VIII.5] which is one of the possible methods to over-approximate
-# attainable sets of a particular cell based on the state reach by its center. Therefore, it is used
-# to compute the relations in the abstraction based on the feedback refinement relation.
+# attainable sets of a particular cell based on the state reach by its center. 
 #
 # For this reachability problem, the abstraction controller is built using a solver that lazily builds the abstraction, constructing the abstraction 
 # at the same time as the controller.
 
-# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots].
+# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots](https://github.com/JuliaPlots/Plots.jl).
 using StaticArrays, JuMP, Plots
 
 # At this point, we import Dionysos.
@@ -34,7 +29,7 @@ const PR = DI.Problem
 const OP = DI.Optim
 const AB = OP.Abstraction
 
-include("../../../problems/simple_problem.jl")
+include(joinpath(dirname(dirname(pathof(Dionysos))), "problems", "simple_problem.jl"))
 
 ## specific functions
 function post_image(abstract_system, concrete_system, xpos, u)
@@ -126,9 +121,9 @@ AB.LazyAbstraction.set_optimizer!(
     Ugrid,
 )
 
-# Build the state feedback abstraction and solve the optimal control problem using A* algorithm
+# Build the abstraction and solve the optimal control problem using A* algorithm
 using Suppressor
-@suppress begin # this is a workaround to supress the undesired output of SDPA
+@suppress begin
     MOI.optimize!(optimizer)
 end
 
@@ -181,7 +176,13 @@ plot!(cost_control_trajectory; ms = 0.5)
 
 # # Display the abstraction and Lyapunov-like function
 fig = plot(; aspect_ratio = :equal);
-plot!(abstract_system; dims = [1, 2], cost = true, lyap_fun = optimizer.lyap_fun)
+plot!(
+    abstract_system;
+    dims = [1, 2],
+    cost = true,
+    lyap_fun = optimizer.lyap_fun,
+    label = false,
+)
 
 # # Display the Bellman-like value function (heuristic)
 fig = plot(; aspect_ratio = :equal)
@@ -191,12 +192,9 @@ plot!(
     dims = [1, 2],
     cost = true,
     lyap_fun = optimizer.bell_fun,
+    label = false,
 )
 
 # # Display the results of the A* algorithm
 fig = plot(; aspect_ratio = :equal)
 plot!(optimizer.lazy_search_problem)
-
-# ### References
-# 1. G. Reissig, A. Weber and M. Rungger, "Feedback Refinement Relations for the Synthesis of Symbolic Controllers," in IEEE Transactions on Automatic Control, vol. 62, no. 4, pp. 1781-1796.
-# 2. K. J. Aström and R. M. Murray, Feedback systems. Princeton University Press, Princeton, NJ, 2008.

docs/src/examples/Path planning.jl → docs/src/examples/solvers/Path planning.jl

@@ -1,5 +1,5 @@
 using Test     #src
-# # Example: Path planning problem
+# # Example: Path planning problem solved by [Naive abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/Path planning.ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/Path planning.ipynb)
@@ -23,21 +23,14 @@ using Test     #src
 #
 # In order to study the concrete system and its symbolic abstraction in a unified framework, we will solve the problem
 # for the sampled system with a sampling time $\tau$.
-#
-# The abstraction is based on a feedback refinment relation [1,V.2 Definition].
-# Basically, this is equivalent to an alternating simulation relationship with the additional constraint that the input of the
-# concrete and symbolic system preserving the relation must be identical.
-# This allows to easily determine the controller of the concrete system from the abstraction controller by simply adding a quantization step.
-#
 # For the construction of the relations in the abstraction, it is necessary to over-approximate attainable sets of
 # a particular cell. In this example, we consider the used of a growth bound function  [1, VIII.2, VIII.5] which is one of the possible methods to over-approximate
-# attainable sets of a particular cell based on the state reach by its center. Therefore, it is used
-# to compute the relations in the abstraction based on the feedback refinement relation.
+# attainable sets of a particular cell based on the state reach by its center.
 #
-# For this reachability problem, the abstraction controller is built by solving a fixed-point equation which consists in computing the the pre-image
+# For this reachability problem, the abstraction controller is built by solving a fixed-point equation which consists in computing the pre-image
 # of the target set.
 
-# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots].
+# First, let us import [StaticArrays](https://github.com/JuliaArrays/StaticArrays.jl) and [Plots](https://github.com/JuliaPlots/Plots.jl).
 using StaticArrays, Plots
 
 # At this point, we import Dionysos.
@@ -72,10 +65,10 @@ u0 = SVector(0.0, 0.0);
 h = SVector(0.3, 0.3);
 input_grid = DO.GridFree(u0, h);
 
-# We now solve the optimal control problem with the `Abstraction.SCOTSAbstraction.Optimizer`.
+# We now solve the optimal control problem with the `Abstraction.NaiveAbstraction.Optimizer`.
 
 using JuMP
-optimizer = MOI.instantiate(AB.SCOTSAbstraction.Optimizer)
+optimizer = MOI.instantiate(AB.NaiveAbstraction.Optimizer)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), concrete_problem)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), state_grid)
 MOI.set(optimizer, MOI.RawOptimizerAttribute("input_grid"), input_grid)

docs/src/examples/State-feedback Abstraction PWA System.jl → docs/src/examples/solvers/State-feedback Abstraction PWA System.jl

@@ -1,5 +1,5 @@
 using Test     #src
-# # Example: Optimal control of a PWA System by State-feedback Abstractions
+# # Example: Optimal control of a PWA System by State-feedback Abstractions solved by [Ellipsoid abstraction](https://github.com/dionysos-dev/Dionysos.jl/blob/master/docs/src/manual/manual.md#solvers).
 #
 #md # [![Binder](https://mybinder.org/badge_logo.svg)](@__BINDER_ROOT_URL__/generated/State-feedback Abstraction: PWA System.ipynb)
 #md # [![nbviewer](https://img.shields.io/badge/show-nbviewer-579ACA.svg)](@__NBVIEWER_ROOT_URL__/generated/State-feedback Abstraction: PWA System.ipynb)
@@ -53,7 +53,8 @@ const OP = DI.Optim
 const AB = OP.Abstraction
 
 lib = CDDLib.Library() # polyhedron lib
-include("../../../problems/pwa_sys.jl")
+
+include(joinpath(dirname(dirname(pathof(Dionysos))), "problems", "pwa_sys.jl"))
 
 # # Problem parameters
 # Notice that in [1] it was used `Wsz = 5` and `Usz = 50`. These, and other values were changed here to speed up the build time of the documentation.

docs/src/index.md

@@ -24,8 +24,9 @@ Rather than relying on closed-form analysis of a model of the dynamical system,
 
 The documentation is organised as follows.
 * The **Manual** section contains all the useful information to use Dionysos as a user.
+* The **Solvers** section contains a few examples of solving problems with Dionysos. Start with [Getting started](https://dionysos-dev.github.io/Dionysos.jl/dev/generated/Getting%20Started/) if you want to get familiar with Dionysos.
+* The **Utils** section contains some examples of basic Dionysos functions.
 * The **API Reference** sections contains all the functions that we currently use in Dionysos. 
-* The **Examples** section contains a few examples of solving problems with Dionysos. Start with [Getting started](https://dionysos-dev.github.io/Dionysos.jl/dev/generated/Getting%20Started/) if you want to get familiar with Dionysos.
 * The **Developer Docs** section is dedicated to the contributors to Dionysos developement.