{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.State.Transition.Trace.Generator.QuickCheck
( HasTrace (BaseEnv, envGen, sigGen, shrinkSignal, interpretSTS)
, traceFrom
, traceFromInitState
, trace
, shrinkTrace
, forAllTrace
, forAllTraceFromInitState
, onlyValidSignalsAreGenerated
, onlyValidSignalsAreGeneratedFromInitState
, traceLengthsAreClassified
, classifyTraceLength
, classifySize
, mkIntervals
)
where
import Data.Functor.Identity (Identity(..))
import Data.Kind (Type)
import Data.Maybe (fromMaybe)
import Data.Word (Word64)
import qualified Test.QuickCheck as QuickCheck
import Control.State.Transition (Environment, IRC (IRC), STS, Signal, State, TRC (TRC))
import qualified Control.State.Transition.Extended as STS
import Control.State.Transition.Trace (Trace)
import qualified Control.State.Transition.Trace as Trace
class STS sts => HasTrace sts traceGenEnv where
type BaseEnv sts :: Type
type BaseEnv s = ()
interpretSTS :: forall a. (BaseEnv sts -> STS.BaseM sts a -> a)
default interpretSTS :: (STS.BaseM sts ~ Identity) => forall a. BaseEnv sts -> STS.BaseM sts a -> a
interpretSTS BaseEnv sts
_ (Identity x) = a
x
envGen :: traceGenEnv -> QuickCheck.Gen (Environment sts)
sigGen
:: traceGenEnv
-> Environment sts
-> State sts
-> QuickCheck.Gen (Signal sts)
shrinkSignal :: Signal sts -> [Signal sts]
traceFrom
:: forall sts traceGenEnv
. ( HasTrace sts traceGenEnv
)
=> BaseEnv sts
-> Word64
-> traceGenEnv
-> Environment sts
-> State sts
-> QuickCheck.Gen (Trace sts)
traceFrom :: BaseEnv sts
-> Word64
-> traceGenEnv
-> Environment sts
-> State sts
-> Gen (Trace sts)
traceFrom BaseEnv sts
traceEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Environment sts
env State sts
st0 = do
Word64
chosenTraceLength <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
QuickCheck.choose (Word64
0, Word64
maxTraceLength)
Environment sts
-> State sts -> [(State sts, Signal sts)] -> Trace sts
forall s.
Environment s -> State s -> [(State s, Signal s)] -> Trace s
Trace.mkTrace Environment sts
env State sts
st0 ([(State sts, Signal sts)] -> Trace sts)
-> Gen [(State sts, Signal sts)] -> Gen (Trace sts)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop Word64
chosenTraceLength State sts
st0 []
where
loop
:: Word64
-> State sts
-> [(State sts, Signal sts)]
-> QuickCheck.Gen [(State sts, Signal sts)]
loop :: Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop Word64
0 State sts
_ [(State sts, Signal sts)]
acc = [(State sts, Signal sts)] -> Gen [(State sts, Signal sts)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(State sts, Signal sts)] -> Gen [(State sts, Signal sts)])
-> [(State sts, Signal sts)] -> Gen [(State sts, Signal sts)]
forall a b. (a -> b) -> a -> b
$! [(State sts, Signal sts)]
acc
loop !Word64
d State sts
sti [(State sts, Signal sts)]
stSigs = do
Signal sts
sig <- traceGenEnv -> Environment sts -> State sts -> Gen (Signal sts)
forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
traceGenEnv -> Environment sts -> State sts -> Gen (Signal sts)
sigGen @sts @traceGenEnv traceGenEnv
traceGenEnv Environment sts
env State sts
sti
case BaseEnv sts
-> BaseM sts (Either [[PredicateFailure sts]] (State sts))
-> Either [[PredicateFailure sts]] (State sts)
forall sts traceGenEnv a.
HasTrace sts traceGenEnv =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
traceEnv (RuleContext 'Transition sts
-> BaseM sts (Either [[PredicateFailure sts]] (State sts))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s))
Trace.applySTSTest @sts ((Environment sts, State sts, Signal sts) -> TRC sts
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC(Environment sts
env, State sts
sti, Signal sts
sig))) of
Left [[PredicateFailure sts]]
_predicateFailures ->
Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop (Word64
d Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) State sts
sti [(State sts, Signal sts)]
stSigs
Right State sts
sti' ->
Word64
-> State sts
-> [(State sts, Signal sts)]
-> Gen [(State sts, Signal sts)]
loop (Word64
d Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) State sts
sti' ((State sts
sti', Signal sts
sig)(State sts, Signal sts)
-> [(State sts, Signal sts)] -> [(State sts, Signal sts)]
forall a. a -> [a] -> [a]
: [(State sts, Signal sts)]
stSigs)
trace
:: forall sts traceGenEnv
. (HasTrace sts traceGenEnv, Show (Environment sts)
)
=> BaseEnv sts
-> Word64
-> traceGenEnv
-> QuickCheck.Gen (Trace sts)
trace :: BaseEnv sts -> Word64 -> traceGenEnv -> Gen (Trace sts)
trace BaseEnv sts
traceEnv Word64
maxTraceLength traceGenEnv
traceGenEnv =
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> Gen (Trace sts)
forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> Gen (Trace sts)
traceFromInitState BaseEnv sts
traceEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
forall a. Maybe a
Nothing
traceFromInitState
:: forall sts traceGenEnv
. ( HasTrace sts traceGenEnv, Show (Environment sts)
)
=> BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe (IRC sts -> QuickCheck.Gen (Either [[STS.PredicateFailure sts]] (State sts)))
-> QuickCheck.Gen (Trace sts)
traceFromInitState :: BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> Gen (Trace sts)
traceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
genSt0 = do
Environment sts
env <- traceGenEnv -> Gen (Environment sts)
forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
traceGenEnv -> Gen (Environment sts)
envGen @sts @traceGenEnv traceGenEnv
traceGenEnv
Either [[PredicateFailure sts]] (State sts)
res <- (IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> IRC sts
-> Gen (Either [[PredicateFailure sts]] (State sts))
forall a. a -> Maybe a -> a
fromMaybe (Either [[PredicateFailure sts]] (State sts)
-> Gen (Either [[PredicateFailure sts]] (State sts))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [[PredicateFailure sts]] (State sts)
-> Gen (Either [[PredicateFailure sts]] (State sts)))
-> (IRC sts -> Either [[PredicateFailure sts]] (State sts))
-> IRC sts
-> Gen (Either [[PredicateFailure sts]] (State sts))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseEnv sts
-> BaseM sts (Either [[PredicateFailure sts]] (State sts))
-> Either [[PredicateFailure sts]] (State sts)
forall sts traceGenEnv a.
HasTrace sts traceGenEnv =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
baseEnv
(BaseM sts (Either [[PredicateFailure sts]] (State sts))
-> Either [[PredicateFailure sts]] (State sts))
-> (IRC sts
-> BaseM sts (Either [[PredicateFailure sts]] (State sts)))
-> IRC sts
-> Either [[PredicateFailure sts]] (State sts)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRC sts -> BaseM sts (Either [[PredicateFailure sts]] (State sts))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s))
Trace.applySTSTest) Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
genSt0 (IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts))
forall a b. (a -> b) -> a -> b
$ (Environment sts -> IRC sts
forall sts. Environment sts -> IRC sts
IRC Environment sts
env)
case Either [[PredicateFailure sts]] (State sts)
res of
Left [[PredicateFailure sts]]
pf -> [Char] -> Gen (Trace sts)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Gen (Trace sts)) -> [Char] -> Gen (Trace sts)
forall a b. (a -> b) -> a -> b
$ [Char]
"Failed to apply the initial rule to the generated environment.\n"
[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"Generated environment: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Environment sts -> [Char]
forall a. Show a => a -> [Char]
show Environment sts
env
[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"Failure: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[PredicateFailure sts]] -> [Char]
forall a. Show a => a -> [Char]
show [[PredicateFailure sts]]
pf
Right State sts
st0 -> BaseEnv sts
-> Word64
-> traceGenEnv
-> Environment sts
-> State sts
-> Gen (Trace sts)
forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Environment sts
-> State sts
-> Gen (Trace sts)
traceFrom BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Environment sts
env State sts
st0
forAllTraceFromInitState
:: forall sts traceGenEnv prop
. ( HasTrace sts traceGenEnv
, QuickCheck.Testable prop
, Show (Environment sts)
)
=> BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe (IRC sts -> QuickCheck.Gen (Either [[STS.PredicateFailure sts]] (State sts)))
-> (Trace sts -> prop)
-> QuickCheck.Property
forAllTraceFromInitState :: BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
genSt0 Trace sts -> prop
prop =
Gen (Trace sts)
-> (Trace sts -> [Trace sts]) -> (Trace sts -> prop) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QuickCheck.forAllShrinkBlind
(BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> Gen (Trace sts)
forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> Gen (Trace sts)
traceFromInitState @sts @traceGenEnv BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
genSt0)
(BaseEnv sts -> Trace sts -> [Trace sts]
forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts -> Trace sts -> [Trace sts]
shrinkTrace @sts @traceGenEnv BaseEnv sts
baseEnv)
Trace sts -> prop
prop
forAllTrace
:: forall sts traceGenEnv prop
. ( HasTrace sts traceGenEnv
, QuickCheck.Testable prop
, Show (Environment sts)
)
=> BaseEnv sts
-> Word64
-> traceGenEnv
-> (Trace sts -> prop)
-> QuickCheck.Property
forAllTrace :: BaseEnv sts
-> Word64 -> traceGenEnv -> (Trace sts -> prop) -> Property
forAllTrace BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv =
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> (Trace sts -> prop)
-> Property
forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
forall a. Maybe a
Nothing
shrinkTrace
:: forall sts traceGenEnv
. (HasTrace sts traceGenEnv
)
=> BaseEnv sts
-> Trace sts
-> [Trace sts]
shrinkTrace :: BaseEnv sts -> Trace sts -> [Trace sts]
shrinkTrace BaseEnv sts
baseEnv Trace sts
tr =
BaseEnv sts -> BaseM sts [Trace sts] -> [Trace sts]
forall sts traceGenEnv a.
HasTrace sts traceGenEnv =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
baseEnv
(BaseM sts [Trace sts] -> [Trace sts])
-> BaseM sts [Trace sts] -> [Trace sts]
forall a b. (a -> b) -> a -> b
$ Environment sts
-> State sts -> [Signal sts] -> BaseM sts (Trace sts)
forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
Trace.closure Environment sts
env State sts
st0 ([Signal sts] -> BaseM sts (Trace sts))
-> [[Signal sts]] -> BaseM sts [Trace sts]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [Signal sts] -> [[Signal sts]]
forall a. [a] -> [[a]]
shrinkSignals [Signal sts]
signals
where
env :: Environment sts
env = Trace sts -> Environment sts
forall s. Trace s -> Environment s
Trace._traceEnv Trace sts
tr
st0 :: State sts
st0 = Trace sts -> State sts
forall s. Trace s -> State s
Trace._traceInitState Trace sts
tr
signals :: [Signal sts]
signals = TraceOrder -> Trace sts -> [Signal sts]
forall s. TraceOrder -> Trace s -> [Signal s]
Trace.traceSignals TraceOrder
Trace.NewestFirst Trace sts
tr
shrinkSignals :: [a] -> [[a]]
shrinkSignals (a
sn:a
_last:[]) =
[[a
sn]]
shrinkSignals (a
sn:a
sm:[a]
sigs) =
[[a
sn]]
[[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ ((a
sna -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> [[a]] -> [[a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> [[a]]
shrinkSignals (a
sma -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
sigs))
[[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [a
sna -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
sigs]
shrinkSignals [a]
_ = []
onlyValidSignalsAreGenerated
:: forall sts traceGenEnv
. ( HasTrace sts traceGenEnv
, Show (Environment sts)
, Show (Signal sts)
)
=> BaseEnv sts
-> Word64
-> traceGenEnv
-> QuickCheck.Property
onlyValidSignalsAreGenerated :: BaseEnv sts -> Word64 -> traceGenEnv -> Property
onlyValidSignalsAreGenerated BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv =
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> Property
forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts),
Show (Signal sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> Property
onlyValidSignalsAreGeneratedFromInitState @sts BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
forall a. Maybe a
Nothing
onlyValidSignalsAreGeneratedFromInitState
:: forall sts traceGenEnv
. ( HasTrace sts traceGenEnv
, Show (Environment sts)
, Show (Signal sts)
)
=> BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe (IRC sts -> QuickCheck.Gen (Either [[STS.PredicateFailure sts]] (State sts)))
-> QuickCheck.Property
onlyValidSignalsAreGeneratedFromInitState :: BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> Property
onlyValidSignalsAreGeneratedFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
genSt0 =
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> (Trace sts -> Property)
-> Property
forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
Show (Environment sts)) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
-> (Trace sts -> prop)
-> Property
forAllTraceFromInitState BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv Maybe
(IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts)))
genSt0 Trace sts -> Property
validSignalsAreGenerated
where
validSignalsAreGenerated
:: Trace sts
-> QuickCheck.Property
validSignalsAreGenerated :: Trace sts -> Property
validSignalsAreGenerated Trace sts
someTrace =
Gen (Signal sts)
-> (Signal sts -> [Signal sts])
-> (Signal sts -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QuickCheck.forAllShrink
(traceGenEnv -> Environment sts -> State sts -> Gen (Signal sts)
forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
traceGenEnv -> Environment sts -> State sts -> Gen (Signal sts)
sigGen @sts @traceGenEnv traceGenEnv
traceGenEnv Environment sts
env State sts
lastState)
(HasTrace sts traceGenEnv => Signal sts -> [Signal sts]
forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
Signal sts -> [Signal sts]
shrinkSignal @sts @traceGenEnv)
Signal sts -> Property
signalIsValid
where
signalIsValid :: Signal sts -> Property
signalIsValid Signal sts
signal =
case BaseEnv sts
-> BaseM sts (Either [[PredicateFailure sts]] (State sts))
-> Either [[PredicateFailure sts]] (State sts)
forall sts traceGenEnv a.
HasTrace sts traceGenEnv =>
BaseEnv sts -> BaseM sts a -> a
interpretSTS @sts @traceGenEnv BaseEnv sts
baseEnv (RuleContext 'Transition sts
-> BaseM sts (Either [[PredicateFailure sts]] (State sts))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s))
Trace.applySTSTest @sts ((Environment sts, State sts, Signal sts) -> TRC sts
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment sts
env, State sts
lastState, Signal sts
signal))) of
Left [[PredicateFailure sts]]
pf -> [Char] -> Bool -> Property
forall prop. Testable prop => [Char] -> prop -> Property
QuickCheck.counterexample ((Signal sts, [[PredicateFailure sts]]) -> [Char]
forall a. Show a => a -> [Char]
show (Signal sts
signal, [[PredicateFailure sts]]
pf)) Bool
False
Right State sts
_ -> Bool -> Property
forall prop. Testable prop => prop -> Property
QuickCheck.property Bool
True
env :: Environment sts
env = Trace sts -> Environment sts
forall s. Trace s -> Environment s
Trace._traceEnv Trace sts
someTrace
lastState :: State sts
lastState = Trace sts -> State sts
forall s. Trace s -> State s
Trace.lastState Trace sts
someTrace
traceLengthsAreClassified
:: forall sts traceGenEnv
. ( HasTrace sts traceGenEnv
, Show (Environment sts)
)
=> BaseEnv sts
-> Word64
-> Word64
-> traceGenEnv
-> QuickCheck.Property
traceLengthsAreClassified :: BaseEnv sts -> Word64 -> Word64 -> traceGenEnv -> Property
traceLengthsAreClassified BaseEnv sts
baseEnv Word64
maxTraceLength Word64
intervalSize traceGenEnv
traceGenEnv =
BaseEnv sts
-> Word64 -> traceGenEnv -> (Trace sts -> Property) -> Property
forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
Show (Environment sts)) =>
BaseEnv sts
-> Word64 -> traceGenEnv -> (Trace sts -> prop) -> Property
forAllTrace @sts BaseEnv sts
baseEnv Word64
maxTraceLength traceGenEnv
traceGenEnv (Word64 -> Word64 -> Trace sts -> Property
forall s. Word64 -> Word64 -> Trace s -> Property
classifyTraceLength Word64
maxTraceLength Word64
intervalSize)
classifyTraceLength
:: Word64
-> Word64
-> Trace s
-> QuickCheck.Property
classifyTraceLength :: Word64 -> Word64 -> Trace s -> Property
classifyTraceLength Word64
maxTraceLength Word64
step Trace s
tr =
[Char]
-> Trace s -> (Trace s -> Word64) -> Word64 -> Word64 -> Property
forall n a.
(Ord n, Show n, Integral n) =>
[Char] -> a -> (a -> n) -> n -> n -> Property
classifySize [Char]
"trace length:" Trace s
tr (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> (Trace s -> Int) -> Trace s -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace s -> Int
forall s. Trace s -> Int
Trace.traceLength) Word64
maxTraceLength Word64
step
classifySize
:: (Ord n, Show n, Integral n)
=> String
-> a
-> (a -> n)
-> n
-> n
-> QuickCheck.Property
classifySize :: [Char] -> a -> (a -> n) -> n -> n -> Property
classifySize [Char]
prefixLabel a
value a -> n
sizeF n
upBound n
step =
Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (a -> n
sizeF a
value n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
0) ([Char] -> [Char]
mkLabel [Char]
"empty") (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (a -> n
sizeF a
value n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
1) ([Char] -> [Char]
mkLabel [Char]
"singleton") (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (a -> n
sizeF a
value n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
upBound) [Char]
upBoundLabel (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
((n, n) -> Property -> Property)
-> Property -> [(n, n)] -> Property
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (n, n) -> Property -> Property
classifySizeInterval (Bool -> Property
forall prop. Testable prop => prop -> Property
QuickCheck.property Bool
True) (n -> n -> n -> [(n, n)]
forall n. Integral n => n -> n -> n -> [(n, n)]
mkIntervals n
2 (n
upBound n -> n -> n
forall a. Num a => a -> a -> a
- n
1) n
step)
where
upBoundLabel :: [Char]
upBoundLabel = [Char] -> [Char]
mkLabel ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ n -> [Char]
forall a. Show a => a -> [Char]
show n
upBound
mkLabel :: [Char] -> [Char]
mkLabel = (([Char]
prefixLabel [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)
classifySizeInterval :: (n, n) -> Property -> Property
classifySizeInterval (n
low, n
high) Property
prop =
Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
QuickCheck.classify (n
low n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<= a -> n
sizeF a
value Bool -> Bool -> Bool
&& a -> n
sizeF a
value n -> n -> Bool
forall a. Ord a => a -> a -> Bool
< n
high) [Char]
desc Property
prop
where
desc :: [Char]
desc = [Char]
"[" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ n -> [Char]
forall a. Show a => a -> [Char]
show n
low [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ n -> [Char]
forall a. Show a => a -> [Char]
show n
high [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
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)