From 6d76cd267377846e6bfde9aa7d7da757f0f9dfba Mon Sep 17 00:00:00 2001 From: shengjiex98 Date: Wed, 5 Jul 2023 18:06:57 -0400 Subject: [PATCH 1/4] Change `bounded-runs-iter()` to use H instead of t --- src/safety.jl | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/safety.jl b/src/safety.jl index e3e624d..50bb53b 100644 --- a/src/safety.jl +++ b/src/safety.jl @@ -135,17 +135,19 @@ function bounded_runs(a::Automaton, z_0::AbstractVecOrMat, n::Integer) end """ - bounded_runs_iter(a, z_0, n, t) + bounded_runs_iter(a, z_0, n, H) -Iterate [`bounded_runs`](@ref)`(a, z_0, n)` for `t` iterations, returning the reachable -set at each of the `n`×`t+1` time steps. +Iterate [`bounded_runs`](@ref)`(a, z_0, n)` multiple times, returning the reachable set at each +of the `H` time stpes. The number of iterations is the smallest integer `t` such that +`n`×`t`≥`H`. See also [`deviation`](@ref), which can be called with the result of this function to find the deviation from a nominal trajectory. """ -function bounded_runs_iter(a::Automaton, z_0::AbstractVecOrMat, n::Integer, t::Integer; safety_margin::Float64=Inf) +function bounded_runs_iter(a::Automaton, z_0::AbstractVecOrMat, n::Integer, H::Integer; safety_margin::Float64=Inf) + t = ceil(Int64, H / n) # Dimensions: time, augmented state, min/max - all_bounds = Array{Float64}(undef, n*(t+1)+1, a.nz, 2) + all_bounds = Array{Float64}(undef, n*t+1, a.nz, 2) if isa(z_0, AbstractVector) all_bounds[1,:,:] = [z_0 z_0] else @@ -176,7 +178,7 @@ function bounded_runs_iter(a::Automaton, z_0::AbstractVecOrMat, n::Integer, t::I # Dimensions: initial location, final location, time, augmented state, min/max new_bounds = Array{Float64}(undef, nlocations(a), nlocations(a), n+1, a.nz, 2) - for i in 1:t + for i in 2:t # Simulate each box from previous iteration Threads.@threads for i in a.L new_bounds[i,:,:,:,:] = bounded_runs(A[i], bounds[i,end,:,:], n) @@ -186,16 +188,16 @@ function bounded_runs_iter(a::Automaton, z_0::AbstractVecOrMat, n::Integer, t::I merge_bounds!(view(bounds, i, :, :, :), view(new_bounds, :, i, :, :, :)) end # Save the bounds - merge_bounds!(view(all_bounds, n*i+1:n*(i+1)+1, :, :), bounds) + merge_bounds!(view(all_bounds, n*(i-1)+1:n*i+1, :, :), bounds) if isfinite(safety_margin) - d = deviation(a, z_0, all_bounds[n*i+2:n*(i+1)+1,:,:], nominal_trajectory=nom[:,:,n*i+2:n*(i+1)+1]) + d = deviation(a, z_0, all_bounds[n*(i-1)+2:n*i+1,:,:], nominal_trajectory=nom[:,:,n*(i-1)+2:n*i+1]) if maximum(d) > safety_margin - return all_bounds[1:n*(i+1)+1,:,:] + return all_bounds[1:n*i+1,:,:] end end end - all_bounds + all_bounds[1:H+1] end """ From 38a1afa700cdc559bb0243bb8c9cc04c7262acae Mon Sep 17 00:00:00 2001 From: shengjiex98 Date: Wed, 5 Jul 2023 18:22:17 -0400 Subject: [PATCH 2/4] Fix typo in array slicing --- src/safety.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/safety.jl b/src/safety.jl index 50bb53b..0648606 100644 --- a/src/safety.jl +++ b/src/safety.jl @@ -197,7 +197,7 @@ function bounded_runs_iter(a::Automaton, z_0::AbstractVecOrMat, n::Integer, H::I end end end - all_bounds[1:H+1] + all_bounds[1:H+1,:,:] end """ From 0a092daa4a46a577e98961431d2cf24020089246 Mon Sep 17 00:00:00 2001 From: shengjiex98 Date: Wed, 5 Jul 2023 18:29:47 -0400 Subject: [PATCH 3/4] Change all references to `bounded_runs_iter()` --- docs/src/index.md | 5 +++-- src/schedule_synthesis.jl | 8 ++++---- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/docs/src/index.md b/docs/src/index.md index 4aa10a1..b66f2f7 100644 --- a/docs/src/index.md +++ b/docs/src/index.md @@ -31,11 +31,12 @@ zs = zero_skip_next(sys, K, max_misses) To run the Bounded Runs Iteration algorithm for this automaton, first create the initial set, then run the algorithm for a given per-iteration run -length `n` and number of iterations `t`: +length `n` to produce the reachable set of length `H`. The number of iterations +is the smallest integer `t` such that `n`×`t`≥`H`. ```julia augbounds = augment(automaton, bounds) -all_bounds = bounded_runs_iter(automaton, augbounds, n, t) +all_bounds = bounded_runs_iter(automaton, augbounds, n, H) ``` The deviation at each time step can then be computed thusly: diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index ce5522f..b51e7b2 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -72,16 +72,16 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}; slotsize::Int64=1, H::In end """ - synthesize_constraints(sysd, K, z_0, d_max, maxwindow, n, t) + synthesize_constraints(sysd, K, z_0, d_max, maxwindow, n, H) Find all `MeetAny` weakly hard constraints with window size at most `maxwindow` that guarantees the deviation upper bound is at most `d_max`. The system is specified by -[`Automaton`](@ref) `a` and initial state is `z_0`. `n` and `t` are as in +[`Automaton`](@ref) `a` and initial state is `z_0`. `n` and `H` are as in [`bounded_runs_iter`](@ref). """ function synthesize_constraints(sysd::AbstractStateSpace{<:Discrete}, K::AbstractMatrix{Float64}, z_0::AbstractVecOrMat, d_max::Float64, - maxwindow::Int64, n::Int64, t::Int64) + maxwindow::Int64, n::Int64, H::Int64) safe_constraints = MeetAny[] @@ -93,7 +93,7 @@ function synthesize_constraints(sysd::AbstractStateSpace{<:Discrete}, constraint = MeetAny(meet, window) a = hold_kill(sysd, K, constraint) # Check if the deviation bound is within the safety margin - reachable = bounded_runs_iter(a, z_0, n, t) + reachable = bounded_runs_iter(a, z_0, n, H) m = maximum(deviation(a, z_0, reachable)) if m <= d_max # All constraints with (m, window) where m >= meet are valid From c2a20efefe61908208e9bedce1912af82f3856d9 Mon Sep 17 00:00:00 2001 From: shengjiex98 Date: Wed, 5 Jul 2023 19:01:00 -0400 Subject: [PATCH 4/4] Two more changes --- README.md | 5 +++-- notebooks/control_timing_safety.jl | 3 +-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index e1dad2a..4a73036 100644 --- a/README.md +++ b/README.md @@ -35,11 +35,12 @@ zs = zero_skip_next(sys, K, max_misses) To run the Bounded Runs Iteration algorithm for this automaton, first create the initial set, then run the algorithm for a given per-iteration run -length `n` and number of iterations `t`: +length `n` to produce the reachable set of length `H`. The number of iterations +is the smallest integer `t` such that `n`×`t`≥`H`. ```julia augbounds = augment(automaton, bounds) -all_bounds = bounded_runs_iter(automaton, augbounds, n, t) +all_bounds = bounded_runs_iter(automaton, augbounds, n, H) ``` The deviation at each time step can then be computed thusly: diff --git a/notebooks/control_timing_safety.jl b/notebooks/control_timing_safety.jl index 2449670..0672e0b 100644 --- a/notebooks/control_timing_safety.jl +++ b/notebooks/control_timing_safety.jl @@ -370,11 +370,10 @@ This section illustrates the Bounded Runs Iteration algorithm, used to efficient # ╔═╡ efc6aa00-cfdb-45fb-809b-f99c663690f6 begin - t_4 = div(time_4, n_4) all_bounds = let automaton = strat_map[sim_strategy_4](sysd, K, MissRow(max_miss_4)) augbounds = augment(automaton, bounds) - bounded_runs_iter(automaton, augbounds, n_4, t_4) + bounded_runs_iter(automaton, augbounds, n_4, time_4) end md"""