Add satisfies function for weakly hard constraints (#6)

* 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

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

src/RealTimeScheduling.jl

@@ -31,6 +31,9 @@ export AbstractRealTimeTask,
        HardRealTime,
        BestEffort,
        SamplerUniformMissRow,
+       satisfies,
+       ⊢,
+       ⊬,
        # Schedulability tests
        schedulable_fixed_priority
 include("weaklyhard.jl")

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

test/weaklyhard.jl

@@ -1,39 +1,76 @@
 @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)
     g = HardRealTime()
     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