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