From dec9647183548ff0aa312b74cbca4d481f4ba847 Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Thu, 9 Mar 2023 20:50:09 -0500 Subject: [PATCH 01/17] Add schedule synthesis with SHT --- docs/src/schedule_synthesis.md | 7 +++++-- src/ControlTimingSafety.jl | 2 +- src/schedule_synthesis.jl | 33 +++++++++++++++++++++++++++++++++ 3 files changed, 39 insertions(+), 3 deletions(-) diff --git a/docs/src/schedule_synthesis.md b/docs/src/schedule_synthesis.md index 0fc9983..5f433ad 100644 --- a/docs/src/schedule_synthesis.md +++ b/docs/src/schedule_synthesis.md @@ -3,8 +3,11 @@ The main functionality of this section is divided into two 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). diff --git a/src/ControlTimingSafety.jl b/src/ControlTimingSafety.jl index 6f0bb99..9fae80e 100644 --- a/src/ControlTimingSafety.jl +++ b/src/ControlTimingSafety.jl @@ -18,7 +18,7 @@ include("safety.jl") export maximum_deviation_random, estimate_deviation include("probablesafety.jl") -export schedule_xghtc, synthesize_constraints +export schedule_xghtc, synthesize_constraints, estimate_constraints include("schedule_synthesis.jl") end diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index 17617af..ee78f63 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -109,6 +109,39 @@ function synthesize_constraints(sysd::AbstractStateSpace{<:Discrete}, safe_constraints end +""" + estimate_constraints(sysd, K, z_0, d_max, maxwindow, c, B, 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`. This function uses SHT for +estimating the deviation upper bound as in [`estimate_deviation`](@ref). +""" +function estimate_constraints(sysd::AbstractStateSpace{<:Discrete}, + K::AbstractMatrix{Float64}, z_0::AbstractVecOrMat, d_max::Float64, + maxwindow::Int64, c::Float64, B::Float64, H::Int64) + safe_constraints = MeetAny[] + + meet = 1 + for window in 2:maxwindow + while meet < window + constraint = MeetAny(meet, window) + a = hold_kill(sysd, K, constraint) + sampler = SamplerUniformMeetAny(constraint, H) + m = estimate_deviation(a, sampler, z_0, c, B) + if m <= d_max + for i in meet:window-1 + push!(safe_constraints, MeetAny(i, window)) + end + break + end + meet += 1 + end + end + + safe_constraints +end + # Helper functions """ From 849b055df9dfed301d3f887145e0cd8abec127bb Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Wed, 15 Mar 2023 20:26:46 -0400 Subject: [PATCH 02/17] Add verification for SHT schedule synthesis --- src/schedule_synthesis.jl | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index 1bde5fa..311f6d4 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -71,6 +71,25 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}; slotsize::Int64=1, H::In return zeros(Int64, 0, 0) end +function verify_schedule(sysd::AbstractStateSpace{<:Discrete}, + K::AbstractMatrix{Float64}, z_0::AbstractVecOrMat, σ::AbstractVector{Int64}) + a = hold_kill(sysd, K) + + # Convert the actions σ to: 1=hit, 2=miss (instead of 0=miss) + σ = [i == 0 ? 2 : 1 for i in σ] + + z = evol(a, z_0, σ) + + # Convert trajectory to reachable sets by repeating the state twice for min/max + reachable = cat(z, z, dims=3) + maximum(deviation(a, z_0, reachable)) +end + +function schedule_to_sequence(schedule::Matrix{Int64}, task::Int64; H::Int64=100) + σ = schedule[task, :] + [repeat(σ, H ÷ length(σ)); σ[1:H % length(σ)]] +end + """ synthesize_constraints(sysd, K, z_0, d_max, maxwindow, n, t) @@ -80,8 +99,8 @@ guarantees the deviation upper bound is at most `d_max`. The system is specified [`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) + K::AbstractMatrix{Float64}, z_0::AbstractVecOrMat, d_max::Float64, + maxwindow::Int64, n::Int64, t::Int64) safe_constraints = MeetAny[] @@ -118,8 +137,8 @@ guarantees the deviation upper bound is at most `d_max`. The system is specified estimating the deviation upper bound as in [`estimate_deviation`](@ref). """ function estimate_constraints(sysd::AbstractStateSpace{<:Discrete}, - K::AbstractMatrix{Float64}, z_0::AbstractVecOrMat, d_max::Float64, - maxwindow::Int64, c::Float64, B::Float64, H::Int64) + K::AbstractMatrix{Float64}, z_0::AbstractVecOrMat, d_max::Float64, + maxwindow::Int64, c::Float64, B::Float64, H::Int64) safe_constraints = MeetAny[] meet = 1 From d142b49c8916851adb3c26b424fde4e8d7f26e48 Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Wed, 15 Mar 2023 20:32:07 -0400 Subject: [PATCH 03/17] Add export for new functions --- src/ControlTimingSafety.jl | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ControlTimingSafety.jl b/src/ControlTimingSafety.jl index 9fae80e..fbd66fd 100644 --- a/src/ControlTimingSafety.jl +++ b/src/ControlTimingSafety.jl @@ -18,7 +18,8 @@ include("safety.jl") export maximum_deviation_random, estimate_deviation include("probablesafety.jl") -export schedule_xghtc, synthesize_constraints, estimate_constraints +export schedule_xghtc, synthesize_constraints +export estimate_constraints, verify_schedule, schedule_to_sequence include("schedule_synthesis.jl") end From 835e02841310d7a2c3ac616fdb442a72ab8cef4c Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Sun, 19 Mar 2023 16:55:32 -0400 Subject: [PATCH 04/17] H is required --- src/schedule_synthesis.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index 58b8ff8..171c43d 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -85,7 +85,7 @@ function verify_schedule(sysd::AbstractStateSpace{<:Discrete}, maximum(deviation(a, z_0, reachable)) end -function schedule_to_sequence(schedule::Matrix{Int64}, task::Int64; H::Int64=100) +function schedule_to_sequence(schedule::Matrix{Int64}, task::Int64, H::Int64) σ = schedule[task, :] [repeat(σ, H ÷ length(σ)); σ[1:H % length(σ)]] end From 8a94d2f5963f5070f8cf9e3876b656490e772b61 Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Sun, 19 Mar 2023 17:40:53 -0400 Subject: [PATCH 05/17] Add `fullresults` options for constraint synthesis --- src/schedule_synthesis.jl | 141 ++++++++++++++++++++++---------------- 1 file changed, 82 insertions(+), 59 deletions(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index 171c43d..126f218 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -5,8 +5,8 @@ using DataStructures schedule_xghtc(constraints, H; slotsize=1, work_conserving=false) Generate a schedule for a set of weakly hard constraints. The schedule returned has the -type Matrix{Int64}, where the first dimension iterates through tasks, and the second -through time slots. If no safe schedule can be found, an empty Matrix{Int64} is returned. +type Matrix{Integer}, where the first dimension iterates through tasks, and the second +through time slots. If no safe schedule can be found, an empty Matrix{Integer} is returned. If the schedule returned is shorter than then time horizon H, it means the schedule is to be repeated and the system will still be safe until H. @@ -20,11 +20,11 @@ Constraints." ASPDAC 2023. DOI: [10.1145/3566097.3567848](https://doi.org/10.1145/3566097.3567848) """ -function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Int64; slotsize::Int64=1, work_conserving::Bool=false) +function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; slotsize::Integer=1, work_conserving::Bool=false) # Check if "utilization" is greater than available slot size utilization = sum(c -> c.meet/c.window, constraints) if utilization > slotsize - return Vector{Vector{Int64}}() + return Vector{Vector{Integer}}() end # Create the scheduler automaton from individual constraints @@ -33,14 +33,14 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Int64; slotsize::Int6 # Initialize the list of current states from the initial state of # scheduler automaton - current_states = Dict{Int64, LinkedList{Int64}}(AS.l_0 => list(AS.l_0)) + current_states = Dict{Integer, LinkedList{Integer}}(AS.l_0 => list(AS.l_0)) # Traverse the automaton until # (1) the required number of steps is reached, # (2) a cycle is found, or # (3) no more states are valid for exploration for step in 1:H - next_states = Dict{Int64, LinkedList{Int64}}() + next_states = Dict{Integer, LinkedList{Integer}}() for (l, path) in pairs(current_states), σ in AS.Σ l_new = AS.T(l, σ) if !AS.Q_f(l_new) || haskey(next_states, l_new) @@ -54,7 +54,7 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Int64; slotsize::Int6 if isempty(next_states) # No more valid states -> Case (3) - return zeros(Int64, 0, 0) + return zeros(Integer, 0, 0) end current_states = next_states @@ -68,11 +68,11 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Int64; slotsize::Int6 end # If the outer loop ends and accepting state is not found -> Case (1) - return zeros(Int64, 0, 0) + return zeros(Integer, 0, 0) end function verify_schedule(sysd::AbstractStateSpace{<:Discrete}, - K::AbstractMatrix{Float64}, z_0::AbstractVecOrMat, σ::AbstractVector{Int64}) + K::AbstractMatrix{Real}, z_0::AbstractVecOrMat, σ::AbstractVector{Integer}) a = hold_kill(sysd, K) # Convert the actions σ to: 1=hit, 2=miss (instead of 0=miss) @@ -85,7 +85,7 @@ function verify_schedule(sysd::AbstractStateSpace{<:Discrete}, maximum(deviation(a, z_0, reachable)) end -function schedule_to_sequence(schedule::Matrix{Int64}, task::Int64, H::Int64) +function schedule_to_sequence(schedule::Matrix{Integer}, task::Integer, H::Integer) σ = schedule[task, :] [repeat(σ, H ÷ length(σ)); σ[1:H % length(σ)]] end @@ -99,33 +99,51 @@ guarantees the deviation upper bound is at most `d_max`. The system is specified and `t` in [`bounded_runs_iter`](@ref). """ function synthesize_constraints(sysd::AbstractStateSpace{<:Discrete}, - K::AbstractMatrix{Float64}, z_0::AbstractVecOrMat, d_max::Float64, - maxwindow::Int64, n::Int64, H::Int64; iterations::Int64=ceil(H / n)) + K::AbstractMatrix{Real}, z_0::AbstractVecOrMat, d_max::Real, + maxwindow::Integer, n::Integer, H::Integer; fullresults=false) - safe_constraints = MeetAny[] + devs = fill(Inf, maxwindow, maxwindow) + safe_constraints = [MeetAny(1, 1)] - # Do not need to go through all O(maxwindow^2) constraints, - # see paper for optimization argument - meet = 1 - for window in 2:maxwindow - while meet < window - 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, iterations)[1:H, :, :] - m = maximum(deviation(a, z_0, reachable)) - if m <= d_max - # All constraints with (m, window) where m >= meet are valid - for i in meet:window-1 - push!(safe_constraints, MeetAny(i, window)) + if fullresults + for window = 2:maxwindow, meet=1:window + devs[window, meet] = devub(meet, window, sysd, K, z_0, d_max, n, H) + if devs[window, meet] <= d_max && meet < window + push!(safe_constraints, MeetAny(meet, window)) + end + end + else + # Do not need to go through all O(maxwindow^2) constraints, + # see paper for optimization argument + meet = 1 + for window in 1:maxwindow + while meet <= window + devs[window, meet] = devub(meet, window, sysd, K, z_0, d_max, n, H) + if devs[window, meet] <= d_max + # All constraints with (m, window) where m >= meet are valid + for i in meet:window-1 + push!(safe_constraints, MeetAny(i, window)) + end + break end - break + meet += 1 end - meet += 1 end end - safe_constraints + safe_constraints, devs +end + +function devub(meet::Integer, window::Integer, sysd::AbstractStateSpace{<:Discrete}, + K::AbstractMatrix{Real}, z_0::AbstractVecOrMat, d_max::Real, n::Integer, + H::Integer; iterations=ceil(H/n)) + if meet == window + return 0. + end + constraint = MeetAny(meet, window) + a = hold_kill(sysd, K, constraint) + reachable = bounded_runs_iter(a, z_0, n, iterations, safety_margin=d_max)[1:H, :, :] + maximum(deviation(a, z_0, reachable)) end """ @@ -137,28 +155,33 @@ guarantees the deviation upper bound is at most `d_max`. The system is specified estimating the deviation upper bound as in [`estimate_deviation`](@ref). """ function estimate_constraints(sysd::AbstractStateSpace{<:Discrete}, - K::AbstractMatrix{Float64}, z_0::AbstractVecOrMat, d_max::Float64, - maxwindow::Int64, c::Float64, B::Float64, H::Int64) - safe_constraints = MeetAny[] + K::AbstractMatrix{Real}, z_0::AbstractVecOrMat, d_max::Real, + maxwindow::Integer, c::Real, B::Real, H::Integer) + + devs = fill(Inf, maxwindow, maxwindow) + safe_constraints = [MeetAny(1, 1)] - meet = 1 - for window in 2:maxwindow - while meet < window + # meet = 1 + for window in 1:maxwindow + # while meet < window + for meet in 1:window constraint = MeetAny(meet, window) a = hold_kill(sysd, K, constraint) sampler = SamplerUniformMeetAny(constraint, H) m = estimate_deviation(a, sampler, z_0, c, B) - if m <= d_max - for i in meet:window-1 - push!(safe_constraints, MeetAny(i, window)) - end - break - end - meet += 1 + devs[window, meet] = round(m, sigdigits=4) + # if m <= d_max + # for i in meet:window-1 + # push!(safe_constraints, MeetAny(i, window)) + # end + # break + # end + # meet += 1 end end - safe_constraints + # display(devs) + safe_constraints, devs end # Helper functions @@ -172,7 +195,7 @@ julia> ControlTimingSafety._undigit([1, 0, 0]) 4 ``` """ -function _undigit(d::Vector{Int64}; base=2) +function _undigit(d::Vector{Integer}; base=2) s = 0 mult = 1 for val in reverse(d) @@ -188,7 +211,7 @@ end Digits **b**ase **2**, **r**everse A shortcut for `digits(x, base=2, pad=pad) |> reverse` """ -_digits_b2r(x::Int64; pad::Int64=0) = digits(x, base=2, pad=pad) |> reverse +_digits_b2r(x::Integer; pad::Integer=0) = digits(x, base=2, pad=pad) |> reverse """ _state_separation(l, B[, indigits=false]) @@ -200,7 +223,7 @@ list of individual states. For example ```jldoctest julia> ControlTimingSafety._state_separation(6, [1, 2]) -2-element Vector{Int64}: +2-element Vector{Integer}: 1 2 ``` @@ -211,7 +234,7 @@ The explanation of the example is as follows [[1], [1, 0]] -> [1, 2] ``` """ -function _state_separation(l::Int64, B::Vector{Int64}; indigits=false) +function _state_separation(l::Integer, B::Vector{Integer}; indigits=false) @boundscheck l < 2^sum(B) || throw(ArgumentError("l has more bits than the sum of B")) bits = digits(l, base=2, pad=sum(B)) |> reverse @@ -233,13 +256,13 @@ dynamical matrix of the system. """ struct _ConstraintAutomaton # # of locations. Legal locations are in the range 0:L-1. - L::Int64 + L::Integer # # of actions. Legal actions are in the range 0:Σ-1. - Σ::Int64 + Σ::Integer # Transition function. T(l,σ) is a location in 0:L-1. T::Function # Initial location in L. - l_0::Int64 + l_0::Integer # Function that returns whether a location is final Q_f::Function end @@ -275,17 +298,17 @@ Struct for a synthesized automaton from multiple constraint automata. """ struct _SynthesizedAutomaton # # of comprising automata - N::Int64 + N::Integer # List of bits for all comprising controllers - B::Vector{Int64} + B::Vector{Integer} # Locations. Legal locations are in the range 0:L-1. - L::Int64 + L::Integer # List of actions. - Σ::Vector{Int64} + Σ::Vector{Integer} # Transition function. T(l,σ) is a location in 0:L-1. T::Function # Initial location in L. - l_0::Int64 + l_0::Integer # Function that returns whether a location is final. Q_f::Function end @@ -293,10 +316,10 @@ end """ Build a scheduler automaton from a given list of controller automata """ -function _SynthesizedAutomaton(controllers::Vector{_ConstraintAutomaton}; slotsize::Int64=1, work_conserving::Bool=false) +function _SynthesizedAutomaton(controllers::Vector{_ConstraintAutomaton}; slotsize::Integer=1, work_conserving::Bool=false) # Converting tuple to array with collect() N = length(controllers) - B = map(a -> ceil(Int64, log2(a.L)), controllers) |> collect + B = map(a -> ceil(Integer, log2(a.L)), controllers) |> collect L = 2^sum(B) all_actions = 0:2^length(controllers)-1 @@ -329,7 +352,7 @@ function _SynthesizedAutomaton(controllers::Vector{_ConstraintAutomaton}; slotsi _SynthesizedAutomaton(N, B, L, Σ, T, L-1, Q_f) end -function _path_to_schedule(path::Union{LinkedList{Int64}, Vector{Int64}}, AS::_SynthesizedAutomaton) +function _path_to_schedule(path::Union{LinkedList{Integer}, Vector{Integer}}, AS::_SynthesizedAutomaton) # Convert path to Vector path = collect(path) From 68a7dbb3d00054323aa329ea16944b582389d3d6 Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Sun, 19 Mar 2023 18:07:21 -0400 Subject: [PATCH 06/17] Collections now have the correct type for items --- src/schedule_synthesis.jl | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index 126f218..c202404 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -5,8 +5,8 @@ using DataStructures schedule_xghtc(constraints, H; slotsize=1, work_conserving=false) Generate a schedule for a set of weakly hard constraints. The schedule returned has the -type Matrix{Integer}, where the first dimension iterates through tasks, and the second -through time slots. If no safe schedule can be found, an empty Matrix{Integer} is returned. +type Matrix{<:Integer}, where the first dimension iterates through tasks, and the second +through time slots. If no safe schedule can be found, an empty Matrix{<:Integer} is returned. If the schedule returned is shorter than then time horizon H, it means the schedule is to be repeated and the system will still be safe until H. @@ -24,7 +24,7 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; slotsize::In # Check if "utilization" is greater than available slot size utilization = sum(c -> c.meet/c.window, constraints) if utilization > slotsize - return Vector{Vector{Integer}}() + return Vector{Vector{<:Integer}}() end # Create the scheduler automaton from individual constraints @@ -33,14 +33,14 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; slotsize::In # Initialize the list of current states from the initial state of # scheduler automaton - current_states = Dict{Integer, LinkedList{Integer}}(AS.l_0 => list(AS.l_0)) + current_states = Dict{Integer, LinkedList{<:Integer}}(AS.l_0 => list(AS.l_0)) # Traverse the automaton until # (1) the required number of steps is reached, # (2) a cycle is found, or # (3) no more states are valid for exploration for step in 1:H - next_states = Dict{Integer, LinkedList{Integer}}() + next_states = Dict{Integer, LinkedList{<:Integer}}() for (l, path) in pairs(current_states), σ in AS.Σ l_new = AS.T(l, σ) if !AS.Q_f(l_new) || haskey(next_states, l_new) @@ -72,7 +72,7 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; slotsize::In end function verify_schedule(sysd::AbstractStateSpace{<:Discrete}, - K::AbstractMatrix{Real}, z_0::AbstractVecOrMat, σ::AbstractVector{Integer}) + K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, σ::AbstractVector{<:Integer}) a = hold_kill(sysd, K) # Convert the actions σ to: 1=hit, 2=miss (instead of 0=miss) @@ -85,7 +85,7 @@ function verify_schedule(sysd::AbstractStateSpace{<:Discrete}, maximum(deviation(a, z_0, reachable)) end -function schedule_to_sequence(schedule::Matrix{Integer}, task::Integer, H::Integer) +function schedule_to_sequence(schedule::Matrix{<:Integer}, task::Integer, H::Integer) σ = schedule[task, :] [repeat(σ, H ÷ length(σ)); σ[1:H % length(σ)]] end @@ -99,7 +99,7 @@ guarantees the deviation upper bound is at most `d_max`. The system is specified and `t` in [`bounded_runs_iter`](@ref). """ function synthesize_constraints(sysd::AbstractStateSpace{<:Discrete}, - K::AbstractMatrix{Real}, z_0::AbstractVecOrMat, d_max::Real, + K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, d_max::Real, maxwindow::Integer, n::Integer, H::Integer; fullresults=false) devs = fill(Inf, maxwindow, maxwindow) @@ -135,7 +135,7 @@ function synthesize_constraints(sysd::AbstractStateSpace{<:Discrete}, end function devub(meet::Integer, window::Integer, sysd::AbstractStateSpace{<:Discrete}, - K::AbstractMatrix{Real}, z_0::AbstractVecOrMat, d_max::Real, n::Integer, + K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, d_max::Real, n::Integer, H::Integer; iterations=ceil(H/n)) if meet == window return 0. @@ -155,7 +155,7 @@ guarantees the deviation upper bound is at most `d_max`. The system is specified estimating the deviation upper bound as in [`estimate_deviation`](@ref). """ function estimate_constraints(sysd::AbstractStateSpace{<:Discrete}, - K::AbstractMatrix{Real}, z_0::AbstractVecOrMat, d_max::Real, + K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, d_max::Real, maxwindow::Integer, c::Real, B::Real, H::Integer) devs = fill(Inf, maxwindow, maxwindow) @@ -195,7 +195,7 @@ julia> ControlTimingSafety._undigit([1, 0, 0]) 4 ``` """ -function _undigit(d::Vector{Integer}; base=2) +function _undigit(d::Vector{<:Integer}; base=2) s = 0 mult = 1 for val in reverse(d) @@ -223,7 +223,7 @@ list of individual states. For example ```jldoctest julia> ControlTimingSafety._state_separation(6, [1, 2]) -2-element Vector{Integer}: +2-element Vector{<:Integer}: 1 2 ``` @@ -234,7 +234,7 @@ The explanation of the example is as follows [[1], [1, 0]] -> [1, 2] ``` """ -function _state_separation(l::Integer, B::Vector{Integer}; indigits=false) +function _state_separation(l::Integer, B::Vector{<:Integer}; indigits=false) @boundscheck l < 2^sum(B) || throw(ArgumentError("l has more bits than the sum of B")) bits = digits(l, base=2, pad=sum(B)) |> reverse @@ -300,11 +300,11 @@ struct _SynthesizedAutomaton # # of comprising automata N::Integer # List of bits for all comprising controllers - B::Vector{Integer} + B::Vector{<:Integer} # Locations. Legal locations are in the range 0:L-1. L::Integer # List of actions. - Σ::Vector{Integer} + Σ::Vector{<:Integer} # Transition function. T(l,σ) is a location in 0:L-1. T::Function # Initial location in L. @@ -352,7 +352,7 @@ function _SynthesizedAutomaton(controllers::Vector{_ConstraintAutomaton}; slotsi _SynthesizedAutomaton(N, B, L, Σ, T, L-1, Q_f) end -function _path_to_schedule(path::Union{LinkedList{Integer}, Vector{Integer}}, AS::_SynthesizedAutomaton) +function _path_to_schedule(path::Union{LinkedList{<:Integer}, Vector{<:Integer}}, AS::_SynthesizedAutomaton) # Convert path to Vector path = collect(path) From 8269d09a8fea376ecceaaeee90b7bc44303fb2ce Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Tue, 4 Apr 2023 15:18:49 -0400 Subject: [PATCH 07/17] Bayes factor is now calculate with uniform prior --- src/probablesafety.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/probablesafety.jl b/src/probablesafety.jl index 00d8c97..657de09 100644 --- a/src/probablesafety.jl +++ b/src/probablesafety.jl @@ -99,7 +99,7 @@ Base.@propagate_inbounds function estimate_deviation(a::Automaton, @boundscheck nominal_trajectory === nothing || size(nominal_trajectory) == (size(z_0,1), sampler.H+1) || throw(DimensionMismatch("nominal_trajectory must have size (size(z_0,1), sampler.H+1)")) # Compute the number of samples to draw for the required confidence and Bayes factor - K = ceil(Int64, -log(c, B+1)) + K = ceil(Int64, -log(c, c/(1-c)*B+1)) if estimate === nothing # Take our initial estimate from a small random sample estimate = maximum_deviation_random(a, sampler, estimate_samples, z_0, metric=metric, nominal=nominal, nominal_trajectory=nominal_trajectory) From 427a7a087203da8bcc7e5df1da26de1034ec6763 Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Wed, 5 Apr 2023 13:58:44 -0400 Subject: [PATCH 08/17] Revert "Bayes factor is now calculate with uniform prior" This reverts commit 8269d09a8fea376ecceaaeee90b7bc44303fb2ce. --- src/probablesafety.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/probablesafety.jl b/src/probablesafety.jl index 657de09..00d8c97 100644 --- a/src/probablesafety.jl +++ b/src/probablesafety.jl @@ -99,7 +99,7 @@ Base.@propagate_inbounds function estimate_deviation(a::Automaton, @boundscheck nominal_trajectory === nothing || size(nominal_trajectory) == (size(z_0,1), sampler.H+1) || throw(DimensionMismatch("nominal_trajectory must have size (size(z_0,1), sampler.H+1)")) # Compute the number of samples to draw for the required confidence and Bayes factor - K = ceil(Int64, -log(c, c/(1-c)*B+1)) + K = ceil(Int64, -log(c, B+1)) if estimate === nothing # Take our initial estimate from a small random sample estimate = maximum_deviation_random(a, sampler, estimate_samples, z_0, metric=metric, nominal=nominal, nominal_trajectory=nominal_trajectory) From 112b0053883af9abf4d81a0a5066043807c9f5fe Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Tue, 11 Apr 2023 12:47:47 -0400 Subject: [PATCH 09/17] Fix bound error when bounded_runs_iter() returns early --- src/schedule_synthesis.jl | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index ebf486f..cd53e60 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -142,7 +142,8 @@ function devub(meet::Integer, window::Integer, sysd::AbstractStateSpace{<:Discre end constraint = MeetAny(meet, window) a = hold_kill(sysd, K, constraint) - reachable = bounded_runs_iter(a, z_0, n, ceil(Int64, H/n), safety_margin=d_max)[1:H, :, :] + reachable = bounded_runs_iter(a, z_0, n, ceil(Int64, H/n), safety_margin=d_max) + reachable = reachable[1:min(H, size(reachable, 1)), :, :] maximum(deviation(a, z_0, reachable)) end From f73d2f044b30738920cdb2792fe653a344a908dc Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Thu, 29 Jun 2023 11:11:49 -0400 Subject: [PATCH 10/17] Minor changes --- src/schedule_synthesis.jl | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index cd53e60..d7f192b 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -20,7 +20,8 @@ Constraints." ASPDAC 2023. DOI: [10.1145/3566097.3567848](https://doi.org/10.1145/3566097.3567848) """ -function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; slotsize::Integer=1, work_conserving::Bool=false) +function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; + slotsize::Integer=1, work_conserving::Bool=false) # Check if "utilization" is greater than available slot size utilization = sum(c -> c.meet/c.window, constraints) if utilization > slotsize @@ -71,13 +72,25 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; slotsize::In return zeros(Integer, 0, 0) end +function schedule_xghtc(allconstraints::Vector{<:Vector{<:MeetAny}}, H::Integer; + slotsize::Integer=1, work_conserving::Bool=false) + for constraints in Iterators.product(allconstraints...) + sch = schedule_xghtc(collect(constraints), H, + slotsize=slotsize, work_conserving=work_conserving) + if length(sch) > 0 + println(constraints) + return sch + end + end + return zeros(Integer, 0, 0) +end + function verify_schedule(sysd::AbstractStateSpace{<:Discrete}, K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, σ::AbstractVector{<:Integer}) a = hold_kill(sysd, K) # Convert the actions σ to: 1=hit, 2=miss (instead of 0=miss) σ = [i == 0 ? 2 : 1 for i in σ] - z = evol(a, z_0, σ) # Convert trajectory to reachable sets by repeating the state twice for min/max @@ -106,7 +119,7 @@ function synthesize_constraints(sysd::AbstractStateSpace{<:Discrete}, safe_constraints = [MeetAny(1, 1)] if fullresults - for window = 2:maxwindow, meet=1:window + for window = 1:maxwindow, meet=1:window devs[window, meet] = devub(meet, window, sysd, K, z_0, d_max, n, H) if devs[window, meet] <= d_max && meet < window push!(safe_constraints, MeetAny(meet, window)) @@ -144,6 +157,7 @@ function devub(meet::Integer, window::Integer, sysd::AbstractStateSpace{<:Discre a = hold_kill(sysd, K, constraint) reachable = bounded_runs_iter(a, z_0, n, ceil(Int64, H/n), safety_margin=d_max) reachable = reachable[1:min(H, size(reachable, 1)), :, :] + # @info "Data" meet window size(reachable, 1) argmax(deviation(a, z_0, reachable)) maximum(deviation(a, z_0, reachable)) end From 8099240a024f9a479d5df112f0fab0ff0bdd9356 Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Thu, 29 Jun 2023 11:33:05 -0400 Subject: [PATCH 11/17] Only use abstract types for function argument --- src/schedule_synthesis.jl | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index d7f192b..5d2913b 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -25,7 +25,7 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; # Check if "utilization" is greater than available slot size utilization = sum(c -> c.meet/c.window, constraints) if utilization > slotsize - return Vector{Vector{<:Integer}}() + return Vector{Vector{Int64}}() end # Create the scheduler automaton from individual constraints @@ -34,14 +34,14 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; # Initialize the list of current states from the initial state of # scheduler automaton - current_states = Dict{Integer, LinkedList{<:Integer}}(AS.l_0 => list(AS.l_0)) + current_states = Dict{Int64, LinkedList{Int64}}(AS.l_0 => list(AS.l_0)) # Traverse the automaton until # (1) the required number of steps is reached, # (2) a cycle is found, or # (3) no more states are valid for exploration for step in 1:H - next_states = Dict{Integer, LinkedList{<:Integer}}() + next_states = Dict{Int64, LinkedList{Int64}}() for (l, path) in pairs(current_states), σ in AS.Σ l_new = AS.T(l, σ) if !AS.Q_f(l_new) || haskey(next_states, l_new) @@ -55,7 +55,7 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; if isempty(next_states) # No more valid states -> Case (3) - return zeros(Integer, 0, 0) + return zeros(Int64, 0, 0) end current_states = next_states @@ -69,7 +69,7 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; end # If the outer loop ends and accepting state is not found -> Case (1) - return zeros(Integer, 0, 0) + return zeros(Int64, 0, 0) end function schedule_xghtc(allconstraints::Vector{<:Vector{<:MeetAny}}, H::Integer; @@ -82,7 +82,7 @@ function schedule_xghtc(allconstraints::Vector{<:Vector{<:MeetAny}}, H::Integer; return sch end end - return zeros(Integer, 0, 0) + return zeros(Int64, 0, 0) end function verify_schedule(sysd::AbstractStateSpace{<:Discrete}, @@ -271,13 +271,13 @@ dynamical matrix of the system. """ struct _ConstraintAutomaton # # of locations. Legal locations are in the range 0:L-1. - L::Integer + L::Int64 # # of actions. Legal actions are in the range 0:Σ-1. - Σ::Integer + Σ::Int64 # Transition function. T(l,σ) is a location in 0:L-1. T::Function # Initial location in L. - l_0::Integer + l_0::Int64 # Function that returns whether a location is final Q_f::Function end @@ -313,17 +313,17 @@ Struct for a synthesized automaton from multiple constraint automata. """ struct _SynthesizedAutomaton # # of comprising automata - N::Integer + N::Int64 # List of bits for all comprising controllers - B::Vector{<:Integer} + B::Vector{Int64} # Locations. Legal locations are in the range 0:L-1. - L::Integer + L::Int64 # List of actions. - Σ::Vector{<:Integer} + Σ::Vector{Int64} # Transition function. T(l,σ) is a location in 0:L-1. T::Function # Initial location in L. - l_0::Integer + l_0::Int64 # Function that returns whether a location is final. Q_f::Function end @@ -334,7 +334,7 @@ Build a scheduler automaton from a given list of controller automata function _SynthesizedAutomaton(controllers::Vector{_ConstraintAutomaton}; slotsize::Integer=1, work_conserving::Bool=false) # Converting tuple to array with collect() N = length(controllers) - B = map(a -> ceil(Integer, log2(a.L)), controllers) |> collect + B = map(a -> ceil(Int64, log2(a.L)), controllers) |> collect L = 2^sum(B) all_actions = 0:2^length(controllers)-1 From 21ed0c97cd839b862f4b6f29f475f094e2f72f91 Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Fri, 30 Jun 2023 14:52:21 -0400 Subject: [PATCH 12/17] Update function docstrings and tests. --- src/schedule_synthesis.jl | 42 ++++++++++++++++++++++++++------ test/schedule_synthesis_tests.jl | 2 +- 2 files changed, 35 insertions(+), 9 deletions(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index 8751ba9..7e2c2ea 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -2,7 +2,7 @@ using RealTimeScheduling using DataStructures """ - schedule_xghtc(constraints; slotsize=1, H=100, work_conserving=false) + schedule_xghtc(constraints, H; slotsize=1, work_conserving=false) Generate a schedule for a set of weakly hard constraints. The schedule returned has the type Matrix{<:Integer}, where the first dimension iterates through tasks, and the second @@ -72,6 +72,12 @@ function schedule_xghtc(constraints::Vector{<:MeetAny}, H::Integer; return zeros(Int64, 0, 0) end +""" + schedule_xghtc(allconstraints, H; slotsize=1, work_conserving=false) + +Given a list of safe constraints for each system, synthesize a schedule using one safe +constraint from each list. The first successful synthesis result is returned. +""" function schedule_xghtc(allconstraints::Vector{<:Vector{<:MeetAny}}, H::Integer; slotsize::Integer=1, work_conserving::Bool=false) for constraints in Iterators.product(allconstraints...) @@ -85,6 +91,13 @@ function schedule_xghtc(allconstraints::Vector{<:Vector{<:MeetAny}}, H::Integer; return zeros(Int64, 0, 0) end +""" + verify_schedule(sysd, K, z_0, σ) + +Given a discrete state-space model, feedback gain, the initial state, and a sequence of +deadline hits and misses, returns the maximum deviaiton between the resulting trajectory +and the nominal trajectory for that system where all deadlines are met. +""" function verify_schedule(sysd::AbstractStateSpace{<:Discrete}, K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, σ::AbstractVector{<:Integer}) a = hold_kill(sysd, K) @@ -98,6 +111,13 @@ function verify_schedule(sysd::AbstractStateSpace{<:Discrete}, maximum(deviation(a, z_0, reachable)) end +""" + schedule_to_sequence(schedule, task, H) + +Given a schedule in the matrix form, the position of the task in the schedule and the desired +length of the sequence, returns a sequence of 0s and 1s of length H representing the deadline +hits and misses for that task under the given schedule. +""" function schedule_to_sequence(schedule::Matrix{<:Integer}, task::Integer, H::Integer) σ = schedule[task, :] [repeat(σ, H ÷ length(σ)); σ[1:H % length(σ)]] @@ -147,6 +167,12 @@ function synthesize_constraints(sysd::AbstractStateSpace{<:Discrete}, safe_constraints, devs end +""" + devub(meet, window, sysd, K, z_0, d_max, n, H) + +Compute the deviation upper bound for a given system under the weakly hard constraint +(meet, window), over a specified time horizon. +""" function devub(meet::Integer, window::Integer, sysd::AbstractStateSpace{<:Discrete}, K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, d_max::Real, n::Integer, H::Integer) @@ -185,13 +211,13 @@ function estimate_constraints(sysd::AbstractStateSpace{<:Discrete}, sampler = SamplerUniformMeetAny(constraint, H) m = estimate_deviation(a, sampler, z_0, c, B) devs[window, meet] = round(m, sigdigits=4) - # if m <= d_max - # for i in meet:window-1 - # push!(safe_constraints, MeetAny(i, window)) - # end - # break - # end - # meet += 1 + if m <= d_max + for i in meet:window-1 + push!(safe_constraints, MeetAny(i, window)) + end + break + end + meet += 1 end end diff --git a/test/schedule_synthesis_tests.jl b/test/schedule_synthesis_tests.jl index 783c481..df7c154 100644 --- a/test/schedule_synthesis_tests.jl +++ b/test/schedule_synthesis_tests.jl @@ -49,7 +49,7 @@ using RealTimeScheduling RealTimeScheduling.MeetAny(1, 4), RealTimeScheduling.MeetAny(1, 4), RealTimeScheduling.MeetAny(1, 2) - ], slotsize=2) == [ + ], 100, slotsize=2) == [ 0 1 0 0 1 0 0 1 0 0 1 0 1 0 1 1 0 1 1 0 1 1 0 1 1 0 0 0 1 0 0 0 1 0 0 0 From a802338991f4c18da3db1501809809f52649b3da Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Tue, 4 Jul 2023 08:25:31 -0400 Subject: [PATCH 13/17] Should pass all tests now! --- src/schedule_synthesis.jl | 50 ++++++++++++++++++++------------ test/schedule_synthesis_tests.jl | 1 + 2 files changed, 33 insertions(+), 18 deletions(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index 7e2c2ea..28e4147 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -164,7 +164,7 @@ function synthesize_constraints(sysd::AbstractStateSpace{<:Discrete}, end end - safe_constraints, devs + safe_constraints end """ @@ -197,32 +197,46 @@ estimating the deviation upper bound as in [`estimate_deviation`](@ref). """ function estimate_constraints(sysd::AbstractStateSpace{<:Discrete}, K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, d_max::Real, - maxwindow::Integer, c::Real, B::Real, H::Integer) + maxwindow::Integer, c::Real, B::Real, H::Integer; fullresults=false) devs = fill(Inf, maxwindow, maxwindow) safe_constraints = [MeetAny(1, 1)] - # meet = 1 - for window in 1:maxwindow - # while meet < window - for meet in 1:window - constraint = MeetAny(meet, window) - a = hold_kill(sysd, K, constraint) - sampler = SamplerUniformMeetAny(constraint, H) - m = estimate_deviation(a, sampler, z_0, c, B) - devs[window, meet] = round(m, sigdigits=4) - if m <= d_max - for i in meet:window-1 - push!(safe_constraints, MeetAny(i, window)) + if fullresults + for window = 1:maxwindow, meet=1:window + devs[window, meet] = devest(meet, window, sysd, K, z_0, c, B, H) + if devs[window, meet] <= d_max && meet < window + push!(safe_constraints, MeetAny(meet, window)) + end + end + else + meet = 1 + for window in 1:maxwindow + while meet <= window + devs[window, meet] = devest(meet, window, sysd, K, z_0, c, B, H) + if devs[window, meet] <= d_max + for i in meet:window-1 + push!(safe_constraints, MeetAny(i, window)) + end + break end - break + meet += 1 end - meet += 1 end end - # display(devs) - safe_constraints, devs + safe_constraints +end + +function devest(meet::Integer, window::Integer, sysd::AbstractStateSpace{<:Discrete}, + K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, c::Real, B::Real, H::Integer) + if meet == window + return 0. + end + constraint = MeetAny(meet, window) + a = hold_kill(sysd, K, constraint) + sampler = SamplerUniformMeetAny(constraint, H) + estimate_deviation(a, sampler, z_0, c, B) end # Helper functions diff --git a/test/schedule_synthesis_tests.jl b/test/schedule_synthesis_tests.jl index df7c154..5e5f13d 100644 --- a/test/schedule_synthesis_tests.jl +++ b/test/schedule_synthesis_tests.jl @@ -36,6 +36,7 @@ using RealTimeScheduling end @test synthesize_constraints(sysd, K, repeat([10.0], 3), 5.5, 6, 10, 10) == [ + RealTimeScheduling.MeetAny(1, 1), RealTimeScheduling.MeetAny(1, 2), RealTimeScheduling.MeetAny(2, 3), RealTimeScheduling.MeetAny(3, 4), From 3a81e3df207accabcf0a409d5709d12034d62a95 Mon Sep 17 00:00:00 2001 From: Shengjie Xu Date: Wed, 5 Jul 2023 15:16:44 -0400 Subject: [PATCH 14/17] Ignoring all manifest files --- .gitignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index b067edd..ba39cc5 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1 @@ -/Manifest.toml +Manifest.toml From e1d144c1255c95df3e4712ca58712cb2d3460a9b Mon Sep 17 00:00:00 2001 From: shengjiex98 Date: Wed, 5 Jul 2023 19:46:49 -0400 Subject: [PATCH 15/17] Return types should be Int64 instead of Integer --- src/schedule_synthesis.jl | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index 28e4147..7e9d73e 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -5,8 +5,8 @@ using DataStructures schedule_xghtc(constraints, H; slotsize=1, work_conserving=false) Generate a schedule for a set of weakly hard constraints. The schedule returned has the -type Matrix{<:Integer}, where the first dimension iterates through tasks, and the second -through time slots. If no safe schedule can be found, an empty Matrix{<:Integer} is returned. +type Matrix{<:Int64}, where the first dimension iterates through tasks, and the second +through time slots. If no safe schedule can be found, an empty Matrix{<:Int64} is returned. If the schedule returned is shorter than then time horizon H, it means the schedule is to be repeated and the system will still be safe until H. @@ -278,7 +278,7 @@ list of individual states. For example ```jldoctest julia> ControlTimingSafety._state_separation(6, [1, 2]) -2-element Vector{<:Integer}: +2-element Vector{<:Int64}: 1 2 ``` From 3966531d129d0c74bc66c7ce2bf362a105aac779 Mon Sep 17 00:00:00 2001 From: shengjiex98 Date: Wed, 5 Jul 2023 19:47:43 -0400 Subject: [PATCH 16/17] Last commit was almost correct :/ --- src/schedule_synthesis.jl | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index 7e9d73e..276f33a 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -5,8 +5,8 @@ using DataStructures schedule_xghtc(constraints, H; slotsize=1, work_conserving=false) Generate a schedule for a set of weakly hard constraints. The schedule returned has the -type Matrix{<:Int64}, where the first dimension iterates through tasks, and the second -through time slots. If no safe schedule can be found, an empty Matrix{<:Int64} is returned. +type Matrix{Int64}, where the first dimension iterates through tasks, and the second +through time slots. If no safe schedule can be found, an empty Matrix{Int64} is returned. If the schedule returned is shorter than then time horizon H, it means the schedule is to be repeated and the system will still be safe until H. @@ -278,7 +278,7 @@ list of individual states. For example ```jldoctest julia> ControlTimingSafety._state_separation(6, [1, 2]) -2-element Vector{<:Int64}: +2-element Vector{Int64}: 1 2 ``` From 1356fee973fe5fa8864fd6e6b3604c5adcba57bc Mon Sep 17 00:00:00 2001 From: shengjiex98 Date: Wed, 5 Jul 2023 20:09:58 -0400 Subject: [PATCH 17/17] Update documentation for new functions --- docs/src/schedule_synthesis.md | 15 ++++++++++++++- src/ControlTimingSafety.jl | 1 + src/schedule_synthesis.jl | 8 +++++++- 3 files changed, 22 insertions(+), 2 deletions(-) diff --git a/docs/src/schedule_synthesis.md b/docs/src/schedule_synthesis.md index 5f433ad..9fd95e1 100644 --- a/docs/src/schedule_synthesis.md +++ b/docs/src/schedule_synthesis.md @@ -1,6 +1,6 @@ # 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, @@ -14,4 +14,17 @@ The main functionality of this section is divided into two functions ```@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 ``` diff --git a/src/ControlTimingSafety.jl b/src/ControlTimingSafety.jl index fbd66fd..c63eab0 100644 --- a/src/ControlTimingSafety.jl +++ b/src/ControlTimingSafety.jl @@ -20,6 +20,7 @@ include("probablesafety.jl") export schedule_xghtc, synthesize_constraints export estimate_constraints, verify_schedule, schedule_to_sequence +export devub, devest include("schedule_synthesis.jl") end diff --git a/src/schedule_synthesis.jl b/src/schedule_synthesis.jl index 276f33a..cc86e3c 100644 --- a/src/schedule_synthesis.jl +++ b/src/schedule_synthesis.jl @@ -171,7 +171,7 @@ end devub(meet, window, sysd, K, z_0, d_max, n, H) Compute the deviation upper bound for a given system under the weakly hard constraint -(meet, window), over a specified time horizon. +(meet, window), over a specified time horizon. Uses [`bounded_runs_iter`](@ref). """ function devub(meet::Integer, window::Integer, sysd::AbstractStateSpace{<:Discrete}, K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, d_max::Real, n::Integer, @@ -228,6 +228,12 @@ function estimate_constraints(sysd::AbstractStateSpace{<:Discrete}, safe_constraints end +""" + devest(meet, window, sysd, K, z_0, c, B, H) + +Estimate the deviation upper bound for a given system under the weakly hard constraint +(meet, window), over a specified time horizon. Uses [`estimate_deviation`](@ref). +""" function devest(meet::Integer, window::Integer, sysd::AbstractStateSpace{<:Discrete}, K::AbstractMatrix{<:Real}, z_0::AbstractVecOrMat, c::Real, B::Real, H::Integer) if meet == window