packages feed

PropRatt (empty) → 0.1.0.0

raw patch · 16 files changed

+1366/−0 lines, 16 filesdep +AsyncRattusdep +PropRattdep +QuickChecksetup-changed

Dependencies added: AsyncRattus, PropRatt, QuickCheck, base, containers

Files

+ CHANGELOG.md view
@@ -0,0 +1,11 @@+# Changelog for `experiments`++All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),+and this project adheres to the+[Haskell Package Versioning Policy](https://pvp.haskell.org/).++## Unreleased++## 0.1.0.0 - YYYY-MM-DD
+ LICENSE view
@@ -0,0 +1,26 @@+Copyright 2025 Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1.  Redistributions of source code must retain the above copyright notice, this+    list of conditions and the following disclaimer.++2.  Redistributions in binary form must reproduce the above copyright notice,+    this list of conditions and the following disclaimer in the documentation+    and/or other materials provided with the distribution.++3.  Neither the name of the copyright holder nor the names of its contributors+    may be used to endorse or promote products derived from this software+    without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ PropRatt.cabal view
@@ -0,0 +1,86 @@+cabal-version: 2.2+name:           PropRatt+version:        0.1.0.0+synopsis:       Property-based testing framework for testing asynchronous FRP programs.+category:       testing+description:    +                PropRatt is a property-based testing framework for testing Async Rattus programs.+                The key component of PropRatt is its specification language, which extends basic linear temporal logic with+                a means to express properties of several concurrent signals. This+                allows users to express temporal properties that relate data coming from+                different signals at different points in time.+author:         Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr+maintainer:     paba@itu.dk+copyright:      2025 Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr+license:        BSD-3-Clause+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/pa-ba/PropRatt++library+  exposed-modules:+      PropRatt+      PropRatt.Arbitrary+      PropRatt.Core+      PropRatt.HList+      PropRatt.LTL+      PropRatt.Signal+  other-modules:+      PropRatt.Utils+      PropRatt.Value+  hs-source-dirs:+      src+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+  build-depends:+      AsyncRattus >= 0.2 && < 0.3+    , QuickCheck > 2.10 && < 3+    , base >=4.7 && <5+    , containers  >=0.6.5 && < 0.8+  default-language: Haskell2010++executable main-example+  main-is: Main.hs+  hs-source-dirs:+      examples/main+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      AsyncRattus+    , PropRatt+    , QuickCheck+    , base+    , containers+  default-language: Haskell2010++executable timer-example+  main-is: Timer.hs++  hs-source-dirs:+      examples/timer+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      AsyncRattus+    , PropRatt+    , QuickCheck+    , base+    , containers+  default-language: Haskell2010++test-suite PropRatt-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  hs-source-dirs:+      test+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      AsyncRattus+    , PropRatt+    , QuickCheck+    , base >=4.7 && <5+    , containers+  default-language: Haskell2010
+ README.md view
@@ -0,0 +1,8 @@+# PropRatt++PropRatt is a Haskell framework for testing AsyncRattus using property-based testing.++# Running examples++- `stack run main-example`+- `stack run timer-example`
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ examples/main/Main.hs view
@@ -0,0 +1,276 @@+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}+{-# LANGUAGE TypeApplications, FlexibleInstances #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Use zipWith" #-}+{-# HLINT ignore "Redundant bracket" #-}+{-# HLINT ignore "Move brackets to avoid $" #-}+{-# HLINT ignore "Use const" #-}++module Main (main) where+    +import Test.QuickCheck+import PropRatt+import AsyncRattus.InternalPrimitives+import Prelude hiding (zip, map, const)+import AsyncRattus.Signal hiding (filter)+import AsyncRattus.Strict hiding (singleton)+import AsyncRattus.Plugin.Annotation+import Prelude hiding (const, map, zip)+import PropRatt.Signal+import qualified Data.IntSet as IntSet++{-# ANN module AllowLazyData #-}++filterM :: Box (a -> Bool) -> Sig a -> Sig (Maybe' a)+filterM f (x ::: xs) = if unbox f x+  then Just' x ::: delay (filterM f (adv xs))+  else Nothing' ::: delay (filterM f (adv xs))++triggerM :: (Stable b) => Box (a -> b -> c) -> Sig a -> Sig b -> Sig (Maybe' c)+triggerM f (a ::: as) bs@(b:::_) = Just' (unbox f a b) ::: triggerMAwait f as bs++triggerMAwait :: Stable b => Box (a -> b -> c) -> O (Sig a) -> Sig b -> O (Sig (Maybe' c))+triggerMAwait f as (b:::bs) = delay (case select as bs of+            Fst (a' ::: as') bs' -> Just' (unbox f a' b) ::: triggerMAwait f as' (b ::: bs')+            Snd as' bs' -> Nothing' ::: triggerMAwait f as' bs'+            Both (a' ::: as') (b' ::: bs') -> Just' (unbox f a' b') ::: triggerMAwait f as' (b' ::: bs'))++stutter :: (Stable a, Stable b) => Sig a -> Sig b -> Sig a+stutter xs ys = map (box fst') (zip xs ys)++monotonic :: (Stable a, Num a) => Sig a -> Sig a+monotonic xs = scan (box (+)) 0 (map (box abs) xs)++prop_interleave :: Property+prop_interleave = forAll (generateSignals @[Int, Int]) $ \intSignals ->+    let interleaved     = interleave (box (+)) (future $ first intSignals) (future $ second intSignals)+        state           = prependLater interleaved $ flatten intSignals+        predicate       = Next $ Always $ ((Now ((Index First) |==| (Index Second)))+                                        `Or`+                                        (Now ((Index First) |==| (Index Third))))+                                        `Or`+                                        (Now (((Index Second) + (Index Third)) |==| (Index First)))+        result          = evaluate predicate state+    in result++-- Jumped signal should switch once the boxed predicate function is true.+prop_jump :: Property+prop_jump = forAll (generateSignals @Int) $ \intSignals ->+   let  jumpFunc    = box (\n -> if n > 10 then Just' (const 1) else Nothing')+        jumpSig     = jump jumpFunc (first intSignals)+        state       = prepend jumpSig $ flatten intSignals+        predicate   = Always $+                        Now ((Index First) |==| (Index Second))+                        `Or`+                        Now ((Index First) |==| (Pure 1)) --+        result      = evaluate predicate state+    in result++-- Prefix sum is strictly monotonically increasing, but fails for non-natural numbers.+prop_scan_failing :: Property+prop_scan_failing =  forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->+    let prefixSum   = scan (box (+)) 0 (first intSignals)+        state       = prepend prefixSum $ flatten intSignals+        predicate   = Next $ Always $ Now $ Index (Previous First) |<| (Index First)+        result      = evaluate predicate state+    in counterexample ("Must be natural numbers.") result++-- Prefix sum is strictly monotonically increasing is true for natural numbers.+prop_scan :: Property+prop_scan =  forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->+    let absSig      = map (box (\x -> (abs x + 1))) (first intSignals)+        prefixSum   = scan (box (+)) 0 absSig+        state       = prepend prefixSum $ flatten intSignals+        predicate   = Next $ Always $ Now $ Index (Previous First) |<| (Index First)+        result      = evaluate predicate state+    in result++-- A switched signal has values equal to the first signal until its values equal values from the third signal+prop_switchedSignal :: Property+prop_switchedSignal = forAll (generateSignals @[Int, Int]) $ \intSignals ->+    let switched    = switch (first intSignals) (future (second intSignals))+        state       = prepend switched $ flatten intSignals+        predicate   = Until (Now ((Index First) |==| (Index Second))) (Now ((Index First) |==| (Index Third)))+        result      = evaluate predicate state+    in result++-- A buffered signal is always one tick behind.+prop_buffer :: Property+prop_buffer = forAll (generateSignals @Int) $ \intSignals ->+    let bufferedSig = buffer 10 (first intSignals)+        state       = prepend bufferedSig $ flatten intSignals+        predicate   = Next $ Always $ Now $ (Index First) |==| Index (Previous Second)+        result      = evaluate predicate state+    in result++-- A signal becomes constant once the predicate function to "stop" is true.+prop_stop :: Property+prop_stop = forAll (generateSignals @Int) $ \intSignals ->+    let stopped     = stop (box (>100)) (first intSignals)+        state       = prepend stopped $ flatten intSignals+        predicate   = Always $ Implies (Now ((Index First) |>| (Pure 100))) (Always $ Next (Now (Index (Previous First) |==| (Index First))))+        result      = evaluate predicate state+    in result++-- A zipped signal always has fst' values from second signal and snd' values from third signal.+prop_zip :: Property+prop_zip = forAll (generateSignals @[Int, Int]) $ \intSignals ->+    let s1          = zip (first intSignals) (second intSignals)+        state       = prepend s1 $ flatten intSignals+        predicate   = Always $ Now ((fst' <$> (Index First)) |==| (Index Second)) `And` (Now ((snd' <$> (Index First)) |==| (Index Third)))+        result      = evaluate predicate state+    in result++prop_filter :: Property+prop_filter = forAll (generateSignals @Int) $ \intSignals ->+  let filtered      = filterM (box (>= 10)) (first intSignals)+      state         = prepend filtered $ flatten intSignals+      predicate     = Always $ +            Implies (Now ((Index Second) |>=| Pure (10))) (Now ((Index First) |>=| (Pure (Just' 10))))+            `And`+            Implies (Now ((Index Second) |<| Pure (10))) (Now ((Index First) |==| (Pure Nothing')))+      result        = evaluate predicate state+  in result++prop_triggerM :: Property+prop_triggerM = forAll (generateSignals @[Int, Int]) $ \intSignals ->+  let triggered     = triggerM (box (*)) (first intSignals) (second intSignals)+      state         = prepend triggered $ flatten intSignals+      predicate     = Always $ +            Implies (Now ((Ticked Second) |==| (Pure True))) ((Now ((Ticked First) |==| (Pure True))) `And` (Now ((fromMaybe' 0 <$> (Index First)) |==| ((Index Second) * (Index Third)))))+      result        = evaluate predicate state+  in result++prop_parallel :: Property+prop_parallel = forAllShrink (generateSignals @[Int, Int]) shrinkHls $ \intSignals ->+    let paralleled  = parallel (first intSignals) (second intSignals)+        state       = prepend paralleled $ flatten intSignals+        predicate   = Always $+            Implies (Now (Ticked Third)) (Now (Ticked First))+            `And`+            Implies (Now (Ticked Second)) (Now (Ticked First))+        result      = evaluate predicate state+    in result++prop_isStuttering :: Property+prop_isStuttering = forAll (generateSignals @[Int, Int]) $ \intSignals ->+    let stuttered   = stutter (first intSignals) (second intSignals)+        state       = prepend stuttered $ flatten intSignals+        predicate   = Always $+            Implies (Now (Ticked First)) (Now (Index First |==| Index Second))+            `And`+            Next (Implies (And (Now (Ticked Third)) (Not (Now (Ticked Second)))) (Now (Index (Previous First) |==| Index First)))+        result      = evaluate predicate state+    in result++prop_functionIsMonotonic :: Property+prop_functionIsMonotonic = forAll (generateSignals @Int) $ \intSignals ->+    let mono        = monotonic (first intSignals)+        state       = singletonH mono+        predicate   = Always $ Next (Now ((Index First) |>=| (Index (Previous First))))+        result      = evaluate predicate state+    in result++prop_singleSignalAlwaysTicks :: Property+prop_singleSignalAlwaysTicks = forAllShrink (arbitrary :: Gen (Sig Int)) shrink $ \sig ->+    let state       = singletonH sig+        predicate   = Always $ Now ((Ticked First) |==| (Pure True))+        result      = evaluate predicate state+    in result++-- Switched signal equals XS until YS has ticked, from then on the value is constant assuming ys has not produced another const signal+prop_switchR :: Property+prop_switchR = forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->+    let xs                  = first intSignals+        (_ ::: ys)          = (scan (box (\n _ -> n + 1)) 0 (takeN (sigLength xs) mkSigZero)) :: Sig Int+        zs                  = switchR xs (mapAwait (box (\b _ -> const b)) ys)+        state               = prepend zs $ prependLater ys $ flatten intSignals+        predicate           = (Now ((Index First) |==| (Index Third)))+                                `Until`+                                (Now ((Ticked Second) |==| (Pure True)))+                                `And` +                                ((Always $ Next +                                    (((Implies  (Not (Now (Ticked Second))) (Now ((Index (Previous First)) |==| (Index First))))))))+                                `Until`+                               (Next $ (Implies (Now (Ticked Second)) (Not (Now ((Index (Previous First)) |==| (Index First))))))+        result              = evaluate predicate state+    in counterexample (show state) result++prop_switchS :: Property+prop_switchS = forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->+    let xs                  = first intSignals+        gg@(_ ::: ys)       = (scan (box (\n _ -> n + 1)) 0 (takeN (sigLength xs) mkSigZero)) :: Sig Int+        ggg                 = Delay (IntSet.fromList [1,2,3]) (\_ a -> const a)+        zs                  = switchS xs ggg+        state               = prepend zs $ prependLater ys $ flatten intSignals+        predicate           =(Now ((Index First) |==| (Index Third)))+                                `Until`+                                (Now ((Ticked Second) |==| (Pure True)))+                                `And` +                                ((Always $ Next +                                    (((Implies  (Not (Now (Ticked Second))) (Now ((Index (Previous First)) |==| (Index First))))))))+                                `Until`+                               (Next $ (Implies (Now (Ticked Second)) (Not (Now ((Index (Previous First)) |==| (Index First))))))+        result              = evaluate predicate state+    in counterexample (show gg ++ show zs ++ show xs) result++prop_sigLength :: Property+prop_sigLength = forAllShrink (arbitrary :: Gen (Sig Int)) shrink $ \(sig :: Sig Int) ->+        let state       = singletonH (sig :: Sig Int)+            predicate   = Always $ (Now ((Index First) |<| (Pure 50)))+            result      = evaluate predicate state+        in result++prop_sigIsPositive :: Property+prop_sigIsPositive = forAll (generateSignals @Int) $ \sig ->+        let mapped      = map (box (abs)) (first sig)+            state       = singletonH mapped+            predicate   = Next $ Always $ Now ((Index (Prior 1 First)) |>=| (Pure 0))+            result      = evaluate predicate state +        in result++prop_catchsubtle :: Property+prop_catchsubtle = forAllShrink (arbitrary :: Gen (Sig Int)) shrink $ \(sig :: Sig Int) ->+        let state       = singletonH (sig :: Sig Int)+            predicate   = Always $ Implies (Now ((Index First) |>| (Pure 80))) (Next $ (Now ((Index First) |<| (Index (Previous First)))))+            result      = evaluate predicate state+        in result++prop_predLengthOutsideDefault :: Property+prop_predLengthOutsideDefault =  forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->+    let prefixSum   = scan (box (+)) 0 (first intSignals)+        state       = prepend prefixSum $ flatten intSignals+        predicate   = After 100 $ Always $ Now $ Index (Previous First) |<| (Index First)+        result      = evaluate predicate state+    in result++main :: IO ()+main = do+    quickCheck prop_interleave+    quickCheck prop_switchedSignal+    quickCheck prop_buffer+    quickCheck prop_zip+    quickCheck prop_jump+    quickCheck prop_stop+    quickCheck prop_scan+    quickCheck prop_filter+    quickCheck prop_triggerM+    quickCheck prop_parallel+    quickCheck prop_isStuttering+    quickCheck prop_functionIsMonotonic+    quickCheck prop_singleSignalAlwaysTicks+    quickCheck prop_sigIsPositive+    quickCheck prop_switchS++    putStrLn "=== Failing tests ==="+    quickCheck prop_scan_failing+    putStrLn "====================="+    quickCheck prop_sigLength+    putStrLn "====================="+    quickCheck (withMaxSuccess 1000 prop_switchR)+    putStrLn "====================="+    quickCheck (withMaxSuccess 1000 prop_catchsubtle)+    putStrLn "====================="+    quickCheck prop_predLengthOutsideDefault
+ examples/timer/Timer.hs view
@@ -0,0 +1,159 @@+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Main (main) where++import Test.QuickCheck+import PropRatt+import AsyncRattus.Strict+import AsyncRattus.Signal+import AsyncRattus.InternalPrimitives+import Prelude hiding (map, const, zipWith, zip, filter, getLine, putStrLn,null, max)+import qualified Data.IntSet as IntSet+import AsyncRattus.Plugin.Annotation+++{-# ANN module AllowLazyData #-}++{-# ANN everySecondSig AllowRecursion #-}+everySecondSig :: O (Sig ())+everySecondSig = Delay (IntSet.fromList [2]) (\_ -> () ::: everySecondSig)++nats :: O (Sig ()) -> (Int :* Int) -> Sig (Int :* Int)+nats later (n :* max) = stop+    (box (\ (n' :* max') -> n' >= max'))+    (scanAwait (box (\ (n' :* max') _ -> (n' + 1) :* max')) (n :* max) later)++resetTuple :: (Int :* Int) -> (Int :* Int)+resetTuple (_ :* max) = (0 :* max)++setMax :: Int -> (Int :* Int) -> (Int :* Int)+setMax max' (n :* _) = ((min n max') :* max')++timerState :: Sig () -> Sig Int -> Sig (Int :* Int)+timerState (_ ::: rr) sliderSig@(_ ::: ss) =+    let     resetSig    = mapAwait (box (\ _ -> resetTuple)) rr+            currentMax  = current sliderSig+            setMaxSig   = mapAwait (box setMax) ss+            inputSig    = interleave (box (.)) resetSig setMaxSig+            inputSig'   = mapAwait (box ((nats everySecondSig) .)) inputSig+            counterSig  = switchR ((nats everySecondSig) (0 :* currentMax)) inputSig'+    in counterSig++prop_counterSigAlwaysLessThanMax :: Property+prop_counterSigAlwaysLessThanMax = forAll genDouble $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ singletonH slider+            predicate   = Always $ Now ((fst' <$> Index First) |<=| (snd' <$> Index First))+            result      = evaluate predicate state+        in counterexample (show state) result+  where+    genDouble = do+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))+      return (reset, slider)++prop_maxAlwaysEqualsMax :: Property+prop_maxAlwaysEqualsMax = forAll genDouble $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ singletonH slider+            predicate   = Always $ Now ((Index Third) |==| (snd' <$> Index First))+            result      = evaluate predicate state+        in counterexample (show state) result+  where+    genDouble = do+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))+      return (reset, slider)++-- Concurrently resetting and dragging slider yields a reset signal with max value from slider.+prop_concurrentResetAndSlider :: Property+prop_concurrentResetAndSlider = forAll genDouble $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ singletonH slider+            predicate   = Always $ Implies+                (And (Now ((Ticked Second))) (Now ((Ticked Third))))+                ((Now (((Index Third)) |==| (snd' <$> Index First)))+                `And`+                (Now ((Pure 0) |==| (fst' <$> Index First))))+            result      = evaluate predicate state+        in counterexample (show state) result+  where+    genDouble = do+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))+      return (reset, slider)++prop_timerIsStrictlyMonotonicallyIncreasing :: Property+prop_timerIsStrictlyMonotonicallyIncreasing = forAll genDouble $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ singletonH slider+            predicate   = Always $ Next $+                Implies+                ((Now (Ticked First)) `And` ((Not (Now (Ticked Second)) `And` (Not (Now (Ticked Third))))))+                (Now (((fst' <$> (Index First)) |>| (fst' <$> (Index (Previous First))))))+            result      = evaluate predicate state+        in counterexample (show state) result+  where+    genDouble = do+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))+      return (reset, slider)++-- The initial state is set correctly.+prop_init :: Property+prop_init = forAll genDouble $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ singletonH slider+            predicate   = Now ((fst' <$> (Index First)) |==| (Pure 0)) `And` (Now ((snd' <$> (Index First)) |==| (Index Third)))+            result      = evaluate predicate state+        in counterexample (show state) result+  where+    genDouble = do+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))+      return (reset, slider)++-- If the counter signal hits the max value it remains at the max value until it is reset or slider has been moved.+prop_counterSigStaysAtMaxValue :: Property+prop_counterSigStaysAtMaxValue = forAllShrink genDouble shrink $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ singletonH slider+            predicate   = Always $+                Implies+                    (Now ((fst' <$> (Index First)) |==| (snd' <$> (Index First))))+                    (Next $ (Now ((fst' <$> (Index First)) |==| (fst' <$> (Index (Previous First))))+                    `Until`+                    ((Now (Ticked Second)) `Or` (Now (Ticked Third)))))+            result      = evaluate predicate state+        in counterexample (show state) result+  where+    genDouble = do+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))+      return (reset, slider)++prop_counterSigAlwaysTicks :: Property+prop_counterSigAlwaysTicks = forAll genDouble $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ singletonH slider+            predicate   = Always $ Now (Ticked First) `And` (Next $ Now (Ticked First))+            result      = evaluate predicate state+        in counterexample (show state) result+  where+    genDouble = do+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))+      return (reset, slider)++main :: IO ()+main = do+    quickCheck prop_counterSigAlwaysLessThanMax+    quickCheck prop_maxAlwaysEqualsMax+    quickCheck prop_concurrentResetAndSlider+    quickCheck prop_timerIsStrictlyMonotonicallyIncreasing+    quickCheck prop_init+    quickCheck prop_counterSigStaysAtMaxValue+    quickCheck prop_counterSigAlwaysTicks
+ src/PropRatt.hs view
@@ -0,0 +1,13 @@+module PropRatt (+    module PropRatt.Core,+    module PropRatt.LTL,+    module PropRatt.Arbitrary,+    module PropRatt.HList,+    module PropRatt.Utils+) where++import PropRatt.Core+import PropRatt.LTL+import PropRatt.Arbitrary+import PropRatt.HList+import PropRatt.Utils
+ src/PropRatt/Arbitrary.hs view
@@ -0,0 +1,208 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# HLINT ignore "Use const" #-}++module PropRatt.Arbitrary+  ( arbitrarySig,+    arbitrarySigWith,+    arbitrarySigWeighted,+    Sig (..),+    generateSignals,+    Map,+    shrinkSignal,+    shrinkHls+  )+where++import AsyncRattus.InternalPrimitives+import AsyncRattus.Plugin.Annotation+import AsyncRattus.Signal hiding (map)+import qualified Data.IntSet as IntSet+import PropRatt.Utils+import Data.Kind (Type)+import Test.QuickCheck+import Prelude hiding (const)+import PropRatt.HList++type TSig a = [(a, IntSet.IntSet)]++instance (Arbitrary a) => Arbitrary (Sig a) where+  arbitrary :: Gen (Sig a)+  arbitrary = arbitrarySig 100+  shrink :: Sig a -> [Sig a]+  shrink sig = toSignal (shrinkSignal shrink sig)++instance (Show a) => Show (Sig a) where+  show :: Sig a -> String+  show (x ::: xs) = show (toList (x ::: xs))++instance (Eq a) => Eq (Sig a) where+  (==) :: Sig a -> Sig a -> Bool+  (==) sig1 sig2 = toList sig1 == toList sig2++shrinkSignal :: (a -> [a]) -> Sig a -> [TSig a]+shrinkSignal shr sig@(_ ::: (Delay cly _)) =+  if IntSet.null cly+    then shrinkOne testableSignal shr+    else concat [ removes k n testableSignal | k <- takeWhile (>0) (iterate (`div`2) n) ]+    ++ shrinkOne testableSignal shr+  where+    n = sigLength sig+    testableSignal = toTSig sig++{-# ANN shrinkOne AllowRecursion #-}+shrinkOne :: TSig a -> (a -> [a]) -> [TSig a]+shrinkOne [] _ = error "Testable signals are non-empty"+shrinkOne [(x, cl)] shr = [ [(x', cl)] | x' <- shr x ]+shrinkOne ((x, cl) : xs) shr = [ (x', cl) : xs | x'  <- shr x ] ++ [ (x, cl) : xs' | xs' <- shrinkOne xs shr ]++{-# ANN removes AllowRecursion #-}+removes :: Int -> Int -> TSig a -> [TSig a]+removes k n tupleLs =+  if k >= n+    then []+    else let xs1 = take k tupleLs+             xs2 = drop k tupleLs+         in xs1 : xs2 : map (xs1 ++) (removes k (n-k) xs2)++{-# ANN toSignal AllowRecursion #-}+toSignal :: [TSig a] -> [Sig a]+toSignal [] = []+toSignal [x] = [fromTSig x]+toSignal (x : xs) = fromTSig x : toSignal xs++{-# ANN fromTSig AllowRecursion #-}+fromTSig :: TSig a -> Sig a+fromTSig [] = error "Testable signals are non-empty"+fromTSig [(x, _)] = x ::: never+fromTSig ((x, cl) : xs) =+  if IntSet.null cl+    then x ::: never+    else x ::: Delay cl (\_ -> fromTSig xs)++{-# ANN toTSig AllowRecursion #-}+toTSig :: Sig a -> TSig a+toTSig (x ::: (Delay cl f)) =+  if IntSet.null cl+    then [(x, IntSet.empty)]+    else (x, cl) : toTSig (f (InputValue (IntSet.findMin cl) ()))++genClockChannelWeighted :: Gen Int+genClockChannelWeighted = frequency [(1, pure 1), (1, pure 2), (50, pure 3)]++genClock :: Int -> Gen Clock+genClock n = case n of+    1 -> do+      x <- chooseInt (1,3)+      return (IntSet.fromList [x])+    2 -> frequency [(1, return (IntSet.fromList [1,2])),(1, return (IntSet.fromList [2,3])),(1, return (IntSet.fromList [1,3]))]+    3 -> return (IntSet.fromList [1,2,3])+    _ -> error "Partial function doesnt support n > 3"++genClockListWeighted :: Gen [Int]+genClockListWeighted = vectorOf 1 genClockChannelWeighted++{-# ANN arbitrarySig AllowRecursion #-}+arbitrarySig :: (Arbitrary a) => Int -> Gen (Sig a)+arbitrarySig n = do+  if n <= 0+    then error "Cannot create empty signals"+    else+      go n+      where+        go 1 = do+          x <- arbitrary+          return (x ::: never)+        go m = do+          x <- arbitrary+          len <- chooseInt (1, 3)+          cl <- genClock len+          xs <- go (m - 1)+          let later = Delay cl (\_ -> xs)+          return (x ::: later)++{-# ANN arbitrarySigWith AllowRecursion #-}+arbitrarySigWith :: Int -> Gen a -> Gen (Sig a)+arbitrarySigWith n gen = do+  if n <= 0+    then error "Cannot create empty signals"+    else+      go n+      where+        go 1 = do+          x <- gen+          return (x ::: never)+        go m = do+          x <- gen+          len <- chooseInt (1, 3)+          cl <- genClock len+          xs <- go (m - 1)+          let later = Delay cl (\_ -> xs)+          return (x ::: later)++{-# ANN arbitrarySigWeighted AllowRecursion #-}+arbitrarySigWeighted :: (Arbitrary a) => Int -> Gen (Sig a)+arbitrarySigWeighted n = do+  if n <= 0+    then error "Cannot create empty signals"+    else+      go n+      where+        go 1 = do+          x <- arbitrary+          return (x ::: never)+        go m = do+          x <- arbitrary+          cl <- genClockListWeighted+          xs <- go (m - 1)+          let later = Delay (IntSet.fromList cl) (\_ -> xs)+          return (x ::: later)++type family Map (f :: Type -> Type) (xs :: [Type]) :: [Type] where+  Map f '[] = '[]+  Map f (x ': xs) = f x ': Map f xs++-- Use polykinds to allow us to overload generateSignals to work for both Type and Type -> Type+type family ToList (a :: k) :: [Type] where+  ToList (a :: [Type]) = a+  ToList (a :: Type)   = '[a]++class HListGen (ts :: [Type]) where+  generateHList     :: Gen (HList (Map Sig ts))++instance HListGen '[] where+  generateHList = return HNil++instance (Arbitrary (Sig t), HListGen ts) => HListGen (t ': ts) where+  generateHList = do+    x <- arbitrary+    xs <- generateHList @ts+    return (x %: xs)++generateSignals :: forall a. HListGen (ToList a) => Gen (HList (Map Sig (ToList a)))+generateSignals = generateHList @(ToList a)++class ShrinkHList as where+  shrinkHls :: HList as -> [HList as]++instance ShrinkHList '[] where+  shrinkHls _ = []++instance (Arbitrary a, ShrinkHList as) => ShrinkHList (a ': as) where+  shrinkHls (HCons x xs) =+    [ HCons x' xs | x'  <- shrink x ] +++    [ HCons x xs' | xs' <- shrinkHls xs ] +++    [ HCons x' xs' | x'  <- shrink x, xs' <- shrinkHls xs ]
+ src/PropRatt/Core.hs view
@@ -0,0 +1,74 @@+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE PolyKinds #-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}++module PropRatt.Core (+  prepend,+  prependLater,+  flatten,+  singletonH+) where++import AsyncRattus.Signal+import AsyncRattus.Strict hiding (singleton)+import AsyncRattus.InternalPrimitives hiding (never)+import PropRatt.Value+import PropRatt.HList+import Prelude hiding (const)++emptySig :: Sig (HList '[])+emptySig = const HNil++class Stable (HList vals) => Flatten sigs vals | sigs -> vals, vals -> sigs where+  flatten :: HList sigs -> Sig (HList vals)++instance Flatten '[] '[] where+  flatten :: HList '[] -> Sig (HList '[])+  flatten HNil = emptySig++instance (Stable a, Stable (Value a), Flatten as bs, Falsify bs) => Flatten (Sig a ': as) (Value a ': bs) where+  flatten :: HList (Sig a : as) -> Sig (HList (Value a : bs))+  flatten (HCons h t) = prepend h (flatten t)++class Falsify ts where+  toFalse :: HList ts -> HList ts++instance Falsify '[] where+  toFalse :: HList '[] -> HList '[]+  toFalse _ =  HNil++instance (Falsify ts) => Falsify (Value t ': ts) where+  toFalse :: HList (Value t : ts) -> HList (Value t : ts)+  toFalse (HCons (Current _ x) t) = Current (HasTicked False) x %: toFalse t++-- | Like 'prepend', but the new head is delayed by one tick.+--   This emits a dummy value at the head on the first tick, then behaves like 'prepend' on subsequent ticks.+prependLater :: (Stable t, Stable (HList ts), Falsify ts) => O (Sig t) -> Sig (HList ts) -> Sig (HList (Value t ': ts))+prependLater xs (y ::: ys) =+  HCons (Current (HasTicked False) Nil) y ::: prependAwait Nil xs y ys++prepend :: (Stable t, Stable (HList ts), Falsify ts) => Sig t -> Sig (HList ts) -> Sig (HList (Value t ': ts))+prepend (x ::: xs) (y ::: ys) =+  HCons (Current (HasTicked True) (x :! Nil)) y ::: prependAwait (x :! Nil) xs y ys++prependAwait :: (Stable t, Stable hls, hls ~ HList ts, Falsify ts) => List t -> O (Sig t) -> hls -> O (Sig hls) -> O (Sig (HList (Value t ': ts)))+prependAwait x xs y ys  = delay (+  case select xs ys of+     Fst (x' ::: xs')   ys'         -> (Current (HasTicked True) (x' :! x) %: toFalse y)  ::: prependAwait (x' :! x) xs' y ys'+     Snd xs' (y' ::: ys')           -> (Current (HasTicked False) x %: y')                ::: prependAwait x xs' y' ys'+     Both (x' ::: xs') (y' ::: ys') -> (Current (HasTicked True) (x' :! x) %: y')         ::: prependAwait (x' :! x) xs' y' ys')++singletonH :: (Stable t) => Sig t -> Sig (HList '[Value t])+singletonH sig = flatten (sig %: HNil)
+ src/PropRatt/HList.hs view
@@ -0,0 +1,69 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE PolyKinds #-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++module PropRatt.HList (HList(..), (%:), first,second,third,fourth,fifth,sixth,seventh,eighth,ninth,lengthH) where       +import AsyncRattus.InternalPrimitives ( Stable )+import Data.Kind (Type)++data HList :: [Type] -> Type where+  HNil :: HList '[]+  HCons :: !x -> !(HList xs) -> HList (x ': xs)++infixr 5 %:+(%:) :: x -> HList xs -> HList (x ': xs)+(%:) = HCons++instance Show (HList '[]) where+  show :: HList '[] -> String+  show HNil = "HNil"++instance (Show x, (Show (HList xs))) => Show (HList (x ': xs)) where+  show :: (Show x, Show (HList xs)) => HList (x : xs) -> String+  show (HCons x xs) = show x ++ " %: " ++ show xs++instance Stable (HList '[]) where+instance (Stable a, Stable (HList as)) => Stable (HList (a ': as)) where++first :: HList (a ': _) -> a+first (HCons h _) = h++second :: HList (_ ': a ': _) -> a+second (HCons _ (HCons h2 _)) = h2++third :: HList (_ ': _ ': a ': _) -> a+third (HCons _ (HCons _ (HCons h3 _))) = h3++fourth :: HList (_ ': _ ': _ ': a ': _) -> a+fourth (HCons _ (HCons _ (HCons _ (HCons h4 _)))) = h4++fifth :: HList (_ ': _ ': _ ': _ ': a ': _) -> a+fifth (HCons _ (HCons _ (HCons _ (HCons _ (HCons h5 _))))) = h5++sixth :: HList (_ ': _ ': _ ': _ ': _ ': a ': _) -> a+sixth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h6 _)))))) = h6++seventh :: HList (_ ':_ ': _ ': _ ': _ ': _ ': a ': _) -> a+seventh (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h7 _))))))) = h7++eighth :: HList (_ ': _ ': _ ': _ ': _ ': _ ': _ ': a ': _) -> a+eighth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h8 _)))))))) = h8++ninth :: HList (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': a ': _) -> a+ninth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h9 _))))))))) = h9+++lengthH :: HList ts -> Int -> Int+lengthH HNil n = n+lengthH (HCons _ as) n = lengthH as (n+1)
+ src/PropRatt/LTL.hs view
@@ -0,0 +1,295 @@+{-# LANGUAGE GADTs, DataKinds, MultiParamTypeClasses, RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}++module PropRatt.LTL+  ( Pred (..),+    evaluate,+    evaluateWith,+    Expr (..),+    Lookup (..),+    (|<|),+    (|<=|),+    (|>|),+    (|>=|),+    (|==|),+  )+where++import AsyncRattus.InternalPrimitives+import AsyncRattus.Strict+import AsyncRattus.Signal hiding (const)+import qualified Data.IntSet as IntSet+import Data.Kind+import PropRatt.Value+import PropRatt.HList+import PropRatt.Utils++data Pred (ts :: [Type]) where+  Tautology     :: Pred ts+  Contradiction :: Pred ts+  Now           :: Expr ts Bool -> Pred ts+  Not           :: Pred ts -> Pred ts+  And           :: Pred ts -> Pred ts -> Pred ts+  Or            :: Pred ts -> Pred ts -> Pred ts+  Until         :: Pred ts -> Pred ts -> Pred ts+  Next          :: Pred ts -> Pred ts+  Implies       :: Pred ts -> Pred ts -> Pred ts+  Always        :: Pred ts -> Pred ts+  Eventually    :: Pred ts -> Pred ts+  After         :: Int -> Pred ts-> Pred ts+  Release       :: Pred ts -> Pred ts -> Pred ts++data Expr (ts :: [Type]) (t :: Type) where+  Pure    :: t -> Expr ts t+  Apply   :: Expr ts (t -> r) -> Expr ts t -> Expr ts r+  Index   :: Lookup ts t -> Expr ts t+  Ticked  :: Lookup ts t -> Expr ts Bool++data Lookup (ts :: [Type]) (t :: Type) where+  Previous  :: Lookup ts t -> Lookup ts t+  Prior     :: Int -> Lookup ts t -> Lookup ts t+  First     :: Lookup (Value t ': x) t+  Second    :: Lookup (x1 ': Value t ': x2) t+  Third     :: Lookup (x1 ': x2 ': Value t ': x3) t+  Fourth    :: Lookup (x1 ': x2 ': x3 ': Value t ': x4) t+  Fifth     :: Lookup (x1 ': x2 ': x3 ': x4 ': Value t ': x5) t+  Sixth     :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': Value t ': x6) t+  Seventh   :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': Value t ': x7) t+  Eighth    :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': x7 ': Value t ': x8) t+  Ninth     :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': x7 ': x8 ': Value t ': x9) t++instance Functor (Expr ts) where+  fmap :: (t -> r) -> Expr ts t -> Expr ts r+  fmap f (Pure x)     = Pure (f x)+  fmap f (Apply g x)  = Apply (fmap (f .) g) x+  fmap f (Index lu)   = Apply (Pure f) (Index lu)+  fmap f (Ticked lu)  = Apply (Pure f) (Ticked lu)++instance Applicative (Expr ts) where+    pure :: t -> Expr ts t+    pure = Pure+    (<*>) :: Expr ts (t -> r) -> Expr ts t -> Expr ts r+    Pure f <*> x = fmap f x+    Apply f g <*> x = Apply (Apply f g) x+    (<*>) _ _ = error "Expr: unsupported constructor for applicative application."++instance Num t => Num (Expr ts t) where+  (+) :: Expr ts t -> Expr ts t -> Expr ts t+  (+) x y = (+) <$> x <*> y+  (-) :: Expr ts t -> Expr ts t -> Expr ts t+  (-) x y = (-) <$> x <*> y+  (*) :: Expr ts t -> Expr ts t -> Expr ts t+  (*) x y = (*) <$> x <*> y+  negate :: Expr ts t -> Expr ts t+  negate = fmap negate+  abs :: Expr ts t -> Expr ts t+  abs = fmap abs+  signum :: Expr ts t -> Expr ts t+  signum = fmap signum+  fromInteger :: Integer -> Expr ts t+  fromInteger n = pure (fromInteger n)++(|<|) :: (Applicative f, Ord t) => f t -> f t -> f Bool+x |<| y = (<) <$> x <*> y+(|<=|) :: (Applicative f, Ord t) => f t -> f t -> f Bool+x |<=| y = (<=) <$> x <*> y+(|>|) :: (Applicative f, Ord t) => f t -> f t -> f Bool+x |>| y = (>) <$> x <*> y+(|>=|) :: (Applicative f, Ord t) => f t -> f t -> f Bool+x |>=| y = (>=) <$> x <*> y+(|==|) :: (Applicative f, Eq t) => f t -> f t -> f Bool+x |==| y = (==) <$> x <*> y++-- | Checks whether the instances of "previous" is within scope of t "next" operator.+-- This prevents the evaluation from looking too far back in time.+checkScope :: Pred ts -> Bool+checkScope p = checkPred p 0++-- | Traverses the predicate supplied and exits early if it finds a subtree where the scope is negative.+-- The scope is incremented for each next constructor, and decremented for each previous or prior constructor.+checkPred :: Pred ts -> Int -> Bool+checkPred predicate scope =+  valid scope &&+  case predicate of+    Tautology       -> valid scope+    Contradiction   -> valid scope+    Now expr        -> valid (checkExpr expr scope)+    Not p           -> checkPred p scope+    And p1 p2       -> checkPred p1 scope && checkPred p2 scope+    Or p1 p2        -> checkPred p1 scope || checkPred p2 scope+    Until p1 p2     -> checkPred p1 scope && checkPred p2 scope+    Next p          -> checkPred p (scope + 1)+    Implies p1 p2   -> checkPred p1 scope && checkPred p2 scope+    Release p1 p2   -> checkPred p1 scope && checkPred p2 scope+    Always p        -> checkPred p scope+    Eventually p    -> checkPred p scope+    After n p       -> checkPred p (scope + n)+  where+    valid s = s >= 0++-- | Propegates the smallest scope found by traversing the expr.+checkExpr :: Expr ts t -> Int -> Int+checkExpr expr scope =+  case expr of+    Pure _        -> scope+    Apply fun arg -> min (checkExpr fun scope) (checkExpr arg scope)+    Index lu      -> checkLookup lu scope+    Ticked lu     -> checkLookup lu scope++checkLookup :: Lookup ts t -> Int -> Int+checkLookup lu scope =+  case lu of+    Previous lu'  -> checkLookup lu' (scope - 1)+    Prior n lu'   -> checkLookup lu' (scope - n)+    _             -> scope++-- Returns the amount of signal elements needed to evaluate the predicate.+minSigLengthForPred :: Pred ts -> Int -> Int+minSigLengthForPred predicate acc =+    case predicate of+      Not p           -> minSigLengthForPred p acc+      And p1 p2       -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc+      Or p1 p2        -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc+      Until p1 p2     -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc+      Next p          -> minSigLengthForPred p (acc + 1)+      Implies p1 p2   -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc+      Release p1 p2   -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc+      Always p        -> minSigLengthForPred p acc+      Eventually p    -> minSigLengthForPred p acc+      After n p       -> minSigLengthForPred p (acc + n)+      _               -> acc++nthPrevious :: Int -> Value t -> Maybe' (Value t)+nthPrevious n curr@(Current b history)+  | n <= 0    = Just' curr+  | otherwise =+      case history of+        _ :! xs -> nthPrevious (n - 1) (Current b xs)+        Nil     -> Nothing'++evalTicked :: Lookup ts t -> HList ts -> Bool+evalTicked lu hls = case lu of+  Previous _ -> errorTickedPast+  Prior _ _  -> errorTickedPast+  First      -> extract $ first hls+  Second     -> extract $ second hls+  Third      -> extract $ third hls+  Fourth     -> extract $ fourth hls+  Fifth      -> extract $ fifth hls+  Sixth      -> extract $ sixth hls+  Seventh    -> extract $ seventh hls+  Eighth     -> extract $ eighth hls+  Ninth      -> extract $ ninth hls+  where+    errorTickedPast                   = error "Cannot check if signal has ticked in the past."+    extract (Current (HasTicked b) _) = b++evalExpr :: Expr ts t -> HList ts -> Expr ts t+evalExpr (Pure x) _      = pure x+evalExpr (Apply f x) hls = (($) <$> evalExpr f hls) <*> evalExpr x hls+evalExpr (Index lu) hls  =+  case evalLookup lu hls of+    Just' (Current _ (h :! _)) -> pure h+    Just' (Current _ Nil)      -> error "History not found for signal."+    Nothing'                   -> error "Signal not found."+evalExpr (Ticked lu) hls = pure (evalTicked lu hls)++evalLookup :: Lookup ts t -> HList ts -> Maybe' (Value t)+evalLookup lu hls = case lu of+  Previous lu' ->+    case evalLookup lu' hls of+      Just' (Current b history) ->+        case history of+          _ :! xs -> Just' (Current b xs)+          Nil     -> Nothing'+      Nothing' -> Nothing'+  Prior n lu'  -> case evalLookup lu' hls of+    Just' v  -> nthPrevious n v+    Nothing' -> Nothing'+  First         -> Just' (first hls)+  Second        -> Just' (second hls)+  Third         -> Just' (third hls)+  Fourth        -> Just' (fourth hls)+  Fifth         -> Just' (fifth hls)+  Sixth         -> Just' (sixth hls)+  Seventh       -> Just' (seventh hls)+  Eighth        -> Just' (eighth hls)+  Ninth         -> Just' (ninth hls)++-- Evaluate a single timestep. Used exclusively for shrink cases.+evaluateSingle  :: Int -> Pred ts -> Sig (HList ts) -> Bool+evaluateSingle timestepsLeft formulae sig@(x ::: _) =+  timestepsLeft <= 0 || case formulae of+            Tautology       -> True+            Contradiction   -> False+            Now expr        ->+              case evalExpr expr x of+                Pure b -> b+                _ -> error "Unexpected error during evaluation."+            Not phi         -> not (eval phi sig)+            And phi psi     -> eval phi sig && eval psi sig+            Or phi psi      -> eval phi sig || eval psi sig+            Until phi psi   -> eval psi sig || eval phi sig+            Next _          -> True+            Implies phi psi -> not (eval phi sig && not (eval psi sig))+            Always phi      -> eval phi sig+            Eventually phi  -> eval phi sig +            Release _ _     -> True +            After _ _       -> True+        where+          eval = evaluateSingle timestepsLeft++evaluate' :: Int -> Pred ts -> Sig (HList ts) -> Bool+evaluate' timestepsLeft formulae sig@(x ::: Delay cl f) =+  if IntSet.null cl+    then evaluateSingle timestepsLeft formulae sig+    else timestepsLeft <= 0 || case formulae of+            Tautology       -> True+            Contradiction   -> False+            Now expr        ->+              case evalExpr expr x of+                Pure b -> b+                _ -> error "Unexpected error during evaluation."+            Not phi         -> not (eval phi sig)+            And phi psi     -> eval phi sig && eval psi sig+            Or phi psi      -> eval phi sig || eval psi sig+            Until phi psi   -> eval psi sig+                              || (eval phi sig && evaluateNext (phi `Until` psi) advance)+            Next phi        -> evaluateNext phi advance+            Implies phi psi -> not (eval phi sig && not (eval psi sig))+            Always phi      -> eval phi sig && evaluateNext (Always phi) advance+            Eventually phi  -> (eval phi sig || evaluateNext (Eventually phi) advance)+                                && not (timestepsLeft == 1 && not (eval phi sig))+            Release phi psi -> (eval psi sig && eval phi sig)+                                || (eval psi sig && evaluateNext (phi `Until` psi) advance)+            After n phi     -> if n <= 0 then eval phi sig else evaluateNext (After (n - 1) phi) sig+      where+        evaluateNext = evaluate' (timestepsLeft - 1)+        eval = evaluate' timestepsLeft+        advance = f (InputValue (IntSet.findMin cl) ())++-- Finds the minimum length a signal must have for the pred to be tested.+-- If the length of the signal is too short, short circuit evaluation to true (shrink cases).+evaluate :: Pred ts -> Sig (HList ts) -> Bool+evaluate = evaluateWith 100++evaluateWith :: Int -> Pred ts -> Sig (HList ts) -> Bool+evaluateWith defaultTimeStepsToCheck p sig =+  let len       = sigLength sig+      min'      = minSigLengthForPred p 1+      tooShort  = len < min'+      scopeOk   = checkScope p+  in +    if not scopeOk+      then error "Previous must be in scope of next" +    else if min' > defaultTimeStepsToCheck+      then error ("Cannot evaluate more than " ++ show defaultTimeStepsToCheck ++ " values.\n" ++ "Predicate requires " ++ show min' ++ " timesteps. Consider using evaluateWith (>= " ++ show min' ++ ")")+    else+      tooShort || evaluate' (defaultTimeStepsToCheck `min` len) p sig
+ src/PropRatt/Signal.hs view
@@ -0,0 +1,15 @@+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}++module PropRatt.Signal (hlistLen,takeN) where++import AsyncRattus.Signal+import AsyncRattus+import PropRatt.HList++hlistLen :: Sig (HList ts) -> Int+hlistLen (m ::: _) = lengthH m 0++{-# ANN takeN AllowRecursion #-}+takeN :: Int -> Sig a -> Sig a+takeN 1 (x ::: _) = x ::: never+takeN n (x ::: later) = x ::: delay (takeN (n-1) (adv later))
+ src/PropRatt/Utils.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE FlexibleContexts #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Use const" #-}+{-# LANGUAGE GADTs #-}++module PropRatt.Utils (smallest,toList,toListWithClock,toListOfLength,lengthSig,sigLength,mkSigOne,mkSigZero) where++import AsyncRattus.Signal (Sig(..))+import AsyncRattus.InternalPrimitives+import qualified Data.IntSet as IntSet+import Prelude hiding (map, zip, zipWith, take)+++smallest :: IntSet.IntSet -> Int+smallest = IntSet.findMin+++toList :: Sig a -> [a]+toList (x ::: Delay cl f)+    | IntSet.null cl = [x]+    | otherwise = x : toList (f (InputValue (smallest cl) ()))+++toListWithClock :: Sig a -> [(a, IntSet.IntSet)]+toListWithClock (x ::: Delay cl f)+    | IntSet.null cl = [(x, cl)]+    | otherwise = (x, cl) : toListWithClock (f (InputValue (smallest cl) ()))+++toListOfLength :: Int -> Sig a -> [a]+toListOfLength 0 _ = []+toListOfLength n (x ::: Delay cl f) = x : toListOfLength (n-1) (f (InputValue (smallest cl) ()))+++lengthSig :: Sig a -> Int -> Int+lengthSig (_ ::: Delay cl f) acc+    | IntSet.null cl = acc + 1+    | otherwise = lengthSig (f (InputValue (smallest cl) ())) (acc+1)++sigLength :: Sig a -> Int+sigLength sig = lengthSig sig 0++++mkSigOne :: Sig Int+mkSigOne = 1 ::: Delay (IntSet.fromList [1]) (\_ -> mkSigOne)++++mkSigZero :: Sig Int+mkSigZero = 0 ::: Delay (IntSet.fromList [2]) (\_ -> mkSigZero)+
+ src/PropRatt/Value.hs view
@@ -0,0 +1,49 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables, UndecidableInstances #-}++module PropRatt.Value (Value(..),pureVal,current, HasTicked(..)) where+import AsyncRattus.Strict+import AsyncRattus.Signal hiding (current)+import PropRatt.Utils+import AsyncRattus++newtype HasTicked = HasTicked Bool deriving Show++data Value a where+  Current :: !HasTicked -> !(List a) -> Value a++instance Stable (Value a) where +instance Num a => Num (Value a) where+  (+) v1 v2 = pureVal (current v1 + current v2)+  (-) v1 v2 = pureVal (current v1 - current v2)+  (*) v1 v2 = pureVal (current v1 * current v2)+  negate v  = pureVal (negate (current v))+  abs v     = pureVal (abs (current v))+  signum v  = pureVal (signum (current v))+  fromInteger n = pureVal (fromInteger n)++instance Show a => Show (Value a) where+  show (Current t Nil) = show t+  show (Current _ (h :! Nil)) = show h+  show (Current _ (h :! h2 :! _)) =  show h ++ " " ++ show h2++instance Show a => Show (Sig [Value a]) where+  show sig = "Sig [Value a]: " ++ show (toListOfLength 100 sig) ++ "..."++instance Ord a => Ord (Value a) where+  compare v1 v2 = compare (current v1) (current v2)++instance Eq a => Eq (Value a) where+  v1 == v2 = current v1 == current v2++pureVal :: a -> Value a+pureVal x = Current (HasTicked False) (x :! Nil)++current :: Value a -> a+current (Current _ (h :! _)) = h+current _ = undefined
+ test/Spec.hs view
@@ -0,0 +1,23 @@+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}+{-# LANGUAGE TypeApplications, FlexibleInstances #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++import Test.QuickCheck+import PropRatt.Arbitrary+import PropRatt.Core+import PropRatt.HList+import PropRatt.Signal++prop_shouldAddToHList :: Property+prop_shouldAddToHList = forAll (generateSignals @[Int, Int]) $ \intSignals ->+    let flat        = flatten intSignals+        before      = hlistLen flat+        state       = prepend (first intSignals) $ flatten intSignals+        after       = hlistLen state+        result      = (before + 1) == after+    in result++main :: IO ()+main = do+    quickCheck prop_shouldAddToHList