Specify H instead of t in bounded-runs-iter()

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:

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:

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"""

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
 
 """

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