diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,20 @@ # Revision history for `deltaq` +## 1.0.1.0 — 2025-09-26 + +### Added + +* Add combinator `timeout` that returns probabilities conditioned + on completing within a given duration. +* Add functions `retryOverlap` and `retryOverlapN` for modelin retry policies + that race time-delayed, independent copies of an outcome against each other. +* Clarify semantics of `deadline`. +* Bump dependencies, allow `containers-0.8`, `QuickCheck-2.16`, `optparse-applicative-0.19`. + +### Fixed + +* Fix `quantile` to return the correct result when the result is precisely at the boundary between two pieces of the piecewise probability distribution. + ## 1.0.0.0 — 2024-12-23 * Initial release of the domain-specific language for ∆Q System Development. diff --git a/deltaq.cabal b/deltaq.cabal --- a/deltaq.cabal +++ b/deltaq.cabal @@ -2,10 +2,10 @@ name: deltaq -- Package Versioning Policy: https://pvp.haskell.org --- PVP summary: +-+------- breaking API changes --- | | +----- non-breaking API additions --- | | | +--- code changes with no API change -version: 1.0.0.0 +-- PVP summary: +-+------- breaking API changes +-- | | +----- non-breaking API additions +-- | | | +--- code changes with no API change +version: 1.0.1.0 synopsis: Framework for ∆Q System Development description: ∆Q System Development is a paradigm for developing distributed systems @@ -27,23 +27,21 @@ homepage: https://github.com/DeltaQ-SD/deltaq license: BSD-3-Clause license-file: LICENSE -copyright: Predictable Network Solutions Ltd., 2003-2024 +copyright: Predictable Network Solutions Ltd., 2003-2025 author: Neil Davies, Heinrich Apfelmus maintainer: neil.davies@pnsol.ccom - extra-doc-files: CHANGELOG.md README.md -tested-with: - , GHC == 9.10.1 +tested-with: GHC ==8.10.7 || ==9.6.7 || ==9.10.3 common warnings ghc-options: -Wall source-repository head type: git - location: git://github.com/DeltaQ-SD/deltaq.git + location: https://github.com/DeltaQ-SD/deltaq.git subdir: lib/deltaq library @@ -51,11 +49,11 @@ hs-source-dirs: src default-language: Haskell2010 build-depends: - , base >= 4.14.3.0 && < 5 - , deepseq >= 1.4.4.0 && < 1.6 - , Chart >= 1.8 && < 2.0 - , lattices >= 2.2 && < 2.3 - , probability-polynomial >= 1.0 && < 1.1 + , base >=4.14.3.0 && <5 + , Chart >=1.8 && <2 + , deepseq >=1.4.4.0 && <1.6 + , lattices >=2.2 && <2.3 + , probability-polynomial >=1.0.1 && <1.1 exposed-modules: DeltaQ @@ -65,23 +63,19 @@ DeltaQ.Plot test-suite test - import: warnings - type: exitcode-stdio-1.0 - hs-source-dirs: test - default-language: Haskell2010 - + import: warnings + type: exitcode-stdio-1.0 + hs-source-dirs: test + default-language: Haskell2010 build-tool-depends: hspec-discover:hspec-discover - build-depends: , base , deltaq + , hspec >=2.11.0 && <2.12 , probability-polynomial - , hspec >= 2.11.0 && < 2.12 - , QuickCheck >= 2.14 && < 2.16 - - main-is: - Spec.hs + , QuickCheck >=2.14 && <2.17 + main-is: Spec.hs other-modules: DeltaQ.ClassSpec DeltaQ.MethodsSpec @@ -92,21 +86,17 @@ type: exitcode-stdio-1.0 hs-source-dirs: benchmark default-language: Haskell2010 - build-depends: , base - , bytestring >= 0.11 && < 0.13 - , deltaq - , cassava >= 0.5.3.2 && < 0.6 - , criterion >= 1.6 && < 1.7 + , bytestring >=0.11 && <0.13 + , cassava >=0.5.3.2 && <0.6 + , criterion >=1.6 && <1.7 , deepseq - , hvega >= 0.12 && < 0.13 - , optparse-applicative >= 0.18.1.0 && < 0.19 - , statistics >= 0.16 && < 0.17 - , vector >= 0.12 && < 0.14 - - main-is: - Main.hs + , deltaq + , hvega >=0.12 && <0.13 + , optparse-applicative >=0.18.1.0 && <0.20 + , statistics >=0.16 && <0.17 + , vector >=0.12 && <0.14 - other-modules: - Benchmark.Plot + main-is: Main.hs + other-modules: Benchmark.Plot diff --git a/src/DeltaQ/Class.hs b/src/DeltaQ/Class.hs --- a/src/DeltaQ/Class.hs +++ b/src/DeltaQ/Class.hs @@ -176,6 +176,10 @@ -- @choices [(w_1, o_1), (w_2, o_2), …]@ chooses randomly between multiple -- outcomes. The probability @p_i@ for choosing the outcome @o_i@ is -- determined by the weights as @p_i = w_i / (w_1 + w_2 + …)@. + -- + -- Note: The weights @w_i@ have the numeric type @Probability o@, + -- but for convenience, and unlike probabilities, + -- they are not restricted to the unit interval \( [0,1] \). choices :: [(Probability o, o)] -> o choices [] = never choices wos = @@ -341,10 +345,16 @@ > deadline (x ./\. y) = max (deadline x) (deadline y) > > deadline (x .\/. y) = min (deadline x) (deadline y) -> if failure x = 0, failure y = 0 +> if failure x = 0 and failure y = 0 > +> deadline (x .\/. y) = deadline x +> if failure x = 0 and failure y > 0 +> +> deadline (x .\/. y) = max (deadline x) (deadline y) +> if 1 > failure x > 0 and 1 > failure y > 0 +> > deadline (choice p x y) = max (deadline x) (deadline y) -> if p ≠ 0, p ≠ 1, failure x = 0, failure y = 0 +> if p ≠ 0 and p ≠ 1 and failure x < 1 and failure y < 1 > > > deadline (uniform r s) = Occurs s if r <= s diff --git a/src/DeltaQ/Methods.hs b/src/DeltaQ/Methods.hs --- a/src/DeltaQ/Methods.hs +++ b/src/DeltaQ/Methods.hs @@ -17,6 +17,10 @@ , SlackOrHazard (..) , isSlack , isHazard + + -- * Timeouts + , retryOverlapN + , retryOverlap ) where import DeltaQ.Class @@ -25,6 +29,10 @@ , Outcome (..) , eventually ) +import DeltaQ.PiecewisePolynomial + ( DQ + , timeout + ) {----------------------------------------------------------------------------- Methods @@ -83,3 +91,45 @@ p' = o `successWithin` t err = error "distanceToReference: inconsistency" + +{----------------------------------------------------------------------------- + Methods + Timeouts +------------------------------------------------------------------------------} + +-- | Retry an outcome @n@ times, take the first instance that succeeds. +-- +-- More specifically, @retryOverlapN n dt o@ models the completion times +-- of a race of @n@ independent copies of the outcome @o@ against each other, +-- succeeding when any of the copies first succeeds. +-- +-- Copy number @0 <= j < n@ is started after waiting a time @j * dt@. +-- +-- If no copy succeeds within total time @n * dt@, +-- the whole outcome fails. +retryOverlapN :: Int -> Duration DQ -> DQ -> DQ +retryOverlapN n dt = retryOverlap (replicate n dt) + +-- | Retry an outcome multiple times, take the first instance that succeeds. +-- +-- More specifically, @retryOverlap dts o@ models the completion times +-- of a race of @length dts@ independent copies of the outcome @o@ +-- against each other, succeeding when any of the copies first succeeds. +-- +-- Each copy is started after a timeout +-- in the event that the previous copies have not finished yet; +-- the list @dts@ gives the successive timeouts. +-- +-- If no copy succeeds within total time @sum dts@, +-- the whole outcome fails. +retryOverlap :: [Duration DQ] -> DQ -> DQ +retryOverlap dts0 o = go dts0 o + where + go [] _ = never + go (dt:dts) race = + choice p before (wait dt .>>. retry) + where + (before, p, after) = timeout dt race + + -- add another copy of `o` to the race + retry = go dts (after .\/. o) diff --git a/src/DeltaQ/PiecewisePolynomial.hs b/src/DeltaQ/PiecewisePolynomial.hs --- a/src/DeltaQ/PiecewisePolynomial.hs +++ b/src/DeltaQ/PiecewisePolynomial.hs @@ -24,6 +24,7 @@ , meetsQTA , Moments (..) , moments + , timeout -- * Internal , complexity @@ -186,7 +187,7 @@ where goJump _ [] = [] goJump prev ((x1, o) : xos) - | y1 - y0 > 0 = Jump x1 (y0, y1) : nexts + | y0 < y1 = Jump x1 (y0, y1) : nexts | otherwise = nexts where y1 = Poly.eval o x1 @@ -197,7 +198,6 @@ End x1 y1 : goJump o [] goPoly x1 y1 o xos@((x2, _) : _) = Polynomial (x1, x2) (y1, Poly.eval o x2) o : goJump o xos - -- TODO: What about the case where y1 == y2, i.e. a constant Polynomial? {----------------------------------------------------------------------------- Operations @@ -214,13 +214,14 @@ findInSegments [] _ = Nothing findInSegments (Jump x1 (y1, y2) : xys) y - | y1 < y && y <= y2 = Just x1 - | otherwise = findInSegments xys y + | y1 <= y && y < y2 = Just x1 + | otherwise = findInSegments xys y findInSegments (Polynomial (x1, x2) (y1, y2) o : xys) y - | y1 < y && y <= y2 = Poly.root precision y (x1, x2) o + | y1 == y = Just x1 + | y1 < y && y < y2 = Poly.root precision y (x1, x2) o | otherwise = findInSegments xys y findInSegments (End x1 y1 : _) y - | y1 == y = Just x1 + | y1 == y = Just x1 | otherwise = Nothing precision :: Rational @@ -254,9 +255,12 @@ Operations Moments ------------------------------------------------------------------------------} --- | Compute the success probability of a 'DQ', --- and the first commonly used 'Moments' of the --- probability distribution conditioned on success. +-- | For a given 'DQ', compute +-- +-- * the success probability, and +-- +-- * the 'Moments' of the conditional probability (distribution) +-- given that the outcome has succeeded. moments :: DQ -> (Rational, Moments Rational) moments (DQ m) | success == 0 = @@ -266,3 +270,42 @@ where success = Measure.total m conditional = Prob.unsafeFromMeasure $ Measure.scale (1/success) m + +{----------------------------------------------------------------------------- + Operations + Timeout +------------------------------------------------------------------------------} +-- | Given a duration @dt@, +-- decompose a probability distribution of completion times +-- into two conditional probability distributions — +-- one distribution conditional on finishing within @dt@, +-- and the other distribution conditional on finishing after @dt@. +-- +-- > (within, p, after) = timeout dt o +-- > +-- > implies +-- > +-- > o = choice p within (wait dt .>>. after) +-- > p = successWithin o dt +-- > +-- > successWithin within dt = 1 +-- > if p > 0 +-- +-- We define the corner cases as follows: +-- +-- * @successWithin o dt = 0@ implies @before = never@. +-- +-- * @successWithin o dt = 1@ implies @after = never@. +-- +timeout :: Duration DQ -> DQ -> (DQ, Probability DQ, DQ) +timeout dt (DQ m) = (beforeCond, p, afterCond) + where + before = Measure.beforeOrAt dt m + after = Measure.translate (- dt) $ Measure.after dt m + p = Measure.total before + beforeCond + | p == 0 = never + | otherwise = DQ $ Measure.scale (1/p) before + afterCond + | p == 1 = never + | otherwise = DQ $ Measure.scale (1/(1-p)) after diff --git a/test/DeltaQ/MethodsSpec.hs b/test/DeltaQ/MethodsSpec.hs --- a/test/DeltaQ/MethodsSpec.hs +++ b/test/DeltaQ/MethodsSpec.hs @@ -18,10 +18,12 @@ ) import DeltaQ.PiecewisePolynomial ( DQ + , timeout ) import DeltaQ.Methods ( SlackOrHazard (..) , meetsRequirement + , retryOverlap ) import Test.Hspec ( Spec @@ -33,6 +35,7 @@ , Positive (..) , property , withMaxSuccess + , (===) ) {----------------------------------------------------------------------------- @@ -62,3 +65,27 @@ in case deltaq `meetsRequirement` (0, 0.9) of Hazard (Occurs dt) dp -> dt >= 0 && dp >= 0 _ -> False + + describe "retryOverlap" $ do + it "documentation" $ property $ + \(Positive d) (dts' :: [Positive Rational]) -> + let r = 0 + s = r + d + dts = map (\(Positive dt) -> dt) dts' + o = uniform r s :: DQ + in + retryOverlap dts o === retryOverlap' dts o + +-- | Implementation of 'retryOverlap' that matches the description +-- in the documentation. +retryOverlap' :: [Duration DQ] -> DQ -> DQ +retryOverlap' dts o = + cutoff (sum dts) + $ foldr (.\/.) never + [ wait dt .>>. o + | dt <- init (scanl (+) 0 dts) + ] + where + cutoff dt x = choice p before never + where + (before, p, _) = timeout dt x diff --git a/test/DeltaQ/PiecewisePolynomialSpec.hs b/test/DeltaQ/PiecewisePolynomialSpec.hs --- a/test/DeltaQ/PiecewisePolynomialSpec.hs +++ b/test/DeltaQ/PiecewisePolynomialSpec.hs @@ -33,6 +33,7 @@ , fromPositiveMeasure , meetsQTA , moments + , timeout ) import Numeric.Probability.Moments ( Moments (..) @@ -279,6 +280,15 @@ in p' <= q' ==> quantile' o p' <= quantile' o q' + it "interval boundary" $ property $ + \(Probability p) (NonNegative t0) (Positive d1) (Positive d2) -> + let t1 = t0 + d1 + t2 = t1 + d2 + in + p > 0 ==> + quantile' (choice p (uniform t0 t1) (wait t2)) p + === Occurs t1 + it "never" $ property $ \(Probability p) -> p > 0 ==> @@ -353,15 +363,30 @@ deadline' (x ./\. y) === max (deadline' x) (deadline' y) - it ".\\/." $ property $ + it ".\\/., zero failure" $ property $ \x y -> (failure x == 0 && failure y == 0) ==> deadline' (x .\/. y) === min (deadline' x) (deadline' y) + it ".\\/., one failure" $ property $ + \(Probability p) x y -> 0 < p && p < 1 + ==> let y' = choice p y never + in failure x == 0 ==> + deadline' (x .\/. y') + === deadline' x + + it ".\\/., two failure" $ property $ + \(Probability p) x y -> 0 < p && p < 1 + ==> let x' = choice p x never + y' = choice p y never + in (failure x < 1 && failure y < 1) + ==> deadline' (x' .\/. y') + === max (deadline' x') (deadline' y') + it "choice" $ property $ \(Probability p) x y -> - (0 < p && p < 1 && failure x == 0 && failure y == 0) ==> + (0 < p && p < 1 && failure x < 1 && failure y < 1) ==> deadline' (choice p x y) === max (deadline' x) (deadline' y) @@ -439,6 +464,32 @@ \(NonNegative t) -> let ms = Moments{mean = t, variance = 0, skewness = 0, kurtosis = 1} in moments (wait t) === (1, ms) + + describe "timeout" $ do + it "never" $ property $ + \dt -> + timeout dt never === (never, 0, never) + + it "probability" $ property $ + \x dt -> + let (_, p, _) = timeout dt x + in p === successWithin x dt + + it "within" $ property $ + \x dt -> + let (within, p, _) = timeout dt x + in p > 0 ==> + successWithin within dt === 1 + + it "wait" $ property $ + \x dt (Positive d) -> + timeout dt (wait (dt + d) .>>. x) + === (never, 0, wait d .>>. x) + + it "choice" $ property $ + \x dt -> + let (within, p, after) = timeout dt x + in choice p within (wait dt .>>. after) === x describe "complexity" $ do it "grows exponentially with .>>." $ withMaxSuccess 1 $ property $