Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.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 ∷ ∀ a. HasTrace s ⇒ BaseEnv s → BaseM s a → a
envGen ∷ HasTrace s ⇒ Word64 → Gen (Environment s)
sigGen ∷ HasTrace s ⇒ SignalGenerator s
traceSigGen ∷ ∀ s. HasTrace s ⇒ BaseEnv s → TraceLength → SignalGenerator s → Gen (Trace s)
genTrace ∷ ∀ 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 ∷ ∀ s. HasTrace s ⇒ BaseEnv s → Word64 → (Trace s → Bool) → Gen (Trace s)
ofLengthAtLeast ∷ Gen (Trace s) → Int → Gen (Trace s)
suchThatLastState ∷ ∀ s. Gen (Trace s) → (State s → Bool) → Gen (Trace s)
nonTrivialTrace ∷ ∀ s. (HasTrace s, HasSizeInfo (Signal s)) ⇒ BaseEnv s → Word64 → Gen (Trace s)
class HasSizeInfo sig
isTrivial ∷ HasSizeInfo sig ⇒ sig → Bool
sampleMaxTraceSize ∷ ∀ s. HasTrace s ⇒ BaseEnv s → Word64 → Int → Word64 → IO Int
randomTrace ∷ ∀ s. HasTrace s ⇒ BaseEnv s → Word64 → IO (Trace s)
randomTraceOfSize ∷ ∀ 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 ∷ ∀ s. HasTrace s ⇒ BaseEnv s → Word64 → [(Int, SignalGenerator s)] → Gen (Trace s)
classifyTraceLength ∷ Trace s → Word64 → Word64 → PropertyT IO ()
classifySize ∷ (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 ∷ ∀ s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s)) ⇒ BaseEnv s → Word64 → Word64 → Property
onlyValidSignalsAreGenerated ∷ ∀ s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) ⇒ BaseEnv s → Word64 → Property
onlyValidSignalsAreGeneratedForTrace ∷ ∀ s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) ⇒ BaseEnv s → Gen (Trace s) → Property
invalidSignalsAreGenerated ∷ ∀ s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) ⇒ BaseEnv s → [(Int, SignalGenerator s)] → Word64 → (NonEmpty (PredicateFailure s) → PropertyT IO ()) → Property
coverFailures ∷ ∀ 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 ∷ ∀ 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 ∷ ∀ s. HasTrace s ⇒ BaseEnv s → TraceLength → SignalGenerator s → Gen (Trace s) Source #

genTrace Source #

Arguments

∷ ∀ 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 ∷ ∀ s. HasTrace s ⇒ BaseEnv s → Word64 → (Trace s → Bool) → Gen (Trace s) Source #

ofLengthAtLeast ∷ Gen (Trace s) → Int → Gen (Trace s) Source #

suchThatLastState ∷ ∀ s. Gen (Trace s) → (State s → Bool) → Gen (Trace s) Source #

nonTrivialTrace ∷ ∀ 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 Test.Control.State.Transition.Generator Methods isTrivial ∷ [a] → Bool Source #

isTrivial ∷ HasSizeInfo sig ⇒ sig → Bool Source #

sampleMaxTraceSize Source #

Arguments

∷ ∀ 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 ∷ ∀ s. HasTrace s ⇒ BaseEnv s → Word64 → IO (Trace s) Source #

randomTraceOfSize ∷ ∀ 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

∷ ∀ 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

∷ (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

∷ ∀ 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

∷ ∀ 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 ∷ ∀ 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

∷ ∀ s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack)
⇒ BaseEnv s
→ [(Int, SignalGenerator s)]	Failure profile.
→ Word64	Maximum trace length.
→ (NonEmpty (PredicateFailure s) → PropertyT IO ())	Action to run when the an invalid signal is generated.
→ Property

Helpers

coverFailures Source #

Arguments

∷ ∀ m s a. (MonadTest m, HasCallStack, Data (PredicateFailure s), Data a)
⇒ CoverPercentage
→ [PredicateFailure s]	Target predicate failures
→ a	Structure containing the failures
→ m ()