Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.Control.State.Transition.Trace.Generator.QuickCheck

Contents

Trace generator properties
Trace classification
Internal

Synopsis

class STS sts ⇒ HasTrace sts traceGenEnv where
- type BaseEnv sts ∷ Type
- interpretSTS ∷ ∀ a. HasCallStack ⇒ BaseEnv sts → BaseM sts a → a
- envGen ∷ HasCallStack ⇒ traceGenEnv → Gen (Environment sts)
- sigGen ∷ HasCallStack ⇒ traceGenEnv → Environment sts → State sts → Gen (Signal sts)
- shrinkSignal ∷ HasCallStack ⇒ Signal sts → [Signal sts]
traceFrom ∷ ∀ sts traceGenEnv. HasTrace sts traceGenEnv ⇒ BaseEnv sts → Word64 → traceGenEnv → Environment sts → State sts → Gen (Trace sts)
traceFromInitState ∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) ⇒ BaseEnv sts → Word64 → traceGenEnv → Maybe (IRC sts → Gen (Either (NonEmpty (PredicateFailure sts)) (State sts))) → Gen (Trace sts)
trace ∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts)) ⇒ BaseEnv sts → Word64 → traceGenEnv → Gen (Trace sts)
shrinkTrace ∷ ∀ sts traceGenEnv. HasTrace sts traceGenEnv ⇒ BaseEnv sts → Trace sts → [Trace sts]
forAllTrace ∷ ∀ sts traceGenEnv prop. (HasTrace sts traceGenEnv, Testable prop, Show (Environment sts)) ⇒ BaseEnv sts → Word64 → traceGenEnv → (Trace sts → prop) → Property
forAllTraceFromInitState ∷ ∀ sts traceGenEnv prop. (HasTrace sts traceGenEnv, Testable prop, Show (Environment sts)) ⇒ BaseEnv sts → Word64 → traceGenEnv → Maybe (IRC sts → Gen (Either (NonEmpty (PredicateFailure sts)) (State sts))) → (Trace sts → prop) → Property
onlyValidSignalsAreGenerated ∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts), Show (Signal sts)) ⇒ BaseEnv sts → Word64 → traceGenEnv → Property
onlyValidSignalsAreGeneratedFromInitState ∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts), Show (Signal sts)) ⇒ BaseEnv sts → Word64 → traceGenEnv → Maybe (IRC sts → Gen (Either (NonEmpty (PredicateFailure sts)) (State sts))) → Property
traceLengthsAreClassified ∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts)) ⇒ BaseEnv sts → Word64 → Word64 → traceGenEnv → Property
classifyTraceLength ∷ Word64 → Word64 → Trace s → Property
classifySize ∷ (Show n, Integral n) ⇒ String → a → (a → n) → n → n → Property
mkIntervals ∷ Integral n ⇒ n → n → n → [(n, n)]

Documentation

class STS sts ⇒ HasTrace sts traceGenEnv where Source #

State transition systems for which traces can be generated, given a trace generation environment.

The trace generation environment allows to pass relevant data to the trace generation algorithm.

Minimal complete definition

envGen, sigGen, shrinkSignal

Associated Types

type BaseEnv sts ∷ Type Source #

type BaseEnv s = ()

Methods

interpretSTS ∷ ∀ a. HasCallStack ⇒ BaseEnv sts → BaseM sts 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.

default interpretSTS ∷ BaseM sts ~ Identity ⇒ ∀ a. BaseEnv sts → BaseM sts a → a Source #

envGen ∷ HasCallStack ⇒ traceGenEnv → Gen (Environment sts) Source #

sigGen ∷ HasCallStack ⇒ traceGenEnv → Environment sts → State sts → Gen (Signal sts) Source #

shrinkSignal ∷ HasCallStack ⇒ Signal sts → [Signal sts] Source #

traceFrom Source #

Arguments

∷ ∀ sts traceGenEnv. HasTrace sts traceGenEnv
⇒ BaseEnv sts
→ Word64	Maximum trace length.
→ traceGenEnv
→ Environment sts
→ State sts
→ Gen (Trace sts)

Generate a random trace starting in the given environment and initial state.

traceFromInitState Source #

Arguments

∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack)
⇒ BaseEnv sts
→ Word64	Maximum trace length.
→ traceGenEnv
→ Maybe (IRC sts → Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))	Optional generator of STS initial state
→ Gen (Trace sts)

Generate a random trace given a generator for initial state.

Takes an optional generator for initial state, or defaults to applySTS if no initial state is required by the STS.

trace Source #

Arguments

∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts))
⇒ BaseEnv sts
→ Word64	Maximum trace length.
→ traceGenEnv
→ Gen (Trace sts)

Generate a random trace.

shrinkTrace ∷ ∀ sts traceGenEnv. HasTrace sts traceGenEnv ⇒ BaseEnv sts → Trace sts → [Trace sts] Source #

Shrink a trace by shrinking the list of signals and reconstructing traces from these shrunk lists of signals.

When shrinking a trace that is failing some property (often stated in terms of a signal in the trace) then the most recent signal is likely crucial to the failure of the property and must be preserved in the shrunk traces.

Trace generator properties

forAllTrace Source #

Arguments

∷ ∀ sts traceGenEnv prop. (HasTrace sts traceGenEnv, Testable prop, Show (Environment sts))
⇒ BaseEnv sts
→ Word64	Maximum trace length.
→ traceGenEnv
→ (Trace sts → prop)
→ Property

Check a property on the sts traces.

forAllTraceFromInitState Source #

Arguments

∷ ∀ sts traceGenEnv prop. (HasTrace sts traceGenEnv, Testable prop, Show (Environment sts))
⇒ BaseEnv sts
→ Word64	Maximum trace length.
→ traceGenEnv
→ Maybe (IRC sts → Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))	Optional generator of STS initial state
→ (Trace sts → prop)
→ Property

Check a property on the sts traces.

Takes an optional generator for initial state of the STS.

onlyValidSignalsAreGenerated Source #

Arguments

∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts), Show (Signal sts))
⇒ BaseEnv sts
→ Word64	Maximum trace length.
→ traceGenEnv
→ Property

Property that asserts that only valid signals are generated.

onlyValidSignalsAreGeneratedFromInitState Source #

Arguments

∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts), Show (Signal sts))
⇒ BaseEnv sts
→ Word64	Maximum trace length.
→ traceGenEnv
→ Maybe (IRC sts → Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))	Optional generator of STS initial state
→ Property

Property that asserts that only valid signals are generated.

Takes an optional generator for initial state of the STS.

Trace classification

traceLengthsAreClassified Source #

Arguments

∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts))
⇒ BaseEnv sts
→ 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.
→ traceGenEnv	Trace generation environment
→ Property

Property that simply classifies the lengths of the generated traces.

classifyTraceLength Source #

Arguments

∷ Word64	Maximum size of the traces
→ Word64	Steps used to divide the interval
→ Trace s
→ Property

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
→ Property

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.

Internal

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