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