{-# 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 #-}
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
, invalidTrace
, classifyTraceLength
, classifySize
, mkIntervals
, ratio
, traceLengthsAreClassified
, onlyValidSignalsAreGenerated
, onlyValidSignalsAreGeneratedForTrace
, invalidSignalsAreGenerated
, 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 = ()
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
envGen
:: Word64
-> Gen (Environment s)
sigGen
:: SignalGenerator s
trace
:: BaseEnv s
-> Word64
-> 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
-> 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
-> (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 (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
, TraceProfile s -> [(Int, SignalGenerator s)]
failures :: ![(Int, SignalGenerator s)]
}
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 = []
}
generateSignalWithFailureProportions
:: [(Int, SignalGenerator s)]
-> 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
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
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
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
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
genTrace
:: forall s
. (HasTrace s)
=> BaseEnv s
-> Word64
-> Environment s
-> State s
-> SignalGenerator s
-> 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
genTraceWithProfile
:: forall s
. (HasTrace s)
=> BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> 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
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
genTraceOfLength
:: forall s
. (HasTrace s)
=> BaseEnv s
-> Word64
-> TraceProfile s
-> Environment s
-> State s
-> SignalGenerator s
-> 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
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"
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
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
invalidTrace
:: forall s
. HasTrace s
=> BaseEnv s
-> Word64
-> [(Int, SignalGenerator s)]
-> 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
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
sampleMaxTraceSize
:: forall s
. HasTrace s
=> BaseEnv s
-> Word64
-> Int
-> Word64
-> 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)
classifyTraceLength
:: Trace s
-> Word64
-> Word64
-> 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)
classifySize
:: (Ord n, Show n, Integral n)
=> String
-> a
-> (a -> n)
-> n
-> n
-> 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
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]
")"
mkIntervals
:: Integral n
=> n
-> n
-> n
-> [(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)
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)
traceLengthsAreClassified
:: forall s
. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s))
=> BaseEnv s
-> Word64
-> Word64
-> 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
onlyValidSignalsAreGenerated
:: forall s
. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack)
=> BaseEnv s
-> Word64
-> 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)
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))
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]
-> a
-> 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)]
-> Word64
-> ([[PredicateFailure s]] -> PropertyT IO ())
-> 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)
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)