PropRatt 0.1.0.0 → 0.2.0.0

raw patch · 10 files changed

+397/−261 lines, 10 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−8
• PropRatt.cabal +10/−2
• README.md +16/−0
• examples/main/Main.hs +53/−46
• examples/timer/Timer.hs +90/−23
• src/PropRatt/Arbitrary.hs +14/−13
• src/PropRatt/Core.hs +8/−8
• src/PropRatt/HList.hs +15/−17
• src/PropRatt/LTL.hs +177/−138
• src/PropRatt/Value.hs +9/−6

@@ -1,11 +1,8 @@-# Changelog for `experiments`--All notable changes to this project will be documented in this file.+# 0.2.0.0 -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/).+- Revised syntax of specification language.+- Added shorthand syntax. -## Unreleased+# 0.1.0.0 -## 0.1.0.0 - YYYY-MM-DD+Initial release

@@ -1,14 +1,22 @@ cabal-version: 2.2 name:           PropRatt-version:        0.1.0.0+version:        0.2.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.+                PropRatt is a property-based testing framework for testing <https://hackage.haskell.org/package/AsyncRattus 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.+                .+                More details about the specification language can be found in the <https://bahr.io/pubs/files/propratt-paper.pdf accompanying paper>.+                .+                Example specifications written in PropRatt:+                .+                * <https://github.com/pa-ba/PropRatt/blob/main/examples/timer/Timer.hs Specification for a simple GUI application>+                .+                * <https://github.com/pa-ba/PropRatt/blob/main/examples/main/Main.hs Specification for basic signal combinators> (@map@, @zip@, @scan@, etc.) author:         Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr maintainer:     paba@itu.dk copyright:      2025 Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr

@@ -2,7 +2,23 @@  PropRatt is a Haskell framework for testing AsyncRattus using property-based testing. +# Overview++- The [main example file](examples/main/Main.hs) contains example+  specifications that test signal combinators of the Async Rattus+  library.+- The [timer example file](examples/timer/Timer.hs) contains the timer+  example from the paper.+- The implementation of the specification language can be found in the+  [PropRatt.LTL](src/PropRatt/LTL.hs) module.++ # Running examples +Using `stack`: - `stack run main-example` - `stack run timer-example`++Using `cabal`:+- `cabal run main-example`+- `cabal run timer-example`

@@ -1,5 +1,5 @@ {-# OPTIONS -fplugin=AsyncRattus.Plugin #-}-{-# LANGUAGE TypeApplications, FlexibleInstances #-}+{-# LANGUAGE TypeApplications, FlexibleInstances, TypeOperators #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}@@ -23,6 +23,13 @@  {-# ANN module AllowLazyData #-} +zipWrong :: (Stable a, Stable b) => Sig a -> Sig b -> Sig (a :* b)+zipWrong (a ::: as) (b ::: bs) = (a :* b) ::: delay (+        case select as bs of+        Fst (a' ::: as') bs' -> zipWrong (a' ::: as') (b ::: bs')+        Snd as' (b' ::: bs') -> zipWrong (a ::: as') (b ::: bs')+        Both as' bs' -> zipWrong as' bs')+ 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))@@ -47,11 +54,11 @@ 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)))+        predicate       = X $ G $ ((sig1 |==| sig2)                                         `Or`-                                        (Now ((Index First) |==| (Index Third))))+                                        (sig1 |==| sig3))                                         `Or`-                                        (Now (((Index Second) + (Index Third)) |==| (Index First)))+                                        ((sig2 + sig3) |==| sig1)         result          = evaluate predicate state     in result @@ -61,10 +68,7 @@    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)) --+        predicate   = G $ (sig1 |==| sig2) `Or` (sig1 |==| pure 1)         result      = evaluate predicate state     in result @@ -73,7 +77,7 @@ 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)+        predicate   = X $ G $ prev sig1 |<| sig1         result      = evaluate predicate state     in counterexample ("Must be natural numbers.") result @@ -83,7 +87,7 @@     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)+        predicate   = X $ G $ prev sig1 |<| sig1         result      = evaluate predicate state     in result @@ -92,7 +96,7 @@ 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)))+        predicate   = (sig1 |==| sig2) `U` (tick3 `And` G(sig1 |==| sig3))         result      = evaluate predicate state     in result @@ -101,7 +105,7 @@ 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)+        predicate   = X $ G $ sig1 |==| prev sig2         result      = evaluate predicate state     in result @@ -110,7 +114,7 @@ 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))))+        predicate   = G ((sig1 |>| pure 100) :=> (G $ X (prev sig1 |==| sig1)))         result      = evaluate predicate state     in result @@ -119,18 +123,26 @@ 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)))+        predicate   = G $ ((fst' <$> sig1) |==| sig2) `And` ((snd' <$> sig1) |==| sig3)         result      = evaluate predicate state     in result +prop_zipWrong :: Property+prop_zipWrong = forAllShrink (generateSignals @[Int, Int]) shrinkHls $ \intSignals ->+    let s1          = zipWrong (first intSignals) (second intSignals)+        state       = prepend s1 $ flatten intSignals+        predicate   = G (tick3 :=> (sig3 |==| (snd' <$> sig1)))+        result      = evaluate predicate state+    in counterexample (show state) 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))))+      predicate     = G $+            ((sig2 |>=| pure 10) :=> (sig1 |>=| pure (Just' 10)))             `And`-            Implies (Now ((Index Second) |<| Pure (10))) (Now ((Index First) |==| (Pure Nothing')))+            (sig2 |<| pure 10) :=> (sig1 |==| pure Nothing')       result        = evaluate predicate state   in result @@ -138,8 +150,9 @@ 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)))))+      predicate     = G +            tick2 :=> +            (tick1 `And` ((fromMaybe' 0 <$> sig1) |==| (sig2 * sig3)))       result        = evaluate predicate state   in result @@ -147,10 +160,7 @@ 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))+        predicate   = G $ (tick3 :=> tick1) `And`(tick2 :=> tick1)         result      = evaluate predicate state     in result @@ -158,10 +168,10 @@ 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))+        predicate   = G $+            (tick1 :=> (sig1 |==| sig2))             `And`-            Next (Implies (And (Now (Ticked Third)) (Not (Now (Ticked Second)))) (Now (Index (Previous First) |==| Index First)))+            X ((tick3 `And` Not (tick2)) :=> (prev sig1 |==| sig1))         result      = evaluate predicate state     in result @@ -169,14 +179,14 @@ prop_functionIsMonotonic = forAll (generateSignals @Int) $ \intSignals ->     let mono        = monotonic (first intSignals)         state       = singletonH mono-        predicate   = Always $ Next (Now ((Index First) |>=| (Index (Previous First))))+        predicate   = G $ X (sig1 |>=| prev sig1)         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))+        predicate   = G tick1         result      = evaluate predicate state     in result @@ -187,14 +197,11 @@         (_ ::: 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)))+        predicate           = ((sig1 |==| sig3) `U`tick2)                                 `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))))))+                                (G $ X (Not tick2 :=> (prev sig1 |==| sig1)))+                                `U`+                                 (X (tick2 :=> Not (prev sig1 |==| sig1)))         result              = evaluate predicate state     in counterexample (show state) result @@ -205,21 +212,19 @@         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)))+        predicate           =(sig1 |==| sig3)+                                `U`+                                tick2                                 `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))))))+                                (G $ X (Not tick2 :=> (prev sig1 |==| sig1)))+                                `U`(X (tick2 :=> Not (prev sig1 |==| sig1)))         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)))+            predicate   = G (sig1 |<| pure 50)             result      = evaluate predicate state         in result @@ -227,14 +232,14 @@ 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))+            predicate   = X $ G (prevN 1 sig1 |>=| 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)))))+            predicate   = G ((sig1 |>| pure 80) :=> X (sig1 |<| (prev sig1)))             result      = evaluate predicate state         in result @@ -242,7 +247,7 @@ 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)+        predicate   = XN 100 $ G (prev sig1 |<| sig1)         result      = evaluate predicate state     in result @@ -274,3 +279,5 @@     quickCheck (withMaxSuccess 1000 prop_catchsubtle)     putStrLn "====================="     quickCheck prop_predLengthOutsideDefault+    putStrLn "====================="+    quickCheck prop_zipWrong

@@ -17,10 +17,15 @@  {-# ANN module AllowLazyData #-} -{-# ANN everySecondSig AllowRecursion #-}-everySecondSig :: O (Sig ())-everySecondSig = Delay (IntSet.fromList [2]) (\_ -> () ::: everySecondSig)+{-# ANN everySig2Sig' AllowRecursion #-}+everySig2Sig' :: Int -> O (Sig ())+everySig2Sig' 0 = never+everySig2Sig' n = Delay (IntSet.fromList [2]) (\_ -> () ::: everySig2Sig' (n-1)) +everySig2Sig :: O (Sig ())+everySig2Sig = everySig2Sig' 100++ nats :: O (Sig ()) -> (Int :* Int) -> Sig (Int :* Int) nats later (n :* max) = stop     (box (\ (n' :* max') -> n' >= max'))@@ -38,15 +43,15 @@             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'+            inputSig'   = mapAwait (box ((nats everySig2Sig) .)) inputSig+            counterSig  = switchR ((nats everySig2Sig) (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))+            predicate   = G ((fst' <$> sig1) |<=| (snd' <$> sig1))             result      = evaluate predicate state         in counterexample (show state) result   where@@ -59,7 +64,7 @@ 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))+            predicate   = G (sig3 |==| (snd' <$> sig1))             result      = evaluate predicate state         in counterexample (show state) result   where@@ -73,11 +78,11 @@ 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)))+            predicate   = G $ +                ((tick2 `And` tick3) :=>+                ((sig3 |==| (snd' <$> sig1))                 `And`-                (Now ((Pure 0) |==| (fst' <$> Index First))))+                (pure 0 |==| (fst' <$> sig1))))             result      = evaluate predicate state         in counterexample (show state) result   where@@ -86,14 +91,41 @@       reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))       return (reset, slider) +++prop_reset :: Property+prop_reset = forAll genDouble $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ singletonH slider+            predicate   = G (tick2 :=> (pure 0 |==| (fst' <$> sig1)))+            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_max :: Property+prop_max = forAll genDouble $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ singletonH slider+            predicate   = G (sig3 |==| (snd' <$> sig1))+            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))))))+            predicate   = G $ X+                ((tick1 `And` (Not tick2 `And` Not tick3)) :=>+                ((fst' <$> sig1) |>| (fst' <$> prev sig1)))             result      = evaluate predicate state         in counterexample (show state) result   where@@ -107,7 +139,7 @@ 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)))+            predicate   = ((fst' <$> sig1) |==| pure 0) `And` ((snd' <$> sig1) |==| sig3)             result      = evaluate predicate state         in counterexample (show state) result   where@@ -121,12 +153,11 @@ 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)))))+            predicate   = G $+                    (((fst' <$> sig1) |==| (snd' <$> sig1)) :=>+                    (X $ ((fst' <$> sig1) |==| (fst' <$> prev sig1))+                    `U`+                    (tick2 `Or` tick3)))             result      = evaluate predicate state         in counterexample (show state) result   where@@ -139,7 +170,7 @@ 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))+            predicate   = G (tick1 `And` X tick1)             result      = evaluate predicate state         in counterexample (show state) result   where@@ -148,6 +179,38 @@       reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))       return (reset, slider) +++-- the timer is constant unless a second passes or reset is pressed+prop_timerConst :: Property+prop_timerConst = forAllShrink genDouble shrink $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ prepend slider $ singletonH (() ::: everySig2Sig)+            predicate   = G (X ((Not tick2 `And` Not tick4) :=> ((fst' <$> prev sig1) |==| (fst' <$> sig1))))+            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 timer ticks unless it reached its maximum+prop_timerTicks :: Property+prop_timerTicks = forAllShrink genDouble shrink $ \(reset, slider) ->+        let counterSig  = timerState reset slider+            state       = prepend counterSig $ prepend reset $ prepend slider $ singletonH (() ::: everySig2Sig)+            predicate   = G ( ((snd' <$> sig1) |<| sig3 `And` X tick4)  :=> X ((snd' <$> sig1) |==| ((+1) . snd' <$> prev sig1)))+            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@@ -157,3 +220,7 @@     quickCheck prop_init     quickCheck prop_counterSigStaysAtMaxValue     quickCheck prop_counterSigAlwaysTicks+    quickCheck prop_reset+    quickCheck prop_max+    quickCheck prop_timerConst+    quickCheck prop_timerTicks

@@ -103,14 +103,17 @@ genClockChannelWeighted :: Gen Int genClockChannelWeighted = frequency [(1, pure 1), (1, pure 2), (50, pure 3)] -genClock :: Int -> Gen Clock-genClock n = case n of++genClock :: Gen Clock+genClock = do+  n <- chooseInt (1, 3)+  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]))]+    2 -> elements $ map IntSet.fromList [[1,2], [2,3], [1,3]]     3 -> return (IntSet.fromList [1,2,3])-    _ -> error "Partial function doesnt support n > 3"+    _ -> error "genClock: impossible!"  genClockListWeighted :: Gen [Int] genClockListWeighted = vectorOf 1 genClockChannelWeighted@@ -128,8 +131,7 @@           return (x ::: never)         go m = do           x <- arbitrary-          len <- chooseInt (1, 3)-          cl <- genClock len+          cl <- genClock           xs <- go (m - 1)           let later = Delay cl (\_ -> xs)           return (x ::: later)@@ -147,8 +149,7 @@           return (x ::: never)         go m = do           x <- gen-          len <- chooseInt (1, 3)-          cl <- genClock len+          cl <- genClock           xs <- go (m - 1)           let later = Delay cl (\_ -> xs)           return (x ::: later)@@ -190,7 +191,7 @@   generateHList = do     x <- arbitrary     xs <- generateHList @ts-    return (x %: xs)+    return (x :% xs)  generateSignals :: forall a. HListGen (ToList a) => Gen (HList (Map Sig (ToList a))) generateSignals = generateHList @(ToList a)@@ -202,7 +203,7 @@   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 ]+  shrinkHls (x :% xs) =+    [ x' :% xs | x'  <- shrink x ] +++    [ x :% xs' | xs' <- shrinkHls xs ] +++    [ x' :% xs' | x'  <- shrink x, xs' <- shrinkHls xs ]

@@ -40,7 +40,7 @@  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)+  flatten (h :% t) = prepend h (flatten t)  class Falsify ts where   toFalse :: HList ts -> HList ts@@ -51,24 +51,24 @@  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+  toFalse (Current _ x :% t) = Current (HasTick 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+  (Current (HasTick 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+  (Current (HasTick 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')+     Fst (x' ::: xs')   ys'         -> (Current (HasTick True) (x' :! x) :% toFalse y)  ::: prependAwait (x' :! x) xs' y ys'+     Snd xs' (y' ::: ys')           -> (Current (HasTick False) x :% y')                ::: prependAwait x xs' y' ys'+     Both (x' ::: xs') (y' ::: ys') -> (Current (HasTick True) (x' :! x) :% y')         ::: prependAwait (x' :! x) xs' y' ys')  singletonH :: (Stable t) => Sig t -> Sig (HList '[Value t])-singletonH sig = flatten (sig %: HNil)+singletonH sig = flatten (sig :% HNil)

@@ -13,57 +13,55 @@ {-# 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       +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)+  (:%) :: !x -> !(HList xs) -> HList (x ': xs) -infixr 5 %:-(%:) :: x -> HList xs -> HList (x ': xs)-(%:) = HCons+infixr 5 :%  instance Show (HList '[]) where   show :: HList '[] -> String-  show HNil = "HNil"+  show HNil = "\n"  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+  show (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+first (v :% _) = v  second :: HList (_ ': a ': _) -> a-second (HCons _ (HCons h2 _)) = h2+second (_ :% v :% _) = v  third :: HList (_ ': _ ': a ': _) -> a-third (HCons _ (HCons _ (HCons h3 _))) = h3+third (_ :% _ :% v :% _) = v  fourth :: HList (_ ': _ ': _ ': a ': _) -> a-fourth (HCons _ (HCons _ (HCons _ (HCons h4 _)))) = h4+fourth (_ :% _ :% _ :% v :% _) = v  fifth :: HList (_ ': _ ': _ ': _ ': a ': _) -> a-fifth (HCons _ (HCons _ (HCons _ (HCons _ (HCons h5 _))))) = h5+fifth (_ :% _ :% _ :% _ :% v :% _) = v  sixth :: HList (_ ': _ ': _ ': _ ': _ ': a ': _) -> a-sixth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h6 _)))))) = h6+sixth (_ :% _ :% _ :% _ :% _ :% v :% _) = v  seventh :: HList (_ ':_ ': _ ': _ ': _ ': _ ': a ': _) -> a-seventh (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h7 _))))))) = h7+seventh (_ :% _ :% _ :% _ :% _ :% _ :% v :% _) = v  eighth :: HList (_ ': _ ': _ ': _ ': _ ': _ ': _ ': a ': _) -> a-eighth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h8 _)))))))) = h8+eighth (_ :% _ :% _ :% _ :% _ :% _ :% _ :% v :% _) = v  ninth :: HList (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': a ': _) -> a-ninth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h9 _))))))))) = h9+ninth (_ :% _ :% _ :% _ :% _ :% _ :% _ :% _ :% v :% _) = v   lengthH :: HList ts -> Int -> Int lengthH HNil n = n-lengthH (HCons _ as) n = lengthH as (n+1)+lengthH (_ :% as) n = lengthH as (n+1)

@@ -19,6 +19,9 @@     (|>|),     (|>=|),     (|==|),+    tick1,tick2,tick3,tick4,+    sig1,sig2,sig3,sig4,+    prev, prevN   ) where @@ -32,53 +35,52 @@ 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+  TT    :: Pred ts+  FF    :: 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+  U     :: Pred ts -> Pred ts -> Pred ts+  X     :: Pred ts -> Pred ts+  (:=>) :: Pred ts -> Pred ts -> Pred ts+  G     :: Pred ts -> Pred ts+  F     :: Pred ts -> Pred ts+  XN    :: Int -> Pred ts-> Pred ts+  R     :: 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+  Pure  :: t -> Expr ts t+  App   :: Expr ts (t -> r) -> Expr ts t -> Expr ts r+  Val   :: Lookup ts t -> Expr ts t+  Tick  :: 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+  Prev   :: Lookup ts t -> Lookup ts t+  PrevN  :: Int -> Lookup ts t -> Lookup ts t+  Sig1   :: Lookup (Value t ': x) t+  Sig2   :: Lookup (x1 ': Value t ': x2) t+  Sig3   :: Lookup (x1 ': x2 ': Value t ': x3) t+  Sig4   :: Lookup (x1 ': x2 ': x3 ': Value t ': x4) t+  Sig5   :: Lookup (x1 ': x2 ': x3 ': x4 ': Value t ': x5) t+  Sig6   :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': Value t ': x6) t+  Sig7   :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': Value t ': x7) t+  Sig8   :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': x7 ': Value t ': x8) t+  Sig9   :: 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)+  fmap f (App g x)  = App (fmap (f .) g) x+  fmap f (Val lu)   = App (Pure f) (Val lu)+  fmap f (Tick lu)  = App (Pure f) (Tick 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."+    f <*> x = App f x  instance Num t => Num (Expr ts t) where   (+) :: Expr ts t -> Expr ts t -> Expr ts t@@ -96,41 +98,78 @@   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+(|<|) :: Ord t => Expr ts t -> Expr ts t -> Pred ts+x |<| y = Now ((<) <$> x <*> y)+(|<=|) :: Ord t => Expr ts t -> Expr ts t -> Pred ts+x |<=| y = Now ((<=) <$> x <*> y)+(|>|) :: Ord t => Expr ts t -> Expr ts t -> Pred ts+x |>| y = Now ((>) <$> x <*> y)+(|>=|) :: Ord t => Expr ts t -> Expr ts t -> Pred ts+x |>=| y = Now ((>=) <$> x <*> y)+(|==|) :: Ord t => Expr ts t -> Expr ts t -> Pred ts+x |==| y = Now ((==) <$> x <*> y) --- | Checks whether the instances of "previous" is within scope of t "next" operator.+tick1 :: Pred (Value t ': ts)+tick1 = Now (Tick Sig1)++tick2 :: Pred (t1 ': Value t2 ': ts)+tick2 = Now (Tick Sig2)++tick3 :: Pred (t1 ': t2 ': Value t3 ': ts)+tick3 = Now (Tick Sig3)++tick4 :: Pred (t1 ': t2 ': t3 ': Value t4 ': ts)+tick4 = Now (Tick Sig4)+++sig1 :: Expr (Value t ': ts) t+sig1 = Val Sig1++sig2 :: Expr (t1 ': Value t2 ': ts) t2+sig2 = Val Sig2++sig3 :: Expr (t1 ': t2 ': Value t3 ': ts) t3+sig3 = Val Sig3++sig4 :: Expr (t1 ': t2 ': t3 ': Value t4 ': ts) t4+sig4 = Val Sig4++prev :: Expr ts t -> Expr ts t+prev (Pure x)   = Pure x+prev (App f x)  = App (prev f) (prev x)+prev (Val lu)   = Val (Prev lu)+prev (Tick lu)  = Tick (Prev lu)++prevN :: Int -> Expr ts t -> Expr ts t+prevN _ (Pure x)   = Pure x+prevN n (App f x)  = App (prevN n f) (prevN n x)+prevN n (Val lu)   = Val (PrevN n lu)+prevN n (Tick lu)  = Tick (PrevN n lu)++-- | Checks whether the instances of "previous" is within scope of t "X" 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.+-- The scope is incremented for each X 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)+    TT        -> valid scope+    FF        -> 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+    U p1 p2   -> checkPred p1 scope && checkPred p2 scope+    X p       -> checkPred p (scope + 1)+    p1 :=> p2 -> checkPred p1 scope && checkPred p2 scope+    R p1 p2   -> checkPred p1 scope && checkPred p2 scope+    G p       -> checkPred p scope+    F p       -> checkPred p scope+    XN n p    -> checkPred p (scope + n)   where     valid s = s >= 0 @@ -138,111 +177,111 @@ 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+    Pure _      -> scope+    App fun arg -> min (checkExpr fun scope) (checkExpr arg scope)+    Val lu      -> checkLookup lu scope+    Tick 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+    Prev lu'    -> checkLookup lu' (scope - 1)+    PrevN 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+      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+      U p1 p2   -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc+      X p       -> minSigLengthForPred p (acc + 1)+      p1 :=> p2 -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc+      R p1 p2   -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc+      G p       -> minSigLengthForPred p acc+      F p       -> minSigLengthForPred p acc+      XN n p    -> minSigLengthForPred p (acc + n)+      _         -> acc -nthPrevious :: Int -> Value t -> Maybe' (Value t)-nthPrevious n curr@(Current b history)+nthPrev :: Int -> Value t -> Maybe' (Value t)+nthPrev n curr@(Current b history)   | n <= 0    = Just' curr   | otherwise =       case history of-        _ :! xs -> nthPrevious (n - 1) (Current b xs)+        _ :! xs -> nthPrev (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+evalTick :: Lookup ts t -> HList ts -> Bool+evalTick lu hls = case lu of+  Prev _    -> errorTickPast+  PrevN _ _ -> errorTickPast+  Sig1      -> extract $ first hls+  Sig2      -> extract $ second hls+  Sig3      -> extract $ third hls+  Sig4      -> extract $ fourth hls+  Sig5      -> extract $ fifth hls+  Sig6      -> extract $ sixth hls+  Sig7      -> extract $ seventh hls+  Sig8      -> extract $ eighth hls+  Sig9      -> extract $ ninth hls   where-    errorTickedPast                   = error "Cannot check if signal has ticked in the past."-    extract (Current (HasTicked b) _) = b+    errorTickPast                   = error "Cannot check if signal has ticked in the past."+    extract (Current (HasTick 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  =+evalExpr (App f x) hls = (($) <$> evalExpr f hls) <*> evalExpr x hls+evalExpr (Val 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)+evalExpr (Tick lu) hls = pure (evalTick lu hls)  evalLookup :: Lookup ts t -> HList ts -> Maybe' (Value t) evalLookup lu hls = case lu of-  Previous lu' ->+  Prev 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+  PrevN n lu'  -> case evalLookup lu' hls of+    Just' v  -> nthPrev 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)+  Sig1 -> Just' (first hls)+  Sig2 -> Just' (second hls)+  Sig3 -> Just' (third hls)+  Sig4 -> Just' (fourth hls)+  Sig5 -> Just' (fifth hls)+  Sig6 -> Just' (sixth hls)+  Sig7 -> Just' (seventh hls)+  Sig8 -> Just' (eighth hls)+  Sig9 -> 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+            TT -> True+            FF -> 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+            Not phi     -> not (eval phi sig)+            And phi psi -> eval phi sig && eval psi sig+            Or phi psi  -> eval phi sig || eval psi sig+            U phi psi   -> eval psi sig || eval phi sig+            X _         -> True+            phi :=> psi -> not (eval phi sig && not (eval psi sig))+            G phi       -> eval phi sig+            F phi       -> eval phi sig +            R _ _       -> True +            XN _ _      -> True         where           eval = evaluateSingle timestepsLeft @@ -251,27 +290,27 @@   if IntSet.null cl     then evaluateSingle timestepsLeft formulae sig     else timestepsLeft <= 0 || case formulae of-            Tautology       -> True-            Contradiction   -> False-            Now expr        ->+            TT   -> True+            FF   -> 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 phi     -> not (eval phi sig)+            And phi psi -> eval phi sig && eval psi sig+            Or phi psi  -> eval phi sig || eval psi sig+            U phi psi   -> eval psi sig+                              || (eval phi sig && evaluateX (phi `U` psi) advance)+            X phi       -> evaluateX phi advance+            phi :=> psi -> not (eval phi sig && not (eval psi sig))+            G phi       -> eval phi sig && evaluateX (G phi) advance+            F phi       -> (eval phi sig || evaluateX (F 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+            R phi psi   -> (eval psi sig && eval phi sig)+                                || (eval psi sig && evaluateX (phi `U` psi) advance)+            XN n phi    -> if n <= 0 then eval phi sig else evaluateX (XN (n - 1) phi) sig       where-        evaluateNext = evaluate' (timestepsLeft - 1)+        evaluateX = evaluate' (timestepsLeft - 1)         eval = evaluate' timestepsLeft         advance = f (InputValue (IntSet.findMin cl) ()) @@ -288,7 +327,7 @@       scopeOk   = checkScope p   in      if not scopeOk-      then error "Previous must be in scope of next" +      then error "Prev must be in scope of X"      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

@@ -6,16 +6,20 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ScopedTypeVariables, UndecidableInstances #-} -module PropRatt.Value (Value(..),pureVal,current, HasTicked(..)) where+module PropRatt.Value (Value(..),pureVal,current, HasTick(..)) where import AsyncRattus.Strict import AsyncRattus.Signal hiding (current) import PropRatt.Utils import AsyncRattus -newtype HasTicked = HasTicked Bool deriving Show+newtype HasTick = HasTick Bool +instance Show HasTick where+  show (HasTick True) = "!"+  show (HasTick False) = "_"+ data Value a where-  Current :: !HasTicked -> !(List a) -> Value a+  Current :: !HasTick -> !(List a) -> Value a  instance Stable (Value a) where  instance Num a => Num (Value a) where@@ -29,8 +33,7 @@  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+  show (Current t (h :! _)) = show t ++ show h  instance Show a => Show (Sig [Value a]) where   show sig = "Sig [Value a]: " ++ show (toListOfLength 100 sig) ++ "..."@@ -42,7 +45,7 @@   v1 == v2 = current v1 == current v2  pureVal :: a -> Value a-pureVal x = Current (HasTicked False) (x :! Nil)+pureVal x = Current (HasTick False) (x :! Nil)  current :: Value a -> a current (Current _ (h :! _)) = h