    -- |
    -- Module: LTL
    -- Description: Bounded Linear Temporal Logic (LTL) operators
    -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
    --
    -- Bounded Linear Temporal Logic (LTL) operators. For a bound @n@, a property
    -- @p@ holds if it holds on the next @n@ transitions (between periods).  If
    -- @n == 0@, then the trace includes only the current period.  For example,
    --
    -- @
    --   eventually 3 p
    -- @
    --
    -- holds if @p@ holds at least once every four periods (3 transitions).
    --
    -- /Interface:/ See @Examples/LTLExamples.hs@ in the
    -- <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:
    --
    -- @
    --   operator spec
    -- @
    --
    -- For some properties, stream dependencies may not allow their specification.
    -- In particular, you cannot determine the "future" value of an external
    -- 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 #-}

    module Copilot.Library.LTL
      ( next, eventually, always, until, release ) where

    import Copilot.Language
    import Copilot.Library.Utils

    -- | Property @s@ holds at the next period.  For example:
    --
    -- @
    --           0 1 2 3 4 5 6 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.
    next :: Stream Bool -> Stream Bool
    next :: Stream Bool -> Stream Bool
    next = Int -> Stream Bool -> Stream Bool
    forall a. Typed a => Int -> Stream a -> Stream a
    drop ( Int
    1 :: Int )

    -- | Property @s@ holds for the next @n@ periods.  We require @n >= 0@. If @n ==
    -- 0@, then @s@ holds in the current period, e.g., if @p = always 2 s@, then we
    -- have the following relationship between the streams generated:
    --
    -- @
    --      0 1 2 3 4 5 6 7
    -- 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 :: forall a. Integral a => a -> Stream Bool -> Stream Bool
    always a
    n = Int
    -> (Stream Bool -> Stream Bool -> Stream Bool)
    -> Stream Bool
    -> Stream Bool
    forall a.
    Typed a =>
    Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a
    nfoldl1 ( a -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 ) Stream Bool -> Stream Bool -> Stream Bool
    (&&)

    -- | Property @s@ holds at some period in the next @n@ periods.  If @n == 0@,
    -- then @s@ holds in the current period.  We require @n >= 0@.  E.g., if @p =
    -- eventually 2 s@, then we have the following relationship between the streams
    -- generated:
    --
    -- @
    -- 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'
                  -> Stream Bool
    eventually :: forall a. Integral a => a -> Stream Bool -> Stream Bool
    eventually a
    n = Int
    -> (Stream Bool -> Stream Bool -> Stream Bool)
    -> Stream Bool
    -> Stream Bool
    forall a.
    Typed a =>
    Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a
    nfoldl1 ( a -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 ) Stream Bool -> Stream Bool -> Stream Bool
    (||)

    -- | @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 :: forall a.
    Integral a =>
    a -> Stream Bool -> Stream Bool -> Stream Bool
    until a
    0 Stream Bool
    _ Stream Bool
    s1 = Stream Bool
    s1
    until a
    n Stream Bool
    s0 Stream Bool
    s1 = (Stream Bool -> Stream Bool -> Stream Bool)
    -> Stream Bool -> [Stream Bool] -> Stream Bool
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Stream Bool -> Stream Bool -> Stream Bool
    (||) Stream Bool
    s1 [Stream Bool]
    v0
        where
           n' :: Int
    n' = a -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    n
           v0 :: [Stream Bool]
    v0 = [ Int -> Stream Bool -> Stream Bool
    forall a. Integral a => a -> Stream Bool -> Stream Bool
    always ( Int
    i :: Int ) Stream Bool
    s0 Stream Bool -> Stream Bool -> Stream Bool
    && Int -> Stream Bool -> Stream Bool
    forall a. Typed a => Int -> Stream a -> Stream a
    drop ( Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 ) Stream Bool
    s1
                | Int
    i <- [ Int
    0 .. Int
    n' Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 ]
                ]

    -- | @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 :: forall a.
    Integral a =>
    a -> Stream Bool -> Stream Bool -> Stream Bool
    release a
    0 Stream Bool
    _ Stream Bool
    s1 = Stream Bool
    s1
    release a
    n Stream Bool
    s0 Stream Bool
    s1 = a -> Stream Bool -> Stream Bool
    forall a. Integral a => a -> Stream Bool -> Stream Bool
    always a
    n Stream Bool
    s1 Stream Bool -> Stream Bool -> Stream Bool
    || (Stream Bool -> Stream Bool -> Stream Bool)
    -> [Stream Bool] -> Stream Bool
    forall a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldl1 Stream Bool -> Stream Bool -> Stream Bool
    (||) [Stream Bool]
    v0
        where
          n' :: Int
    n' = a -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    n
          v0 :: [Stream Bool]
    v0 = [ Int -> Stream Bool -> Stream Bool
    forall a. Integral a => a -> Stream Bool -> Stream Bool
    always ( Int
    i :: Int ) Stream Bool
    s1 Stream Bool -> Stream Bool -> Stream Bool
    && Int -> Stream Bool -> Stream Bool
    forall a. Typed a => Int -> Stream a -> Stream a
    drop Int
    i Stream Bool
    s0
               | Int
    i <- [ Int
    0 .. Int
    n' Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 ]
               ]