docs updates

src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl

@@ -241,26 +241,55 @@ end
 """
     BFFPSV18 <: ContinuousPost
 
-Implementation of the reachability algorithm for purely continuous linear
-time-invariant systems using block decompositons by S. Bogomolov, M. Forets,
-G. Frehse, A. Podelski, C. Schilling and F. Viry [1].
+Implementation of the reachability algorithm using decompositions from [1].
+
+This algorithm applies to continuous affine ordinary differential equations of
+the form
+
+```
+    x'(t) = Ax(t) + u(t),\\qquad x(0) ∈ X0, u(t) ∈ U ∀ t ∈ [0, T],    (1)
+```
+where `T` is the (finite) time horizon. The result of the algorithm is a sequence
+of sets `Xk` whose union overapproximates the exact flowpipe of (1). 
 
 ### Fields
 
 - `options` -- an `Options` structure that holds the algorithm-specific options
 
-### Notes
-
 The following options are available:
 
 ```julia
 $(print_option_spec(options_BFFPSV18()))
 ```
 
+See the `Notes` below for examples and an explanation of the options.
+
+### Algorithm
+
+We refer to [1] for technical details.
+
+### Notes
+
 The compositional approach offers a tradeoff between accuracy and performance,
-by choosing different partitions and different set representations.
-By default, this algorithm uses a uniform partition of dimension one over all
-variables. For example, consider the two-dimensional example from [2]:
+since one can choose different partitions and different set representations.
+
+These notes illustrate the options that can be passed to the solver. We begin
+by explaining the default options used by the algorithm. Then we show how to
+specify the computation of a subset of the reachpipe, which helps to improve
+performance, specially for large systems.
+
+We continue to show some lower-level options such has how to specify a custom
+block decomposition (the set types used and the sizes of the blocks). 
+
+We conclude showing that there are two different *modes* of operation:
+reachpipe computation and safety property checking, and examples of use.
+
+#### Running example and default options
+
+By default, `BFFPSV18` uses a uniform partition of dimension *one* over all
+variables.
+
+For example, consider the two-dimensional example from [2]:
 
 ```jldoctest BFFPSV18_example_1
 julia> using Reachability, MathematicalSystems
@@ -302,6 +331,8 @@ julia> all([Xi isa Interval for Xi in array(first(sol.Xk).X)])
 true
 ``` 
 
+#### Specifying a subset of all variables
+
 Suppose that we are only interested in variables `1` and `2`. Then we can
 specify it using the `:vars` option:
 
@@ -318,13 +349,15 @@ julia> all([Xi isa Hyperrectangle for Xi in first(sol.Xk).X.array])
 true
 ```
 
+#### Specifying the set type
+
 We can as well specify using other set types for the overapproximation of the
 flowpipe, such as hyperrectangles. It can be specified using the `:overapproximation`
 option:
 
 ```jldoctest BFFPSV18_example_1
 julia> sol = solve(problem, Options(:T=>5.0),
-                   op=BFFPSV18(Options(:δ=>0.04, :vars=>[1,2], :overapproximation=>Hyperrectangle)));
+                   op=BFFPSV18(Options(:δ=>0.04, :vars=>[1,2], :set_type=>Hyperrectangle)));
 
 julia> first(sol.Xk).X.array isa Hyperrectangle
 true
@@ -336,7 +369,7 @@ we use octagonal directions:
 
 ```jldoctest BFFPSV18_example_1
 julia> sol = solve(problem, Options(:T=>5.0),
-                   op=BFFPSV18(Options(:δ=>0.04, :vars=>[1,2], :overapproximation=>:oct)));
+                   op=BFFPSV18(Options(:δ=>0.04, :vars=>[1,2], :template_directions=>:oct)));
 
 julia> first(sol.Xk).X.array isa HPolygon # CHECK: are these polygons or polytopes?
 true
@@ -346,7 +379,7 @@ Another possibility is to use epsilon-close approximation using polygons:
 
 ```jldoctest BFFPSV18_example_1
 julia> sol = solve(problem, Options(:T=>5.0),
-                   op=BFFPSV18(Options(:δ=>0.04, :vars=>[1,2], :overapproximation=>HPolygon, :ε=>1e-3)));
+                   op=BFFPSV18(Options(:δ=>0.04, :vars=>[1,2], :set_type=>HPolygon, :ε=>1e-3)));
 
 julia> first(sol.Xk).X.array isa HPolygon
 true
@@ -362,9 +395,11 @@ julia> first(sol.Xk).X.array isa HPolygon
 true
 ```
 
-### Algorithm
+##### Different decomposition strategies at different stages
 
-We refer to [1] for technical details.
+
+
+### References
 
 [1] [Reach Set Approximation through Decomposition with Low-dimensional Sets
 and High-dimensional Matrices](https://dl.acm.org/citation.cfm?id=3178128).