small-steps-1.1.0.1: Small step semantics
Safe HaskellSafe-Inferred
LanguageHaskell2010

Test.Control.State.Transition.Generator

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

Documentation

class STS s ⇒ HasTrace s Source #

Minimal complete definition

envGen, sigGen

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.

sigGenHasTrace s ⇒ SignalGenerator s Source #

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

traceSigGen ∷ ∀ s. HasTrace s ⇒ BaseEnv s → TraceLengthSignalGenerator 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) 

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 #

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

nonTrivialTrace ∷ ∀ s. (HasTrace s, HasSizeInfo (Signal s)) ⇒ BaseEnv s → Word64Gen (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 #

isTrivialHasSizeInfo 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 → Word64IO (Trace s) Source #

randomTraceOfSize ∷ ∀ s. HasTrace s ⇒ BaseEnv s → Word64IO (Trace s) Source #

data TraceProfile s Source #

Constructors

TraceProfile 

Fields

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

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