Safe Haskell	None
Language	Haskell2010

Control.State.Transition.Generator

Contents

Invalid trace generation
Trace classification
Trace properties
Helpers

Description

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

Synopsis

class STS s => HasTrace s
type SignalGenerator s = Environment s -> State s -> Gen (Signal s)
type family BaseEnv s :: Type
interpretSTS :: forall a. HasTrace s => BaseEnv s -> BaseM s a -> a
envGen :: HasTrace s => Word64 -> Gen (Environment s)
sigGen :: HasTrace s => SignalGenerator s
traceSigGen :: forall s. HasTrace s => BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
genTrace :: forall s. HasTrace s => BaseEnv s -> Word64 -> Environment s -> State s -> SignalGenerator s -> Gen (Trace s)
trace :: HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
traceWithProfile :: HasTrace s => BaseEnv s -> Word64 -> TraceProfile s -> Gen (Trace s)
traceOfLength :: HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
traceOfLengthWithInitState :: HasTrace s => BaseEnv s -> Word64 -> (Environment s -> Gen (State s)) -> Gen (Trace s)
traceSuchThat :: forall s. HasTrace s => BaseEnv s -> Word64 -> (Trace s -> Bool) -> Gen (Trace s)
ofLengthAtLeast :: Gen (Trace s) -> Int -> Gen (Trace s)
suchThatLastState :: forall s. Gen (Trace s) -> (State s -> Bool) -> Gen (Trace s)
nonTrivialTrace :: forall s. (HasTrace s, HasSizeInfo (Signal s)) => BaseEnv s -> Word64 -> Gen (Trace s)
class HasSizeInfo sig
isTrivial :: HasSizeInfo sig => sig -> Bool
sampleMaxTraceSize :: forall s. HasTrace s => BaseEnv s -> Word64 -> Int -> Word64 -> IO Int
randomTrace :: forall s. HasTrace s => BaseEnv s -> Word64 -> IO (Trace s)
randomTraceOfSize :: forall s. HasTrace s => BaseEnv s -> Word64 -> IO (Trace s)
data TraceLength
- = Maximum Word64
- | Desired Word64
data TraceProfile s = TraceProfile {
- proportionOfValidSignals :: !Int
- failures :: ![(Int, SignalGenerator s)]
}
proportionOfInvalidSignals :: TraceProfile s -> Int
invalidTrace :: forall s. HasTrace s => BaseEnv s -> Word64 -> [(Int, SignalGenerator s)] -> Gen (Trace s)
classifyTraceLength :: Trace s -> Word64 -> Word64 -> PropertyT IO ()
classifySize :: (Ord n, Show n, Integral n) => String -> a -> (a -> n) -> n -> n -> PropertyT IO ()
mkIntervals :: Integral n => n -> n -> n -> [(n, n)]
ratio :: Integral a => (Trace s -> a) -> Trace s -> Double
traceLengthsAreClassified :: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s)) => BaseEnv s -> Word64 -> Word64 -> Property
onlyValidSignalsAreGenerated :: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) => BaseEnv s -> Word64 -> Property
onlyValidSignalsAreGeneratedForTrace :: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) => BaseEnv s -> Gen (Trace s) -> Property
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
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)
coverFailures :: forall m s a. (MonadTest m, HasCallStack, Data (PredicateFailure s), Data a) => CoverPercentage -> [PredicateFailure s] -> a -> m ()

Documentation

class STS s => HasTrace s Source #

Minimal complete definition

envGen, sigGen

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

type family BaseEnv s :: Type Source #

interpretSTS :: forall a. HasTrace s => BaseEnv s -> BaseM s a -> a Source #

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.

envGen Source #

Arguments

:: HasTrace s
=> Word64	Trace length that will be used by `trace` or `traceOfLength`.
-> Gen (Environment s)

Generate an initial environment that is based on the given trace length.

sigGen :: HasTrace s => SignalGenerator s Source #

Generate a (valid) signal given an environment and a pre-state.

traceSigGen :: forall s. HasTrace s => BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s) Source #

genTrace Source #

Arguments

:: 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)

Return a (valid) trace generator given an initial state, environment, and signal generator.

trace Source #

Arguments

:: HasTrace s
=> BaseEnv s
-> Word64	Maximum length of the generated traces. The actual length will be between 0 and this maximum.
-> Gen (Trace s)

traceWithProfile :: HasTrace s => BaseEnv s -> Word64 -> TraceProfile s -> Gen (Trace s) Source #

traceOfLength Source #

Arguments

:: HasTrace s
=> 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)

traceOfLengthWithInitState Source #

Arguments

:: HasTrace s
=> 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)

traceSuchThat :: forall s. HasTrace s => BaseEnv s -> Word64 -> (Trace s -> Bool) -> Gen (Trace s) Source #

ofLengthAtLeast :: Gen (Trace s) -> Int -> Gen (Trace s) Source #

suchThatLastState :: forall s. Gen (Trace s) -> (State s -> Bool) -> Gen (Trace s) Source #

nonTrivialTrace :: forall s. (HasTrace s, HasSizeInfo (Signal s)) => BaseEnv s -> Word64 -> Gen (Trace s) Source #

Generate a trace that contains at least one non-trivial signal. See HasSizeInfo.

class HasSizeInfo sig Source #

Minimal complete definition

isTrivial

Instances

Instances details

HasSizeInfo [a] Source #
Instance details Defined in Control.State.Transition.Generator Methods isTrivial :: [a] -> Bool Source #

isTrivial :: HasSizeInfo sig => sig -> Bool Source #

sampleMaxTraceSize Source #

Arguments

:: forall s. HasTrace s
=> BaseEnv s
-> Word64	Trace's upper bound
-> Int	Generator size
-> Word64	Number of samples to take
-> IO Int

Sample the maximum trace size, given the generator size and number of samples.

randomTrace :: forall s. HasTrace s => BaseEnv s -> Word64 -> IO (Trace s) Source #

randomTraceOfSize :: forall s. HasTrace s => BaseEnv s -> Word64 -> IO (Trace s) Source #

data TraceLength Source #

Constructors

Maximum Word64
Desired Word64

data TraceProfile s Source #

Constructors

TraceProfile
Fields proportionOfValidSignals :: !Int Proportion of valid signals to generate. 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 Source #

Invalid trace generation

invalidTrace Source #

Arguments

:: 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 (Trace s)

Generate an invalid trace

Trace classification

classifyTraceLength Source #

Arguments

:: Trace s
-> Word64	Maximum size of the traces
-> Word64	Steps used to divide the interval
-> PropertyT IO ()

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.

classifySize Source #

Arguments

:: (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 ()

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.

mkIntervals Source #

Arguments

:: 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)]

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)]
[]

ratio :: Integral a => (Trace s -> a) -> Trace s -> Double Source #

Given a function that computes an integral value from a trace, return that value as a ratio of the trace length.

Trace properties

traceLengthsAreClassified Source #

Arguments

:: 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

Property that simply classifies the lengths of the generated traces.

onlyValidSignalsAreGenerated Source #

Arguments

:: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack)
=> BaseEnv s
-> Word64	Maximum trace length.
-> Property

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 Source #

Check that the signal generator of s only generate valid signals.

invalidSignalsAreGenerated Source #

Arguments

:: 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

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) Source #

coverFailures Source #

Arguments

:: forall m s a. (MonadTest m, HasCallStack, Data (PredicateFailure s), Data a)
=> CoverPercentage
-> [PredicateFailure s]	Target predicate failures
-> a	Structure containing the failures
-> m ()