From 19a14cf7c87e4e33edd979546d98e3225140d79f Mon Sep 17 00:00:00 2001 From: mforets Date: Mon, 25 Feb 2019 18:12:56 -0300 Subject: [PATCH 1/4] WIP options docstring --- .../ContinuousPost/BFFPSV18/BFFPSV18.jl | 110 ++++++++++++++++++ 1 file changed, 110 insertions(+) diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl index 2fb3667a..b36c3e97 100644 --- a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl +++ b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl @@ -156,6 +156,113 @@ The following options are available: $(print_option_spec(options_BFFPSV18())) ``` +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]: + +```jldoctest BFFPSV18_example_1 +julia> using Reachability, MathematicalSystems + +julia> A = [-1 -4 0 0 0; + 4 -1 0 0 0; + 0 0 -3 1 0; + 0 0 -1 3 0; + 0 0 0 0 -2] + +julia> X₀ = BallInf(ones(5), 0.1); + +juoia> problem = InitialValueProblem(LinearContinuousSystem(A), X₀); + +julia> sol = solve(problem, Options(:T=>5.0), op=BFFPSV18(Options(:δ=>0.04))); +``` +Let's check that the dimension of the first set computed is 2: + +```jldoctest BFFPSV18_example_1 +julia> dim(first(sol.Xk).X) +5 + +julia> sol.options[:partition] +5-element Array{Array{Int64,1},1}: + [1] + [2] + [3] + [4] + [5] +``` +Here, `[1]` corresponds to a block of size one for variable `5`, etc until variable +`5`. Let's check the set type used is interval: + +# FIX: to use Interval for 1D partitions by default + +```jldoctest BFFPSV18_example_1 +julia> sol.options[:set_type] +Interval + +julia> all([Xi isa Interval for Xi in array(first(sol.Xk).X)]) +true +``` + +Suppose that we are only interested in variables `1` and `2`. Then we can +specify it using the `:vars` option: + +```jldoctest BFFPSV18_example_1 +julia> sol = solve(problem, Options(:T=>5.0), op=BFFPSV18(Options(:δ=>0.04, :vars=>[1,2]))); + +julia> dim(first(sol.Xk).X) +2 +``` +The set types used are still intevals: + +```jldoctest BFFPSV18_example_1 +julia> all([Xi isa Hyperrectangle for Xi in first(sol.Xk).X.array]) +true +``` + +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))); + +julia> first(sol.Xk).X.array isa Hyperrectangle +true +``` + +To increase the accuracy, the `overapproximation` option offers other possibilities. +For example, one can use template directions instead of a fixed set type. Below +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))); + +julia> first(sol.Xk).X.array isa HPolygon # CHECK: are these polygons or polytopes? +true +``` + +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))); + +julia> first(sol.Xk).X.array isa HPolygon +true +``` +In this case, the overapproximation option can be ommited. The previous options +are equivalent to: + +```jldoctest BFFPSV18_example_1 +julia> sol = solve(problem, Options(:T=>5.0), + op=BFFPSV18(Options(:δ=>0.04, :vars=>[1,2], :ε=>1e-3))); + +julia> first(sol.Xk).X.array isa HPolygon +true +``` + ### Algorithm We refer to [1] for technical details. @@ -165,6 +272,9 @@ and High-dimensional Matrices](https://dl.acm.org/citation.cfm?id=3178128). S. Bogomolov, M. Forets, G. Frehse, A. Podelski, C. Schilling, F. Viry. HSCC '18 Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week). + +[2] Althoff, Matthias. Reachability analysis and its application to the safety +assessment of autonomous cars. Diss. Technische Universität München, 2010. """ struct BFFPSV18 <: ContinuousPost options::TwoLayerOptions From 168bbf49463c8cf426e3ff23d26006a3fc4a5a24 Mon Sep 17 00:00:00 2001 From: mforets Date: Mon, 25 Feb 2019 18:15:34 -0300 Subject: [PATCH 2/4] doc tweaks --- src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl index b36c3e97..767a6726 100644 --- a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl +++ b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl @@ -176,7 +176,7 @@ juoia> problem = InitialValueProblem(LinearContinuousSystem(A), X₀); julia> sol = solve(problem, Options(:T=>5.0), op=BFFPSV18(Options(:δ=>0.04))); ``` -Let's check that the dimension of the first set computed is 2: +Let's check that the dimension of the first set computed is 5: ```jldoctest BFFPSV18_example_1 julia> dim(first(sol.Xk).X) @@ -190,11 +190,9 @@ julia> sol.options[:partition] [4] [5] ``` -Here, `[1]` corresponds to a block of size one for variable `5`, etc until variable +Here, `[1]` corresponds to a block of size one for variable `5`, etc., until variable `5`. Let's check the set type used is interval: -# FIX: to use Interval for 1D partitions by default - ```jldoctest BFFPSV18_example_1 julia> sol.options[:set_type] Interval @@ -212,7 +210,7 @@ julia> sol = solve(problem, Options(:T=>5.0), op=BFFPSV18(Options(:δ=>0.04, :va julia> dim(first(sol.Xk).X) 2 ``` -The set types used are still intevals: +The sets used are intevals: ```jldoctest BFFPSV18_example_1 julia> all([Xi isa Hyperrectangle for Xi in first(sol.Xk).X.array]) From 8f6b531108eba2b3307925fc7ff0ad49067fb8fe Mon Sep 17 00:00:00 2001 From: mforets Date: Fri, 1 Mar 2019 21:22:14 -0300 Subject: [PATCH 3/4] 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 767a6726..e75f1d3f 100644 --- a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl +++ b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl @@ -140,26 +140,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 @@ -201,6 +230,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: @@ -217,13 +248,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 @@ -235,7 +268,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 @@ -245,7 +278,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 @@ -261,9 +294,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). From c359d11ab4449e7602c34d31fd6ac453c067f41c Mon Sep 17 00:00:00 2001 From: schillic Date: Thu, 19 Sep 2019 16:50:33 +0200 Subject: [PATCH 4/4] typos --- src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl index e75f1d3f..a3114a67 100644 --- a/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl +++ b/src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl @@ -174,14 +174,14 @@ 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 +specify the computation of a subset of the flowpipe, which helps to improve performance, specially for large systems. -We continue to show some lower-level options such has how to specify a custom +We continue to show some lower-level options such as 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. +flowpipe computation and safety property checking, and examples of use. #### Running example and default options