Merge pull request #719 from JuliaReach/schillic/718

#718 - Add Flowpipe type

src/ReachSets/ContinuousPost/ASB07/post.jl

@@ -35,7 +35,7 @@ function post(𝒜::ASB07,
     reach_ASB07!(Rsets, Ω0, U, Φ, N, δ, max_order)
     end # timing
 
-    Rsol = ReachSolution(Rsets, 𝑂)
+    Rsol = ReachSolution(Flowpipe(Rsets), 𝑂)
 
     # ==========
     # Projection

src/ReachSets/ContinuousPost/ASB07_decomposed/post.jl

@@ -41,7 +41,7 @@ function post(𝒜::ASB07_decomposed,
                             blocks)
     end # timing
 
-    Rsol = ReachSolution(Rsets, 𝑂)
+    Rsol = ReachSolution(Flowpipe(Rsets), 𝑂)
 
     # ==========
     # Projection

src/ReachSets/ContinuousPost/BFFPS19/reach.jl

@@ -108,7 +108,7 @@ function reach_mixed(problem::Union{IVP{<:CLDS{NUM}, <:LazySet{NUM}},
         res[1] = res_type(
             CartesianProductArray{NUM, LazySet{NUM}}(Xhat0[blocks]),
             zero(NUM), options[:δ])
-        return res
+        return Flowpipe(res)
     end
     push!(args, Xhat0)
 
@@ -228,7 +228,7 @@ function reach_mixed(problem::Union{IVP{<:CLDS{NUM}, <:LazySet{NUM}},
     end
 
     # return the result
-    return res
+    return Flowpipe(res)
 end
 
 function reach_mixed(problem::Union{IVP{<:CLCS{NUM}, <:LazySet{NUM}},

src/ReachSets/ContinuousPost/BFFPSV18/BFFPSV18.jl

@@ -248,19 +248,19 @@ function post(𝒫::BFFPSV18, 𝑆::AbstractSystem, 𝑂_input::Options)
     if 𝑂[:mode] == "reach"
         info("Reachable States Computation...")
         @timing begin
-            Rsets = reach(𝑆, 𝑂)
+            flowpipe = reach(𝑆, 𝑂)
             info("- Total")
         end
 
         # Projection
         if 𝑂[:project_reachset]
             info("Projection...")
-            RsetsProj = @timing project(Rsets, 𝑂)
+            flowpipe_proj = @timing project(flowpipe, 𝑂)
         else
-            RsetsProj = Rsets
+            flowpipe_proj = flowpipe
         end
 
-        return ReachSolution(RsetsProj, 𝑂_input)
+        return ReachSolution(flowpipe_proj, 𝑂_input)
 
     elseif 𝑂[:mode] == "check"
         info("invariants are currently not supported in 'check' mode")

src/ReachSets/ContinuousPost/BFFPSV18/reach.jl

@@ -88,7 +88,7 @@ function reach(problem::Union{IVP{<:CLDS{NUM}, <:LazySet{NUM}},
         res[1] = res_type(
             CartesianProductArray{NUM, LazySet{NUM}}(Xhat0[blocks]),
             zero(NUM), options[:δ])
-        return res
+        return Flowpipe(res)
     end
     push!(args, Xhat0)
 
@@ -203,7 +203,7 @@ function reach(problem::Union{IVP{<:CLDS{NUM}, <:LazySet{NUM}},
     end
 
     # return the result
-    return res
+    return Flowpipe(res)
 end
 
 function reach(problem::Union{IVP{<:CLCS{NUM}, <:LazySet{NUM}},

src/ReachSets/ContinuousPost/GLGM06/GLGM06.jl

@@ -18,4 +18,3 @@ GLGM06() = GLGM06(Options())
 include("init.jl")
 include("post.jl")
 include("reach.jl")
-include("project.jl")

src/ReachSets/ContinuousPost/GLGM06/post.jl

@@ -36,7 +36,7 @@ function post(𝒜::GLGM06,
     end
     end # timing
 
-    Rsol = ReachSolution(Rsets, 𝑂)
+    Rsol = ReachSolution(Flowpipe(Rsets), 𝑂)
 
     # ===========
     # Projection

src/ReachSets/ContinuousPost/TMJets/TMJets.jl

@@ -21,5 +21,4 @@ TMJets() = TMJets(Options())
 
 include("init.jl")
 include("post.jl")
-include("project.jl")
 include("reach.jl")

src/ReachSets/ContinuousPost/TMJets/post.jl

@@ -126,7 +126,7 @@ function post(𝒜::TMJets,
         Rsets = _to_zonotope(tTM, vTM, n)
     end
 
-    Rsol = ReachSolution(Rsets, 𝑂)
+    Rsol = ReachSolution(Flowpipe(Rsets), 𝑂)
 
     # ===========
     # Projection

src/ReachSets/DiscretePost/ConcreteDiscretePost.jl

@@ -54,16 +54,14 @@ function init!(𝒫::ConcreteDiscretePost, 𝒮::AbstractSystem, 𝑂::Options)
     return 𝑂out
 end
 
-function tube⋂inv!(𝒫::ConcreteDiscretePost,
-                   reach_tube::Vector{<:AbstractReachSet{<:LazySet{N}}},
-                   invariant,
-                   Rsets,
-                   start_interval
-                  ) where {N}
+function tube⋂inv(𝒫::ConcreteDiscretePost,
+                  reach_tube::Vector{<:AbstractReachSet{<:LazySet{N}}},
+                  invariant,
+                  start_interval
+                 ) where {N}
     # take intersection with source invariant
 
-    # counts the number of sets R⋂I added to Rsets
-    count = 0
+    Rsets = Vector{AbstractReachSet{<:LazySet{N}}}()
     for reach_set in reach_tube
         rs = set(reach_set)
         if rs isa CartesianProductArray && length(array(rs)) == 1
@@ -77,10 +75,9 @@ function tube⋂inv!(𝒫::ConcreteDiscretePost,
               substitute(reach_set, set=intersection(rs, invariant),
                          time_start=time_start(reach_set) + start_interval[1],
                          time_end=time_end(reach_set) + start_interval[2]))
-        count = count + 1
     end
 
-    return count
+    return Rsets
 end
 
 function post(𝒫::ConcreteDiscretePost,
@@ -89,7 +86,6 @@ function post(𝒫::ConcreteDiscretePost,
               passed_list,
               source_loc_id,
               tube⋂inv,
-              count_Rsets,
               jumps,
               options
              ) where {N}
@@ -104,8 +100,8 @@ function post(𝒫::ConcreteDiscretePost,
 
         # perform jumps
         post_jump = Vector{ReachSet{LazySet{N}}}()
-        sizehint!(post_jump, count_Rsets)
-        for reach_set in tube⋂inv[length(tube⋂inv) - count_Rsets + 1 : end]
+        sizehint!(post_jump, length(tube⋂inv))
+        for reach_set in tube⋂inv
             # check intersection with guard
             R⋂G = intersection(guard, set(reach_set))
             if isempty(R⋂G)

src/ReachSets/DiscretePost/DecomposedDiscretePost.jl

@@ -46,25 +46,22 @@ function init!(𝒫::DecomposedDiscretePost, 𝒮::AbstractSystem, 𝑂::Options
     return 𝑂out
 end
 
-function tube⋂inv!(𝒫::DecomposedDiscretePost,
-                   reach_tube::Vector{<:SparseReachSet{<:LazySet{N}}},
-                   invariant,
-                   Rsets,
-                   start_interval
-                  ) where {N}
-
-    # counts the number of sets R⋂I added to Rsets
-    count = 0
+function tube⋂inv(𝒫::DecomposedDiscretePost,
+                  reach_tube::Vector{<:SparseReachSet{<:LazySet{N}}},
+                  invariant,
+                  start_interval
+                 ) where {N}
+
+    Rsets = Vector{AbstractReachSet{<:LazySet{N}}}()
     @inbounds for reach_set in reach_tube
         # intersection with invariant is computed inside BFFPS19 CPost operator
         push!(Rsets,
               substitute(reach_set,
                          time_start=time_start(reach_set) + start_interval[1],
                          time_end=time_end(reach_set) + start_interval[2]))
-        count = count + 1
     end
 
-    return count
+    return Rsets
 end
 
 function post(𝒫::DecomposedDiscretePost,
@@ -73,7 +70,6 @@ function post(𝒫::DecomposedDiscretePost,
               passed_list,
               source_loc_id,
               tube⋂inv,
-              count_Rsets,
               jumps,
               options
              ) where {N}
@@ -92,8 +88,8 @@ function post(𝒫::DecomposedDiscretePost,
         guard = stateset(constrained_map)
         # perform jumps
         post_jump = Vector{ReachSet{LazySet{N}}}()
-        sizehint!(post_jump, count_Rsets)
-        for reach_set in tube⋂inv[length(tube⋂inv) - count_Rsets + 1 : end]
+        sizehint!(post_jump, length(tube⋂inv))
+        for reach_set in tube⋂inv
             if (dim(set(reach_set)) == n_lowdim && n_lowdim < n)
                 continue
             end

src/ReachSets/DiscretePost/DiscretePost.jl

@@ -10,8 +10,8 @@ Abstract supertype of all discrete post operators.
 All discrete post operators should provide the following method, in addition
 to those provided for general post operators:
 ```julia
-tube⋂inv!(𝒫::DiscretePost, reach_tube::Vector{<:AbstractReachSet{<:LazySet, N}},
-          invariant, Rsets, start_interval) where {N}
+tube⋂inv(𝒫::DiscretePost, reach_tube::Vector{<:AbstractReachSet{<:LazySet, N}},
+         invariant, start_interval) where {N}
 ```
 """
 abstract type DiscretePost <: PostOperator end

src/ReachSets/DiscretePost/LazyDiscretePost.jl

@@ -81,17 +81,15 @@ function init!(𝒫::LazyDiscretePost, 𝒮::AbstractSystem, 𝑂::Options)
     return 𝑂out
 end
 
-function tube⋂inv!(𝒫::LazyDiscretePost,
-                   reach_tube::Vector{<:AbstractReachSet{<:LazySet{N}}},
-                   invariant,
-                   Rsets,
-                   start_interval
-                  ) where {N}
+function tube⋂inv(𝒫::LazyDiscretePost,
+                  reach_tube::Vector{<:AbstractReachSet{<:LazySet{N}}},
+                  invariant,
+                  start_interval
+                 ) where {N}
 
     dirs = 𝒫.options[:overapproximation]
 
-    # counts the number of sets R⋂I added to Rsets
-    count = 0
+    Rsets = Vector{AbstractReachSet{<:LazySet{N}}}()
     @inbounds for reach_set in reach_tube
         R⋂I = Intersection(set(reach_set), invariant)
         if 𝒫.options[:check_invariant_intersection] && isempty(R⋂I)
@@ -104,10 +102,9 @@ function tube⋂inv!(𝒫::LazyDiscretePost,
               substitute(reach_set, set=R⋂I,
                          time_start=time_start(reach_set) + start_interval[1],
                          time_end=time_end(reach_set) + start_interval[2]))
-        count = count + 1
     end
 
-    return count
+    return Rsets
 end
 
 function post(𝒫::LazyDiscretePost,
@@ -116,7 +113,6 @@ function post(𝒫::LazyDiscretePost,
               passed_list,
               source_loc_id,
               tube⋂inv,
-              count_Rsets,
               jumps,
               options
              ) where {N}
@@ -145,8 +141,8 @@ function post(𝒫::LazyDiscretePost,
 
         # perform jumps
         post_jump = Vector{ReachSet{LazySet{N}}}()
-        sizehint!(post_jump, count_Rsets)
-        for reach_set in tube⋂inv[length(tube⋂inv) - count_Rsets + 1 : end]
+        sizehint!(post_jump, length(tube⋂inv))
+        for reach_set in tube⋂inv
             # check intersection with guard
             if combine_constraints
                 R⋂G = Intersection(set(reach_set).X, invariant_guard)

src/ReachSets/Flowpipe.jl

@@ -0,0 +1,17 @@
+"""
+    Flowpipe{SN, RSN<:AbstractReachSet{SN}} <: AbstractSolution
+
+Wrapper of a sequence of sets (the solution of a continuous-post operator).
+
+### Fields
+
+- `reachsets` -- the list of [`AbstractReachSet`](@ref)s
+"""
+struct Flowpipe{SN, RSN<:AbstractReachSet{SN}}
+    reachsets::Vector{RSN}
+end
+
+# projection
+function project(fp::Flowpipe, M::AbstractMatrix)
+    return Flowpipe([project(X, M) for X in fp.reachsets])
+end