small-steps-test-0.1.0.0: Small step semantics testing library
Safe HaskellNone
LanguageHaskell2010

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

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) 

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 #

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

Constructors

TraceProfile 

Fields

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