From c113b47590db8e42be0fb1183800af7926627a2c Mon Sep 17 00:00:00 2001 From: mforets Date: Fri, 1 Mar 2019 21:22:14 -0300 Subject: [PATCH] docs updates --- .../ContinuousPost/BFFPSV18/BFFPSV18.jl | 61 +++++++++++++++---- 1 file changed, 48 insertions(+), 13 deletions(-) diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl index f8ccef59..92d584a6 100644 --- a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl +++ b/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).