{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Test.Control.State.Transition.Trace.Generator.QuickCheck (
  HasTrace (BaseEnv, envGen, sigGen, shrinkSignal, interpretSTS),
  traceFrom,
  traceFromInitState,
  trace,
  shrinkTrace,

  -- * Trace generator properties
  forAllTrace,
  forAllTraceFromInitState,
  onlyValidSignalsAreGenerated,
  onlyValidSignalsAreGeneratedFromInitState,

  -- * Trace classification
  traceLengthsAreClassified,
  classifyTraceLength,
  classifySize,

  -- * Internal
  mkIntervals,
) where

import Control.State.Transition (Environment, IRC (IRC), STS, Signal, State, TRC (TRC))
import qualified Control.State.Transition.Extended as STS
import Data.Functor.Identity (Identity (..))
import Data.Kind (Type)
import Data.List.NonEmpty (NonEmpty)
import Data.Maybe (fromMaybe)
import Data.Word (Word64)
import GHC.Stack
import Test.Control.State.Transition.Trace (Trace)
import qualified Test.Control.State.Transition.Trace as Trace
import qualified Test.QuickCheck as QuickCheck

-- | State transition systems for which traces can be generated, given a trace
-- generation environment.
--
-- The trace generation environment allows to pass relevant data to the trace
-- generation algorithm.
class STS sts => HasTrace sts traceGenEnv where
  type BaseEnv sts :: Type
  type BaseEnv s = ()

  -- | Interpret the action from the base monad into a pure value, given some
  -- initial environment. This obviously places some contraints on the nature of
  -- the base monad for a trace to be completed.
  interpretSTS :: forall a. HasCallStack => (BaseEnv sts -> STS.BaseM sts a -> a)
  default interpretSTS :: STS.BaseM sts ~ Identity => forall a. BaseEnv sts -> STS.BaseM sts a -> a
  interpretSTS BaseEnv sts
_ (Identity a
x) = a
x

  envGen :: HasCallStack => traceGenEnv -> QuickCheck.Gen (Environment sts)

  sigGen ::
    HasCallStack =>
    traceGenEnv ->
    Environment sts ->
    State sts ->
    QuickCheck.Gen (Signal sts)

  shrinkSignal :: HasCallStack => Signal sts -> [Signal sts]

-- | Generate a random trace starting in the given environment and initial state.
traceFrom ::
  forall sts traceGenEnv.
  HasTrace sts traceGenEnv =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  Environment sts ->
  State sts ->
  QuickCheck.Gen (Trace sts)
traceFrom :: forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Environment sts
-> State sts
-> Gen (Trace sts)
traceFrom BaseEnv sts
traceEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Environment sts
env State sts
st0 = do
  Word64
chosenTraceLength <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
QuickCheck.choose (Word64
0, Word64
maxTraceLength)
  Environment sts
-> State sts -> [(State sts, Signal sts)] -> Trace sts
forall s.
Environment s -> State s -> [(State s, Signal s)] -> Trace s
Trace.mkTrace Environment sts
env State sts
st0 ([(State sts, Signal sts)] -> Trace sts)
-> Gen [(State sts, Signal sts)] -> Gen (Trace sts)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop Word64
chosenTraceLength State sts
st0 []
  where
    loop ::
      Word64 ->
      State sts ->
      [(State sts, Signal sts)] ->
      QuickCheck.Gen [(State sts, Signal sts)]
    loop :: Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop Word64
0 State sts
_ ![(State sts, Signal sts)]
acc = [(State sts, Signal sts)] -> Gen [(State sts, Signal sts)]
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(State sts, Signal sts)]
acc
    loop Word64
d !State sts
sti ![(State sts, Signal sts)]
stSigs = do
      Signal sts
sig <- forall sts traceGenEnv.
(HasTrace sts traceGenEnv, HasCallStack) =>
traceGenEnv -> Environment sts -> State sts -> Gen (Signal sts)
sigGen @sts @traceGenEnv traceGenEnv
traceGenEnv Environment sts
env State sts
sti
      case forall sts traceGenEnv a.
(HasTrace sts traceGenEnv, HasCallStack) =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
traceEnv (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
Trace.applySTSTest @sts ((Environment sts, State sts, Signal sts) -> TRC sts
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment sts
env, State sts
sti, Signal sts
sig))) of
        Left NonEmpty (PredicateFailure sts)
_predicateFailures ->
          Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop (Word64
d Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) State sts
sti [(State sts, Signal sts)]
stSigs
        Right State sts
sti' ->
          Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop (Word64
d Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) State sts
sti' ((State sts
sti', Signal sts
sig) (State sts, Signal sts)
-> [(State sts, Signal sts)] -> [(State sts, Signal sts)]
forall a. a -> [a] -> [a]
: [(State sts, Signal sts)]
stSigs)

-- | Generate a random trace.
trace ::
  forall sts traceGenEnv.
  ( HasTrace sts traceGenEnv
  , Show (Environment sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  QuickCheck.Gen (Trace sts)
trace :: forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts)) =>
BaseEnv sts -> Word64 -> traceGenEnv -> Gen (Trace sts)
trace BaseEnv sts
traceEnv Word64
maxTraceLength traceGenEnv
traceGenEnv =
  BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState BaseEnv sts
traceEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
forall a. Maybe a
Nothing

-- | Generate a random trace given a generator for initial state.
--
-- Takes an optional generator for initial state, or defaults to 'applySTS'
-- if no initial state is required by the STS.
traceFromInitState ::
  forall sts traceGenEnv.
  ( HasTrace sts traceGenEnv
  , Show (Environment sts)
  , HasCallStack
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  -- | Optional generator of STS initial state
  Maybe (IRC sts -> QuickCheck.Gen (Either (NonEmpty (STS.PredicateFailure sts)) (State sts))) ->
  QuickCheck.Gen (Trace sts)
traceFromInitState :: forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0 = do
  Environment sts
env <- forall sts traceGenEnv.
(HasTrace sts traceGenEnv, HasCallStack) =>
traceGenEnv -> Gen (Environment sts)
envGen @sts @traceGenEnv traceGenEnv
traceGenEnv
  Either (NonEmpty (PredicateFailure sts)) (State sts)
res <-
    (IRC sts
 -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> IRC sts
-> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts))
forall a. a -> Maybe a -> a
fromMaybe
      ( Either (NonEmpty (PredicateFailure sts)) (State sts)
-> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          (Either (NonEmpty (PredicateFailure sts)) (State sts)
 -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (IRC sts
    -> Either (NonEmpty (PredicateFailure sts)) (State sts))
-> IRC sts
-> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sts traceGenEnv a.
(HasTrace sts traceGenEnv, HasCallStack) =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
baseEnv
          (BaseM sts (Either (NonEmpty (PredicateFailure sts)) (State sts))
 -> Either (NonEmpty (PredicateFailure sts)) (State sts))
-> (IRC sts
    -> BaseM
         sts (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> IRC sts
-> Either (NonEmpty (PredicateFailure sts)) (State sts)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RuleContext 'Initial sts
-> BaseM sts (Either (NonEmpty (PredicateFailure sts)) (State sts))
IRC sts
-> BaseM sts (Either (NonEmpty (PredicateFailure sts)) (State sts))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
Trace.applySTSTest
      )
      Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0
      (IRC sts
 -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> IRC sts
-> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts))
forall a b. (a -> b) -> a -> b
$ Environment sts -> IRC sts
forall sts. Environment sts -> IRC sts
IRC Environment sts
env

  case Either (NonEmpty (PredicateFailure sts)) (State sts)
res of
    Left NonEmpty (PredicateFailure sts)
pf ->
      [Char] -> Gen (Trace sts)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Gen (Trace sts)) -> [Char] -> Gen (Trace sts)
forall a b. (a -> b) -> a -> b
$
        [Char]
"Failed to apply the initial rule to the generated environment.\n"
          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"Generated environment: "
          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Environment sts -> [Char]
forall a. Show a => a -> [Char]
show Environment sts
env
          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"Failure: "
          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ NonEmpty (PredicateFailure sts) -> [Char]
forall a. Show a => a -> [Char]
show NonEmpty (PredicateFailure sts)
pf
    Right State sts
st0 -> BaseEnv sts
-> Word64
-> traceGenEnv
-> Environment sts
-> State sts
-> Gen (Trace sts)
forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Environment sts
-> State sts
-> Gen (Trace sts)
traceFrom BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Environment sts
env State sts
st0

-- | Check a property on the 'sts' traces.
--
-- Takes an optional generator for initial state of the STS.
forAllTraceFromInitState ::
  forall sts traceGenEnv prop.
  ( HasTrace sts traceGenEnv
  , QuickCheck.Testable prop
  , Show (Environment sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  -- | Optional generator of STS initial state
  Maybe (IRC sts -> QuickCheck.Gen (Either (NonEmpty (STS.PredicateFailure sts)) (State sts))) ->
  (Trace sts -> prop) ->
  QuickCheck.Property
forAllTraceFromInitState :: forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0 Trace sts -> prop
prop =
  Gen (Trace sts)
-> (Trace sts -> [Trace sts]) -> (Trace sts -> prop) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QuickCheck.forAllShrinkBlind
    (forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState @sts @traceGenEnv BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0)
    (forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts -> Trace sts -> [Trace sts]
shrinkTrace @sts @traceGenEnv BaseEnv sts
baseEnv)
    Trace sts -> prop
prop

-- | Check a property on the 'sts' traces.
forAllTrace ::
  forall sts traceGenEnv prop.
  ( HasTrace sts traceGenEnv
  , QuickCheck.Testable prop
  , Show (Environment sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  (Trace sts -> prop) ->
  QuickCheck.Property
forAllTrace :: forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64 -> traceGenEnv -> (Trace sts -> prop) -> Property
forAllTrace BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv =
  BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (Trace sts -> prop)
-> Property
forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
forall a. Maybe a
Nothing

-- | Shrink a trace by shrinking the list of signals and reconstructing traces from these
-- shrunk lists of signals.
--
-- When shrinking a trace that is failing some property (often stated in terms of a signal in the trace)
-- then the most recent signal is likely crucial to the failure of the property and must be preserved
-- in the shrunk traces.
shrinkTrace ::
  forall sts traceGenEnv.
  HasTrace sts traceGenEnv =>
  BaseEnv sts ->
  Trace sts ->
  [Trace sts]
shrinkTrace :: forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts -> Trace sts -> [Trace sts]
shrinkTrace BaseEnv sts
baseEnv Trace sts
tr =
  forall sts traceGenEnv a.
(HasTrace sts traceGenEnv, HasCallStack) =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
baseEnv (BaseM sts [Trace sts] -> [Trace sts])
-> BaseM sts [Trace sts] -> [Trace sts]
forall a b. (a -> b) -> a -> b
$
    Environment sts
-> State sts -> [Signal sts] -> BaseM sts (Trace sts)
forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure Environment sts
env State sts
st0 ([Signal sts] -> BaseM sts (Trace sts))
-> [[Signal sts]] -> BaseM sts [Trace sts]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
`traverse` [Signal sts] -> [[Signal sts]]
forall {a}. [a] -> [[a]]
shrinkSignals [Signal sts]
signals
  where
    env :: Environment sts
env = Trace sts -> Environment sts
forall s. Trace s -> Environment s
Trace._traceEnv Trace sts
tr
    st0 :: State sts
st0 = Trace sts -> State sts
forall s. Trace s -> State s
Trace._traceInitState Trace sts
tr
    signals :: [Signal sts]
signals = TraceOrder -> Trace sts -> [Signal sts]
forall s. TraceOrder -> Trace s -> [Signal s]
Trace.traceSignals TraceOrder
Trace.NewestFirst Trace sts
tr

    -- Shrink a list of signals such that we preserve the most recent signal in the shrunk lists.
    -- This shrinker
    --   - recursively omits all but the most recent signal
    --   - builds up lists of signals starting with the most recent signal and
    --     building up to a list excluding the first (oldest) signal
    --   - explicitly shrinks in order from small to larger lists of signals
    --     (i.e. ordered by most to least aggressive shrinking)
    shrinkSignals :: [a] -> [[a]]
shrinkSignals (a
sn : a
_last : []) =
      [[a
sn]]
    shrinkSignals (a
sn : a
sm : [a]
sigs) =
      [[a
sn]] -- a trace with only the most recent signal
        [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ ((a
sn a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> [[a]] -> [[a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> [[a]]
shrinkSignals (a
sm a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
sigs)) -- shrink the tail
        [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [a
sn a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
sigs] -- discard the second most recent signal

    -- shrink to [] if there is one or no signals
    shrinkSignals [a]
_ = []

-- | Property that asserts that only valid signals are generated.
onlyValidSignalsAreGenerated ::
  forall sts traceGenEnv.
  ( HasTrace sts traceGenEnv
  , Show (Environment sts)
  , Show (Signal sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  QuickCheck.Property
onlyValidSignalsAreGenerated :: forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts),
 Show (Signal sts)) =>
BaseEnv sts -> Word64 -> traceGenEnv -> Property
onlyValidSignalsAreGenerated BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv =
  forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts),
 Show (Signal sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Property
onlyValidSignalsAreGeneratedFromInitState @sts BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
forall a. Maybe a
Nothing

-- | Property that asserts that only valid signals are generated.
--
-- Takes an optional generator for initial state of the STS.
onlyValidSignalsAreGeneratedFromInitState ::
  forall sts traceGenEnv.
  ( HasTrace sts traceGenEnv
  , Show (Environment sts)
  , Show (Signal sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length.
  Word64 ->
  traceGenEnv ->
  -- | Optional generator of STS initial state
  Maybe (IRC sts -> QuickCheck.Gen (Either (NonEmpty (STS.PredicateFailure sts)) (State sts))) ->
  QuickCheck.Property
onlyValidSignalsAreGeneratedFromInitState :: forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts),
 Show (Signal sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Property
onlyValidSignalsAreGeneratedFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0 =
  BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (Trace sts -> Property)
-> Property
forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
  (IRC sts
   -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
genSt0 Trace sts -> Property
validSignalsAreGenerated
  where
    validSignalsAreGenerated ::
      Trace sts ->
      QuickCheck.Property
    validSignalsAreGenerated :: Trace sts -> Property
validSignalsAreGenerated Trace sts
someTrace =
      Gen (Signal sts)
-> (Signal sts -> [Signal sts])
-> (Signal sts -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QuickCheck.forAllShrink
        (forall sts traceGenEnv.
(HasTrace sts traceGenEnv, HasCallStack) =>
traceGenEnv -> Environment sts -> State sts -> Gen (Signal sts)
sigGen @sts @traceGenEnv traceGenEnv
traceGenEnv Environment sts
env State sts
lastState)
        (forall sts traceGenEnv.
(HasTrace sts traceGenEnv, HasCallStack) =>
Signal sts -> [Signal sts]
shrinkSignal @sts @traceGenEnv)
        Signal sts -> Property
signalIsValid
      where
        signalIsValid :: Signal sts -> Property
signalIsValid Signal sts
signal =
          case forall sts traceGenEnv a.
(HasTrace sts traceGenEnv, HasCallStack) =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
baseEnv (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
Trace.applySTSTest @sts ((Environment sts, State sts, Signal sts) -> TRC sts
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment sts
env, State sts
lastState, Signal sts
signal))) of
            Left NonEmpty (PredicateFailure sts)
pf -> [Char] -> Bool -> Property
forall prop. Testable prop => [Char] -> prop -> Property
QuickCheck.counterexample ((Signal sts, NonEmpty (PredicateFailure sts)) -> [Char]
forall a. Show a => a -> [Char]
show (Signal sts
signal, NonEmpty (PredicateFailure sts)
pf)) Bool
False
            Right State sts
_ -> Bool -> Property
forall prop. Testable prop => prop -> Property
QuickCheck.property Bool
True
        env :: Environment sts
env = Trace sts -> Environment sts
forall s. Trace s -> Environment s
Trace._traceEnv Trace sts
someTrace
        lastState :: State sts
lastState = Trace sts -> State sts
forall s. Trace s -> State s
Trace.lastState Trace sts
someTrace

--------------------------------------------------------------------------------
-- Trace classification
--------------------------------------------------------------------------------

-- | Property that simply classifies the lengths of the generated traces.
traceLengthsAreClassified ::
  forall sts traceGenEnv.
  ( HasTrace sts traceGenEnv
  , Show (Environment sts)
  ) =>
  BaseEnv sts ->
  -- | Maximum trace length that the signal generator of 's' can generate.
  Word64 ->
  -- | Lengths of the intervals in which the lengths range should be split.
  Word64 ->
  -- | Trace generation environment
  traceGenEnv ->
  QuickCheck.Property
traceLengthsAreClassified :: forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts)) =>
BaseEnv sts -> Word64 -> Word64 -> traceGenEnv -> Property
traceLengthsAreClassified BaseEnv sts
baseEnv Word64
maxTraceLength Word64
intervalSize traceGenEnv
traceGenEnv =
  forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64 -> traceGenEnv -> (Trace sts -> prop) -> Property
forAllTrace @sts
    BaseEnv sts
baseEnv
    Word64
maxTraceLength
    traceGenEnv
traceGenEnv
    (Word64 -> Word64 -> Trace sts -> Property
forall s. Word64 -> Word64 -> Trace s -> Property
classifyTraceLength Word64
maxTraceLength Word64
intervalSize)

-- | Classify the trace length as either:
--
-- - being empty
-- - being a singleton
-- - having the given maximum size
-- - belonging to one of the intervals between 2 and the maximum size - 1. The
--   number of intervals are determined by the @step@ parameter.
classifyTraceLength ::
  -- | Maximum size of the traces
  Word64 ->
  -- | Steps used to divide the interval
  Word64 ->
  Trace s ->
  QuickCheck.Property
classifyTraceLength :: forall s. Word64 -> Word64 -> Trace s -> Property
classifyTraceLength Word64
maxTraceLength Word64
step Trace s
tr =
  [Char]
-> Trace s -> (Trace s -> Word64) -> Word64 -> Word64 -> Property
forall n a.
(Show n, Integral n) =>
[Char] -> a -> (a -> n) -> n -> n -> Property
classifySize [Char]
"trace length:" Trace s
tr (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> (Trace s -> Int) -> Trace s -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace s -> Int
forall s. Trace s -> Int
Trace.traceLength) Word64
maxTraceLength Word64
step

-- | Classify the value size as either:
--
-- - being empty
-- - being a singleton
-- - having the given maximum size
-- - belonging to one of the intervals between 2 and the maximum size - 1. The
--   number of intervals are determined by the @step@ parameter.
classifySize ::
  (Show n, Integral n) =>
  -- | Prefix to be added to the label intervals
  String ->
  -- | Value to classify
  a ->
  -- | Size function
  (a -> n) ->
  -- | Maximum value size
  n ->
  -- | Steps used to divide the size interval
  n ->
  QuickCheck.Property
classifySize :: forall n a.
(Show n, Integral n) =>
[Char] -> a -> (a -> n) -> n -> n -> Property
classifySize [Char]
prefixLabel a
value a -> n
sizeF n
upBound n
step =
  Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (a -> n
sizeF a
value n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
0) ([Char] -> [Char]
mkLabel [Char]
"empty") (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (a -> n
sizeF a
value n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
1) ([Char] -> [Char]
mkLabel [Char]
"singleton") (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (a -> n
sizeF a
value n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
upBound) [Char]
upBoundLabel (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        ((n, n) -> Property -> Property)
-> Property -> [(n, n)] -> Property
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (n, n) -> Property -> Property
classifySizeInterval (Bool -> Property
forall prop. Testable prop => prop -> Property
QuickCheck.property Bool
True) (n -> n -> n -> [(n, n)]
forall n. Integral n => n -> n -> n -> [(n, n)]
mkIntervals n
2 (n
upBound n -> n -> n
forall a. Num a => a -> a -> a
- n
1) n
step)
  where
    upBoundLabel :: [Char]
upBoundLabel = [Char] -> [Char]
mkLabel ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ n -> [Char]
forall a. Show a => a -> [Char]
show n
upBound
    mkLabel :: [Char] -> [Char]
mkLabel = (([Char]
prefixLabel [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)
    classifySizeInterval :: (n, n) -> Property -> Property
classifySizeInterval (n
low, n
high) Property
prop =
      Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (n
low n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<= a -> n
sizeF a
value Bool -> Bool -> Bool
&& a -> n
sizeF a
value n -> n -> Bool
forall a. Ord a => a -> a -> Bool
< n
high) [Char]
desc Property
prop
      where
        desc :: [Char]
desc = [Char]
"[" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ n -> [Char]
forall a. Show a => a -> [Char]
show n
low [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ n -> [Char]
forall a. Show a => a -> [Char]
show n
high [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

-- | Given a lower bound @low@,  an upper bound @high@ and a step size @step@
-- (both of which must be positive), divide the interval @[0, ub]@ into
-- sub-intervals of @step@ size.
--
-- If any of these values is negative the empty list will be returned.
--
-- Examples:
--
-- >>> mkIntervals 0 0 0 :: [(Int, Int)]
-- []
--
-- >>> mkIntervals 0 10 2 :: [(Int, Int)]
-- [(0,2),(2,4),(4,6),(6,8),(8,10)]
--
-- >>> mkIntervals 1 10 2 :: [(Int, Int)]
-- [(1,3),(3,5),(5,7),(7,9),(9,10)]
--
--
-- >>> mkIntervals 3 10 3 :: [(Int, Int)]
-- [(3,6),(6,9),(9,10)]
--
-- >>> mkIntervals 5 2 3 :: [(Int, Int)]
-- []
--
-- >>> mkIntervals (-1) 10 3 :: [(Int, Int)]
-- []
--
-- >>> mkIntervals 1 (-10) 3 :: [(Int, Int)]
-- []
--
-- >>> mkIntervals 1 1000 (-100) :: [(Int, Int)]
-- []
mkIntervals ::
  Integral n =>
  -- | Interval lower bound
  n ->
  -- | Interval upper bound
  n ->
  -- | Step size, used to divide the interval in sub-intervals of the same
  -- length.
  n ->
  [(n, n)]
mkIntervals :: forall n. Integral n => n -> n -> n -> [(n, n)]
mkIntervals n
low n
high n
step
  | n
0 n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<= n
low Bool -> Bool -> Bool
&& n
low n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<= n
high Bool -> Bool -> Bool
&& n
0 n -> n -> Bool
forall a. Ord a => a -> a -> Bool
< n
step =
      [(n
low n -> n -> n
forall a. Num a => a -> a -> a
+ n
i n -> n -> n
forall a. Num a => a -> a -> a
* n
step, n
high n -> n -> n
forall a. Ord a => a -> a -> a
`min` (n
low n -> n -> n
forall a. Num a => a -> a -> a
+ (n
i n -> n -> n
forall a. Num a => a -> a -> a
+ n
1) n -> n -> n
forall a. Num a => a -> a -> a
* n
step)) | n
i <- [n
0 .. n
n n -> n -> n
forall a. Num a => a -> a -> a
- n
1]]
  | Bool
otherwise = []
  where
    highNorm :: n
highNorm = n
high n -> n -> n
forall a. Num a => a -> a -> a
- n
low
    n :: n
n = n
highNorm n -> n -> n
forall a. Integral a => a -> a -> a
`div` n
step n -> n -> n
forall a. Num a => a -> a -> a
+ n
1 n -> n -> n
forall a. Ord a => a -> a -> a
`min` (n
highNorm n -> n -> n
forall a. Integral a => a -> a -> a
`mod` n
step)