Merge pull request #549 from JuliaReach/schillic/538

#538 - Analysis with unbounded time
JuliaReach · Mar 16, 2019 · 6bf1e2e · 6bf1e2e
2 parents fe9bd10 + 29ab546
commit 6bf1e2e
Show file tree

Hide file tree

Showing 7 changed files with 133 additions and 67 deletions.
diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/check_blocks.jl b/src/ReachSets/ContinuousPost/BFFPSV18/check_blocks.jl
@@ -29,12 +29,14 @@ function check_blocks(ϕ::SparseMatrixCSC{NUM, Int},
                        U::Union{ConstantInput, Nothing},
                        overapproximate_inputs::Function,
                        n::Int,
-                       N::Int,
+                       N::Union{Int, Nothing},
                        blocks::AbstractVector{Int},
                        partition::AbstractVector{<:Union{AbstractVector{Int}, Int}},
                        eager_checking::Bool,
-                       prop::Property
+                       prop::Property,
+                       progress_meter::Union{Progress, Nothing}
                        )::Int where {NUM}
+    update!(progress_meter, 1)
     violation_index = 0
     if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
@@ -59,9 +61,8 @@ function check_blocks(ϕ::SparseMatrixCSC{NUM, Int},
     end
 
     k = 2
-    p = Progress(N, 1, "Computing successors ")
     @inbounds while true
-        update!(p, k)
+        update!(progress_meter, k)
         for i in 1:b
             bi = partition[blocks[i]]
             Xhatk_bi = ZeroSet(length(bi))
@@ -106,12 +107,14 @@ function check_blocks(ϕ::AbstractMatrix{NUM},
                        U::Union{ConstantInput, Nothing},
                        overapproximate_inputs::Function,
                        n::Int,
-                       N::Int,
+                       N::Union{Int, Nothing},
                        blocks::AbstractVector{Int},
                        partition::AbstractVector{<:Union{AbstractVector{Int}, Int}},
                        eager_checking::Bool,
-                       prop::Property
+                       prop::Property,
+                       progress_meter::Union{Progress, Nothing}
                        )::Int where {NUM}
+    update!(progress_meter, 1)
     violation_index = 0
     if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
@@ -138,9 +141,8 @@ function check_blocks(ϕ::AbstractMatrix{NUM},
 
     arr_length = (U == nothing) ? length(partition) : length(partition) + 1
     k = 2
-    p = Progress(N, 1, "Computing successors ")
     @inbounds while true
-        update!(p, k)
+        update!(progress_meter, k)
         for i in 1:b
             bi = partition[blocks[i]]
             arr = Vector{LazySet{NUM}}(undef, arr_length)
@@ -187,12 +189,14 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
                        U::Union{ConstantInput, Nothing},
                        overapproximate_inputs::Function,
                        n::Int,
-                       N::Int,
+                       N::Union{Int, Nothing},
                        blocks::AbstractVector{Int},
                        partition::AbstractVector{<:Union{AbstractVector{Int}, Int}},
                        eager_checking::Bool,
-                       prop::Property
+                       prop::Property,
+                       progress_meter::Union{Progress, Nothing}
                        )::Int where {NUM}
+    update!(progress_meter, 1)
     violation_index = 0
     if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
@@ -217,9 +221,8 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
     end
 
     k = 2
-    p = Progress(N, 1, "Computing successors ")
     @inbounds while true
-        update!(p, k)
+        update!(progress_meter, k)
         for i in 1:b
             bi = partition[blocks[i]]
             ϕpowerk_πbi = row(ϕpowerk, bi)
@@ -262,12 +265,14 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
                        U::Union{ConstantInput, Nothing},
                        overapproximate_inputs::Function,
                        n::Int,
-                       N::Int,
+                       N::Union{Int, Nothing},
                        blocks::AbstractVector{Int},
                        partition::AbstractVector{<:Union{AbstractVector{Int}, Int}},
                        eager_checking::Bool,
-                       prop::Property
+                       prop::Property,
+                       progress_meter::Union{Progress, Nothing}
                        )::Int where {NUM}
+    update!(progress_meter, 1)
     violation_index = 0
     if !check(prop, CartesianProductArray(Xhat0[blocks]))
         if eager_checking
@@ -293,9 +298,8 @@ function check_blocks(ϕ::SparseMatrixExp{NUM},
 
     arr_length = (U == nothing) ? length(partition) : length(partition) + 1
     k = 2
-    p = Progress(N, 1, "Computing successors ")
     @inbounds while true
-        update!(p, k)
+        update!(progress_meter, k)
         for i in 1:b
             bi = partition[blocks[i]]
             arr = Vector{LazySet{NUM}}(undef, arr_length)

diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl b/src/ReachSets/ContinuousPost/BFFPSV18/check_property.jl
@@ -35,7 +35,8 @@ function check_property(S::IVP{<:AbstractDiscreteSystem},
     n = statedim(S)
     blocks = options[:blocks]
     partition = convert_partition(options[:partition])
-    N = ceil(Int, options[:T] / options[:δ])
+    T = options[:T]
+    N = (T == Inf) ? nothing : ceil(Int, T / options[:δ])
 
     # Cartesian decomposition of the initial set
     if length(partition) == 1 && length(partition[1]) == n &&
@@ -138,8 +139,15 @@ function check_property(S::IVP{<:AbstractDiscreteSystem},
     # add property
     push!(args, property)
 
-    # call the adequate function with the given arguments list
     info("- Computing successors")
+
+    # progress meter
+    progress_meter = (N != nothing) ?
+        Progress(N, 1, "Computing successors ") :
+        nothing
+    push!(args, progress_meter)
+
+    # call the adequate function with the given arguments list
     answer =
         @timing available_algorithms_check[algorithm_backend]["func"](args...)
 

diff --git a/src/ReachSets/ContinuousPost/BFFPSV18/reach.jl b/src/ReachSets/ContinuousPost/BFFPSV18/reach.jl
@@ -4,6 +4,7 @@ using LazySets: CacheMinkowskiSum,
                  isdisjoint
 
 import LazySets.Approximations: overapproximate
+import ProgressMeter: update!
 
 """
     reach(S, invariant, options)
@@ -50,7 +51,8 @@ function reach(S::Union{IVP{<:LDS{NUM}, <:LazySet{NUM}},
     n = statedim(S)
     blocks = options[:blocks]
     partition = convert_partition(options[:partition])
-    N = ceil(Int, options[:T] / options[:δ])
+    T = options[:T]
+    N = (T == Inf) ? nothing : ceil(Int, T / options[:δ])
 
     # Cartesian decomposition of the initial set
     if length(partition) == 1 && length(partition[1]) == n &&
@@ -76,7 +78,7 @@ function reach(S::Union{IVP{<:LDS{NUM}, <:LazySet{NUM}},
     else
         res_type = ReachSet{Hyperrectangle{NUM}, NUM}
     end
-    res = Vector{res_type}(undef, N)
+    res = (N == nothing) ? Vector{res_type}() : Vector{res_type}(undef, N)
 
     # shortcut if only the initial set is required
     if N == 1
@@ -160,14 +162,17 @@ function reach(S::Union{IVP{<:LDS{NUM}, <:LazySet{NUM}},
     push!(args, options[:δ])
 
     # termination function
-    if invariant == nothing
-        termination = (k, set, t0) -> termination_N(N, k, set, t0)
-    else
-        termination =
-            (k, set, t0) -> termination_inv_N(N, invariant, k, set, t0)
-    end
+    termination = get_termination_function(N, invariant)
     push!(args, termination)
 
+    info("- Computing successors")
+
+    # progress meter
+    progress_meter = (N != nothing) ?
+        Progress(N, 1, "Computing successors ") :
+        nothing
+    push!(args, progress_meter)
+
     # choose algorithm backend
     algorithm = options[:algorithm]
     if algorithm == "explicit"
@@ -180,14 +185,16 @@ function reach(S::Union{IVP{<:LDS{NUM}, <:LazySet{NUM}},
     push!(args, res)
 
     # call the adequate function with the given arguments list
-    info("- Computing successors")
     @timing begin
         index, skip = available_algorithms[algorithm_backend]["func"](args...)
-        if index < N || skip
-            # shrink result array
-            info("terminated prematurely, only computed $index/$N steps")
-            deleteat!(res, (skip ? index : index + 1):N)
+    end
+
+    # shrink result array
+    if skip || index < N
+        if N != nothing
+            info("termination after only $index of $N steps")
         end
+        deleteat!(res, (skip ? index : index + 1):length(res))
     end
 
     # return the result
@@ -210,10 +217,41 @@ function reach(system::IVP{<:AbstractContinuousSystem},
     return reach(Δ, invariant, options)
 end
 
-function termination_N(N, k, set, t0)
+function get_termination_function(N::Nothing, invariant::Nothing)
+    termination_function = (k, set, t0) -> termination_unconditioned()
+    warn("no termination condition specified; the reachability analysis will " *
+         "not terminate")
+    return termination_function
+end
+
+function get_termination_function(N::Int, invariant::Nothing)
+    return (k, set, t0) -> termination_N(N, k, t0)
+end
+
+function get_termination_function(N::Nothing, invariant::LazySet)
+    return (k, set, t0) -> termination_inv(invariant, set, t0)
+end
+
+function get_termination_function(N::Int, invariant::LazySet)
+    return (k, set, t0) -> termination_inv_N(N, invariant, k, set, t0)
+end
+
+function termination_unconditioned()
+    return (false, false)
+end
+
+function termination_N(N, k, t0)
     return (k >= N, false)
 end
 
+function termination_inv(inv, set, t0)
+    if isdisjoint(set, inv)
+        return (true, true)
+    else
+        return (false, false)
+    end
+end
+
 function termination_inv_N(N, inv, k, set, t0)
     if k >= N
         return (true, false)
@@ -257,3 +295,6 @@ end
 function has_constant_directions(block_options, i::Int)
     return true
 end
+
+# no-op progress meter for unbounded time
+function update!(::Nothing, ::Int) end