copilot-libraries 3.5 → 3.6

raw patch · 7 files changed

+41/−16 lines, 7 filesdep ~copilot-languagePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-language

API changes (from Hackage documentation)

Files

CHANGELOG +5/−0
README.md +2/−2
copilot-libraries.cabal +2/−2
src/Copilot/Library/Clocks.hs +3/−3
src/Copilot/Library/LTL.hs +24/−4
src/Copilot/Library/PTLTL.hs +1/−1
src/Copilot/Library/Voting.hs +4/−4

CHANGELOG view

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

README.md view

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

copilot-libraries.cabal view

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

src/Copilot/Library/Clocks.hs view

@@ -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--- <https://github.com/leepike/Copilot/tree/master/Examples Copilot repository>.+--+-- Also see @examples/Clock.hs@ in the+-- <https://github.com/Copilot-Language/copilot/blob/master/copilot/examples/ Copilot repository>. -- -- @ --     'clk' ( 'period' 3 ) ( 'phase' 1 )

src/Copilot/Library/LTL.hs view

@@ -14,8 +14,8 @@ -- holds if @p@ holds at least once every four periods (3 transitions). -- -- /Interface:/ See @Examples/LTLExamples.hs@ in the--- <https://github.com/leepike/Copilot/tree/master/Examples Copilot repository>.--- +-- <https://github.com/Copilot-Language/copilot/blob/v2.2.1/Examples Copilot repository>.+-- -- 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

src/Copilot/Library/PTLTL.hs view

@@ -6,7 +6,7 @@ -- Provides past-time linear-temporal logic (ptLTL operators). -- -- /Interface:/ See @Examples/PTLTLExamples.hs@ in the--- <https://github.com/leepike/Copilot/tree/master/Examples Copilot repository>.+-- <https://github.com/Copilot-Language/copilot/blob/v2.2.1/Examples Copilot repository>. -- -- You can embed a ptLTL specification within a Copilot specification using -- the form:

src/Copilot/Library/Voting.hs view

@@ -13,8 +13,8 @@ -- -- * <ftp://net9.cs.utexas.edu/pub/techreports/tr81-32.pdf Robert S. Boyer and J Strother Moore, \"MJRTY - A Fast Majority Vote Algorithm\", 1981> ----- In addition, <https://github.com/leepike/copilot-discussion/blob/master/tutorial/copilot_tutorial.pdf An Introduction to Copilot> in--- <https://github.com/leepike/copilot-discussion copilot-discussion> explains+-- In addition, <https://copilot-language.github.io/downloads/copilot_tutorial.pdf An Introduction to Copilot> and+-- <https://github.com/Copilot-Language/copilot-discussion copilot-discussion> 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--- <https://github.com/leepike/Copilot/tree/master/Examples Copilot repository>.+-- For other examples, see @examples/Voting.hs@ in the+-- <https://github.com/Copilot-Language/copilot/blob/master/copilot/examples/ Copilot repository>.  {-# LANGUAGE RebindableSyntax #-}