From a4444d61e613e1b454ce66547943ff70f0f04415 Mon Sep 17 00:00:00 2001 From: Clara Hobbs Date: Thu, 10 Nov 2022 12:29:22 -0500 Subject: [PATCH] Add satisfies function for weakly hard constraints (#6) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add satisfies function * Add tests for weakly hard rand and satisfies * Add satisfies to documentation * Test satisfies for HRT and BE constraints * Add ⊬ operator for negation of ⊢ * Document and test the ⊬ operator --- docs/src/weaklyhard.md | 17 ++++++- src/RealTimeScheduling.jl | 3 ++ src/weaklyhard.jl | 69 +++++++++++++++++++++++++++++ test/weaklyhard.jl | 93 +++++++++++++++++++++++++++------------ 4 files changed, 153 insertions(+), 29 deletions(-) diff --git a/docs/src/weaklyhard.md b/docs/src/weaklyhard.md index a6ad2de..6da5664 100644 --- a/docs/src/weaklyhard.md +++ b/docs/src/weaklyhard.md @@ -7,7 +7,8 @@ RealTimeScheduling provides basic support for weakly hard constraints. still very incomplete. For now, we mainly support the constraints themselves, as well as comparisons between them. -Constraints that are logically equivalent compare as equal: +Constraints that are logically equivalent compare as equal, even if they are +represented differently. ```@jldoctest julia> MeetAny(1, 1) == MeetRow(3, 5) == MissRow(0) == HardRealTime() @@ -20,6 +21,17 @@ julia> MeetRow(4, 5) == MeetRow(2, 5) false ``` +Testing whether a `BitVector` satisfies a [`WeaklyHardConstraint`](@ref) is +supported. + +```@jldoctest +julia> BitVector([0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 1, 1]) ⊢ MeetRow(2, 5) +true + +julia> BitVector([0, 1, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1]) ⊢ MeetRow(2, 5) +false +``` + ```@docs WeaklyHardConstraint @@ -29,6 +41,9 @@ MeetRow MissRow HardRealTime BestEffort +satisfies +⊢ +⊬ ``` ## Sampling from Weakly Hard Constraints diff --git a/src/RealTimeScheduling.jl b/src/RealTimeScheduling.jl index c4d885f..0099d13 100644 --- a/src/RealTimeScheduling.jl +++ b/src/RealTimeScheduling.jl @@ -31,6 +31,9 @@ export AbstractRealTimeTask, HardRealTime, BestEffort, SamplerUniformMissRow, + satisfies, + ⊢, + ⊬, # Schedulability tests schedulable_fixed_priority include("weaklyhard.jl") diff --git a/src/weaklyhard.jl b/src/weaklyhard.jl index fb9ac0e..26656c2 100644 --- a/src/weaklyhard.jl +++ b/src/weaklyhard.jl @@ -232,3 +232,72 @@ function Random.rand(rng::Random.AbstractRNG, sp::SamplerUniformMissRow) a = falses(sp.H) Random.rand!(rng, a, sp) end + + +# Satisfaction +""" + satisfies(bv::BitVector, c::WeaklyHardConstraint) + ⊢(bv::BitVector, c::WeaklyHardConstraint) + +Check that the `BitVector` `bv` satisfies the weakly hard constraint given by `c`. +""" +satisfies(_::BitVector, c::WeaklyHardConstraint{<:Integer}) = throw(MethodError(satisfies, (typeof(c)))) +@doc (@doc satisfies) +⊢(bv::BitVector, c::WeaklyHardConstraint) = satisfies(bv, c) +""" + ⊬(bv::BitVector, c::WeaklyHardConstraint) + +Check that the `BitVector` `bv` does *not* satisfy the weakly hard constraint given by `c`. +""" +⊬(bv::BitVector, c::WeaklyHardConstraint) = !satisfies(bv, c) +# First, the trivial methods +satisfies(bv::BitVector, _::HardRealTime) = all(bv) +satisfies(_::BitVector, _::BestEffort) = true +# For MissRow, check that it doesn't contain one miss too many in a row +function satisfies(bv::BitVector, c::MissRow) + @boundscheck length(bv) >= c.miss || throw(ArgumentError("bv must be at least as long as c.miss")) + misses = 0 + for b in bv + if !b + misses += 1 + misses <= c.miss || return false + else + misses = 0 + end + end + true +end +# For MeetAny, check that all windows contain enough hits +function satisfies(bv::BitVector, c::MeetAny) + @boundscheck length(bv) >= c.window || throw(ArgumentError("bv must be at least as long as c.window")) + # Initialize our counter + meets = count(bv[1:c.window]) + meets >= c.meet || return false + # Check that there are at least c.meet deadlines met in each c.window + for i in 1:(length(bv) - c.window) + meets += bv[i + c.window] - bv[i] + meets >= c.meet || return false + end + true +end +# For MeetRow, check that all windows contain a run of hits +function satisfies(bv::BitVector, c::MeetRow) + @boundscheck length(bv) >= c.window || throw(ArgumentError("bv must be at least as long as c.window")) + # Initialize + meets = 0 + safe = c.window - 1 + # Check that there is a row of at least c.meet deadlines met in each c.window + for i in eachindex(bv) + if bv[i] + meets += 1 + if meets >= c.meet + safe = i + c.window - c.meet + safe < length(bv) || return true + end + else + meets = 0 + i <= safe - c.meet + 1 || return false + end + end + return true +end diff --git a/test/weaklyhard.jl b/test/weaklyhard.jl index cd52894..db69368 100644 --- a/test/weaklyhard.jl +++ b/test/weaklyhard.jl @@ -1,23 +1,7 @@ @testset "Weakly hard constraints" begin - # Construction - @test_throws DomainError MeetAny(-1, 5) - @test_throws DomainError MeetAny(1, -1) - @test_throws DomainError MeetAny(-1, -1) - @test_throws DomainError MeetAny(6, 5) a = MeetAny(1, 5) - @test a.meet == 1 - @test a.window == 5 - @test_throws DomainError MeetRow(-1, 5) - @test_throws DomainError MeetRow(1, -1) - @test_throws DomainError MeetRow(-1, -1) - @test_throws DomainError MeetRow(6, 5) - b = MeetRow(1, 5) - @test b.meet == 1 - @test b.window == 5 - @test_throws DomainError MissRow(-1) + b = MeetRow(2, 5) c = MissRow(3) - @test c.miss == 3 - # Equality d = MissRow(0) e = MeetRow(3, 5) f = MeetAny(4, 4) @@ -25,15 +9,68 @@ h = MeetRow(0, 5) i = MeetAny(0, 3) j = BestEffort() - C = [a b c d e f g h i j] .== [a;b;c;d;e;f;g;h;i;j] - @test C == [1 0 0 0 0 0 0 0 0 0 - 0 1 0 0 0 0 0 0 0 0 - 0 0 1 0 0 0 0 0 0 0 - 0 0 0 1 1 1 1 0 0 0 - 0 0 0 1 1 1 1 0 0 0 - 0 0 0 1 1 1 1 0 0 0 - 0 0 0 1 1 1 1 0 0 0 - 0 0 0 0 0 0 0 1 1 1 - 0 0 0 0 0 0 0 1 1 1 - 0 0 0 0 0 0 0 1 1 1] + @testset "Construction invariants" begin + @test_throws DomainError MeetAny(-1, 5) + @test_throws DomainError MeetAny(1, -1) + @test_throws DomainError MeetAny(-1, -1) + @test_throws DomainError MeetAny(6, 5) + + @test_throws DomainError MeetRow(-1, 5) + @test_throws DomainError MeetRow(1, -1) + @test_throws DomainError MeetRow(-1, -1) + @test_throws DomainError MeetRow(6, 5) + + @test_throws DomainError MissRow(-1) + end + @testset "Properties" begin + @test a.meet == 1 + @test a.window == 5 + @test b.meet == 2 + @test b.window == 5 + @test c.miss == 3 + end + @testset "Equality" begin + C = [a b c d e f g h i j] .== [a;b;c;d;e;f;g;h;i;j] + @test C == [1 0 0 0 0 0 0 0 0 0 + 0 1 0 0 0 0 0 0 0 0 + 0 0 1 0 0 0 0 0 0 0 + 0 0 0 1 1 1 1 0 0 0 + 0 0 0 1 1 1 1 0 0 0 + 0 0 0 1 1 1 1 0 0 0 + 0 0 0 1 1 1 1 0 0 0 + 0 0 0 0 0 0 0 1 1 1 + 0 0 0 0 0 0 0 1 1 1 + 0 0 0 0 0 0 0 1 1 1] + end + @testset "Satisfaction" begin + bv = Matrix{BitVector}(undef, 1, 4) + bv[1,1] = BitVector([0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 1, 1]) + bv[1,2] = BitVector([0, 1, 1, 1, 1, 0, 0, 0, 1, 0, 1, 1]) + bv[1,3] = BitVector([0, 1, 1, 1, 0, 0, 0, 0, 1, 0, 1, 1]) + bv[1,4] = BitVector([0, 1, 1, 0, 0, 0, 0, 0, 1, 0, 1, 1]) + S = satisfies.(bv, [a;b;c;g;j]) + @test S == [1 1 1 0 + 1 0 0 0 + 1 1 0 0 + 0 0 0 0 + 1 1 1 1] + S = bv .⊢ [a;b;c;g;j] + @test S == [1 1 1 0 + 1 0 0 0 + 1 1 0 0 + 0 0 0 0 + 1 1 1 1] + S = bv .⊬ [a;b;c;g;j] + @test S == [0 0 0 1 + 0 1 1 1 + 0 0 1 1 + 1 1 1 1 + 0 0 0 0] + end + @testset "Random generation" begin + # Test that all samples satisfy the constraint + sp = SamplerUniformMissRow(c, 100) + seqs = rand(sp, 1000) + @test all(seqs .⊢ c) + end end