diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,8 @@ +2021-11-07 + * Version bump (3.6). (#264) + * Improve documentation of LTL module. (#131) + * Fix outdated/broken links. (#252) + 2021-08-19 * Version bump (3.5). (#247) * Update travis domain in README. (#222) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://travis-ci.com/Copilot-Language/copilot) +[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) # Copilot: a stream DSL User-supplied libraries for Copilot, including linear-temporal logic, @@ -30,4 +30,4 @@ ## License Copilot is distributed under the BSD-3-Clause license, which can be found -[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/LICENSE). +[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-libraries/LICENSE). diff --git a/copilot-libraries.cabal b/copilot-libraries.cabal --- a/copilot-libraries.cabal +++ b/copilot-libraries.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-libraries -version: 3.5 +version: 3.6 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -41,7 +41,7 @@ , data-reify >= 0.6 && < 0.7 , mtl >= 2.0 && < 2.3 , parsec >= 2.0 && < 3.2 - , copilot-language >= 3.5 && < 3.6 + , copilot-language >= 3.6 && < 3.7 exposed-modules: Copilot.Library.Libraries diff --git a/src/Copilot/Library/Clocks.hs b/src/Copilot/Library/Clocks.hs --- a/src/Copilot/Library/Clocks.hs +++ b/src/Copilot/Library/Clocks.hs @@ -6,9 +6,9 @@ -- This library generates new clocks based on a base period and phase. -- -- = Example Usage --- --- Also see @Examples/ClockExamples.hs@ in the --- . +-- +-- Also see @examples/Clock.hs@ in the +-- . -- -- @ -- 'clk' ( 'period' 3 ) ( 'phase' 1 ) diff --git a/src/Copilot/Library/LTL.hs b/src/Copilot/Library/LTL.hs --- a/src/Copilot/Library/LTL.hs +++ b/src/Copilot/Library/LTL.hs @@ -14,8 +14,8 @@ -- holds if @p@ holds at least once every four periods (3 transitions). -- -- /Interface:/ See @Examples/LTLExamples.hs@ in the --- . --- +-- . +-- -- You can embed an LTL specification within a Copilot specification using the -- form: -- @@ -25,7 +25,17 @@ -- -- For some properties, stream dependencies may not allow their specification. -- In particular, you cannot determine the "future" value of an external --- variable. In general, the "Copilot.Library.PTLTL" library is probably more useful. +-- variable. +-- +-- Formulas defined with this module require that predicates have enough +-- history, which is only true if they have an append directly in front of +-- them. This results in a limited ability to nest applications of temporal +-- operators, since simple application of pointwise combinators (e.g., @always +-- n1 (p ==> eventually n2 p2)@) will hinder Copilot's ability to determine +-- that there is enough of a buffer to carry out the necessary drops to look +-- into the future. +-- +-- In general, the "Copilot.Library.PTLTL" library is probably more useful. {-# LANGUAGE NoImplicitPrelude #-} @@ -43,7 +53,7 @@ -- s => F F F T F F T F ... -- next s => F F T F F T F ... -- @ --- Note: s must have sufficient history to 'drop' a value from it. +-- Note: @s@ must have sufficient history to 'drop' a value from it. next :: Stream Bool -> Stream Bool next = drop ( 1 :: Int ) @@ -57,6 +67,8 @@ -- s => T T T F T T T T ... -- p => T F F F T T ... -- @ +-- +-- Note: @s@ must have sufficient history to 'drop' @n@ values from it. always :: ( Integral a ) => a -> Stream Bool -> Stream Bool always n = nfoldl1 ( fromIntegral n + 1 ) (&&) @@ -70,6 +82,8 @@ -- s => F F F T F F F T ... -- p => F T T T F T T T ... -- @ +-- +-- Note: @s@ must have sufficient history to 'drop' @n@ values from it. eventually :: ( Integral a ) => a -- ^ 'n' -> Stream Bool -- ^ 's' @@ -79,6 +93,9 @@ -- | @until n s0 s1@ means that @eventually n s1@, and up until at least the -- period before @s1@ holds, @s0@ continuously holds. +-- +-- Note: Both argument streams must have sufficient history to 'drop' @n@ +-- values from them. until :: ( Integral a ) => a -> Stream Bool -> Stream Bool -> Stream Bool until 0 _ s1 = s1 until n s0 s1 = foldl (||) s1 v0 @@ -90,6 +107,9 @@ -- | @release n s0 s1@ means that either @always n s1@, or @s1@ holds up to and -- including the period at which @s0@ becomes true. +-- +-- Note: Both argument streams must have sufficient history to 'drop' @n@ +-- values from them. release :: ( Integral a ) => a -> Stream Bool -> Stream Bool -> Stream Bool release 0 _ s1 = s1 release n s0 s1 = always n s1 || foldl1 (||) v0 diff --git a/src/Copilot/Library/PTLTL.hs b/src/Copilot/Library/PTLTL.hs --- a/src/Copilot/Library/PTLTL.hs +++ b/src/Copilot/Library/PTLTL.hs @@ -6,7 +6,7 @@ -- Provides past-time linear-temporal logic (ptLTL operators). -- -- /Interface:/ See @Examples/PTLTLExamples.hs@ in the --- . +-- . -- -- You can embed a ptLTL specification within a Copilot specification using -- the form: diff --git a/src/Copilot/Library/Voting.hs b/src/Copilot/Library/Voting.hs --- a/src/Copilot/Library/Voting.hs +++ b/src/Copilot/Library/Voting.hs @@ -13,8 +13,8 @@ -- -- * -- --- In addition, in --- explains +-- In addition, and +-- explain -- a form of this code in section 4. -- -- For instance, with four streams passed to 'majority', and the candidate stream @@ -29,8 +29,8 @@ -- 1 1 1 1 1 true -- @ -- --- For other examples, see @Examples/VotingExamples.hs@ in the --- . +-- For other examples, see @examples/Voting.hs@ in the +-- . {-# LANGUAGE RebindableSyntax #-}