Closed mforets closed 4 years ago
2) is actually not a problem of :projection_matrix
(this option is just ignored) but of :project_reachset
. The vector of ReachSet
s after projection is not concretely typed, which causes the creation of the ReachSolution
to crash. This sounds tricky to solve.
:projection_matrix
implies that one wants to project, and we ignore :project_reachset
then.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:
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.
The following can be addressed in separate PRs, but are related to using the options
project_reachset
andprojection_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
For 1:
For 2:
For 3:
EDIT: for these examples and some comments see this notebook