{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Generators for transition systems.
--
--   How should these work?
--   - We start with some initial environment.
--   - We start with some initial base state.
--   - We generate a stream of signals. These might be influenced by some running state
--   - We run each signal through
module Test.Control.State.Transition.Generator (
  HasTrace,
  SignalGenerator,
  BaseEnv,
  interpretSTS,
  envGen,
  sigGen,
  traceSigGen,
  genTrace,
  trace,
  traceWithProfile,
  traceOfLength,
  traceOfLengthWithInitState,
  traceSuchThat,
  ofLengthAtLeast,
  suchThatLastState,
  nonTrivialTrace,
  HasSizeInfo,
  isTrivial,
  sampleMaxTraceSize,
  randomTrace,
  randomTraceOfSize,
  TraceLength (Maximum, Desired),
  TraceProfile (TraceProfile, proportionOfValidSignals, failures),
  proportionOfInvalidSignals,

  -- * Invalid trace generation
  invalidTrace,

  -- * Trace classification
  classifyTraceLength,
  classifySize,
  mkIntervals,
  ratio,

  -- * Trace properties
  traceLengthsAreClassified,
  onlyValidSignalsAreGenerated,
  onlyValidSignalsAreGeneratedForTrace,
  invalidSignalsAreGenerated,

  -- * Helpers
  coverFailures,
) where

import Control.Arrow (second)
import Control.Monad (forM, void)
import Control.Monad.Trans.Maybe (MaybeT)
import Control.State.Transition.Extended (
  BaseM,
  Environment,
  IRC (IRC),
  PredicateFailure,
  STS,
  Signal,
  State,
  TRC (TRC),
 )
import Data.Data (Constr, Data, toConstr)
import Data.Either (isLeft)
import Data.Foldable (traverse_)
import Data.Functor.Identity (Identity (..))
import Data.Kind (Type)
import Data.List.NonEmpty (NonEmpty)
import Data.Maybe (fromMaybe)
import Data.String (fromString)
import Data.Word (Word64)
import GHC.Stack (HasCallStack)
import Hedgehog (
  Gen,
  MonadTest,
  Property,
  PropertyT,
  classify,
  cover,
  evalEither,
  footnoteShow,
  forAll,
  property,
  success,
 )
import qualified Hedgehog.Gen as Gen
import Hedgehog.Internal.Gen (integral_, runDiscardEffectT)
import Hedgehog.Internal.Property (CoverPercentage)
import Hedgehog.Internal.Tree (NodeT (NodeT), TreeT, nodeChildren, treeValue)
import Hedgehog.Range (Size (Size))
import qualified Hedgehog.Range as Range
import qualified Test.Control.State.Transition.Invalid.Trace as Invalid
import Test.Control.State.Transition.Trace (
  Trace,
  TraceOrder (OldestFirst),
  applySTSTest,
  closure,
  extractValues,
  lastState,
  mkTrace,
  traceLength,
  traceSignals,
  _traceEnv,
 )
import Test.Hedgehog.Extra.Manual (Manual)
import qualified Test.Hedgehog.Extra.Manual as Manual

class STS s => HasTrace s where
  type BaseEnv s :: 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. (BaseEnv s -> BaseM s a -> a)
  default interpretSTS :: BaseM s ~ Identity => forall a. BaseEnv s -> BaseM s a -> a
  interpretSTS BaseEnv s
_ (Identity a
x) = a
x

  -- | Generate an initial environment that is based on the given trace length.
  envGen ::
    -- | Trace length that will be used by 'trace' or 'traceOfLength'.
    Word64 ->
    Gen (Environment s)

  -- | Generate a (valid) signal given an environment and a pre-state.
  sigGen ::
    SignalGenerator s

  trace ::
    BaseEnv s ->
    -- | Maximum length of the generated traces. The actual length will be
    -- between 0 and this maximum.
    Word64 ->
    Gen (Trace s)
  trace BaseEnv s
baseEnv Word64
n = forall s.
HasTrace s =>
BaseEnv s -> Word64 -> TraceProfile s -> Gen (Trace s)
traceWithProfile @s BaseEnv s
baseEnv Word64
n TraceProfile s
forall s. TraceProfile s
allValid

  traceWithProfile ::
    BaseEnv s ->
    Word64 ->
    TraceProfile s ->
    Gen (Trace s)
  traceWithProfile BaseEnv s
baseEnv Word64
n TraceProfile s
p = BaseEnv s
-> TraceLength
-> TraceProfile s
-> SignalGenerator s
-> Gen (Trace s)
forall s.
HasTrace s =>
BaseEnv s
-> TraceLength
-> TraceProfile s
-> SignalGenerator s
-> Gen (Trace s)
traceSigGenWithProfile BaseEnv s
baseEnv (Word64 -> TraceLength
Maximum Word64
n) TraceProfile s
p (forall s. HasTrace s => SignalGenerator s
sigGen @s)

  traceOfLength ::
    BaseEnv s ->
    -- | Desired length of the generated trace. If the signal generator can generate invalid signals
    -- then the resulting trace might not have the given length.
    Word64 ->
    Gen (Trace s)
  traceOfLength BaseEnv s
baseEnv Word64
n = BaseEnv s
-> TraceLength
-> TraceProfile s
-> SignalGenerator s
-> Gen (Trace s)
forall s.
HasTrace s =>
BaseEnv s
-> TraceLength
-> TraceProfile s
-> SignalGenerator s
-> Gen (Trace s)
traceSigGenWithProfile BaseEnv s
baseEnv (Word64 -> TraceLength
Desired Word64
n) TraceProfile s
forall s. TraceProfile s
allValid (forall s. HasTrace s => SignalGenerator s
sigGen @s)

  traceOfLengthWithInitState ::
    BaseEnv s ->
    -- | Desired length of the generated trace. If the signal generator can generate invalid signals
    -- then the resulting trace might not have the given length.
    Word64 ->
    -- | A generator for Initial State, given the STS environment
    (Environment s -> Gen (State s)) ->
    Gen (Trace s)
  traceOfLengthWithInitState BaseEnv s
baseEnv Word64
n Environment s -> Gen (State s)
mkSt0 =
    BaseEnv s
-> TraceLength
-> TraceProfile s
-> SignalGenerator s
-> (Environment s -> Gen (State s))
-> Gen (Trace s)
forall s.
HasTrace s =>
BaseEnv s
-> TraceLength
-> TraceProfile s
-> SignalGenerator s
-> (Environment s -> Gen (State s))
-> Gen (Trace s)
traceSigGenWithProfileAndInitState BaseEnv s
baseEnv (Word64 -> TraceLength
Desired Word64
n) TraceProfile s
forall s. TraceProfile s
allValid (forall s. HasTrace s => SignalGenerator s
sigGen @s) Environment s -> Gen (State s)
mkSt0

type SignalGenerator s = Environment s -> State s -> Gen (Signal s)

data TraceLength = Maximum Word64 | Desired Word64

data TraceProfile s = TraceProfile
  { forall s. TraceProfile s -> Int
proportionOfValidSignals :: !Int
  -- ^ Proportion of valid signals to generate.
  , forall s. TraceProfile s -> [(Int, SignalGenerator s)]
failures :: ![(Int, SignalGenerator s)]
  -- ^ List of failure conditions to try generate when generating an invalid signal, and the
  -- proportion of each failure.
  }

proportionOfInvalidSignals :: TraceProfile s -> Int
proportionOfInvalidSignals :: forall s. TraceProfile s -> Int
proportionOfInvalidSignals = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int)
-> (TraceProfile s -> [Int]) -> TraceProfile s -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Environment s -> State s -> Gen (Signal s)) -> Int)
-> [(Int, Environment s -> State s -> Gen (Signal s))] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Environment s -> State s -> Gen (Signal s)) -> Int
forall a b. (a, b) -> a
fst ([(Int, Environment s -> State s -> Gen (Signal s))] -> [Int])
-> (TraceProfile s
    -> [(Int, Environment s -> State s -> Gen (Signal s))])
-> TraceProfile s
-> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TraceProfile s
-> [(Int, Environment s -> State s -> Gen (Signal s))]
forall s. TraceProfile s -> [(Int, SignalGenerator s)]
failures

allValid :: TraceProfile s
allValid :: forall s. TraceProfile s
allValid =
  TraceProfile
    { proportionOfValidSignals :: Int
proportionOfValidSignals = Int
1
    , failures :: [(Int, SignalGenerator s)]
failures = []
    }

-- | Generate a signal by combining the generators using @hedgehog@'s
-- 'frequency' combinator.
generateSignalWithFailureProportions ::
  -- | Failure proportions. See 'failures' in 'TraceProfile'.
  [(Int, SignalGenerator s)] ->
  SignalGenerator s
generateSignalWithFailureProportions :: forall s. [(Int, SignalGenerator s)] -> SignalGenerator s
generateSignalWithFailureProportions [(Int, SignalGenerator s)]
proportions Environment s
env State s
st =
  [(Int, GenT Identity (Signal s))] -> GenT Identity (Signal s)
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency ([(Int, GenT Identity (Signal s))] -> GenT Identity (Signal s))
-> [(Int, GenT Identity (Signal s))] -> GenT Identity (Signal s)
forall a b. (a -> b) -> a -> b
$ (SignalGenerator s -> GenT Identity (Signal s))
-> (Int, SignalGenerator s) -> (Int, GenT Identity (Signal s))
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second SignalGenerator s -> GenT Identity (Signal s)
aSigGenWithFailure ((Int, SignalGenerator s) -> (Int, GenT Identity (Signal s)))
-> [(Int, SignalGenerator s)] -> [(Int, GenT Identity (Signal s))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, SignalGenerator s)]
proportions
  where
    aSigGenWithFailure :: SignalGenerator s -> GenT Identity (Signal s)
aSigGenWithFailure SignalGenerator s
invalidSigGen = SignalGenerator s
invalidSigGen Environment s
env State s
st

-- | Extract the maximum or desired integer value of the trace length.
traceLengthValue :: TraceLength -> Word64
traceLengthValue :: TraceLength -> Word64
traceLengthValue (Maximum Word64
n) = Word64
n
traceLengthValue (Desired Word64
n) = Word64
n

traceSigGen ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  TraceLength ->
  SignalGenerator s ->
  Gen (Trace s)
traceSigGen :: forall s.
HasTrace s =>
BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen BaseEnv s
baseEnv TraceLength
aTraceLength = BaseEnv s
-> TraceLength
-> TraceProfile s
-> (Environment s -> State s -> GenT Identity (Signal s))
-> GenT Identity (Trace s)
forall s.
HasTrace s =>
BaseEnv s
-> TraceLength
-> TraceProfile s
-> SignalGenerator s
-> Gen (Trace s)
traceSigGenWithProfile BaseEnv s
baseEnv TraceLength
aTraceLength TraceProfile s
forall s. TraceProfile s
allValid

traceSigGenWithProfile ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  TraceLength ->
  TraceProfile s ->
  SignalGenerator s ->
  Gen (Trace s)
traceSigGenWithProfile :: forall s.
HasTrace s =>
BaseEnv s
-> TraceLength
-> TraceProfile s
-> SignalGenerator s
-> Gen (Trace s)
traceSigGenWithProfile BaseEnv s
baseEnv TraceLength
aTraceLength TraceProfile s
profile SignalGenerator s
gen = do
  Environment s
env <- forall s. HasTrace s => Word64 -> Gen (Environment s)
envGen @s (TraceLength -> Word64
traceLengthValue TraceLength
aTraceLength)
  case forall s a. HasTrace s => BaseEnv s -> BaseM s a -> a
interpretSTS @s BaseEnv s
baseEnv (BaseM s (Either (NonEmpty (PredicateFailure s)) (State s))
 -> Either (NonEmpty (PredicateFailure s)) (State s))
-> BaseM s (Either (NonEmpty (PredicateFailure s)) (State s))
-> Either (NonEmpty (PredicateFailure s)) (State s)
forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest @s (Environment s -> IRC s
forall sts. Environment sts -> IRC sts
IRC Environment s
env) of
    -- Hedgehog will give up if the generators fail to produce any valid
    -- initial state, hence we don't have a risk of entering an infinite
    -- recursion.
    Left NonEmpty (PredicateFailure s)
_pf -> BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
forall s.
HasTrace s =>
BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen BaseEnv s
baseEnv TraceLength
aTraceLength SignalGenerator s
gen
    -- Applying an initial rule with an environment and state will simply
    -- validate that state, so we do not care which state 'applySTS' returns.
    Right State s
st -> BaseEnv s
-> TraceLength
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
forall s.
HasTrace s =>
BaseEnv s
-> TraceLength
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTraceOfMaxOrDesiredLength BaseEnv s
baseEnv TraceLength
aTraceLength TraceProfile s
profile Environment s
env State s
st SignalGenerator s
gen

-- | A variation of 'traceSigGenWithProfile' which takes an argument generator
-- for the initial state of the given trace
traceSigGenWithProfileAndInitState ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  TraceLength ->
  TraceProfile s ->
  SignalGenerator s ->
  (Environment s -> Gen (State s)) ->
  Gen (Trace s)
traceSigGenWithProfileAndInitState :: forall s.
HasTrace s =>
BaseEnv s
-> TraceLength
-> TraceProfile s
-> SignalGenerator s
-> (Environment s -> Gen (State s))
-> Gen (Trace s)
traceSigGenWithProfileAndInitState BaseEnv s
baseEnv TraceLength
aTraceLength TraceProfile s
profile SignalGenerator s
gen Environment s -> Gen (State s)
mkSt0 = do
  Environment s
env <- forall s. HasTrace s => Word64 -> Gen (Environment s)
envGen @s (TraceLength -> Word64
traceLengthValue TraceLength
aTraceLength)
  State s
st0 <- Environment s -> Gen (State s)
mkSt0 Environment s
env

  BaseEnv s
-> TraceLength
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
forall s.
HasTrace s =>
BaseEnv s
-> TraceLength
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTraceOfMaxOrDesiredLength BaseEnv s
baseEnv TraceLength
aTraceLength TraceProfile s
profile Environment s
env State s
st0 SignalGenerator s
gen

genTraceOfMaxOrDesiredLength ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  TraceLength ->
  TraceProfile s ->
  Environment s ->
  State s ->
  SignalGenerator s ->
  Gen (Trace s)
genTraceOfMaxOrDesiredLength :: forall s.
HasTrace s =>
BaseEnv s
-> TraceLength
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTraceOfMaxOrDesiredLength BaseEnv s
baseEnv TraceLength
aTraceLength TraceProfile s
profile Environment s
env State s
st0 SignalGenerator s
gen =
  case TraceLength
aTraceLength of
    Maximum Word64
n -> BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
forall s.
HasTrace s =>
BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTraceWithProfile BaseEnv s
baseEnv Word64
n TraceProfile s
profile Environment s
env State s
st0 SignalGenerator s
gen
    Desired Word64
n -> BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
forall s.
HasTrace s =>
BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTraceOfLength BaseEnv s
baseEnv Word64
n TraceProfile s
profile Environment s
env State s
st0 SignalGenerator s
gen

-- | Return a (valid) trace generator given an initial state, environment, and
-- signal generator.
genTrace ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  -- | Trace upper bound. This will be linearly scaled as a function of the
  -- generator size.
  Word64 ->
  -- | Environment, which remains constant in the system.
  Environment s ->
  -- | Initial state.
  State s ->
  -- | Signal generator. This generator relies on an environment and a state to
  -- generate a signal.
  SignalGenerator s ->
  Gen (Trace s)
genTrace :: forall s.
HasTrace s =>
BaseEnv s
-> Word64
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTrace BaseEnv s
baseEnv Word64
ub = BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> (Environment s -> State s -> GenT Identity (Signal s))
-> GenT Identity (Trace s)
forall s.
HasTrace s =>
BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTraceWithProfile BaseEnv s
baseEnv Word64
ub TraceProfile s
forall s. TraceProfile s
allValid

-- | Return a trace generator given an initial state, environment, and signal generator.
genTraceWithProfile ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  -- | Trace upper bound. This will be linearly scaled as a function of the
  -- generator size.
  Word64 ->
  TraceProfile s ->
  -- | Environment, which remains constant in the system.
  Environment s ->
  -- | Initial state.
  State s ->
  -- | Signal generator. This generator relies on an environment and a state to
  -- generate a signal.
  SignalGenerator s ->
  Gen (Trace s)
genTraceWithProfile :: forall s.
HasTrace s =>
BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTraceWithProfile BaseEnv s
baseEnv Word64
ub TraceProfile s
profile Environment s
env State s
st0 SignalGenerator s
aSigGen =
  do
    -- Generate the initial size of the trace, but don't shrink it (notice the
    -- use of 'integral_') since we will be shrinking the traces manually (so it
    -- doesn't make sense to shrink the trace size).
    --
    -- Note that the length of the resulting trace might be less than the
    -- generated value if invalid signals (according to some current state) are
    -- generated in 'loop'.
    --
    -- A linear range will generate about one third of empty traces, which does
    -- not seem sensible. Furthermore, in most cases it won't generate any trace
    -- of size @ub@. Hence we need to tweak the frequency of the trace lengths.
    Word64
n <-
      [(Int, GenT Identity Word64)] -> GenT Identity Word64
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency
        [ (Int
5, Word64 -> GenT Identity Word64
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
0)
        , (Int
85, Range Word64 -> GenT Identity Word64
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
integral_ (Range Word64 -> GenT Identity Word64)
-> Range Word64 -> GenT Identity Word64
forall a b. (a -> b) -> a -> b
$ Word64 -> Word64 -> Range Word64
forall a. Integral a => a -> a -> Range a
Range.linear Word64
1 Word64
ub)
        , (Int
5, Word64 -> GenT Identity Word64
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
ub)
        ]
    BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
forall s.
HasTrace s =>
BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTraceOfLength BaseEnv s
baseEnv Word64
n TraceProfile s
profile Environment s
env State s
st0 SignalGenerator s
aSigGen

-- | Return a (valid) trace generator that generates traces of the given size. If the signal
-- generator can generate invalid signals, then the size of resulting trace is not guaranteed.
genTraceOfLength ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  -- | Desired trace length.
  Word64 ->
  TraceProfile s ->
  -- | Environment, which remains constant in the system.
  Environment s ->
  -- | Initial state.
  State s ->
  -- | Signal generator. This generator relies on an environment and a state to
  -- generate a signal.
  SignalGenerator s ->
  Gen (Trace s)
genTraceOfLength :: forall s.
HasTrace s =>
BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> Gen (Trace s)
genTraceOfLength BaseEnv s
baseEnv Word64
aTraceLength TraceProfile s
profile Environment s
env State s
st0 SignalGenerator s
aSigGen =
  Manual (TreeT (MaybeT Identity) (Trace s)) -> Gen (Trace s)
forall a. Manual (TreeT (MaybeT Identity) a) -> Gen a
Manual.fromManual (Manual (TreeT (MaybeT Identity) (Trace s)) -> Gen (Trace s))
-> Manual (TreeT (MaybeT Identity) (Trace s)) -> Gen (Trace s)
forall a b. (a -> b) -> a -> b
$ ([(State s, TreeT (MaybeT Identity) (Signal s))]
 -> TreeT (MaybeT Identity) (Trace s))
-> Manual [(State s, TreeT (MaybeT Identity) (Signal s))]
-> Manual (TreeT (MaybeT Identity) (Trace s))
forall a b. (a -> b) -> Manual a -> Manual b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(State s, TreeT (MaybeT Identity) (Signal s))]
-> TreeT (MaybeT Identity) (Trace s)
interleaveSigs (Manual [(State s, TreeT (MaybeT Identity) (Signal s))]
 -> Manual (TreeT (MaybeT Identity) (Trace s)))
-> Manual [(State s, TreeT (MaybeT Identity) (Signal s))]
-> Manual (TreeT (MaybeT Identity) (Trace s))
forall a b. (a -> b) -> a -> b
$ Word64
-> State s
-> [(State s, TreeT (MaybeT Identity) (Signal s))]
-> Manual [(State s, TreeT (MaybeT Identity) (Signal s))]
loop Word64
aTraceLength State s
st0 []
  where
    loop ::
      Word64 ->
      State s ->
      [(State s, TreeT (MaybeT Identity) (Signal s))] ->
      Manual [(State s, TreeT (MaybeT Identity) (Signal s))]
    loop :: Word64
-> State s
-> [(State s, TreeT (MaybeT Identity) (Signal s))]
-> Manual [(State s, TreeT (MaybeT Identity) (Signal s))]
loop Word64
0 State s
_ [(State s, TreeT (MaybeT Identity) (Signal s))]
acc = [(State s, TreeT (MaybeT Identity) (Signal s))]
-> Manual [(State s, TreeT (MaybeT Identity) (Signal s))]
forall a. a -> Manual a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(State s, TreeT (MaybeT Identity) (Signal s))]
acc
    loop !Word64
d State s
sti [(State s, TreeT (MaybeT Identity) (Signal s))]
acc = do
      TreeT (MaybeT Identity) (Signal s)
sigTree :: TreeT (MaybeT Identity) (Signal s) <-
        Gen (Signal s) -> Manual (TreeT (MaybeT Identity) (Signal s))
forall a. Gen a -> Manual (TreeT (MaybeT Identity) a)
Manual.toManual (Gen (Signal s) -> Manual (TreeT (MaybeT Identity) (Signal s)))
-> Gen (Signal s) -> Manual (TreeT (MaybeT Identity) (Signal s))
forall a b. (a -> b) -> a -> b
$
          [(Int, Gen (Signal s))] -> Gen (Signal s)
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency
            [
              ( TraceProfile s -> Int
forall s. TraceProfile s -> Int
proportionOfValidSignals TraceProfile s
profile
              , SignalGenerator s
aSigGen Environment s
env State s
sti
              )
            ,
              ( TraceProfile s -> Int
forall s. TraceProfile s -> Int
proportionOfInvalidSignals TraceProfile s
profile
              , forall s. [(Int, SignalGenerator s)] -> SignalGenerator s
generateSignalWithFailureProportions @s (TraceProfile s -> [(Int, SignalGenerator s)]
forall s. TraceProfile s -> [(Int, SignalGenerator s)]
failures TraceProfile s
profile) Environment s
env State s
sti
              )
            ]
      let
        --  Take the root of the next-state signal tree.
        mSig :: Maybe (Signal s)
mSig = Tree (Maybe (Signal s)) -> Maybe (Signal s)
forall a. Tree a -> a
treeValue (Tree (Maybe (Signal s)) -> Maybe (Signal s))
-> Tree (Maybe (Signal s)) -> Maybe (Signal s)
forall a b. (a -> b) -> a -> b
$ TreeT (MaybeT Identity) (Signal s) -> Tree (Maybe (Signal s))
forall (m :: * -> *) a.
Monad m =>
TreeT (MaybeT m) a -> TreeT m (Maybe a)
runDiscardEffectT TreeT (MaybeT Identity) (Signal s)
sigTree
      case Maybe (Signal s)
mSig of
        Maybe (Signal s)
Nothing ->
          Word64
-> State s
-> [(State s, TreeT (MaybeT Identity) (Signal s))]
-> Manual [(State s, TreeT (MaybeT Identity) (Signal s))]
loop (Word64
d Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) State s
sti [(State s, TreeT (MaybeT Identity) (Signal s))]
acc
        Just Signal s
sig ->
          case forall s a. HasTrace s => BaseEnv s -> BaseM s a -> a
interpretSTS @s BaseEnv s
baseEnv (BaseM s (Either (NonEmpty (PredicateFailure s)) (State s))
 -> Either (NonEmpty (PredicateFailure s)) (State s))
-> BaseM s (Either (NonEmpty (PredicateFailure s)) (State s))
-> Either (NonEmpty (PredicateFailure s)) (State s)
forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest @s ((Environment s, State s, Signal s) -> TRC s
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment s
env, State s
sti, Signal s
sig)) of
            Left NonEmpty (PredicateFailure s)
_err -> Word64
-> State s
-> [(State s, TreeT (MaybeT Identity) (Signal s))]
-> Manual [(State s, TreeT (MaybeT Identity) (Signal s))]
loop (Word64
d Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) State s
sti [(State s, TreeT (MaybeT Identity) (Signal s))]
acc
            Right State s
sti' -> Word64
-> State s
-> [(State s, TreeT (MaybeT Identity) (Signal s))]
-> Manual [(State s, TreeT (MaybeT Identity) (Signal s))]
loop (Word64
d Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) State s
sti' ((State s
sti', TreeT (MaybeT Identity) (Signal s)
sigTree) (State s, TreeT (MaybeT Identity) (Signal s))
-> [(State s, TreeT (MaybeT Identity) (Signal s))]
-> [(State s, TreeT (MaybeT Identity) (Signal s))]
forall a. a -> [a] -> [a]
: [(State s, TreeT (MaybeT Identity) (Signal s))]
acc)

    interleaveSigs ::
      [(State s, TreeT (MaybeT Identity) (Signal s))] ->
      TreeT (MaybeT Identity) (Trace s)
    interleaveSigs :: [(State s, TreeT (MaybeT Identity) (Signal s))]
-> TreeT (MaybeT Identity) (Trace s)
interleaveSigs [(State s, TreeT (MaybeT Identity) (Signal s))]
stateSignalTrees =
      Maybe (NodeT (MaybeT Identity) (Trace s))
-> TreeT (MaybeT Identity) (Trace s)
forall a.
Maybe (NodeT (MaybeT Identity) a) -> TreeT (MaybeT Identity) a
Manual.wrapTreeT (Maybe (NodeT (MaybeT Identity) (Trace s))
 -> TreeT (MaybeT Identity) (Trace s))
-> Maybe (NodeT (MaybeT Identity) (Trace s))
-> TreeT (MaybeT Identity) (Trace s)
forall a b. (a -> b) -> a -> b
$
        NodeT (MaybeT Identity) (Trace s)
-> Maybe (NodeT (MaybeT Identity) (Trace s))
forall a. a -> Maybe a
Just (NodeT (MaybeT Identity) (Trace s)
 -> Maybe (NodeT (MaybeT Identity) (Trace s)))
-> NodeT (MaybeT Identity) (Trace s)
-> Maybe (NodeT (MaybeT Identity) (Trace s))
forall a b. (a -> b) -> a -> b
$
          Trace s
-> [TreeT (MaybeT Identity) (Trace s)]
-> NodeT (MaybeT Identity) (Trace s)
forall (m :: * -> *) a. a -> [TreeT m a] -> NodeT m a
NodeT
            Trace s
rootTrace
            ((TreeT (MaybeT Identity) [Signal s]
 -> TreeT (MaybeT Identity) (Trace s))
-> [TreeT (MaybeT Identity) [Signal s]]
-> [TreeT (MaybeT Identity) (Trace s)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Signal s] -> Trace s)
-> TreeT (MaybeT Identity) [Signal s]
-> TreeT (MaybeT Identity) (Trace s)
forall a b.
(a -> b) -> TreeT (MaybeT Identity) a -> TreeT (MaybeT Identity) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall s a. HasTrace s => BaseEnv s -> BaseM s a -> a
interpretSTS @s BaseEnv s
baseEnv (BaseM s (Trace s) -> Trace s)
-> ([Signal s] -> BaseM s (Trace s)) -> [Signal s] -> Trace s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
closure @s Environment s
env State s
st0)) [TreeT (MaybeT Identity) [Signal s]]
signalShrinksChilren)
      where
        rootStates :: [State s]
        signalTrees :: [TreeT (MaybeT Identity) (Signal s)]
        ([State s]
rootStates, [TreeT (MaybeT Identity) (Signal s)]
signalTrees) = [(State s, TreeT (MaybeT Identity) (Signal s))]
-> ([State s], [TreeT (MaybeT Identity) (Signal s)])
forall a b. [(a, b)] -> ([a], [b])
unzip [(State s, TreeT (MaybeT Identity) (Signal s))]
stateSignalTrees
        rootSignals :: [Signal s]
        rootSignals :: [Signal s]
rootSignals = (TreeT (MaybeT Identity) (Signal s) -> Signal s)
-> [TreeT (MaybeT Identity) (Signal s)] -> [Signal s]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Signal s -> Maybe (Signal s) -> Signal s
forall a. a -> Maybe a -> a
fromMaybe Signal s
forall {a}. a
err (Maybe (Signal s) -> Signal s)
-> (TreeT (MaybeT Identity) (Signal s) -> Maybe (Signal s))
-> TreeT (MaybeT Identity) (Signal s)
-> Signal s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree (Maybe (Signal s)) -> Maybe (Signal s)
forall a. Tree a -> a
treeValue (Tree (Maybe (Signal s)) -> Maybe (Signal s))
-> (TreeT (MaybeT Identity) (Signal s) -> Tree (Maybe (Signal s)))
-> TreeT (MaybeT Identity) (Signal s)
-> Maybe (Signal s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TreeT (MaybeT Identity) (Signal s) -> Tree (Maybe (Signal s))
forall (m :: * -> *) a.
Monad m =>
TreeT (MaybeT m) a -> TreeT m (Maybe a)
runDiscardEffectT) [TreeT (MaybeT Identity) (Signal s)]
signalTrees
        err :: a
err = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"genTraceOfLength: the tree nodes must always contain a signal"
        -- The states ensuing the root signals were calculated at 'loop'
        -- already, so there is no need to apply the STS again.
        rootTrace :: Trace s
        rootTrace :: Trace s
rootTrace = Environment s -> State s -> [(State s, Signal s)] -> Trace s
forall s.
Environment s -> State s -> [(State s, Signal s)] -> Trace s
mkTrace Environment s
env State s
st0 ([State s] -> [Signal s] -> [(State s, Signal s)]
forall a b. [a] -> [b] -> [(a, b)]
zip [State s]
rootStates [Signal s]
rootSignals)
        signalShrinks :: TreeT (MaybeT Identity) [Signal s]
        signalShrinks :: TreeT (MaybeT Identity) [Signal s]
signalShrinks = [TreeT (MaybeT Identity) (Signal s)]
-> TreeT (MaybeT Identity) [Signal s]
forall a.
[TreeT (MaybeT Identity) a] -> TreeT (MaybeT Identity) [a]
Manual.interleave [TreeT (MaybeT Identity) (Signal s)]
signalTrees
        -- The signals at the root of 'signalShrinks' are already included in
        -- the 'rootTrace' so there is no need to include them again in the tree
        -- of traces. Thus we only need to apply 'closure' to the children of
        -- the shrink tree.
        signalShrinksChilren :: [TreeT (MaybeT Identity) [Signal s]]
        signalShrinksChilren :: [TreeT (MaybeT Identity) [Signal s]]
signalShrinksChilren = NodeT (MaybeT Identity) [Signal s]
-> [TreeT (MaybeT Identity) [Signal s]]
forall (m :: * -> *) a. NodeT m a -> [TreeT m a]
nodeChildren (NodeT (MaybeT Identity) [Signal s]
 -> [TreeT (MaybeT Identity) [Signal s]])
-> NodeT (MaybeT Identity) [Signal s]
-> [TreeT (MaybeT Identity) [Signal s]]
forall a b. (a -> b) -> a -> b
$ NodeT (MaybeT Identity) [Signal s]
-> Maybe (NodeT (MaybeT Identity) [Signal s])
-> NodeT (MaybeT Identity) [Signal s]
forall a. a -> Maybe a -> a
fromMaybe NodeT (MaybeT Identity) [Signal s]
forall {a}. a
err (Maybe (NodeT (MaybeT Identity) [Signal s])
 -> NodeT (MaybeT Identity) [Signal s])
-> Maybe (NodeT (MaybeT Identity) [Signal s])
-> NodeT (MaybeT Identity) [Signal s]
forall a b. (a -> b) -> a -> b
$ TreeT (MaybeT Identity) [Signal s]
-> Maybe (NodeT (MaybeT Identity) [Signal s])
forall a.
TreeT (MaybeT Identity) a -> Maybe (NodeT (MaybeT Identity) a)
Manual.unwrapTreeT TreeT (MaybeT Identity) [Signal s]
signalShrinks

-- | Generate an invalid trace
invalidTrace ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  -- | Maximum length of the generated traces.
  Word64 ->
  -- | Trace failure profile to be used to get an invalid signal.
  [(Int, SignalGenerator s)] ->
  Gen (Invalid.Trace s)
invalidTrace :: forall s.
HasTrace s =>
BaseEnv s -> Word64 -> [(Int, SignalGenerator s)] -> Gen (Trace s)
invalidTrace BaseEnv s
baseEnv Word64
maxTraceLength [(Int, SignalGenerator s)]
failureProfile = do
  Trace s
tr <- forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @s BaseEnv s
baseEnv Word64
maxTraceLength
  let env :: Environment s
env = Trace s -> Environment s
forall s. Trace s -> Environment s
_traceEnv Trace s
tr
      st :: State s
st = Trace s -> State s
forall s. Trace s -> State s
lastState Trace s
tr
  Signal s
iSig <- forall s. [(Int, SignalGenerator s)] -> SignalGenerator s
generateSignalWithFailureProportions @s [(Int, SignalGenerator s)]
failureProfile Environment s
env State s
st
  let est' :: Either (NonEmpty (PredicateFailure s)) (State s)
est' = forall s a. HasTrace s => BaseEnv s -> BaseM s a -> a
interpretSTS @s BaseEnv s
baseEnv (BaseM s (Either (NonEmpty (PredicateFailure s)) (State s))
 -> Either (NonEmpty (PredicateFailure s)) (State s))
-> BaseM s (Either (NonEmpty (PredicateFailure s)) (State s))
-> Either (NonEmpty (PredicateFailure s)) (State s)
forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest @s (RuleContext 'Transition s
 -> BaseM s (Either (NonEmpty (PredicateFailure s)) (State s)))
-> RuleContext 'Transition s
-> BaseM s (Either (NonEmpty (PredicateFailure s)) (State s))
forall a b. (a -> b) -> a -> b
$ (Environment s, State s, Signal s) -> TRC s
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment s
env, State s
st, Signal s
iSig)
  Trace s -> Gen (Trace s)
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Trace s -> Gen (Trace s)) -> Trace s -> Gen (Trace s)
forall a b. (a -> b) -> a -> b
$!
    Invalid.Trace
      { validPrefix :: Trace s
Invalid.validPrefix = Trace s
tr
      , signal :: Signal s
Invalid.signal = Signal s
iSig
      , errorOrLastState :: Either (NonEmpty (PredicateFailure s)) (State s)
Invalid.errorOrLastState = Either (NonEmpty (PredicateFailure s)) (State s)
est'
      }

traceSuchThat ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  Word64 ->
  (Trace s -> Bool) ->
  Gen (Trace s)
traceSuchThat :: forall s.
HasTrace s =>
BaseEnv s -> Word64 -> (Trace s -> Bool) -> Gen (Trace s)
traceSuchThat BaseEnv s
baseEnv Word64
n Trace s -> Bool
cond = (Trace s -> Bool)
-> GenT Identity (Trace s) -> GenT Identity (Trace s)
forall (m :: * -> *) a.
(MonadGen m, GenBase m ~ Identity) =>
(a -> Bool) -> m a -> m a
Gen.filter Trace s -> Bool
cond (forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @s BaseEnv s
baseEnv Word64
n)

ofLengthAtLeast :: Gen (Trace s) -> Int -> Gen (Trace s)
ofLengthAtLeast :: forall s. Gen (Trace s) -> Int -> Gen (Trace s)
ofLengthAtLeast Gen (Trace s)
traceGen Int
minLength =
  (Trace s -> Bool) -> Gen (Trace s) -> Gen (Trace s)
forall (m :: * -> *) a.
(MonadGen m, GenBase m ~ Identity) =>
(a -> Bool) -> m a -> m a
Gen.filter ((Int
minLength Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=) (Int -> Bool) -> (Trace s -> Int) -> Trace s -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace s -> Int
forall s. Trace s -> Int
traceLength) Gen (Trace s)
traceGen

suchThatLastState ::
  forall s.
  Gen (Trace s) ->
  (State s -> Bool) ->
  Gen (Trace s)
suchThatLastState :: forall s. Gen (Trace s) -> (State s -> Bool) -> Gen (Trace s)
suchThatLastState Gen (Trace s)
traceGen State s -> Bool
cond = (Trace s -> Bool) -> Gen (Trace s) -> Gen (Trace s)
forall (m :: * -> *) a.
(MonadGen m, GenBase m ~ Identity) =>
(a -> Bool) -> m a -> m a
Gen.filter (State s -> Bool
cond (State s -> Bool) -> (Trace s -> State s) -> Trace s -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace s -> State s
forall s. Trace s -> State s
lastState) Gen (Trace s)
traceGen

-- | Generate a trace that contains at least one non-trivial signal. See
-- 'HasSizeInfo'.
nonTrivialTrace ::
  forall s.
  (HasTrace s, HasSizeInfo (Signal s)) =>
  BaseEnv s ->
  Word64 ->
  Gen (Trace s)
nonTrivialTrace :: forall s.
(HasTrace s, HasSizeInfo (Signal s)) =>
BaseEnv s -> Word64 -> Gen (Trace s)
nonTrivialTrace BaseEnv s
baseEnv Word64
ub =
  (Trace s -> Bool)
-> GenT Identity (Trace s) -> GenT Identity (Trace s)
forall (m :: * -> *) a.
(MonadGen m, GenBase m ~ Identity) =>
(a -> Bool) -> m a -> m a
Gen.filter ((Signal s -> Bool) -> [Signal s] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (Signal s -> Bool) -> Signal s -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signal s -> Bool
forall sig. HasSizeInfo sig => sig -> Bool
isTrivial) ([Signal s] -> Bool) -> (Trace s -> [Signal s]) -> Trace s -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TraceOrder -> Trace s -> [Signal s]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst) (BaseEnv s -> Word64 -> GenT Identity (Trace s)
forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace BaseEnv s
baseEnv Word64
ub)

class HasSizeInfo sig where
  isTrivial :: sig -> Bool

instance HasSizeInfo [a] where
  isTrivial :: [a] -> Bool
isTrivial = [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null

--------------------------------------------------------------------------------
-- Trace sampling utilities
--------------------------------------------------------------------------------

-- | Sample the maximum trace size, given the generator size and number of
-- samples.
sampleMaxTraceSize ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  -- | Trace's upper bound
  Word64 ->
  -- | Generator size
  Int ->
  -- | Number of samples to take
  Word64 ->
  IO Int
sampleMaxTraceSize :: forall s.
HasTrace s =>
BaseEnv s -> Word64 -> Int -> Word64 -> IO Int
sampleMaxTraceSize BaseEnv s
baseEnv Word64
ub Int
d Word64
n =
  [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
    ([Int] -> Int) -> IO [Int] -> IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Word64] -> (Word64 -> IO Int) -> IO [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Word64
0 .. Word64
n] (IO Int -> Word64 -> IO Int
forall a b. a -> b -> a
const (IO Int -> Word64 -> IO Int) -> IO Int -> Word64 -> IO Int
forall a b. (a -> b) -> a -> b
$ Trace s -> Int
forall s. Trace s -> Int
traceLength (Trace s -> Int) -> IO (Trace s) -> IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Trace s) -> IO (Trace s)
forall (m :: * -> *) a. MonadIO m => Gen a -> m a
Gen.sample (Size -> Gen (Trace s) -> Gen (Trace s)
forall (m :: * -> *) a. MonadGen m => Size -> m a -> m a
Gen.resize (Int -> Size
Size Int
d) (forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @s BaseEnv s
baseEnv Word64
ub)))

randomTrace ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  Word64 ->
  IO (Trace s)
randomTrace :: forall s. HasTrace s => BaseEnv s -> Word64 -> IO (Trace s)
randomTrace BaseEnv s
baseEnv Word64
ub = Gen (Trace s) -> IO (Trace s)
forall (m :: * -> *) a. MonadIO m => Gen a -> m a
Gen.sample (BaseEnv s -> Word64 -> Gen (Trace s)
forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace BaseEnv s
baseEnv Word64
ub)

randomTraceOfSize ::
  forall s.
  HasTrace s =>
  BaseEnv s ->
  Word64 ->
  IO (Trace s)
randomTraceOfSize :: forall s. HasTrace s => BaseEnv s -> Word64 -> IO (Trace s)
randomTraceOfSize BaseEnv s
baseEnv Word64
desiredTraceLength = Gen (Trace s) -> IO (Trace s)
forall (m :: * -> *) a. MonadIO m => Gen a -> m a
Gen.sample (BaseEnv s -> Word64 -> Gen (Trace s)
forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
traceOfLength BaseEnv s
baseEnv Word64
desiredTraceLength)

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

-- | 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 ::
  Trace s ->
  -- | Maximum size of the traces
  Word64 ->
  -- | Steps used to divide the interval
  Word64 ->
  PropertyT IO ()
classifyTraceLength :: forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace s
tr = [Char]
-> Trace s
-> (Trace s -> Word64)
-> Word64
-> Word64
-> PropertyT IO ()
forall n a.
(Show n, Integral n) =>
[Char] -> a -> (a -> n) -> n -> n -> PropertyT IO ()
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
traceLength)

-- | 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 ->
  PropertyT IO ()
classifySize :: forall n a.
(Show n, Integral n) =>
[Char] -> a -> (a -> n) -> n -> n -> PropertyT IO ()
classifySize [Char]
prefixLabel a
value a -> n
sizeF n
upBound n
step = do
  LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
LabelName -> Bool -> m ()
classify ([Char] -> LabelName
mkLabel [Char]
"empty") (Bool -> PropertyT IO ()) -> Bool -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ a -> n
sizeF a
value n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
0
  LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
LabelName -> Bool -> m ()
classify ([Char] -> LabelName
mkLabel [Char]
"singleton") (Bool -> PropertyT IO ()) -> Bool -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ a -> n
sizeF a
value n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
1
  ((n, n) -> PropertyT IO ()) -> [(n, n)] -> PropertyT IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (n, n) -> PropertyT IO ()
classifySizeInterval ([(n, n)] -> PropertyT IO ()) -> [(n, n)] -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ 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
  LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
LabelName -> Bool -> m ()
classify LabelName
upBoundLabel (Bool -> PropertyT IO ()) -> Bool -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ a -> n
sizeF a
value n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
upBound
  where
    upBoundLabel :: LabelName
upBoundLabel = [Char] -> LabelName
mkLabel ([Char] -> LabelName) -> [Char] -> LabelName
forall a b. (a -> b) -> a -> b
$ n -> [Char]
forall a. Show a => a -> [Char]
show n
upBound
    mkLabel :: [Char] -> LabelName
mkLabel = [Char] -> LabelName
forall a. IsString a => [Char] -> a
fromString ([Char] -> LabelName) -> ([Char] -> [Char]) -> [Char] -> LabelName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Char]
prefixLabel [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)
    classifySizeInterval :: (n, n) -> PropertyT IO ()
classifySizeInterval (n
low, n
high) =
      LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
LabelName -> Bool -> m ()
classify LabelName
desc (Bool -> PropertyT IO ()) -> Bool -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$! 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
      where
        -- Hedgehog's LabelName doesn't have a monoid instance at the moment...
        desc :: LabelName
desc = [Char] -> LabelName
mkLabel ([Char] -> LabelName) -> [Char] -> LabelName
forall a b. (a -> b) -> a -> b
$ [Char]
"[" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> n -> [Char]
forall a. Show a => a -> [Char]
show n
low [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
", " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> n -> [Char]
forall a. Show a => a -> [Char]
show n
high [Char] -> [Char] -> [Char]
forall a. Semigroup 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)

-- | Given a function that computes an integral value from a trace, return that
-- value as a ratio of the trace length.
ratio ::
  Integral a =>
  (Trace s -> a) ->
  Trace s ->
  Double
ratio :: forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio Trace s -> a
f Trace s
tr = a -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Trace s -> a
f Trace s
tr) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Trace s -> Int
forall s. Trace s -> Int
traceLength Trace s
tr)

--------------------------------------------------------------------------------
-- Trace properties
--------------------------------------------------------------------------------

-- | Property that simply classifies the lengths of the generated traces.
traceLengthsAreClassified ::
  forall s.
  (HasTrace s, Show (Environment s), Show (State s), Show (Signal s)) =>
  BaseEnv s ->
  -- | 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 ->
  Property
traceLengthsAreClassified :: forall s.
(HasTrace s, Show (Environment s), Show (State s),
 Show (Signal s)) =>
BaseEnv s -> Word64 -> Word64 -> Property
traceLengthsAreClassified BaseEnv s
baseEnv Word64
maximumTraceLength Word64
intervalSize =
  HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
    Trace s
traceSample <- Gen (Trace s) -> PropertyT IO (Trace s)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @s BaseEnv s
baseEnv Word64
maximumTraceLength)
    Trace s -> Word64 -> Word64 -> PropertyT IO ()
forall s. Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace s
traceSample Word64
maximumTraceLength Word64
intervalSize
    PropertyT IO ()
forall (m :: * -> *). MonadTest m => m ()
success

-- | Check that the signal generator of 's' only generate valid signals.
onlyValidSignalsAreGenerated ::
  forall s.
  (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) =>
  BaseEnv s ->
  -- | Maximum trace length.
  Word64 ->
  Property
onlyValidSignalsAreGenerated :: forall s.
(HasTrace s, Show (Environment s), Show (State s), Show (Signal s),
 HasCallStack) =>
BaseEnv s -> Word64 -> Property
onlyValidSignalsAreGenerated BaseEnv s
baseEnv Word64
maximumTraceLength =
  BaseEnv s -> Gen (Trace s) -> Property
forall s.
(HasTrace s, Show (Environment s), Show (State s), Show (Signal s),
 HasCallStack) =>
BaseEnv s -> Gen (Trace s) -> Property
onlyValidSignalsAreGeneratedForTrace BaseEnv s
baseEnv (forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @s BaseEnv s
baseEnv Word64
maximumTraceLength)

-- | Check that the signal generator of 's' only generate valid signals.
onlyValidSignalsAreGeneratedForTrace ::
  forall s.
  (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) =>
  BaseEnv s ->
  Gen (Trace s) ->
  Property
onlyValidSignalsAreGeneratedForTrace :: forall s.
(HasTrace s, Show (Environment s), Show (State s), Show (Signal s),
 HasCallStack) =>
BaseEnv s -> Gen (Trace s) -> Property
onlyValidSignalsAreGeneratedForTrace BaseEnv s
baseEnv Gen (Trace s)
traceGen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  Trace s
tr <- Gen (Trace s) -> PropertyT IO (Trace s)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (Trace s)
traceGen
  let env :: Environment s
      env :: Environment s
env = Trace s -> Environment s
forall s. Trace s -> Environment s
_traceEnv Trace s
tr

      st' :: State s
      st' :: State s
st' = Trace s -> State s
forall s. Trace s -> State s
lastState Trace s
tr
  Signal s
sig <- Gen (Signal s) -> PropertyT IO (Signal s)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (forall s. HasTrace s => SignalGenerator s
sigGen @s Environment s
env State s
st')
  let result :: Either (NonEmpty (PredicateFailure s)) (State s)
result = forall s a. HasTrace s => BaseEnv s -> BaseM s a -> a
interpretSTS @s BaseEnv s
baseEnv (BaseM s (Either (NonEmpty (PredicateFailure s)) (State s))
 -> Either (NonEmpty (PredicateFailure s)) (State s))
-> BaseM s (Either (NonEmpty (PredicateFailure s)) (State s))
-> Either (NonEmpty (PredicateFailure s)) (State s)
forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest @s ((Environment s, State s, Signal s) -> TRC s
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment s
env, State s
st', Signal s
sig))
  -- TODO: For some reason the result that led to the failure is not shown
  -- (even without using tasty, and setting the condition to True === False)
  State s -> PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, Show a) => a -> m ()
footnoteShow State s
st'
  Signal s -> PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, Show a) => a -> m ()
footnoteShow Signal s
sig
  Either (NonEmpty (PredicateFailure s)) (State s) -> PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, Show a) => a -> m ()
footnoteShow Either (NonEmpty (PredicateFailure s)) (State s)
result
  PropertyT IO (State s) -> PropertyT IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (PropertyT IO (State s) -> PropertyT IO ())
-> PropertyT IO (State s) -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ Either (NonEmpty (PredicateFailure s)) (State s)
-> PropertyT IO (State s)
forall (m :: * -> *) x a.
(MonadTest m, Show x, HasCallStack) =>
Either x a -> m a
evalEither Either (NonEmpty (PredicateFailure s)) (State s)
result

coverFailures ::
  forall m s a.
  ( MonadTest m
  , HasCallStack
  , Data (PredicateFailure s)
  , Data a
  ) =>
  CoverPercentage ->
  -- | Target predicate failures
  [PredicateFailure s] ->
  -- | Structure containing the failures
  a ->
  m ()
coverFailures :: forall (m :: * -> *) s a.
(MonadTest m, HasCallStack, Data (PredicateFailure s), Data a) =>
CoverPercentage -> [PredicateFailure s] -> a -> m ()
coverFailures CoverPercentage
coverPercentage [PredicateFailure s]
targetFailures a
failureStructure = do
  (PredicateFailure s -> m ()) -> [PredicateFailure s] -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (Constr -> m ()
coverFailure (Constr -> m ())
-> (PredicateFailure s -> Constr) -> PredicateFailure s -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredicateFailure s -> Constr
forall a. Data a => a -> Constr
toConstr) [PredicateFailure s]
targetFailures
  where
    coverFailure :: Constr -> m ()
coverFailure Constr
predicateFailureConstructor =
      CoverPercentage -> LabelName -> Bool -> m ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
        CoverPercentage
coverPercentage
        ([Char] -> LabelName
forall a. IsString a => [Char] -> a
fromString ([Char] -> LabelName) -> [Char] -> LabelName
forall a b. (a -> b) -> a -> b
$ Constr -> [Char]
forall a. Show a => a -> [Char]
show Constr
predicateFailureConstructor)
        (Constr
predicateFailureConstructor Constr -> [Constr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Constr]
failuresConstructors)
      where
        subFailures :: [PredicateFailure s]
        subFailures :: [PredicateFailure s]
subFailures = a -> [PredicateFailure s]
forall d a. (Data d, Typeable a) => d -> [a]
extractValues a
failureStructure

        failuresConstructors :: [Constr]
        failuresConstructors :: [Constr]
failuresConstructors = PredicateFailure s -> Constr
forall a. Data a => a -> Constr
toConstr (PredicateFailure s -> Constr) -> [PredicateFailure s] -> [Constr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PredicateFailure s]
subFailures

invalidSignalsAreGenerated ::
  forall s.
  (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) =>
  BaseEnv s ->
  -- | Failure profile.
  [(Int, SignalGenerator s)] ->
  -- | Maximum trace length.
  Word64 ->
  -- | Action to run when the an invalid signal is generated.
  (NonEmpty (PredicateFailure s) -> PropertyT IO ()) ->
  Property
invalidSignalsAreGenerated :: forall s.
(HasTrace s, Show (Environment s), Show (State s), Show (Signal s),
 HasCallStack) =>
BaseEnv s
-> [(Int, SignalGenerator s)]
-> Word64
-> (NonEmpty (PredicateFailure s) -> PropertyT IO ())
-> Property
invalidSignalsAreGenerated BaseEnv s
baseEnv [(Int, SignalGenerator s)]
failureProfile Word64
maximumTraceLength NonEmpty (PredicateFailure s) -> PropertyT IO ()
checkFailures = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  Trace s
tr <- Gen (Trace s) -> PropertyT IO (Trace s)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (forall s.
HasTrace s =>
BaseEnv s -> Word64 -> [(Int, SignalGenerator s)] -> Gen (Trace s)
invalidTrace @s BaseEnv s
baseEnv Word64
maximumTraceLength [(Int, SignalGenerator s)]
failureProfile)

  CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
    CoverPercentage
80
    LabelName
"Invalid signals are generated when requested"
    (Either (NonEmpty (PredicateFailure s)) (State s) -> Bool
forall a b. Either a b -> Bool
isLeft (Either (NonEmpty (PredicateFailure s)) (State s) -> Bool)
-> Either (NonEmpty (PredicateFailure s)) (State s) -> Bool
forall a b. (a -> b) -> a -> b
$ Trace s -> Either (NonEmpty (PredicateFailure s)) (State s)
forall s.
Trace s -> Either (NonEmpty (PredicateFailure s)) (State s)
Invalid.errorOrLastState Trace s
tr)

  (NonEmpty (PredicateFailure s) -> PropertyT IO ())
-> (State s -> PropertyT IO ())
-> Either (NonEmpty (PredicateFailure s)) (State s)
-> PropertyT IO ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either NonEmpty (PredicateFailure s) -> PropertyT IO ()
checkFailures (PropertyT IO () -> State s -> PropertyT IO ()
forall a b. a -> b -> a
const PropertyT IO ()
forall (m :: * -> *). MonadTest m => m ()
success) (Trace s -> Either (NonEmpty (PredicateFailure s)) (State s)
forall s.
Trace s -> Either (NonEmpty (PredicateFailure s)) (State s)
Invalid.errorOrLastState Trace s
tr)