Safety margin issue

.gitignore

@@ -1 +1 @@
-/Manifest.toml
+Manifest.toml

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:

docs/src/schedule_synthesis.md

@@ -1,14 +1,30 @@
 # Schedule Synthesis
 
-The main functionality of this section is divided into two functions
+The main functionality of this section is divided into three functions
 1. [`synthesize_constraints`](@ref): given the dynamics and safety margin of **one**
    control task, find all weakly-hard constraints (up to a maximum window size `maxwindow`)
-   with which the system behaves safely, and
-2. [`schedule_xghtc`](@ref): given the lists of safe weakly-hard constraints for **all** 
+   with which the system behaves safely,
+2. [`estimate_constraints`](@ref): similar to [`synthesize_constraints`](@ref), but uses 
+   the statistical method [`estimate_deviation`](@ref) to find the deviation upper bound of
+   each weakly-hard constraints.
+3. [`schedule_xghtc`](@ref): given the lists of safe weakly-hard constraints for **all** 
    control tasks, synthesizes a schedule so that they all behave safely (if such schedules 
    exist).
 
 ```@docs
 synthesize_constraints
 schedule_xghtc
+estimate_constraints
+```
+
+## Utility Functions
+
+A few utility functions are exported as well.  These support the implementation
+of the above functions, and are potentially useful to their callers as well.
+
+```@docs
+schedule_to_sequence
+verify_schedule
+devub
+devest
 ```

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/ControlTimingSafety.jl

@@ -19,6 +19,8 @@ export maximum_deviation_random, estimate_deviation
 include("probablesafety.jl")
 
 export schedule_xghtc, synthesize_constraints
+export estimate_constraints, verify_schedule, schedule_to_sequence
+export devub, devest
 include("schedule_synthesis.jl")
 
 end

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::Real=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
 
 """