{-# 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 TypeInType #-}
{-# 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 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
  , tinkerWithSigGen
  , coverFailures
  )
where

import           Control.Arrow (second)
import           Control.Monad (forM, void)
import           Control.Monad.Trans.Maybe (MaybeT)
import           Control.Monad.Trans.State.Strict (evalState)
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.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.Property (CoverPercentage)
import           Hedgehog.Range (Size (Size))
import qualified Hedgehog.Range as Range

import           Hedgehog.Internal.Gen (integral_, runDiscardEffectT)
import           Hedgehog.Internal.Tree (NodeT (NodeT), TreeT, nodeChildren, treeValue)

import           Control.State.Transition.Extended (BaseM, Environment, IRC (IRC), PredicateFailure, STS, Signal,
                     State, TRC (TRC))
import qualified Control.State.Transition.Invalid.Trace as Invalid
import           Control.State.Transition.Trace (Trace, TraceOrder (OldestFirst), closure,
                     extractValues, lastState, mkTrace, traceLength, traceSignals, _traceEnv
                     , applySTSTest)
import           Hedgehog.Extra.Manual (Manual)
import qualified Hedgehog.Extra.Manual as Manual

import           Test.Goblin (Goblin (..), GoblinData, SeedGoblin (..))

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 x) = a
x

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

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

  trace
    :: BaseEnv s
    -> Word64
    -- ^ Maximum length of the generated traces. The actual length will be
    -- between 0 and this maximum.
    -> Gen (Trace s)
  trace BaseEnv s
baseEnv Word64
n = BaseEnv s -> Word64 -> TraceProfile s -> Gen (Trace s)
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 (HasTrace s => SignalGenerator s
forall s. HasTrace s => SignalGenerator s
sigGen @s)

  traceOfLength
    :: BaseEnv s
    -> Word64
    -- ^ Desired length of the generated trace. If the signal generator can generate invalid signals
    -- then the resulting trace might not have the given length.
    -> 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 (HasTrace s => SignalGenerator s
forall s. HasTrace s => SignalGenerator s
sigGen @s)

  traceOfLengthWithInitState
    :: BaseEnv s
    -> Word64
    -- ^ Desired length of the generated trace. If the signal generator can generate invalid signals
    -- then the resulting trace might not have the given length.
    -> (Environment s -> Gen (State s))
    -- ^ A generator for Initial State, given the STS environment
    -> 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 (HasTrace s => SignalGenerator s
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
  { TraceProfile s -> Int
proportionOfValidSignals :: !Int
    -- ^ Proportion of valid signals to generate.
  , 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 :: TraceProfile s -> Int
proportionOfInvalidSignals = [Int] -> Int
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 (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 :: TraceProfile s
allValid
  = TraceProfile :: forall s. Int -> [(Int, SignalGenerator s)] -> TraceProfile s
TraceProfile
    { proportionOfValidSignals :: Int
proportionOfValidSignals = Int
1
    , failures :: [(Int, SignalGenerator s)]
failures = []
    }

-- | Generate a signal by combining the generators using @hedgehog@'s
-- 'frequency' combinator.
generateSignalWithFailureProportions
  :: [(Int, SignalGenerator s)]
  -- ^ Failure proportions. See 'failures' in 'TraceProfile'.
  -> SignalGenerator s
generateSignalWithFailureProportions :: [(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 (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 :: BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
traceSigGen BaseEnv s
baseEnv TraceLength
aTraceLength = 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 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 :: 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 <- Word64 -> Gen (Environment s)
forall s. HasTrace s => Word64 -> Gen (Environment s)
envGen @s (TraceLength -> Word64
traceLengthValue TraceLength
aTraceLength)
  case BaseEnv s
-> BaseM s (Either [[PredicateFailure s]] (State s))
-> Either [[PredicateFailure s]] (State s)
forall s a. HasTrace s => BaseEnv s -> BaseM s a -> a
interpretSTS @s BaseEnv s
baseEnv (BaseM s (Either [[PredicateFailure s]] (State s))
 -> Either [[PredicateFailure s]] (State s))
-> BaseM s (Either [[PredicateFailure s]] (State s))
-> Either [[PredicateFailure s]] (State s)
forall a b. (a -> b) -> a -> b
$ RuleContext 'Initial s
-> BaseM s (Either [[PredicateFailure s]] (State s))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (Either [[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 [[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 :: 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 <- Word64 -> Gen (Environment s)
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 :: 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
  -> Word64
  -- ^ Trace upper bound. This will be linearly scaled as a function of the
  -- generator size.
  -> Environment s
  -- ^ Environment, which remains constant in the system.
  -> State s
  -- ^ Initial state.
  -> SignalGenerator s
  -- ^ Signal generator. This generator relies on an environment and a state to
  -- generate a signal.
  -> Gen (Trace s)
genTrace :: 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
-> 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
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
  -> Word64
  -- ^ Trace upper bound. This will be linearly scaled as a function of the
  -- generator size.
  -> TraceProfile s
  -> Environment s
  -- ^ Environment, which remains constant in the system.
  -> State s
  -- ^ Initial state.
  -> SignalGenerator s
  -- ^ Signal generator. This generator relies on an environment and a state to
  -- generate a signal.
  -> Gen (Trace s)
genTraceWithProfile :: 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 (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 (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
  -> Word64
  -- ^ Desired trace length.
  -> TraceProfile s
  -> Environment s
  -- ^ Environment, which remains constant in the system.
  -> State s
  -- ^ Initial state.
  -> SignalGenerator s
  -- ^ Signal generator. This generator relies on an environment and a state to
  -- generate a signal.
  -> Gen (Trace s)
genTraceOfLength :: 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 (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 (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
      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
                 , [(Int, SignalGenerator s)] -> SignalGenerator s
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 BaseEnv s
-> BaseM s (Either [[PredicateFailure s]] (State s))
-> Either [[PredicateFailure s]] (State s)
forall s a. HasTrace s => BaseEnv s -> BaseM s a -> a
interpretSTS @s BaseEnv s
baseEnv (BaseM s (Either [[PredicateFailure s]] (State s))
 -> Either [[PredicateFailure s]] (State s))
-> BaseM s (Either [[PredicateFailure s]] (State s))
-> Either [[PredicateFailure s]] (State s)
forall a b. (a -> b) -> a -> b
$ RuleContext 'Transition s
-> BaseM s (Either [[PredicateFailure s]] (State s))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (Either [[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 [[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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BaseEnv s -> BaseM s (Trace s) -> Trace s
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
. Environment s -> State s -> [Signal s] -> BaseM s (Trace s)
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 (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
  -> Word64
  -- ^ Maximum length of the generated traces.
  -> [(Int, SignalGenerator s)]
  -- ^ Trace failure profile to be used to get an invalid signal.
  -> Gen (Invalid.Trace s)
invalidTrace :: BaseEnv s -> Word64 -> [(Int, SignalGenerator s)] -> Gen (Trace s)
invalidTrace BaseEnv s
baseEnv Word64
maxTraceLength [(Int, SignalGenerator s)]
failureProfile = do
  Trace s
tr <- BaseEnv s -> Word64 -> Gen (Trace s)
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 <- [(Int, SignalGenerator s)] -> SignalGenerator s
forall s. [(Int, SignalGenerator s)] -> SignalGenerator s
generateSignalWithFailureProportions @s [(Int, SignalGenerator s)]
failureProfile Environment s
env State s
st
  let est' :: Either [[PredicateFailure s]] (State s)
est' = BaseEnv s
-> BaseM s (Either [[PredicateFailure s]] (State s))
-> Either [[PredicateFailure s]] (State s)
forall s a. HasTrace s => BaseEnv s -> BaseM s a -> a
interpretSTS @s BaseEnv s
baseEnv (BaseM s (Either [[PredicateFailure s]] (State s))
 -> Either [[PredicateFailure s]] (State s))
-> BaseM s (Either [[PredicateFailure s]] (State s))
-> Either [[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 [[PredicateFailure s]] (State s))
forall (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s))
applySTSTest @s (RuleContext 'Transition s
 -> BaseM s (Either [[PredicateFailure s]] (State s)))
-> RuleContext 'Transition s
-> BaseM s (Either [[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 (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
$! Trace :: forall s.
Trace s
-> Signal s -> Either [[PredicateFailure s]] (State s) -> Trace s
Invalid.Trace
            { validPrefix :: Trace s
Invalid.validPrefix = Trace s
tr
            , signal :: Signal s
Invalid.signal = Signal s
iSig
            , errorOrLastState :: Either [[PredicateFailure s]] (State s)
Invalid.errorOrLastState = Either [[PredicateFailure s]] (State s)
est'
            }


traceSuchThat
  :: forall s
   . HasTrace s
  => BaseEnv s
  -> Word64
  -> (Trace s -> Bool)
  -> Gen (Trace s)
traceSuchThat :: BaseEnv s -> Word64 -> (Trace s -> Bool) -> Gen (Trace s)
traceSuchThat BaseEnv s
baseEnv Word64
n Trace 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 Trace s -> Bool
cond (BaseEnv s -> Word64 -> Gen (Trace s)
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 :: 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 :: 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 :: BaseEnv s -> Word64 -> Gen (Trace s)
nonTrivialTrace BaseEnv s
baseEnv Word64
ub =
  (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 ((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 -> Gen (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 (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
  -> Word64
  -- ^ Trace's upper bound
  -> Int
  -- ^ Generator size
  -> Word64
  -- ^ Number of samples to take
  -> IO Int
sampleMaxTraceSize :: BaseEnv s -> Word64 -> Int -> Word64 -> IO Int
sampleMaxTraceSize BaseEnv s
baseEnv Word64
ub Int
d Word64
n =
  [Int] -> Int
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) (BaseEnv s -> Word64 -> Gen (Trace s)
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 :: 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 :: 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
  -> Word64
  -- ^ Maximum size of the traces
  -> Word64
  -- ^ Steps used to divide the interval
  -> PropertyT IO ()
classifyTraceLength :: Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifyTraceLength Trace s
tr = [Char]
-> Trace s
-> (Trace s -> Word64)
-> Word64
-> Word64
-> PropertyT IO ()
forall n a.
(Ord n, 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
  :: (Ord n, Show n, Integral n)
  => String
  -- ^ Prefix to be added to the label intervals
  -> a
  -- ^ Value to classify
  -> (a -> n)
  -- ^ Size function
  -> n
  -- ^ Maximum value size
  -> n
  -- ^ Steps used to divide the size interval
  -> PropertyT IO ()
classifySize :: [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
  => 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)]
mkIntervals :: 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 :: (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
  -> Word64
  -- ^ Maximum trace length that the signal generator of 's' can generate.
  -> Word64
  -- ^ Lengths of the intervals in which the lengths range should be split.
  -> Property
traceLengthsAreClassified :: 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 (BaseEnv s -> Word64 -> Gen (Trace s)
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
  -> Word64
  -- ^ Maximum trace length.
  -> Property
onlyValidSignalsAreGenerated :: 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 (BaseEnv s -> Word64 -> Gen (Trace s)
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 :: 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 (SignalGenerator s
forall s. HasTrace s => SignalGenerator s
sigGen @s Environment s
env State s
st')
  let result :: Either [[PredicateFailure s]] (State s)
result = BaseEnv s
-> BaseM s (Either [[PredicateFailure s]] (State s))
-> Either [[PredicateFailure s]] (State s)
forall s a. HasTrace s => BaseEnv s -> BaseM s a -> a
interpretSTS @s BaseEnv s
baseEnv (BaseM s (Either [[PredicateFailure s]] (State s))
 -> Either [[PredicateFailure s]] (State s))
-> BaseM s (Either [[PredicateFailure s]] (State s))
-> Either [[PredicateFailure s]] (State s)
forall a b. (a -> b) -> a -> b
$ RuleContext 'Transition s
-> BaseM s (Either [[PredicateFailure s]] (State s))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (Either [[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 [[PredicateFailure s]] (State s) -> PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, Show a) => a -> m ()
footnoteShow Either [[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 [[PredicateFailure s]] (State s) -> PropertyT IO (State s)
forall (m :: * -> *) x a.
(MonadTest m, Show x, HasCallStack) =>
Either x a -> m a
evalEither Either [[PredicateFailure s]] (State s)
result

coverFailures
  :: forall m s a
   . ( MonadTest m
     , HasCallStack
     , Data (PredicateFailure s)
     , Data a
     )
  => CoverPercentage
  -> [PredicateFailure s]
  -- ^ Target predicate failures
  -> a
  -- ^ Structure containing the failures
  -> m ()
coverFailures :: CoverPercentage -> [PredicateFailure s] -> a -> m ()
coverFailures CoverPercentage
coverPercentage [PredicateFailure s]
targetFailures a
failureStructure = do
  (Constr -> m ()) -> [Constr] -> m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Constr -> m ()
coverFailure (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]
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 (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
  -> [(Int, SignalGenerator s)]
  -- ^ Failure profile.
  -> Word64
  -- ^ Maximum trace length.
  -> ([[PredicateFailure s]] -> PropertyT IO ())
  -- ^ Action to run when the an invalid signal is generated.
  -> Property
invalidSignalsAreGenerated :: BaseEnv s
-> [(Int, SignalGenerator s)]
-> Word64
-> ([[PredicateFailure s]] -> PropertyT IO ())
-> Property
invalidSignalsAreGenerated BaseEnv s
baseEnv [(Int, SignalGenerator s)]
failureProfile Word64
maximumTraceLength [[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 (BaseEnv s -> Word64 -> [(Int, SignalGenerator s)] -> Gen (Trace s)
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 [[PredicateFailure s]] (State s) -> Bool
forall a b. Either a b -> Bool
isLeft (Either [[PredicateFailure s]] (State s) -> Bool)
-> Either [[PredicateFailure s]] (State s) -> Bool
forall a b. (a -> b) -> a -> b
$ Trace s -> Either [[PredicateFailure s]] (State s)
forall s. Trace s -> Either [[PredicateFailure s]] (State s)
Invalid.errorOrLastState Trace s
tr)

  ([[PredicateFailure s]] -> PropertyT IO ())
-> (State s -> PropertyT IO ())
-> Either [[PredicateFailure s]] (State s)
-> PropertyT IO ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [[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 [[PredicateFailure s]] (State s)
forall s. Trace s -> Either [[PredicateFailure s]] (State s)
Invalid.errorOrLastState Trace s
tr)


--------------------------------------------------------------------------------
-- Helpers
--------------------------------------------------------------------------------

tinkerWithSigGen
  :: forall g sts
   . ( HasTrace sts, Goblin g (Signal sts)
     , SeedGoblin (Environment sts)
     , SeedGoblin (State sts) )
  => GoblinData g
  -> Environment sts
  -> State sts
  -> Gen (Signal sts)
tinkerWithSigGen :: GoblinData g -> Environment sts -> State sts -> Gen (Signal sts)
tinkerWithSigGen GoblinData g
gd Environment sts
env State sts
state = (State (GoblinData g) (Gen (Signal sts))
 -> GoblinData g -> Gen (Signal sts))
-> GoblinData g
-> State (GoblinData g) (Gen (Signal sts))
-> Gen (Signal sts)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (GoblinData g) (Gen (Signal sts))
-> GoblinData g -> Gen (Signal sts)
forall s a. State s a -> s -> a
evalState GoblinData g
gd (State (GoblinData g) (Gen (Signal sts)) -> Gen (Signal sts))
-> State (GoblinData g) (Gen (Signal sts)) -> Gen (Signal sts)
forall a b. (a -> b) -> a -> b
$
  Environment sts -> TinkerM g ()
forall a g. SeedGoblin a => a -> TinkerM g ()
seeder Environment sts
env TinkerM g () -> TinkerM g () -> TinkerM g ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> State sts -> TinkerM g ()
forall a g. SeedGoblin a => a -> TinkerM g ()
seeder State sts
state TinkerM g ()
-> State (GoblinData g) (Gen (Signal sts))
-> State (GoblinData g) (Gen (Signal sts))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Gen (Signal sts) -> State (GoblinData g) (Gen (Signal sts))
forall g a. Goblin g a => Gen a -> TinkerM g (Gen a)
tinker (Environment sts -> State sts -> Gen (Signal sts)
forall s. HasTrace s => SignalGenerator s
sigGen @sts Environment sts
env State sts
state)