Errors with projection

The following can be addressed in separate PRs, but are related to using the options project_reachset and projection_matrix:

1 - UndefVarError with projection projection matrix

2 - MethodError if projection matrix is passed in the incorrect options structure

3 - Inconsistency in parsing the projection options

A = rand(4, 4)
S = LinearContinuousSystem(A)
X0 = rand(Hyperrectangle, dim=4)
M = rand(2, 4)
P = InitialValueProblem(S, X0)

For 1:

opts = Options(:T=>1.0, :project_reachset=>true, :projection_matrix=>M)
opts_algo = Options(:δ=>0.1, :vars=>[1, 2]);

For 2:

opts = Options(:T=>1.0, :project_reachset=>true)
opts_algo = Options(:δ=>0.1, :vars=>[1, 2], :projection_matrix=>M);

For 3:

opts = Options(:T=>1.0, :project_reachset=>false, :projection_matrix=>M)
opts_algo = Options(:δ=>0.1, :vars=>[1, 2]);

EDIT: for these examples and some comments see this notebook

is actually not a problem of :projection_matrix (this option is just ignored) but of :project_reachset. The vector of ReachSets after projection is not concretely typed, which causes the creation of the ReachSolution to crash. This sounds tricky to solve.

happens because we once decided that passing a :projection_matrix implies that one wants to project, and we ignore :project_reachset then.

Reachability.jl/src/solve.jl

Lines 242 to 244 in 4e3fe6c

    
           if options[:project_reachset] || options[:projection_matrix] != nothing 
        
               info("Projection...") 
        
               RsetsProj = @timing project(Rsets, options)

#469 proposed to unify those options. If we do not want to go for that, I am fine with changing this policy (both choices are arbitrary to me).

AssertionError: a linear map of size (2, 4) cannot be applied to a set of dimension 2

at least, a better error message should be sent

This message comes from LazySets. Should we check compatibility here, too? If the user enables the log, they know that this happens in the projection.

is actually not a problem of :projection_matrix (this option is just ignored) but of :project_reachset. The vector of ReachSets after projection is not concretely typed, which causes the creation of the ReachSolution to crash. This sounds tricky to solve.

More precisely, the problem is this line:

Reachability.jl/src/ReachSets/project_reach.jl

Line 44 in 4e3fe6c

RsetsProj = Vector{ReachSet{<:set_type{N}}}(undef, length(Rsets))

By passing the option :set_type => Hyperrectangle (default), some type parameters are not instantiated. We do not allow to pass Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}} directly, and this would be awkward.

A workaround is to not use :project_reachset, replacing that line by

    RsetsProj = Vector{ReachSet{set_type}}(undef, length(Rsets))

and calling project_reach manually.

Example for the Building model:

include("building.jl")

𝑂_BLDF01 = Options(:T => time_horizon, :mode => "reach", :property => pBDS01)
𝑂_dense_BLDF01 = Options(:vars => [25], :partition => [1:24, [25], 26:48],
                         :δ => 0.003, :block_options_init => LazySets.LinearMap)

res = solve(build_TV, 𝑂_BLDF01, op=BFFPSV18(𝑂_dense_BLDF01))  # unprojected solution

projection_options = Options(:n => 48, :ε_proj => Inf,
    :set_type_proj => Hyperrectangle{Float64, Vector{Float64}, Vector{Float64}},
    :projection_matrix => nothing, :transformation_matrix => nothing)

rs = ReachSolution(project_reach(res.Xk, [0, 25], projection_options))  # projection

plot(rs, vars=[0, 1])  # solution is 1D, so the variables need to be specified

The first error got resolved in #717. That example now produces the second error.

This issue will be closed in #719. As explained above, 3. is not a bug. 1. and 2. will result in an assertion error about M = rand(2, 4) having two dimensions. Again, this is not a bug.

	if options[:project_reachset] \|\| options[:projection_matrix] != nothing
	info("Projection...")
	RsetsProj = @timing project(Rsets, options)