diff --git a/src/Properties/check_blocks.jl b/src/Properties/check_blocks.jl index e30d115e..ce659525 100644 --- a/src/Properties/check_blocks.jl +++ b/src/Properties/check_blocks.jl @@ -29,9 +29,12 @@ The first time index where the property is violated, and 0 if the property is sa @inline proj(bi::Int, n::Int) = sparse([1], [bi], ones(1), 1, n) @inline row(ϕpowerk::AbstractMatrix, bi::UnitRange{Int}) = ϕpowerk[bi, :] @inline row(ϕpowerk::AbstractMatrix, bi::Int) = ϕpowerk[[bi], :] -@inline block(ϕpowerk_πbi::SparseMatrixCSC, bj::UnitRange{Int}) = +@inline row(ϕpowerk::SparseMatrixExp, bi::UnitRange{Int}) = + get_rows(ϕpowerk, bi) +@inline row(ϕpowerk::SparseMatrixExp, bi::Int) = get_row(ϕpowerk, bi) +@inline block(ϕpowerk_πbi::AbstractMatrix, bj::UnitRange{Int}) = ϕpowerk_πbi[:, bj] -@inline block(ϕpowerk_πbi::SparseMatrixCSC, bj::Int) = ϕpowerk_πbi[:, [bj]] +@inline block(ϕpowerk_πbi::AbstractMatrix, bj::Int) = ϕpowerk_πbi[:, [bj]] # sparse function check_blocks!(ϕ::SparseMatrixCSC{NUM, Int}, @@ -208,7 +211,7 @@ function check_blocks!(ϕ::SparseMatrixExp{NUM}, for i in 1:b bi = partition[blocks[i]] arr = Vector{LazySet{NUM}}(arr_length) - ϕpowerk_πbi = get_rows(ϕpowerk, bi) + ϕpowerk_πbi = row(ϕpowerk, bi) for (j, bj) in enumerate(partition) arr[j] = block(ϕpowerk_πbi, bj) * Xhat0[j] end @@ -227,7 +230,7 @@ function check_blocks!(ϕ::SparseMatrixExp{NUM}, if U != nothing for i in 1:b bi = partition[blocks[i]] - ϕpowerk_πbi = get_rows(ϕpowerk, bi) + ϕpowerk_πbi = row(ϕpowerk, bi) Whatk[i] = overapproximate(blocks[i], Whatk[i] + ϕpowerk_πbi * inputs) end diff --git a/src/ReachSets/reach_blocks.jl b/src/ReachSets/reach_blocks.jl index f9ca242b..ac4df69f 100644 --- a/src/ReachSets/reach_blocks.jl +++ b/src/ReachSets/reach_blocks.jl @@ -32,9 +32,12 @@ nondeterministic inputs. @inline proj(bi::Int, n::Int) = sparse([1], [bi], ones(1), 1, n) @inline row(ϕpowerk::AbstractMatrix, bi::UnitRange{Int}) = ϕpowerk[bi, :] @inline row(ϕpowerk::AbstractMatrix, bi::Int) = ϕpowerk[[bi], :] -@inline block(ϕpowerk_πbi::SparseMatrixCSC, bj::UnitRange{Int}) = +@inline row(ϕpowerk::SparseMatrixExp, bi::UnitRange{Int}) = + get_rows(ϕpowerk, bi) +@inline row(ϕpowerk::SparseMatrixExp, bi::Int) = get_row(ϕpowerk, bi) +@inline block(ϕpowerk_πbi::AbstractMatrix, bj::UnitRange{Int}) = ϕpowerk_πbi[:, bj] -@inline block(ϕpowerk_πbi::SparseMatrixCSC, bj::Int) = ϕpowerk_πbi[:, [bj]] +@inline block(ϕpowerk_πbi::AbstractMatrix, bj::Int) = ϕpowerk_πbi[:, [bj]] # sparse function reach_blocks!(ϕ::SparseMatrixCSC{NUM, Int}, @@ -206,7 +209,7 @@ function reach_blocks!(ϕ::SparseMatrixExp{NUM}, update!(p, k) for i in 1:b bi = partition[blocks[i]] - ϕpowerk_πbi = get_rows(ϕpowerk, bi) + ϕpowerk_πbi = row(ϕpowerk, bi) Xhatk_bi = ZeroSet(length(bi)) for (j, bj) in enumerate(partition) πbi = block(ϕpowerk_πbi, bj)